Grcov report - sat_log

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!(SATLogInt, "sat_log_int");

12

13

#[derive(Clone, Debug)]

14

pub struct SATLogInt {

15

    src_var: Name,

16

    bits: u32,

17

18

19

impl SATLogInt {

20

    /// Returns the names of the representation variable

21

14625

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

22

64656

        (0..self.bits).map(move |index| self.index_to_name(index))

23

14625

24

25

    /// Gets the representation variable name for a specific index.

26

64656

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

27

64656

        Name::Represented(Box::new((

28

64656

            self.src_var.clone(),

29

64656

            self.repr_name().into(),

30

64656

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

31

64656

)))

32

64656

33

34

35

impl Representation for SATLogInt {

36

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

37

171

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

38

171

        let domain = symtab.resolve_domain(name)?;

39

40

171

        if !domain.is_finite() {

41

            return None;

42

171

43

44

171

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

45

            return None;

46

};

47

48

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

49

171

        let (min, max) =

50

171

            ranges

51

171

                .iter()

52

201

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

53

201

                    let lb = range.low()?;

54

201

                    let ub = range.high()?;

55

201

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

56

201

                })?;

57

58

        // calculate the bits needed to represent the integer

59

171

        let bit_count = (1..=32)

60

699

            .find(|&bits| {

61

699

                let min_possible = -(1i64 << (bits - 1));

62

699

                let max_possible = (1i64 << (bits - 1)) - 1;

63

699

                (min as i64) >= min_possible && (max as i64) <= max_possible

64

699

})

65

            .unwrap_or_else(|| bug!("Should never be reached: i32 integer should always be with storable with 32 bits.")); // safe unwrap as i32 fits in 32 bits

66

67

171

        Some(SATLogInt {

68

171

            src_var: name.clone(),

69

171

            bits: bit_count,

70

171

})

71

171

72

73

    /// The variable being represented.

74

    fn variable_name(&self) -> &Name {

75

        &self.src_var

76

77

78

    /// Given the integer assignment for `self`, creates assignments for its representation variables.

79

    fn value_down(

80

        &self,

81

        value: Literal,

82

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

83

        let Literal::Int(mut value_i32) = value else {

84

            return Err(ApplicationError::RuleNotApplicable);

85

};

86

87

        let mut result = std::collections::BTreeMap::new();

88

89

        // name_0 is the least significant bit, name_<final> is the sign bit

90

        for name in self.names() {

91

            result.insert(name, Literal::Bool((value_i32 & 1) != 0));

92

            value_i32 >>= 1;

93

94

95

        Ok(result)

96

97

98

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

99

13374

    fn value_up(

100

13374

        &self,

101

13374

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

102

13374

    ) -> Result<Literal, ApplicationError> {

103

13374

        let mut out: i32 = 0;

104

13374

        let mut power: i32 = 1;

105

106

59706

        for name in self.names() {

107

59706

            let value = values

108

59706

                .get(&name)

109

59706

                .ok_or(ApplicationError::RuleNotApplicable)?;

110

111

59706

            if let Literal::Int(value) = value {

112

59706

                out += *value * power;

113

59706

                power <<= 1;

114

59706

            } else {

115

                return Err(ApplicationError::RuleNotApplicable);

116

117

118

119

13374

        let sign_bit = 1 << (self.bits - 1);

120

        // Mask to `BITS` bits

121

13374

        out &= (sign_bit << 1) - 1;

122

123

        // If the sign bit is set, convert to negative using two's complement

124

13374

        if out & sign_bit != 0 {

125

1467

            out -= sign_bit << 1;

126

11907

127

128

13374

        Ok(Literal::Int(out))

129

13374

130

131

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

132

738

    fn expression_down(

133

738

        &self,

134

738

        st: &SymbolTable,

135

738

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

136

738

        Ok(self

137

738

            .names()

138

738

            .enumerate()

139

2853

            .map(|(index, name)| {

140

2853

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

141

2853

142

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

143

2853

                    Name::Machine(index as i32),

144

2853

                    Expression::Atomic(

145

2853

                        Metadata::new(),

146

2853

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

147

2853

),

148

2853

149

2853

})

150

738

            .collect())

151

738

152

153

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

154

513

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

155

513

        Ok(self

156

513

            .names()

157

2097

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

158

513

            .collect())

159

513

160

161

    /// The rule name for this representaion.

162

65619

    fn repr_name(&self) -> &str {

163

65619

        "sat_log_int"

164

65619

165

166

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

167

62775

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

168

62775

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

169

62775

170