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

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

22

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

23

24

25

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

26

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

27

        Name::Represented(Box::new((

28

            self.src_var.clone(),

29

            self.repr_name().into(),

30

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

31

)))

32

33

34

35

impl Representation for SATLogInt {

36

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

37

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

38

        let domain = symtab.resolve_domain(name)?;

39

40

        if !domain.is_finite() {

41

            return None;

42

43

44

        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

        let (min, max) =

50

            ranges

51

                .iter()

52

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

53

                    let lb = range.low()?;

54

                    let ub = range.high()?;

55

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

56

                })?;

57

58

        // calculate the bits needed to represent the integer

59

        let bit_count = (1..=32)

60

            .find(|&bits| {

61

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

62

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

63

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

64

})

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

        Some(SATLogInt {

68

            src_var: name.clone(),

69

            bits: bit_count,

70

})

71

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

    fn value_up(

100

        &self,

101

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

102

    ) -> Result<Literal, ApplicationError> {

103

        let mut out: i32 = 0;

104

        let mut power: i32 = 1;

105

106

        for name in self.names() {

107

            let value = values

108

                .get(&name)

109

                .ok_or(ApplicationError::RuleNotApplicable)?;

110

111

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

112

                out += *value * power;

113

                power <<= 1;

114

            } else {

115

                return Err(ApplicationError::RuleNotApplicable);

116

117

118

119

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

120

        // Mask to `BITS` bits

121

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

122

123

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

124

        if out & sign_bit != 0 {

125

            out -= sign_bit << 1;

126

127

128

        Ok(Literal::Int(out))

129

130

131

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

132

    fn expression_down(

133

        &self,

134

        st: &SymbolTable,

135

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

136

        Ok(self

137

            .names()

138

            .enumerate()

139

            .map(|(index, name)| {

140

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

141

142

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

143

                    Name::Machine(index as i32),

144

                    Expression::Atomic(

145

                        Metadata::new(),

146

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

147

),

148

149

})

150

            .collect())

151

152

153

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

154

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

155

        Ok(self

156

            .names()

157

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

158

            .collect())

159

160

161

    /// The rule name for this representaion.

162

    fn repr_name(&self) -> &str {

163

        "sat_log_int"

164

165

166

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

167

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

168

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

169

170