conjure_core/solver/adaptors/
sat_common.rs

1//! Common code for SAT adaptors.
2//! Primarily, this is CNF related code.
3
4use std::cell::Ref;
5use std::collections::HashMap;
6use std::rc::Rc;
7
8use thiserror::Error;
9
10use crate::{
11    ast as conjure_ast, solver::SolverError, solver::SolverError::*, Model as ConjureModel,
12};
13// (nd60, march 24) - i basically copied all this from @gskorokod's SAT implemention for the old
14// solver interface.
15use crate::metadata::Metadata;
16
17/// A representation of a model in CNF.
18///
19/// Expects Model to be in the Conjunctive Normal Form:
20///
21/// - All variables must be boolean
22/// - Expressions must be `Reference`, `Not(Reference)`, or `Or(Reference1, Not(Reference2), ...)`
23/// - The top level And() may contain nested Or()s. Any other nested expressions are not allowed.
24#[derive(Debug, Clone)]
25pub struct CNFModel {
26    pub clauses: Vec<Vec<i32>>,
27    variables: HashMap<conjure_ast::Name, i32>,
28    next_ind: i32,
29}
30impl CNFModel {
31    pub fn new() -> CNFModel {
32        CNFModel {
33            clauses: Vec::new(),
34            variables: HashMap::new(),
35            next_ind: 1,
36        }
37    }
38
39    pub fn from_conjure(conjure_model: ConjureModel) -> Result<CNFModel, SolverError> {
40        let mut ans: CNFModel = CNFModel::new();
41
42        let submodel = conjure_model.as_submodel();
43        let symtab = submodel.symbols();
44        for (name, decl) in symtab.clone().into_iter() {
45            // ignore symbols that are not variables.
46            let Some(var) = decl.as_var() else {
47                continue;
48            };
49
50            // Check that domain has the correct type
51            if var.domain != conjure_ast::Domain::BoolDomain {
52                return Err(ModelFeatureNotSupported(format!(
53                    "variable {:?} is not BoolDomain",
54                    name
55                )));
56            }
57
58            ans.add_variable(&name);
59        }
60
61        for expr in submodel.constraints() {
62            match ans.add_expression(expr) {
63                Ok(_) => {}
64                Err(error) => {
65                    let message = format!("{:?}", error);
66                    return Err(ModelFeatureNotSupported(message));
67                }
68            }
69        }
70
71        Ok(ans)
72    }
73
74    /// Gets all the Conjure variables in the CNF.
75    #[allow(dead_code)] // It will be used once we actually run kissat
76    pub fn get_variables(&self) -> Vec<&conjure_ast::Name> {
77        let mut ans: Vec<&conjure_ast::Name> = Vec::new();
78
79        for key in self.variables.keys() {
80            ans.push(key);
81        }
82
83        ans
84    }
85
86    /// Gets the index of a Conjure variable.
87    pub fn get_index(&self, var: &conjure_ast::Name) -> Option<i32> {
88        self.variables.get(var).copied()
89    }
90
91    /// Gets a Conjure variable by index.
92    pub fn get_name(&self, ind: i32) -> Option<&conjure_ast::Name> {
93        for key in self.variables.keys() {
94            let idx = self.get_index(key)?;
95            if idx == ind {
96                return Some(key);
97            }
98        }
99
100        None
101    }
102
103    /// Adds a new Conjure variable to the CNF representation.
104    pub fn add_variable(&mut self, var: &conjure_ast::Name) {
105        self.variables.insert(var.clone(), self.next_ind);
106        self.next_ind += 1;
107    }
108
109    /**
110     * Check if a Conjure variable or index is present in the CNF
111     */
112    pub fn has_variable<T: HasVariable>(&self, value: T) -> bool {
113        value.has_variable(self)
114    }
115
116    /**
117     * Add a new clause to the CNF. Must be a vector of indices in CNF format
118     */
119    pub fn add_clause(&mut self, vec: &Vec<i32>) -> Result<(), CNFError> {
120        for idx in vec {
121            if !self.has_variable(idx.abs()) {
122                return Err(CNFError::ClauseIndexNotFound(*idx));
123            }
124        }
125        self.clauses.push(vec.clone());
126        Ok(())
127    }
128
129    /**
130     * Add a new Conjure expression to the CNF. Must be a logical expression in CNF form
131     */
132    pub fn add_expression(&mut self, expr: &conjure_ast::Expression) -> Result<(), CNFError> {
133        for row in self.handle_expression(expr)? {
134            self.add_clause(&row)?;
135        }
136        Ok(())
137    }
138
139    /**
140     * Convert the CNF to a Conjure expression
141     */
142    #[allow(dead_code)] // It will be used once we actually run kissat
143    pub fn as_expression(&self) -> Result<conjure_ast::Expression, CNFError> {
144        let mut expr_clauses: Vec<conjure_ast::Expression> = Vec::new();
145
146        for clause in &self.clauses {
147            expr_clauses.push(self.clause_to_expression(clause)?);
148        }
149
150        Ok(conjure_ast::Expression::And(Metadata::new(), expr_clauses))
151    }
152
153    /**
154     * Convert a single clause to a Conjure expression
155     */
156    fn clause_to_expression(&self, clause: &Vec<i32>) -> Result<conjure_ast::Expression, CNFError> {
157        let mut ans: Vec<conjure_ast::Expression> = Vec::new();
158
159        for idx in clause {
160            match self.get_name(idx.abs()) {
161                None => return Err(CNFError::ClauseIndexNotFound(*idx)),
162                Some(name) => {
163                    if *idx > 0 {
164                        ans.push(conjure_ast::Expression::Atomic(
165                            Metadata::new(),
166                            conjure_ast::Atom::Reference(name.clone()),
167                        ));
168                    } else {
169                        let expression: conjure_ast::Expression = conjure_ast::Expression::Atomic(
170                            Metadata::new(),
171                            conjure_ast::Atom::Reference(name.clone()),
172                        );
173                        ans.push(conjure_ast::Expression::Not(
174                            Metadata::new(),
175                            Box::from(expression),
176                        ))
177                    }
178                }
179            }
180        }
181
182        Ok(conjure_ast::Expression::Or(Metadata::new(), ans))
183    }
184
185    /**
186     * Get the index for a Conjure Reference or return an error
187     * @see get_index
188     * @see conjure_ast::Expression::Reference
189     */
190    fn get_reference_index(&self, name: &conjure_ast::Name) -> Result<i32, CNFError> {
191        match self.get_index(name) {
192            None => Err(CNFError::VariableNameNotFound(name.clone())),
193            Some(ind) => Ok(ind),
194        }
195    }
196
197    /**
198     * Convert the contents of a single Reference to a row of the CNF format
199     * @see get_reference_index
200     * @see conjure_ast::Expression::Reference
201     */
202    fn handle_reference(&self, name: &conjure_ast::Name) -> Result<Vec<i32>, CNFError> {
203        Ok(vec![self.get_reference_index(name)?])
204    }
205
206    /**
207     * Convert the contents of a single Not() to CNF
208     */
209    fn handle_not(&self, expr: &conjure_ast::Expression) -> Result<Vec<i32>, CNFError> {
210        match expr {
211            // Expression inside the Not()
212            conjure_ast::Expression::Atomic(_metadata, conjure_ast::Atom::Reference(name)) => {
213                Ok(vec![-self.get_reference_index(name)?])
214            }
215            _ => Err(CNFError::UnexpectedExpressionInsideNot(expr.clone())),
216        }
217    }
218
219    /**
220     * Convert the contents of a single Or() to a row of the CNF format
221     */
222    fn handle_or(&self, expressions: &Vec<conjure_ast::Expression>) -> Result<Vec<i32>, CNFError> {
223        let mut ans: Vec<i32> = Vec::new();
224
225        for expr in expressions {
226            let ret = self.handle_flat_expression(expr)?;
227            for ind in ret {
228                ans.push(ind);
229            }
230        }
231
232        Ok(ans)
233    }
234
235    /**
236     * Convert a single Reference, `Not` or `Or` into a clause of the CNF format
237     */
238    fn handle_flat_expression(
239        &self,
240        expression: &conjure_ast::Expression,
241    ) -> Result<Vec<i32>, CNFError> {
242        match expression {
243            conjure_ast::Expression::Atomic(_metadata, conjure_ast::Atom::Reference(name)) => {
244                self.handle_reference(name)
245            }
246            conjure_ast::Expression::Not(_metadata, var_box) => self.handle_not(var_box),
247            conjure_ast::Expression::Or(_metadata, expressions) => self.handle_or(expressions),
248            _ => Err(CNFError::UnexpectedExpression(expression.clone())),
249        }
250    }
251
252    /**
253     * Convert a single And() into a vector of clauses in the CNF format
254     */
255    fn handle_and(
256        &self,
257        expressions: &Vec<conjure_ast::Expression>,
258    ) -> Result<Vec<Vec<i32>>, CNFError> {
259        let mut ans: Vec<Vec<i32>> = Vec::new();
260
261        for expression in expressions {
262            match expression {
263                conjure_ast::Expression::And(_metadata, _expressions) => {
264                    return Err(CNFError::NestedAnd(expression.clone()));
265                }
266                _ => {
267                    ans.push(self.handle_flat_expression(expression)?);
268                }
269            }
270        }
271
272        Ok(ans)
273    }
274
275    /**
276     * Convert a single Conjure expression into a vector of clauses of the CNF format
277     */
278    fn handle_expression(
279        &self,
280        expression: &conjure_ast::Expression,
281    ) -> Result<Vec<Vec<i32>>, CNFError> {
282        match expression {
283            conjure_ast::Expression::And(_metadata, expressions) => self.handle_and(expressions),
284            _ => Ok(vec![self.handle_flat_expression(expression)?]),
285        }
286    }
287}
288
289impl Default for CNFModel {
290    fn default() -> Self {
291        Self::new()
292    }
293}
294
295#[derive(Error, Debug)]
296pub enum CNFError {
297    #[error("Variable with name `{0}` not found")]
298    VariableNameNotFound(conjure_ast::Name),
299
300    #[error("Clause with index `{0}` not found")]
301    ClauseIndexNotFound(i32),
302
303    #[error("Unexpected Expression `{0}` inside Not(). Only Not(Reference) allowed!")]
304    UnexpectedExpressionInsideNot(conjure_ast::Expression),
305
306    #[error(
307        "Unexpected Expression `{0}` found. Only Reference, Not(Reference) and Or(...) allowed!"
308    )]
309    UnexpectedExpression(conjure_ast::Expression),
310
311    #[error("Unexpected nested And: {0}")]
312    NestedAnd(conjure_ast::Expression),
313}
314
315/// Helper trait for checking if a variable is present in the CNF polymorphically (i32 or conjure_ast::Name)
316pub trait HasVariable {
317    fn has_variable(self, cnf: &CNFModel) -> bool;
318}
319
320impl HasVariable for i32 {
321    fn has_variable(self, cnf: &CNFModel) -> bool {
322        cnf.get_name(self).is_some()
323    }
324}
325
326impl HasVariable for &conjure_ast::Name {
327    fn has_variable(self, cnf: &CNFModel) -> bool {
328        cnf.get_index(self).is_some()
329    }
330}
conjure_core/solver/adaptors/sat_common.rs

conjure_core/solver/adaptors/
sat_common.rs
