Grcov report - materialise.rs

1

use conjure_cp::ast::{Atom, Expression as Expr, SATIntEncoding, SymbolTable};

2

use conjure_cp::rule_engine::{

3

    ApplicationError, ApplicationError::RuleNotApplicable, ApplicationResult, RuleEffect,

4

    register_rule,

5

};

6

7

use crate::types::int::{

8

    IntBinaryOffset, IntBinaryRank, IntBinarySignMagnitude, IntBinaryTwosComplement,

9

};

10

11

/// Normalise logarithmic SAT integer operands to a common bit width.

12

608090

pub(super) fn validate_log_int_operands(

13

608090

    exprs: Vec<Expr>,

14

608090

    bit_count: Option<u32>,

15

608090

) -> Result<Vec<Vec<Expr>>, ApplicationError> {

16

608090

    let mut out: Vec<Vec<Expr>> = exprs

17

608090

        .into_iter()

18

850430

        .map(|expr| match expr {

19

            Expr::SATInt(_, SATIntEncoding::Log, inner, _) => {

20

489594

                inner.as_ref().clone().into_list().ok_or(RuleNotApplicable)

21

22

360836

            _ => Err(RuleNotApplicable),

23

850430

})

24

360836

        .collect::<Result<_, _>>()?;

25

26

247254

    let max_len = bit_count

27

4431

        .map(|bits| bits as usize)

28

242823

        .unwrap_or_else(|| out.iter().map(Vec::len).max().unwrap_or(0));

29

247254

    for bits in &mut out {

30

489594

        if bits.len() < max_len {

31

155575

            if let Some(last) = bits.last().cloned() {

32

155575

                bits.resize(max_len, last);

33

34

        } else {

35

334019

            bits.truncate(max_len);

36

37

38

247254

    Ok(out)

39

608090

40

41

/// Replace a log-represented reference with its bit vector.

42

#[register_rule("SAT", 9500, [Atomic])]

43

38411602

fn integer_decision_representation_log(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

44

38411602

    let Expr::Atomic(_, Atom::Reference(reference)) = expr else {

45

13192416

        return Err(RuleNotApplicable);

46

};

47

25219186

    let state = reference

48

25219186

        .get_repr_as::<IntBinaryTwosComplement>()

49

25219186

        .ok_or(RuleNotApplicable)?;

50

48615

    Ok(RuleEffect::pure(state.sat_int_expr()))

51

38411602

52

53

/// Number of bits required to encode an `i32` in two's complement.

54

987597

pub(in crate::backends::sat) fn bit_magnitude(value: i32) -> usize {

55

987597

    if value >= 0 {

56

923785

        (1 + (32 - value.leading_zeros())).try_into().unwrap()

57

    } else {

58

63812

        (33 - (!value).leading_zeros()).try_into().unwrap()

59

60

987597

61

62

/// Sign-extend the shorter of two bit vectors to the length of the longer one.

63

24430

pub(super) fn match_bits_length(mut lhs: Vec<Expr>, mut rhs: Vec<Expr>) -> (Vec<Expr>, Vec<Expr>) {

64

24430

    if lhs.len() < rhs.len() {

65

245

        lhs.resize(rhs.len(), lhs.last().cloned().unwrap());

66

24185

    } else if rhs.len() < lhs.len() {

67

665

        rhs.resize(lhs.len(), rhs.last().cloned().unwrap());

68

23520

69

24430

    (lhs, rhs)

70

24430

71

72

/// Materialise unsigned codes without treating rank as the semantic numeric value.

73

#[register_rule("SAT", 9500, [Atomic])]

74

38411602

fn integer_decision_representation_unsigned(expr: &Expr, _: &SymbolTable) -> ApplicationResult {

75

38411602

    let Expr::Atomic(_, Atom::Reference(reference)) = expr else {

76

13192416

        return Err(RuleNotApplicable);

77

};

78

25219186

    let represented = if let Some(state) = reference.get_repr_as::<IntBinaryOffset>() {

79

60256

        state.sat_int_expr()

80

25158930

    } else if let Some(state) = reference.get_repr_as::<IntBinaryRank>() {

81

67596

        state.sat_int_expr()

82

25091334

    } else if let Some(state) = reference.get_repr_as::<IntBinarySignMagnitude>() {

83

48615

        state.sat_int_expr()

84

    } else {

85

25042719

        return Err(RuleNotApplicable);

86

};

87

176467

    Ok(RuleEffect::pure(represented))

88

38411602