Grcov report - integer

1

use conjure_cp::ast::SymbolTable;

2

use conjure_cp::ast::{Expression as Expr, GroundDomain};

3

use conjure_cp::rule_engine::{

4

    ApplicationError, ApplicationError::RuleNotApplicable, ApplicationResult, Reduction,

5

    register_rule,

6

};

7

8

use conjure_cp::ast::Metadata;

9

use conjure_cp::ast::{Atom, Literal, Moo, Range};

10

use conjure_cp::into_matrix_expr;

11

12

use conjure_cp::essence_expr;

13

14

// The number of bits used to represent the integer.

15

// This is a fixed value for the representation, but could be made dynamic if needed.

16

pub const BITS: usize = 8; // FIXME: Make it dynamic

17

18

/// This function takes a target expression and a vector of ranges and creates an expression representing the ranges with the target expression as the subject

19

///

20

/// E.g. x : int(4), int(10..20), int(30..) ~~> Or(x=4, 10<=x<=20, x>=30)

21

fn int_domain_to_expr(subject: Expr, ranges: &Vec<Range<i32>>) -> Expr {

22

    let mut output = vec![];

23

24

    let value = Moo::new(subject);

25

26

    for range in ranges {

27

        match range {

28

            Range::Single(x) => output.push(essence_expr!(&value = &x)),

29

            Range::Bounded(x, y) => output.push(essence_expr!("&value >= &x /\\ &value <= &y")),

30

            Range::UnboundedR(x) => output.push(essence_expr!(&value >= &x)),

31

            Range::UnboundedL(x) => output.push(essence_expr!(&value <= &x)),

32

            Range::Unbounded => todo!(),

33

34

35

36

    Expr::Or(Metadata::new(), Moo::new(into_matrix_expr!(output)))

37

38

39

/// This function confirms that all of the input expressions are SATInts, and returns vectors for each input of their bits

40

pub fn validate_sat_int_operands(exprs: Vec<Expr>) -> Result<Vec<Vec<Expr>>, ApplicationError> {

41

    let out: Result<Vec<Vec<_>>, _> = exprs

42

        .into_iter()

43

        .map(|expr| {

44

            let Expr::SATInt(_, inner) = expr else {

45

                return Err(RuleNotApplicable);

46

};

47

            let Some(bits) = inner.as_ref().clone().unwrap_list() else {

48

                return Err(RuleNotApplicable);

49

};

50

            Ok(bits)

51

})

52

        .collect();

53

54

out

55

56

57

/// Converts an integer decision variable to SATInt form, creating a new representation of boolean variables if

58

/// one does not yet exist

59

///

60

/// ```text

61

///  x

62

///  ~~>

63

///  SATInt([x#00, x#01, ...])

64

///

65

///  new variables:

66

///  find x#00: bool

67

///  find x#01: bool

68

///  ...

69

///

70

/// ```

71

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

72

fn integer_decision_representation(expr: &Expr, symbols: &SymbolTable) -> ApplicationResult {

73

    // thing we are representing must be a reference

74

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

75

        return Err(RuleNotApplicable);

76

};

77

78

    // thing we are representing must be a variable

79

    // symbols

80

    //     .lookup(name)

81

    //     .ok_or(RuleNotApplicable)?

82

    //     .as_var()

83

    //     .ok_or(RuleNotApplicable)?;

84

85

    // thing we are representing must be an integer

86

    let dom = name.resolved_domain().ok_or(RuleNotApplicable)?;

87

    let GroundDomain::Int(ranges) = dom.as_ref() else {

88

        return Err(RuleNotApplicable);

89

};

90

91

    let mut symbols = symbols.clone();

92

93

    let new_name = &name.name().to_owned();

94

95

    let repr_exists = symbols

96

        .get_representation(new_name, &["sat_log_int"])

97

        .is_some();

98

99

    let representation = symbols

100

        .get_or_add_representation(new_name, &["sat_log_int"])

101

        .ok_or(RuleNotApplicable)?;

102

103

    let bits = representation[0]

104

        .clone()

105

        .expression_down(&symbols)?

106

        .into_values()

107

        .collect();

108

109

    let cnf_int = Expr::SATInt(Metadata::new(), Moo::new(into_matrix_expr!(bits)));

110

111

    if !repr_exists {

112

        // add domain ranges as constraints if this is the first time the representation is added

113

        Ok(Reduction::new(

114

            cnf_int.clone(),

115

            vec![int_domain_to_expr(cnf_int, ranges)], // contains domain rules

116

            symbols,

117

))

118

    } else {

119

        Ok(Reduction::pure(cnf_int))

120

121

122

123

/// Converts an integer literal to SATInt form

124

///

125

/// ```text

126

///  3

127

///  ~~>

128

///  SATInt([true,true,false,false,false,false,false,false;int(1..)])

129

///

130

/// ```

131

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

132

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

133

    let mut value = {

134

        if let Expr::Atomic(_, Atom::Literal(Literal::Int(v))) = expr {

135

*v

136

        } else {

137

            return Err(RuleNotApplicable);

138

139

};

140

141

    //TODO: add support for negatives

142

143

    let mut binary_encoding = vec![];

144

145

    for _ in 0..BITS {

146

        binary_encoding.push(Expr::Atomic(

147

            Metadata::new(),

148

            Atom::Literal(Literal::Bool((value & 1) != 0)),

149

));

150

        value >>= 1;

151

152

153

    Ok(Reduction::pure(Expr::SATInt(

154

        Metadata::new(),

155

        Moo::new(into_matrix_expr!(binary_encoding)),

156

)))

157