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
    fn names(&self) -> impl Iterator<Item = Name> + '_ {
23
        (self.lower_bound..self.upper_bound).map(move |index| self.index_to_name(index))
24
    }
25

            
26
    /// Gets the representation variable name corresponding to a concrete integer value.
27
    fn index_to_name(&self, index: i32) -> Name {
28
        Name::Represented(Box::new((
29
            self.src_var.clone(),
30
            self.repr_name().into(),
31
            format!("{index:02}").into(), // stored as _00, _01, ...
32
        )))
33
    }
34
}
35

            
36
impl Representation for SatOrderInt {
37
    /// Creates a order int representation object for the given name.
38
    fn init(name: &Name, symtab: &SymbolTable) -> Option<Self> {
39
        let domain = symtab.resolve_domain(name)?;
40

            
41
        if !domain.is_finite() {
42
            return None;
43
        }
44

            
45
        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
        let (min, max) =
51
            ranges
52
                .iter()
53
                .try_fold((i32::MAX, i32::MIN), |(min_a, max_b), range| {
54
                    let lb = range.low()?;
55
                    let ub = range.high()?;
56
                    Some((min_a.min(*lb), max_b.max(*ub)))
57
                })?;
58

            
59
        Some(SatOrderInt {
60
            src_var: name.clone(),
61
            lower_bound: min,
62
            upper_bound: max + 1,
63
        })
64
    }
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
    fn value_up(
83
        &self,
84
        values: &std::collections::BTreeMap<Name, Literal>,
85
    ) -> Result<Literal, ApplicationError> {
86
        let mut first_false_candidate: Option<i32> = None;
87

            
88
        for value_candidate in self.lower_bound..self.upper_bound {
89
            let name = self.index_to_name(value_candidate);
90
            let value_literal = values
91
                .get(&name)
92
                .ok_or(ApplicationError::RuleNotApplicable)?;
93

            
94
            let is_true = match value_literal {
95
                Literal::Int(1) | Literal::Bool(true) => true,
96
                Literal::Int(0) | Literal::Bool(false) => false,
97
                _ => return Err(ApplicationError::RuleNotApplicable),
98
            };
99

            
100
            if !is_true && first_false_candidate.is_none() {
101
                first_false_candidate = Some(value_candidate);
102
            }
103

            
104
            if is_true && first_false_candidate.is_some() {
105
                // we have a true after a false
106
                return Err(ApplicationError::RuleNotApplicable);
107
            }
108
        }
109

            
110
        if let Some(first_false) = first_false_candidate {
111
            return Ok(Literal::Int(first_false - 1));
112
        }
113

            
114
        // if we are here, all are true. So the value is the last one.
115
        Ok(Literal::Int(self.upper_bound - 1))
116
    }
117

            
118
    /// Returns [`Expression`]s representing each boolean representation variable.
119
    fn expression_down(
120
        &self,
121
        st: &SymbolTable,
122
    ) -> Result<std::collections::BTreeMap<Name, Expression>, ApplicationError> {
123
        Ok(self
124
            .names()
125
            .enumerate()
126
            .map(|(index, name)| {
127
                let decl = st.lookup(&name).unwrap();
128
                (
129
                    // Machine names are used so that the derived ordering matches the correct ordering of the representation variables
130
                    Name::Machine(index as i32),
131
                    Expression::Atomic(
132
                        Metadata::new(),
133
                        Atom::Reference(conjure_cp::ast::Reference { ptr: decl }),
134
                    ),
135
                )
136
            })
137
            .collect())
138
    }
139

            
140
    /// Creates declarations for the boolean representation variables of `self`.
141
    fn declaration_down(&self) -> Result<Vec<DeclarationPtr>, ApplicationError> {
142
        let temp_a = self
143
            .names()
144
            .map(|name| DeclarationPtr::new_find(name, Domain::bool()))
145
            .collect();
146

            
147
        Ok(temp_a)
148
    }
149

            
150
    /// The rule name for this representation.
151
    fn repr_name(&self) -> &str {
152
        "sat_order_int"
153
    }
154

            
155
    /// Makes a clone of `self` into a `Representation` trait object.
156
    fn box_clone(&self) -> Box<dyn Representation> {
157
        Box::new(self.clone()) as _
158
    }
159
}