monster/solver/
mod.rs

1mod bitvec;
2mod monster;
3mod smt;
4
5#[cfg(feature = "boolector")]
6mod boolector;
7
8#[cfg(feature = "z3")]
9mod z3;
10
11#[cfg(feature = "boolector")]
12pub use self::boolector::*;
13
14#[cfg(feature = "z3")]
15pub use self::z3::*;
16
17pub use self::{bitvec::*, monster::*, smt::*};
18
19use log::debug;
20use std::marker::Sync;
21use std::{collections::HashMap, convert::From, fmt, io, ops::Index};
22use strum::{EnumString, EnumVariantNames, IntoStaticStr};
23use thiserror::Error;
24
25pub type Assignment = HashMap<SymbolId, BitVector>;
26
27pub trait Solver: Default + Sync + Sized {
28    fn name() -> &'static str;
29
30    fn solve<F: Formula>(&self, formula: &F) -> Result<Option<Assignment>, SolverError> {
31        debug!("try to solve with {} backend", Self::name());
32
33        time_debug!("finished solving formula", { self.solve_impl(formula) })
34    }
35
36    fn solve_impl<F: Formula>(&self, formula: &F) -> Result<Option<Assignment>, SolverError>;
37}
38
39pub trait SmtSolver: Solver {
40    fn smt_options() -> &'static str;
41}
42
43#[derive(Debug, Error, Clone)]
44pub enum SolverError {
45    #[error("failed to compute satisfiability within the given limits")]
46    SatUnknown,
47
48    #[error("could not find a satisfiable assignment before timing out")]
49    Timeout,
50
51    #[error("solver failed with IO error")]
52    IoError(String),
53}
54
55#[derive(Debug, EnumString, EnumVariantNames, IntoStaticStr)]
56#[strum(serialize_all = "kebab_case")]
57pub enum SolverType {
58    Monster,
59    #[cfg(feature = "boolector")]
60    Boolector,
61    #[cfg(feature = "z3")]
62    Z3,
63}
64
65impl From<io::Error> for SolverError {
66    fn from(err: io::Error) -> Self {
67        SolverError::IoError(err.to_string())
68    }
69}
70
71#[derive(Clone, Debug, Copy, Eq, Hash, PartialEq)]
72pub enum OperandSide {
73    Lhs,
74    Rhs,
75}
76
77impl OperandSide {
78    #[allow(dead_code)]
79    pub fn other(&self) -> Self {
80        match self {
81            OperandSide::Lhs => OperandSide::Rhs,
82            OperandSide::Rhs => OperandSide::Lhs,
83        }
84    }
85}
86
87#[derive(Debug, Copy, Clone, Hash, Eq, PartialEq)]
88pub enum BVOperator {
89    Add,
90    Sub,
91    Mul,
92    Divu,
93    Sltu,
94    Remu,
95    Not,
96    Equals,
97    BitwiseAnd,
98}
99
100impl BVOperator {
101    pub fn is_unary(&self) -> bool {
102        *self == BVOperator::Not
103    }
104    pub fn is_binary(&self) -> bool {
105        !self.is_unary()
106    }
107}
108
109impl fmt::Display for BVOperator {
110    fn fmt(&self, f: &mut fmt::Formatter) -> fmt::Result {
111        write!(
112            f,
113            "{}",
114            match self {
115                BVOperator::Add => "+",
116                BVOperator::Sub => "-",
117                BVOperator::Mul => "*",
118                BVOperator::Divu => "/",
119                BVOperator::Not => "!",
120                BVOperator::Remu => "%",
121                BVOperator::Equals => "=",
122                BVOperator::BitwiseAnd => "&",
123                BVOperator::Sltu => "<",
124            }
125        )
126    }
127}
128
129#[derive(Clone, Debug, Eq, Hash, PartialEq)]
130pub enum Symbol {
131    Constant(BitVector),
132    Input(String),
133    Operator(BVOperator),
134}
135
136pub type SymbolId = usize;
137
138pub trait Formula: Index<SymbolId, Output = Symbol> {
139    type DependencyIter: Iterator<Item = SymbolId>;
140    type SymbolIdsIter: Iterator<Item = SymbolId>;
141
142    fn root(&self) -> SymbolId;
143
144    fn operands(&self, sym: SymbolId) -> (SymbolId, Option<SymbolId>);
145
146    fn operand(&self, sym: SymbolId) -> SymbolId;
147
148    fn dependencies(&self, sym: SymbolId) -> Self::DependencyIter;
149    //where
150    //Iter: Iterator<Item = SymbolId>;
151
152    fn symbol_ids(&self) -> Self::SymbolIdsIter;
153    //where
154    //Iter: Iterator<Item = SymbolId>;
155
156    fn is_operand(&self, sym: SymbolId) -> bool;
157
158    fn traverse<V, R>(&self, n: SymbolId, visit_map: &mut HashMap<SymbolId, R>, v: &mut V) -> R
159    where
160        V: FormulaVisitor<R>,
161        R: Clone;
162}
163
164pub trait FormulaVisitor<T>: Sized {
165    fn input(&mut self, idx: SymbolId, name: &str) -> T;
166    fn constant(&mut self, idx: SymbolId, v: BitVector) -> T;
167    fn unary(&mut self, idx: SymbolId, op: BVOperator, v: T) -> T;
168    fn binary(&mut self, idx: SymbolId, op: BVOperator, lhs: T, rhs: T) -> T;
169}
monster/solver/mod.rs

monster/solver/
mod.rs
