taco_smt_encoder/
expression_encoding.rs

1//! Encoding of expressions into [`SMTExpr`]
2//!
3//! This module provides traits and types to encode boolean or integer
4//! expressions into SMT expressions. The encoding is done using the `easy-smt`
5//! crate, therefore the expressions are encoded into `SExpr` types.
6
7use std::{collections::HashMap, fmt, io};
8
9use std::hash::Hash;
10
11use easy_smt::SExpr;
12use taco_threshold_automaton::{
13    RuleDefinition,
14    expressions::{
15        Atomic, BooleanConnective, BooleanExpression, ComparisonOp, IntegerExpression, IntegerOp,
16        Location, Parameter, Variable,
17    },
18    general_threshold_automaton::Rule,
19};
20
21use crate::{SMTExpr, SMTSolution, SMTSolver, SMTSolverBuilder, SMTSolverContext};
22
23pub mod config_ctx;
24pub mod ctx_mgr;
25pub mod step_ctx;
26pub mod ta_encoding;
27
28/// Trait defining the encoding of type `T` into an S[`SMTExpr`] given a context
29///
30/// If this trait is implemented for a type `T`, expressions of type `T` can be
31/// encoded into an SMT expression, using the given SMT solver and context of
32/// type `C`. This trait does not restrict the type of the context.
33pub trait EncodeToSMT<T, C> {
34    /// Encode the type into an SMT expression
35    ///
36    /// Encode the expression of type `T` into an SMT expression using the
37    /// given SMT solver and context of type `C`.
38    fn encode_to_smt_with_ctx(
39        &self,
40        solver: &SMTSolver,
41        ctx: &C,
42    ) -> Result<SMTExpr, SMTSolverError>;
43}
44
45/// Trait of a context that provides mapping from type declaring SMT variables
46/// `T` to  associated SMT expression
47///
48/// This trait is implemented by contexts that can provide the corresponding
49/// [`SMTExpr`] for a given expression stored in the context. Implementing
50/// this trait allows to encode integer and boolean expressions into
51/// [`SMTExpr`]s.
52pub trait SMTVariableContext<T> {
53    /// Get the corresponding [`SMTExpr`] for the given expression of type
54    /// `T`
55    ///
56    /// This function returns an error if the expression is not stored in the
57    /// context, or it tried to declare a variable and the connection to the
58    /// SMT solver broke.
59    fn get_expr_for(&self, expr: &T) -> Result<SMTExpr, SMTSolverError>;
60
61    /// Get all expressions for which the current context holds an assignment
62    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a T>
63    where
64        T: 'a;
65
66    /// Get the solution assignment
67    fn get_solution<'a>(
68        &'a self,
69        solver: &mut SMTSolver,
70        res: SMTSolution,
71    ) -> Result<HashMap<T, u32>, SMTSolverError>
72    where
73        T: 'a + Eq + Hash + Clone,
74    {
75        match res {
76            SMTSolution::UNSAT => Err(SMTSolverError::ExtractionFromUnsat),
77            SMTSolution::SAT => {
78                let expr_vec = self
79                    .get_exprs()
80                    .into_iter()
81                    .map(|t| self.get_expr_for(t))
82                    .collect::<Result<Vec<_>, _>>()?;
83
84                let solution = solver.get_value(expr_vec)?;
85
86                solution
87                    .into_iter()
88                    .zip(self.get_exprs())
89                    .map(|((_, sol), t)| {
90                        let solution_value = solver.get_u32(sol).ok_or_else(|| {
91                            let sol = solver.display(sol);
92                            SMTSolverError::SolutionExtractionParseIntError(sol.to_string())
93                        })?;
94
95                        Ok((t.clone(), solution_value))
96                    })
97                    .collect::<Result<HashMap<T, u32>, SMTSolverError>>()
98            }
99        }
100    }
101}
102
103impl<T: Hash + Eq + DeclaresVariable> SMTVariableContext<T> for HashMap<T, SExpr> {
104    fn get_expr_for(&self, expr: &T) -> Result<SMTExpr, SMTSolverError> {
105        self.get(expr)
106            .ok_or_else(|| expr.get_undeclared_error())
107            .copied()
108    }
109
110    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a T>
111    where
112        T: 'a,
113    {
114        self.keys()
115    }
116}
117
118/// Trait for types that have associated SMT variables
119///
120/// This trait is implemented by types that are usually encoded as variables
121/// when constructing formulas over threshold automata. A type implementing this
122/// trait needs to provide a naming scheme for the smt variables associated with
123/// the type and a method to construct an error if the variable is not declared.
124pub trait DeclaresVariable {
125    /// Get the name of the associated variable for the given index
126    ///
127    /// This function should return the name of the variable associated with
128    /// the type for the given index. The naming scheme **must** result in a
129    /// unique name across all variables used in the SMT solver.
130    ///
131    /// The `index` field is used for variables that are usually indexed. For
132    /// example, along a path, the location variable (representing the number of
133    /// processes in this location) is usually indexed by the configuration.
134    fn get_name(&self, index: u32) -> String;
135
136    /// Declare the variable in the SMT solver
137    ///
138    /// This function declares the variable in the SMT solver and returns the
139    /// SMT expression. Returns an error if the connection to the SMT solver
140    /// broke.
141    fn declare_variable(
142        &self,
143        solver: &mut SMTSolver,
144        index: u32,
145    ) -> Result<SMTExpr, SMTSolverError> {
146        let name = self.get_name(index);
147        Ok(solver.declare_const(&name, solver.int_sort())?)
148    }
149
150    /// Returns an error indicating that `self` was not declared in the current
151    /// SMT context.
152    fn get_undeclared_error(&self) -> SMTSolverError;
153}
154
155impl DeclaresVariable for Location {
156    fn get_name(&self, index: u32) -> String {
157        format!("loc_{}_{}", self.name(), index)
158    }
159
160    fn get_undeclared_error(&self) -> SMTSolverError {
161        SMTSolverError::UndeclaredLocation(self.clone())
162    }
163}
164
165impl DeclaresVariable for Parameter {
166    fn get_name(&self, _index: u32) -> String {
167        format!("param_{}", self.name())
168    }
169
170    fn get_undeclared_error(&self) -> SMTSolverError {
171        SMTSolverError::UndeclaredParameter(self.clone())
172    }
173}
174
175impl DeclaresVariable for Variable {
176    fn get_name(&self, index: u32) -> String {
177        format!("var_{}_{}", self.name(), index)
178    }
179
180    fn get_undeclared_error(&self) -> SMTSolverError {
181        SMTSolverError::UndeclaredVariable(self.clone())
182    }
183}
184
185impl DeclaresVariable for Rule {
186    fn get_name(&self, index: u32) -> String {
187        format!("rule_{}_{}", self.id(), index)
188    }
189
190    fn get_undeclared_error(&self) -> SMTSolverError {
191        SMTSolverError::UndeclaredRule(self.clone())
192    }
193}
194
195/// Trait that allows to extract the assignment of a variable from the solution
196/// found by the SMT solver
197///
198/// This trait is implemented by contexts allowing to extract the solution found
199/// by the SMT solver for a given variable.
200pub trait GetAssignment<T>: SMTVariableContext<T> + SMTSolverContext
201where
202    T: DeclaresVariable,
203{
204    /// Get the assigned solution of the variable
205    ///
206    /// This function returns the assignment of the variable from the SMT
207    /// solver. If the query is unsatisfiable, it returns `None`. If the query
208    /// is satisfiable, it returns the assigned value.
209    ///
210    /// Returns an error if the connection to the SMT solver broke.
211    fn get_assignment(&mut self, res: SMTSolution, var: &T) -> Result<Option<u64>, SMTSolverError> {
212        match res {
213            SMTSolution::SAT => {
214                let expr = self.get_expr_for(var)?;
215                let solver = self.get_smt_solver_mut();
216
217                let solution = solver.get_value(vec![expr])?;
218                debug_assert!(solution.len() == 1);
219                debug_assert!(solution[0].0 == expr);
220
221                let solution_int = solver.get_u64(solution[0].1);
222
223                let sol = solution_int.ok_or_else(|| {
224                    let sol = solver.display(expr);
225                    SMTSolverError::SolutionExtractionParseIntError(sol.to_string())
226                })?;
227
228                Ok(Some(sol))
229            }
230            SMTSolution::UNSAT => Err(SMTSolverError::ExtractionFromUnsat),
231        }
232    }
233}
234
235impl<T, U> EncodeToSMT<IntegerExpression<T>, U> for IntegerExpression<T>
236where
237    U: SMTVariableContext<T> + SMTVariableContext<Parameter>,
238    T: DeclaresVariable + Atomic,
239{
240    fn encode_to_smt_with_ctx(&self, solver: &SMTSolver, ctx: &U) -> Result<SExpr, SMTSolverError> {
241        match self {
242            IntegerExpression::Atom(a) => ctx.get_expr_for(a),
243            IntegerExpression::Const(c) => Ok(solver.numeral(*c)),
244            IntegerExpression::Param(parameter) => ctx.get_expr_for(parameter),
245            IntegerExpression::BinaryExpr(lhs, op, rhs) => {
246                let lhs = lhs.encode_to_smt_with_ctx(solver, ctx)?;
247                let rhs = rhs.encode_to_smt_with_ctx(solver, ctx)?;
248
249                Ok(match op {
250                    IntegerOp::Add => solver.plus(lhs, rhs),
251                    IntegerOp::Sub => solver.sub(lhs, rhs),
252                    IntegerOp::Mul => solver.times(lhs, rhs),
253                    IntegerOp::Div => solver.div(lhs, rhs),
254                })
255            }
256            IntegerExpression::Neg(expr) => {
257                let expr = expr.encode_to_smt_with_ctx(solver, ctx)?;
258                Ok(solver.negate(expr))
259            }
260        }
261    }
262}
263
264impl<T, U> EncodeToSMT<BooleanExpression<T>, U> for BooleanExpression<T>
265where
266    U: SMTVariableContext<T> + SMTVariableContext<Parameter>,
267    T: DeclaresVariable + Atomic,
268{
269    fn encode_to_smt_with_ctx(&self, solver: &SMTSolver, ctx: &U) -> Result<SExpr, SMTSolverError> {
270        match self {
271            BooleanExpression::ComparisonExpression(lhs, op, rhs) => {
272                let lhs = lhs.encode_to_smt_with_ctx(solver, ctx)?;
273                let rhs = rhs.encode_to_smt_with_ctx(solver, ctx)?;
274
275                Ok(match op {
276                    ComparisonOp::Gt => solver.gt(lhs, rhs),
277                    ComparisonOp::Geq => solver.gte(lhs, rhs),
278                    ComparisonOp::Eq => solver.eq(lhs, rhs),
279                    ComparisonOp::Neq => solver.not(solver.eq(lhs, rhs)),
280                    ComparisonOp::Leq => solver.lte(lhs, rhs),
281                    ComparisonOp::Lt => solver.lt(lhs, rhs),
282                })
283            }
284            BooleanExpression::BinaryExpression(lhs, op, rhs) => {
285                let lhs = lhs.encode_to_smt_with_ctx(solver, ctx)?;
286                let rhs = rhs.encode_to_smt_with_ctx(solver, ctx)?;
287
288                Ok(match op {
289                    BooleanConnective::And => solver.and(lhs, rhs),
290                    BooleanConnective::Or => solver.or(lhs, rhs),
291                })
292            }
293            BooleanExpression::Not(expr) => {
294                let expr = expr.encode_to_smt_with_ctx(solver, ctx)?;
295
296                Ok(solver.not(expr))
297            }
298            BooleanExpression::True => Ok(solver.true_()),
299            BooleanExpression::False => Ok(solver.false_()),
300        }
301    }
302}
303
304/// Error occurring in the interaction with the SMT solver
305#[derive(Debug)]
306pub enum SMTSolverError {
307    /// Error from the SMT solver
308    EasySMTErr(io::Error),
309    /// Timeout in the SMT solver
310    SolverTimeout,
311    /// Undeclared Parameter accessed
312    UndeclaredParameter(Parameter),
313    /// Undeclared Location accessed
314    UndeclaredLocation(Location),
315    /// Undeclared Variable accessed
316    UndeclaredVariable(Variable),
317    /// Failed to parse integer from solution
318    SolutionExtractionParseIntError(String),
319    /// Undeclared Rule accessed
320    UndeclaredRule(Rule),
321    /// Attempted to extract solution from an unsatisfiable expression
322    ExtractionFromUnsat,
323    /// Specification is trivially unsatisfiable, reason in spec
324    TriviallyUnsat(String),
325}
326
327impl std::error::Error for SMTSolverError {}
328
329impl fmt::Display for SMTSolverError {
330    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
331        match self {
332            SMTSolverError::EasySMTErr(err) => {
333                write!(f, "Error from connection to SMT solver: {err}")
334            }
335            SMTSolverError::UndeclaredParameter(param) => {
336                write!(f, "Undeclared parameter: {param}")
337            }
338            SMTSolverError::UndeclaredLocation(location) => {
339                write!(f, "Undeclared location: {location}")
340            }
341            SMTSolverError::UndeclaredVariable(variable) => {
342                write!(f, "Undeclared variable: {variable}")
343            }
344            SMTSolverError::SolverTimeout => write!(f, "Timeout in SMT solver"),
345            SMTSolverError::SolutionExtractionParseIntError(s) => write!(
346                f,
347                "Failed to parse SMT solver supplied solution into integer: {s} not an integer"
348            ),
349            SMTSolverError::UndeclaredRule(rule) => write!(f, "Undeclared rule: {rule}"),
350            SMTSolverError::ExtractionFromUnsat => write!(
351                f,
352                "Attempted to extract the solution assignment from an unsatisfiable expression"
353            ),
354            SMTSolverError::TriviallyUnsat(r) => {
355                write!(f, "Specification can never be true. Reason: {r}")
356            }
357        }
358    }
359}
360
361impl From<io::Error> for SMTSolverError {
362    fn from(error: io::Error) -> Self {
363        SMTSolverError::EasySMTErr(error)
364    }
365}
366
367/// A simple static context for encoding expressions related to threshold
368/// automata into SMT constraints and checking satisfiability
369///
370/// This context is used to encode expressions into SMT constraints and check
371/// their satisfiability. It should be only used to encode simple expressions,
372/// and is not designed to handle expressions over multiple configurations.
373pub struct StaticSMTContext {
374    solver: SMTSolver,
375    params: HashMap<Parameter, SMTExpr>,
376    locs: HashMap<Location, SMTExpr>,
377    vars: HashMap<Variable, Vec<SMTExpr>>,
378}
379
380impl StaticSMTContext {
381    /// Create a new static SMT context
382    ///
383    /// This function creates a new static SMT context with the given solver
384    /// builder and declares variables for the given parameters, locations, and
385    /// variables.
386    pub fn new(
387        solver_builder: SMTSolverBuilder,
388        params: impl IntoIterator<Item = Parameter>,
389        locs: impl IntoIterator<Item = Location>,
390        vars: impl IntoIterator<Item = Variable>,
391    ) -> Result<Self, SMTSolverError> {
392        let mut solver = solver_builder.new_solver();
393
394        let params = params
395            .into_iter()
396            .map(|p| {
397                let expr = p.declare_variable(&mut solver, 0)?;
398                Ok((p, expr))
399            })
400            .collect::<Result<HashMap<_, _>, SMTSolverError>>()?;
401
402        let locs = locs
403            .into_iter()
404            .map(|l| {
405                let expr = l.declare_variable(&mut solver, 0)?;
406                Ok((l, expr))
407            })
408            .collect::<Result<HashMap<_, _>, SMTSolverError>>()?;
409
410        let vars = vars
411            .into_iter()
412            .map(|v| {
413                let expr = v.declare_variable(&mut solver, 0)?;
414                Ok((v, vec![expr]))
415            })
416            .collect::<Result<HashMap<_, _>, SMTSolverError>>()?;
417
418        Ok(StaticSMTContext {
419            solver,
420            params,
421            locs,
422            vars,
423        })
424    }
425
426    /// Get the SMT expression for the `true` value
427    pub fn get_true(&self) -> SMTExpr {
428        self.solver.true_()
429    }
430
431    /// Declare a fresh variable
432    pub fn declare_new_int(&mut self, name: &str) -> Result<SMTExpr, SMTSolverError> {
433        let int_sort = self.solver.int_sort();
434        self.solver
435            .declare_const(name, int_sort)
436            .map_err(|e| e.into())
437    }
438
439    /// Encode the given expression into an SMT expression and return the
440    /// expression
441    pub fn encode_to_smt<T>(&self, expr: &T) -> Result<SMTExpr, SMTSolverError>
442    where
443        T: EncodeToSMT<T, Self>,
444    {
445        expr.encode_to_smt_with_ctx(&self.solver, self)
446    }
447}
448
449impl SMTSolverContext for StaticSMTContext {
450    fn get_smt_solver_mut(&mut self) -> &mut SMTSolver {
451        &mut self.solver
452    }
453
454    fn get_smt_solver(&self) -> &SMTSolver {
455        &self.solver
456    }
457}
458
459impl SMTVariableContext<Parameter> for StaticSMTContext {
460    fn get_expr_for(&self, param: &Parameter) -> Result<SMTExpr, SMTSolverError> {
461        self.params
462            .get(param)
463            .cloned()
464            .ok_or_else(|| SMTSolverError::UndeclaredParameter(param.clone()))
465    }
466
467    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a Parameter>
468    where
469        Parameter: 'a,
470    {
471        self.params.keys()
472    }
473}
474
475impl SMTVariableContext<Location> for StaticSMTContext {
476    fn get_expr_for(&self, loc: &Location) -> Result<SMTExpr, SMTSolverError> {
477        self.locs
478            .get(loc)
479            .cloned()
480            .ok_or_else(|| SMTSolverError::UndeclaredLocation(loc.clone()))
481    }
482
483    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a Location>
484    where
485        Location: 'a,
486    {
487        self.locs.keys()
488    }
489}
490
491impl SMTVariableContext<Variable> for StaticSMTContext {
492    fn get_expr_for(&self, var: &Variable) -> Result<SMTExpr, SMTSolverError> {
493        self.vars
494            .get(var)
495            .and_then(|v| v.first().cloned())
496            .ok_or_else(|| SMTSolverError::UndeclaredVariable(var.clone()))
497    }
498
499    fn get_exprs<'a>(&'a self) -> impl IntoIterator<Item = &'a Variable>
500    where
501        Variable: 'a,
502    {
503        self.vars.keys()
504    }
505}
506
507impl GetAssignment<Parameter> for StaticSMTContext {}
508impl GetAssignment<Variable> for StaticSMTContext {}
509impl GetAssignment<Location> for StaticSMTContext {}
510
511#[cfg(test)]
512mod tests {
513    use std::vec;
514
515    use easy_smt::Response;
516    use taco_threshold_automaton::general_threshold_automaton::builder::RuleBuilder;
517
518    use super::*;
519
520    #[test]
521    fn test_get_true() {
522        let builder = SMTSolverBuilder::default();
523
524        let mut ctx = StaticSMTContext::new(
525            builder,
526            vec![Parameter::new("p")],
527            vec![Location::new("loc")],
528            vec![Variable::new("x")],
529        )
530        .unwrap();
531
532        let top = ctx.get_true();
533
534        assert_eq!(top, ctx.get_smt_solver_mut().true_())
535    }
536
537    #[test]
538    fn test_rule_variable_name() {
539        let r = RuleBuilder::new(42, Location::new("src"), Location::new("tgt")).build();
540
541        assert!(r.get_name(0).contains("rule"));
542        assert!(r.get_name(0).contains("42"));
543        assert!(r.get_name(0).contains("0"));
544    }
545
546    #[test]
547    fn test_boolean_expr_encoding_true_false() {
548        let builder = SMTSolverBuilder::default();
549
550        let true_expr: BooleanExpression<Variable> = BooleanExpression::True;
551        let false_expr: BooleanExpression<Variable> = BooleanExpression::False;
552
553        let mut ctx = StaticSMTContext::new(
554            builder,
555            vec![Parameter::new("p")],
556            vec![Location::new("loc")],
557            vec![Variable::new("x")],
558        )
559        .unwrap();
560
561        let true_encoded = ctx.encode_to_smt(&true_expr).unwrap();
562        let false_encoded = ctx.encode_to_smt(&false_expr).unwrap();
563
564        let solver = ctx.get_smt_solver_mut();
565        let true_str = solver.display(true_encoded).to_string();
566        let false_str = solver.display(false_encoded).to_string();
567        assert_eq!(true_str, "true");
568        assert_eq!(false_str, "false");
569
570        solver.assert(true_encoded).unwrap();
571        assert_eq!(solver.check().unwrap(), Response::Sat);
572
573        solver.assert(false_encoded).unwrap();
574        assert_eq!(solver.check().unwrap(), Response::Unsat);
575    }
576
577    #[test]
578    fn test_boolean_expr_encoding_two_var_gt() {
579        let builder = SMTSolverBuilder::default();
580
581        let expr = BooleanExpression::ComparisonExpression(
582            Box::new(IntegerExpression::Atom(Variable::new("x"))),
583            ComparisonOp::Gt,
584            Box::new(IntegerExpression::Atom(Variable::new("y"))),
585        );
586
587        let mut ctx = StaticSMTContext::new(
588            builder,
589            vec![Parameter::new("p")],
590            vec![Location::new("loc")],
591            vec![Variable::new("x"), Variable::new("y")],
592        )
593        .unwrap();
594
595        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
596
597        let solver = ctx.get_smt_solver_mut();
598        let encoded_str = solver.display(encoded_expr).to_string();
599        assert_eq!(encoded_str, "(> var_x_0 var_y_0)");
600
601        solver.assert(encoded_expr).unwrap();
602        assert_eq!(solver.check().unwrap(), Response::Sat);
603    }
604
605    #[test]
606    fn test_boolean_expr_encoding_var_eq_const() {
607        let builder = SMTSolverBuilder::default();
608
609        let expr = BooleanExpression::ComparisonExpression(
610            Box::new(IntegerExpression::Atom(Variable::new("x"))),
611            ComparisonOp::Eq,
612            Box::new(IntegerExpression::Const(5)),
613        );
614
615        let mut ctx = StaticSMTContext::new(
616            builder,
617            vec![Parameter::new("p")],
618            vec![Location::new("loc")],
619            vec![Variable::new("x")],
620        )
621        .unwrap();
622
623        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
624
625        let solver = ctx.get_smt_solver_mut();
626        let encoded_str = solver.display(encoded_expr).to_string();
627        assert_eq!(encoded_str, "(= var_x_0 5)");
628
629        solver.assert(encoded_expr).unwrap();
630        assert_eq!(solver.check().unwrap(), Response::Sat);
631    }
632
633    #[test]
634    fn test_boolean_expr_encoding_var_and_const() {
635        let builder = SMTSolverBuilder::default();
636
637        let expr = BooleanExpression::BinaryExpression(
638            Box::new(BooleanExpression::ComparisonExpression(
639                Box::new(IntegerExpression::Atom(Variable::new("x"))),
640                ComparisonOp::Geq,
641                Box::new(IntegerExpression::Const(5)),
642            )),
643            BooleanConnective::And,
644            Box::new(BooleanExpression::ComparisonExpression(
645                Box::new(IntegerExpression::Atom(Variable::new("y"))),
646                ComparisonOp::Lt,
647                Box::new(IntegerExpression::Const(10)),
648            )),
649        );
650
651        let mut ctx = StaticSMTContext::new(
652            builder,
653            vec![Parameter::new("p")],
654            vec![Location::new("loc")],
655            vec![Variable::new("x"), Variable::new("y")],
656        )
657        .unwrap();
658
659        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
660
661        let solver = ctx.get_smt_solver_mut();
662        let encoded_str = solver.display(encoded_expr).to_string();
663        assert_eq!(encoded_str, "(and (>= var_x_0 5) (< var_y_0 10))");
664
665        solver.assert(encoded_expr).unwrap();
666        assert_eq!(solver.check().unwrap(), Response::Sat);
667    }
668
669    #[test]
670    fn test_boolean_expr_encoding_var_or_const() {
671        let builder = SMTSolverBuilder::default();
672
673        let expr = BooleanExpression::BinaryExpression(
674            Box::new(BooleanExpression::ComparisonExpression(
675                Box::new(IntegerExpression::Atom(Variable::new("x"))),
676                ComparisonOp::Leq,
677                Box::new(IntegerExpression::Const(5)),
678            )),
679            BooleanConnective::Or,
680            Box::new(BooleanExpression::ComparisonExpression(
681                Box::new(IntegerExpression::Param(Parameter::new("p"))),
682                ComparisonOp::Neq,
683                Box::new(IntegerExpression::Const(10)),
684            )),
685        );
686
687        let mut ctx = StaticSMTContext::new(
688            builder,
689            vec![Parameter::new("p")],
690            vec![Location::new("loc")],
691            vec![Variable::new("x"), Variable::new("y")],
692        )
693        .unwrap();
694
695        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
696
697        let solver = ctx.get_smt_solver_mut();
698        let encoded_str = solver.display(encoded_expr).to_string();
699        assert_eq!(encoded_str, "(or (<= var_x_0 5) (not (= param_p 10)))");
700
701        solver.assert(encoded_expr).unwrap();
702        assert_eq!(solver.check().unwrap(), Response::Sat);
703    }
704
705    #[test]
706    fn test_boolean_expr_encoding_not_var() {
707        let builder = SMTSolverBuilder::default();
708
709        let expr = BooleanExpression::Not(Box::new(BooleanExpression::ComparisonExpression(
710            Box::new(IntegerExpression::Atom(Location::new("loc"))),
711            ComparisonOp::Eq,
712            Box::new(IntegerExpression::Const(5)),
713        )));
714
715        let mut ctx = StaticSMTContext::new(
716            builder,
717            vec![Parameter::new("p")],
718            vec![Location::new("loc")],
719            vec![Variable::new("x")],
720        )
721        .unwrap();
722
723        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
724
725        let solver = ctx.get_smt_solver_mut();
726        let encoded_str = solver.display(encoded_expr).to_string();
727        assert_eq!(encoded_str, "(not (= loc_loc_0 5))");
728
729        solver.assert(encoded_expr).unwrap();
730        assert_eq!(solver.check().unwrap(), Response::Sat);
731    }
732
733    #[test]
734    fn test_integer_expr_encoding_add() {
735        let builder = SMTSolverBuilder::default();
736
737        let expr = IntegerExpression::BinaryExpr(
738            Box::new(IntegerExpression::Atom(Parameter::new("p"))),
739            IntegerOp::Add,
740            Box::new(IntegerExpression::Const(5)),
741        );
742
743        let mut ctx = StaticSMTContext::new(
744            builder,
745            vec![Parameter::new("p")],
746            vec![Location::new("loc")],
747            vec![Variable::new("x")],
748        )
749        .unwrap();
750
751        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
752
753        let solver = ctx.get_smt_solver_mut();
754        let encoded_str = solver.display(encoded_expr).to_string();
755        assert_eq!(encoded_str, "(+ param_p 5)");
756    }
757
758    #[test]
759    fn test_integer_expr_encoding_sub() {
760        let builder = SMTSolverBuilder::default();
761
762        let expr = IntegerExpression::BinaryExpr(
763            Box::new(IntegerExpression::Atom(Parameter::new("p"))),
764            IntegerOp::Sub,
765            Box::new(IntegerExpression::Const(3)),
766        );
767
768        let mut ctx = StaticSMTContext::new(
769            builder,
770            vec![Parameter::new("p")],
771            vec![Location::new("loc")],
772            vec![Variable::new("x")],
773        )
774        .unwrap();
775
776        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
777
778        let solver = ctx.get_smt_solver_mut();
779        let encoded_str = solver.display(encoded_expr).to_string();
780        assert_eq!(encoded_str, "(- param_p 3)");
781    }
782
783    #[test]
784    fn test_integer_expr_encoding_mul() {
785        let builder = SMTSolverBuilder::default();
786
787        let expr = IntegerExpression::BinaryExpr(
788            Box::new(IntegerExpression::Atom(Parameter::new("p"))),
789            IntegerOp::Mul,
790            Box::new(IntegerExpression::Const(2)),
791        );
792
793        let mut ctx = StaticSMTContext::new(
794            builder,
795            vec![Parameter::new("p")],
796            vec![Location::new("loc")],
797            vec![Variable::new("x")],
798        )
799        .unwrap();
800
801        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
802
803        let solver = ctx.get_smt_solver_mut();
804        let encoded_str = solver.display(encoded_expr).to_string();
805        assert_eq!(encoded_str, "(* param_p 2)");
806    }
807
808    #[test]
809    fn test_integer_expr_encoding_div() {
810        let builder = SMTSolverBuilder::default();
811
812        let expr = IntegerExpression::BinaryExpr(
813            Box::new(IntegerExpression::Atom(Variable::new("x"))),
814            IntegerOp::Div,
815            Box::new(IntegerExpression::Const(4)),
816        );
817
818        let mut ctx = StaticSMTContext::new(
819            builder,
820            vec![Parameter::new("p")],
821            vec![Location::new("loc")],
822            vec![Variable::new("x")],
823        )
824        .unwrap();
825
826        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
827
828        let solver = ctx.get_smt_solver_mut();
829        let encoded_str = solver.display(encoded_expr).to_string();
830        assert_eq!(encoded_str, "(div var_x_0 4)");
831    }
832
833    #[test]
834    fn test_integer_expr_encoding_neg() {
835        let builder = SMTSolverBuilder::default();
836
837        let expr = IntegerExpression::Neg(Box::new(IntegerExpression::Atom(Parameter::new("p"))));
838
839        let mut ctx = StaticSMTContext::new(
840            builder,
841            vec![Parameter::new("p")],
842            vec![Location::new("loc")],
843            vec![Variable::new("x")],
844        )
845        .unwrap();
846
847        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
848
849        let solver = ctx.get_smt_solver_mut();
850        let encoded_str = solver.display(encoded_expr).to_string();
851        assert_eq!(encoded_str, "(- param_p)");
852    }
853
854    #[test]
855    fn test_get_assignment_sat() {
856        let builder = SMTSolverBuilder::default();
857
858        let expr = BooleanExpression::BinaryExpression(
859            Box::new(BooleanExpression::ComparisonExpression(
860                Box::new(IntegerExpression::Atom(Variable::new("x"))),
861                ComparisonOp::Leq,
862                Box::new(IntegerExpression::Const(5)),
863            )),
864            BooleanConnective::And,
865            Box::new(BooleanExpression::ComparisonExpression(
866                Box::new(IntegerExpression::Atom(Variable::new("x"))),
867                ComparisonOp::Gt,
868                Box::new(IntegerExpression::Const(4)),
869            )),
870        );
871
872        let mut ctx = StaticSMTContext::new(
873            builder,
874            vec![Parameter::new("p")],
875            vec![Location::new("loc")],
876            vec![Variable::new("x"), Variable::new("y")],
877        )
878        .unwrap();
879
880        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
881        let res = ctx.assert_and_check_expr(encoded_expr).unwrap();
882
883        let assignment = ctx.get_assignment(res, &Variable::new("x")).unwrap();
884
885        assert_eq!(assignment, Some(5));
886    }
887
888    #[test]
889    fn test_get_assignment_unsat() {
890        let builder = SMTSolverBuilder::default();
891
892        let expr = BooleanExpression::BinaryExpression(
893            Box::new(BooleanExpression::ComparisonExpression(
894                Box::new(IntegerExpression::Atom(Variable::new("x"))),
895                ComparisonOp::Leq,
896                Box::new(IntegerExpression::Const(5)),
897            )),
898            BooleanConnective::And,
899            Box::new(BooleanExpression::ComparisonExpression(
900                Box::new(IntegerExpression::Atom(Variable::new("x"))),
901                ComparisonOp::Gt,
902                Box::new(IntegerExpression::Const(5)),
903            )),
904        );
905
906        let mut ctx = StaticSMTContext::new(
907            builder,
908            vec![Parameter::new("p")],
909            vec![Location::new("loc")],
910            vec![Variable::new("x"), Variable::new("y")],
911        )
912        .unwrap();
913
914        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
915        let res = ctx.assert_and_check_expr(encoded_expr).unwrap();
916
917        let assignment = ctx.get_assignment(res, &Variable::new("x"));
918
919        assert!(assignment.is_err());
920        assert!(matches!(
921            assignment.unwrap_err(),
922            SMTSolverError::ExtractionFromUnsat
923        ));
924    }
925
926    #[test]
927    fn test_get_expr_smt_context() {
928        let builder = SMTSolverBuilder::default();
929
930        let ctx = StaticSMTContext::new(
931            builder,
932            vec![Parameter::new("p")],
933            vec![Location::new("loc")],
934            vec![Variable::new("x")],
935        )
936        .unwrap();
937
938        let exprs = SMTVariableContext::<Parameter>::get_exprs(&ctx)
939            .into_iter()
940            .cloned()
941            .collect::<Vec<Parameter>>();
942        assert_eq!(exprs.len(), 1);
943        assert!(exprs.contains(&Parameter::new("p")));
944
945        let exprs = SMTVariableContext::<Location>::get_exprs(&ctx)
946            .into_iter()
947            .cloned()
948            .collect::<Vec<Location>>();
949        assert_eq!(exprs.len(), 1);
950        assert!(exprs.contains(&Location::new("loc")));
951
952        let exprs = SMTVariableContext::<Variable>::get_exprs(&ctx)
953            .into_iter()
954            .cloned()
955            .collect::<Vec<Variable>>();
956        assert_eq!(exprs.len(), 1);
957        assert!(exprs.contains(&Variable::new("x")));
958    }
959
960    #[test]
961    fn test_get_assignment_no_solution() {
962        let builder = SMTSolverBuilder::default();
963
964        let mut solver = builder.new_solver();
965
966        let vars = vec![Variable::new("x")];
967        let vars_smt = vars
968            .into_iter()
969            .map(|v| (v.clone(), v.declare_variable(&mut solver, 0).unwrap()))
970            .collect::<HashMap<_, _>>();
971
972        let res = solver.assert_and_check_expr(solver.false_());
973        let sol = vars_smt.get_solution(&mut solver, res.unwrap());
974
975        assert!(sol.is_err());
976        assert!(matches!(
977            sol.unwrap_err(),
978            SMTSolverError::ExtractionFromUnsat
979        ));
980    }
981
982    #[test]
983    fn test_parse_int_err_get_sol() {
984        let builder = SMTSolverBuilder::default();
985
986        let mut solver = builder.new_solver();
987
988        let vars = vec![Variable::new("x")];
989        let vars_smt = vars
990            .into_iter()
991            .map(|v| (v.clone(), v.declare_variable(&mut solver, 0).unwrap()))
992            .collect::<HashMap<_, _>>();
993
994        let expr = solver.lt(vars_smt[&Variable::new("x")], solver.numeral(0));
995
996        let res = solver.assert_and_check_expr(expr);
997        let sol = vars_smt.get_solution(&mut solver, res.unwrap());
998
999        assert!(sol.is_err());
1000        assert!(matches!(
1001            sol.unwrap_err(),
1002            SMTSolverError::SolutionExtractionParseIntError(_)
1003        ));
1004    }
1005
1006    #[test]
1007    fn test_parse_int_err_get_assignment() {
1008        let builder = SMTSolverBuilder::default();
1009
1010        let expr = BooleanExpression::ComparisonExpression(
1011            Box::new(IntegerExpression::Atom(Variable::new("x"))),
1012            ComparisonOp::Lt,
1013            Box::new(IntegerExpression::Const(0)),
1014        );
1015
1016        let mut ctx = StaticSMTContext::new(
1017            builder,
1018            vec![Parameter::new("p")],
1019            vec![Location::new("loc")],
1020            vec![Variable::new("x"), Variable::new("y")],
1021        )
1022        .unwrap();
1023
1024        let encoded_expr = ctx.encode_to_smt(&expr).unwrap();
1025        let res = ctx.assert_and_check_expr(encoded_expr).unwrap();
1026
1027        let sol = ctx.get_assignment(res, &Variable::new("x"));
1028
1029        assert!(sol.is_err());
1030        assert!(matches!(
1031            sol.unwrap_err(),
1032            SMTSolverError::SolutionExtractionParseIntError(_)
1033        ));
1034    }
1035
1036    #[test]
1037    fn test_get_undeclared_error() {
1038        let loc = Location::new("loc");
1039        let param = Parameter::new("param");
1040        let var = Variable::new("var");
1041        let rule = RuleBuilder::new(42, loc.clone(), loc.clone()).build();
1042
1043        assert!(matches!(
1044            loc.get_undeclared_error(),
1045            SMTSolverError::UndeclaredLocation(_)
1046        ));
1047        assert!(matches!(
1048            param.get_undeclared_error(),
1049            SMTSolverError::UndeclaredParameter(_)
1050        ));
1051        assert!(matches!(
1052            var.get_undeclared_error(),
1053            SMTSolverError::UndeclaredVariable(_)
1054        ));
1055        assert!(matches!(
1056            rule.get_undeclared_error(),
1057            SMTSolverError::UndeclaredRule(_)
1058        ));
1059    }
1060
1061    #[test]
1062    fn test_from_io_error() {
1063        let io_error = io::Error::other("Some error");
1064        let err = SMTSolverError::from(io_error);
1065
1066        assert!(matches!(err, SMTSolverError::EasySMTErr(_)));
1067    }
1068
1069    #[test]
1070    fn test_display_smt_err() {
1071        let err = SMTSolverError::EasySMTErr(io::Error::other("Some error"));
1072        let display = err.to_string();
1073        assert!(display.contains("Error from connection to SMT solver"));
1074
1075        let err = SMTSolverError::UndeclaredParameter(Parameter::new("p"));
1076        let display = err.to_string();
1077        assert!(display.contains("Undeclared parameter"));
1078        assert!(display.contains(Parameter::new("p").name()));
1079
1080        let err = SMTSolverError::UndeclaredLocation(Location::new("loc"));
1081        let display = err.to_string();
1082        assert!(display.contains("Undeclared location"));
1083        assert!(display.contains(Location::new("loc").name()));
1084
1085        let err = SMTSolverError::UndeclaredVariable(Variable::new("x"));
1086        let display = err.to_string();
1087        assert!(display.contains("Undeclared variable"));
1088        assert!(display.contains(Variable::new("x").name()));
1089
1090        let err = SMTSolverError::SolverTimeout;
1091        let display = err.to_string();
1092        assert!(display.contains("Timeout in SMT solver"));
1093
1094        let err = SMTSolverError::SolutionExtractionParseIntError("not_an_int".to_string());
1095        let display = err.to_string();
1096        assert!(display.contains("Failed to parse SMT solver supplied solution into integer"));
1097        assert!(display.contains("not_an_int"));
1098
1099        let err = SMTSolverError::UndeclaredRule(
1100            RuleBuilder::new(42, Location::new("src"), Location::new("tgt")).build(),
1101        );
1102        let display = err.to_string();
1103        assert!(display.contains("Undeclared rule"));
1104        assert!(display.contains("42"));
1105
1106        let err = SMTSolverError::ExtractionFromUnsat;
1107        let display = err.to_string();
1108        assert!(display.contains(
1109            "Attempted to extract the solution assignment from an unsatisfiable expression"
1110        ));
1111
1112        let err = SMTSolverError::TriviallyUnsat("Some reason".to_string());
1113        let display = err.to_string();
1114        assert!(display.contains("Specification can never be true"));
1115        assert!(display.contains("Some reason"));
1116    }
1117}
taco_smt_encoder/expression_encoding.rs

taco_smt_encoder/
expression_encoding.rs
