Grcov report - sat_order

1

// https://conjure-cp.github.io/conjure-oxide/docs/conjure_core/representation/trait.Representation.html

2

use conjure_cp::ast::GroundDomain;

3

use conjure_cp::bug;

4

use conjure_cp::{

5

    ast::{Atom, DeclarationPtr, Domain, Expression, Literal, Metadata, Name, SymbolTable},

6

    register_representation,

7

    representation::Representation,

8

    rule_engine::ApplicationError,

9

};

10

11

register_representation!(SatOrderInt, "sat_order_int");

12

13

#[derive(Clone, Debug)]

14

pub struct SatOrderInt {

15

    src_var: Name,

16

    upper_bound: i32,

17

    lower_bound: i32,

18

19

20

impl SatOrderInt {

21

    /// Returns the names of the boolean variables used in the order encoding.

22

1458

    fn names(&self) -> impl Iterator<Item = Name> + '_ {

23

6798

        (self.lower_bound..self.upper_bound).map(move |index| self.index_to_name(index))

24

1458

25

26

    /// Gets the representation variable name corresponding to a concrete integer value.

27

200196

    fn index_to_name(&self, index: i32) -> Name {

28

200196

        Name::Represented(Box::new((

29

200196

            self.src_var.clone(),

30

200196

            self.repr_name().into(),

31

200196

            format!("{index:02}").into(), // stored as _00, _01, ...

32

200196

)))

33

200196

34

35

36

impl Representation for SatOrderInt {

37

    /// Creates a order int representation object for the given name.

38

462

    fn init(name: &Name, symtab: &SymbolTable) -> Option<Self> {

39

462

        let domain = symtab.resolve_domain(name)?;

40

41

462

        if !domain.is_finite() {

42

            return None;

43

462

44

45

462

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

46

            return None;

47

};

48

49

        // Determine min/max and return None if range is unbounded

50

462

        let (min, max) =

51

462

            ranges

52

462

                .iter()

53

462

                .try_fold((i32::MAX, i32::MIN), |(min_a, max_b), range| {

54

462

                    let lb = range.low()?;

55

462

                    let ub = range.high()?;

56

462

                    Some((min_a.min(*lb), max_b.max(*ub)))

57

462

                })?;

58

59

462

        Some(SatOrderInt {

60

462

            src_var: name.clone(),

61

462

            lower_bound: min,

62

462

            upper_bound: max + 1,

63

462

})

64

462

65

66

    /// The variable being represented.

67

    fn variable_name(&self) -> &Name {

68

        &self.src_var

69

70

71

    fn value_down(

72

        &self,

73

        _value: Literal,

74

    ) -> Result<std::collections::BTreeMap<Name, Literal>, ApplicationError> {

75

        // NOTE: It's unclear where and when `value_down` would be called for

76

        // order encoding. This is also never called in log encoding, so we

77

        // deliberately fail here to surface unexpected usage.

78

        bug!("value_down is not implemented for order encoding and should not be called")

79

80

81

    /// Given the values for its boolean representation variables, creates an assignment for `self` - the integer form.

82

18810

    fn value_up(

83

18810

        &self,

84

18810

        values: &std::collections::BTreeMap<Name, Literal>,

85

18810

    ) -> Result<Literal, ApplicationError> {

86

18810

        let mut first_false_candidate: Option<i32> = None;

87

88

193398

        for value_candidate in self.lower_bound..self.upper_bound {

89

193398

            let name = self.index_to_name(value_candidate);

90

193398

            let value_literal = values

91

193398

                .get(&name)

92

193398

                .ok_or(ApplicationError::RuleNotApplicable)?;

93

94

193398

            let is_true = match value_literal {

95

101616

                Literal::Int(1) | Literal::Bool(true) => true,

96

91782

                Literal::Int(0) | Literal::Bool(false) => false,

97

                _ => return Err(ApplicationError::RuleNotApplicable),

98

};

99

100

193398

            if !is_true && first_false_candidate.is_none() {

101

16776

                first_false_candidate = Some(value_candidate);

102

176622

103

104

193398

            if is_true && first_false_candidate.is_some() {

105

                // we have a true after a false

106

                return Err(ApplicationError::RuleNotApplicable);

107

193398

108

109

110

18810

        if let Some(first_false) = first_false_candidate {

111

16776

            return Ok(Literal::Int(first_false - 1));

112

2034

113

114

        // if we are here, all are true. So the value is the last one.

115

2034

        Ok(Literal::Int(self.upper_bound - 1))

116

18810

117

118

    /// Returns [`Expression`]s representing each boolean representation variable.

119

996

    fn expression_down(

120

996

        &self,

121

996

        st: &SymbolTable,

122

996

    ) -> Result<std::collections::BTreeMap<Name, Expression>, ApplicationError> {

123

996

        Ok(self

124

996

            .names()

125

996

            .enumerate()

126

4512

            .map(|(index, name)| {

127

4512

                let decl = st.lookup(&name).unwrap();

128

4512

129

                    // Machine names are used so that the derived ordering matches the correct ordering of the representation variables

130

4512

                    Name::Machine(index as i32),

131

4512

                    Expression::Atomic(

132

4512

                        Metadata::new(),

133

4512

                        Atom::Reference(conjure_cp::ast::Reference { ptr: decl }),

134

4512

),

135

4512

136

4512

})

137

996

            .collect())

138

996

139

140

    /// Creates declarations for the boolean representation variables of `self`.

141

462

    fn declaration_down(&self) -> Result<Vec<DeclarationPtr>, ApplicationError> {

142

462

        let temp_a = self

143

462

            .names()

144

2286

            .map(|name| DeclarationPtr::new_find(name, Domain::bool()))

145

462

            .collect();

146

147

462

        Ok(temp_a)

148

462

149

150

    /// The rule name for this representation.

151

202650

    fn repr_name(&self) -> &str {

152

202650

        "sat_order_int"

153

202650

154

155

    /// Makes a clone of `self` into a `Representation` trait object.

156

29817

    fn box_clone(&self) -> Box<dyn Representation> {

157

29817

        Box::new(self.clone()) as _

158

29817

159