-
Notifications
You must be signed in to change notification settings - Fork 3
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: add Z3 SMT solver support (#68)
- also refactor the solver interface - fix small bug in boolector interface - improve toolchain setup description
- Loading branch information
1 parent
465e35c
commit af9ef1b
Showing
13 changed files
with
385 additions
and
221 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -6,3 +6,4 @@ | |
| **/*.png | ||
| **/*.s | ||
| .DS_Store | ||
| .z3-trace | ||
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -1,127 +1,101 @@ | ||
| use crate::bitvec::BitVector; | ||
| use crate::solver::{Assignment, Solver}; | ||
| use crate::symbolic_state::{ | ||
| BVOperator, Formula, | ||
| get_operands, BVOperator, Formula, | ||
| Node::{Constant, Input, Operator}, | ||
| OperandSide, | ||
| SymbolId, | ||
| }; | ||
| use boolector::{ | ||
| option::{BtorOption, ModelGen, OutputFileFormat}, | ||
| Btor, SolverResult, BV, | ||
| }; | ||
| use log::debug; | ||
| use petgraph::{graph::NodeIndex, Direction}; | ||
| use std::collections::HashMap; | ||
| use std::rc::Rc; | ||
|
|
||
| fn solve(graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> { | ||
| let solver = Rc::new(Btor::new()); | ||
| solver.set_opt(BtorOption::ModelGen(ModelGen::All)); | ||
| solver.set_opt(BtorOption::Incremental(true)); | ||
| solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2)); | ||
|
|
||
| let mut bvs = HashMap::new(); | ||
| let bv = traverse(graph, root, &solver, &mut bvs); | ||
| bv.assert(); | ||
| pub struct Boolector {} | ||
|
|
||
| if let SolverResult::Sat = solver.sat() { | ||
| let assignments = graph | ||
| .node_indices() | ||
| .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap())) | ||
| .collect(); | ||
| impl Boolector { | ||
| pub fn new() -> Self { | ||
| Self {} | ||
| } | ||
| } | ||
|
|
||
| Some(assignments) | ||
| } else { | ||
| None | ||
| impl Default for Boolector { | ||
| fn default() -> Self { | ||
| Self::new() | ||
| } | ||
| } | ||
|
|
||
| fn get_operands( | ||
| graph: &Formula, | ||
| node: NodeIndex, | ||
| solver: &Rc<Btor>, | ||
| bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>, | ||
| ) -> (BV<Rc<Btor>>, Option<BV<Rc<Btor>>>) { | ||
| let mut operands = graph.neighbors_directed(node, Direction::Incoming).detach(); | ||
| impl Solver for Boolector { | ||
| fn name() -> &'static str { | ||
| "Boolector" | ||
| } | ||
|
|
||
| match operands.next(graph) { | ||
| Some(p) if graph[p.0] == OperandSide::Lhs => (traverse(graph, p.1, solver, bvs), { | ||
| if let Some(node) = operands.next(graph) { | ||
| Some(traverse(graph, node.1, solver, bvs)) | ||
| } else { | ||
| None | ||
| } | ||
| }), | ||
| Some(p) if graph[p.0] == OperandSide::Rhs => ( | ||
| traverse(graph, p.1, solver, bvs), | ||
| if let Some(node) = operands.next(graph) { | ||
| Some(traverse(graph, node.1, solver, bvs)) | ||
| } else { | ||
| None | ||
| }, | ||
| ), | ||
| _ => unreachable!(), | ||
| fn solve_impl(&mut self, graph: &Formula, root: SymbolId) -> Option<Assignment<BitVector>> { | ||
| let solver = Rc::new(Btor::new()); | ||
| solver.set_opt(BtorOption::ModelGen(ModelGen::All)); | ||
| solver.set_opt(BtorOption::Incremental(true)); | ||
| solver.set_opt(BtorOption::OutputFileFormat(OutputFileFormat::SMTLIBv2)); | ||
|
|
||
| let mut bvs = HashMap::new(); | ||
| let bv = traverse(graph, root, &solver, &mut bvs); | ||
| bv.assert(); | ||
|
|
||
| if let SolverResult::Sat = solver.sat() { | ||
| let assignments = graph | ||
| .node_indices() | ||
| .filter(|i| matches!(graph[*i], Input(_))) | ||
| .map(|i| BitVector(bvs.get(&i).unwrap().get_a_solution().as_u64().unwrap())) | ||
| .collect(); | ||
|
|
||
| Some(assignments) | ||
| } else { | ||
| None | ||
| } | ||
| } | ||
| } | ||
|
|
||
| fn traverse<'a>( | ||
| graph: &Formula, | ||
| node: NodeIndex, | ||
| node: SymbolId, | ||
| solver: &'a Rc<Btor>, | ||
| bvs: &mut HashMap<NodeIndex, BV<Rc<Btor>>>, | ||
| bvs: &mut HashMap<SymbolId, BV<Rc<Btor>>>, | ||
| ) -> BV<Rc<Btor>> { | ||
| let bv = match &graph[node] { | ||
| Operator(op) => { | ||
| match get_operands(graph, node, solver, bvs) { | ||
| let bv = | ||
| match &graph[node] { | ||
| Operator(op) => match get_operands(graph, node) { | ||
| (lhs, Some(rhs)) => { | ||
| match op { | ||
| BVOperator::Add => lhs.add(&rhs), | ||
| BVOperator::Sub => lhs.sub(&rhs), | ||
| BVOperator::Mul => lhs.mul(&rhs), | ||
| BVOperator::Equals => lhs._eq(&rhs), | ||
| BVOperator::BitwiseAnd => lhs.and(&rhs), | ||
| //BVOperator::GreaterThan => lhs.ugt(&rhs), | ||
| BVOperator::Add => traverse(graph, lhs, solver, bvs) | ||
| .add(&traverse(graph, rhs, solver, bvs)), | ||
| BVOperator::Sub => traverse(graph, lhs, solver, bvs) | ||
| .sub(&traverse(graph, rhs, solver, bvs)), | ||
| BVOperator::Mul => traverse(graph, lhs, solver, bvs) | ||
| .mul(&traverse(graph, rhs, solver, bvs)), | ||
| BVOperator::Equals => traverse(graph, lhs, solver, bvs) | ||
| ._eq(&traverse(graph, rhs, solver, bvs)), | ||
| BVOperator::BitwiseAnd => traverse(graph, lhs, solver, bvs) | ||
| .and(&traverse(graph, rhs, solver, bvs)), | ||
| i => unimplemented!("binary operator: {:?}", i), | ||
| } | ||
| } | ||
| (lhs, None) => match op { | ||
| BVOperator::Not => lhs._eq(&BV::from_u64(solver.clone(), 0, 1)), | ||
| BVOperator::Not => { | ||
| traverse(graph, lhs, solver, bvs)._eq(&BV::from_u64(solver.clone(), 0, 1)) | ||
| } | ||
| i => unimplemented!("unary operator: {:?}", i), | ||
| }, | ||
| }, | ||
| Input(name) => { | ||
| if let Some(value) = bvs.get(&node) { | ||
| value.clone() | ||
| } else { | ||
| BV::new(solver.clone(), 64, Some(name)) | ||
| } | ||
| } | ||
| } | ||
| Input(name) => { | ||
| if let Some(value) = bvs.get(&node) { | ||
| value.clone() | ||
| } else { | ||
| BV::new(solver.clone(), 64, Some(name)) | ||
| } | ||
| } | ||
| Constant(c) => BV::from_u64(solver.clone(), *c, 64), | ||
| }; | ||
| Constant(c) => BV::from_u64(solver.clone(), *c, 64), | ||
| }; | ||
|
|
||
| bvs.insert(node, bv.clone()); | ||
| bv | ||
| } | ||
|
|
||
| pub struct Boolector {} | ||
|
|
||
| impl Boolector { | ||
| pub fn new() -> Self { | ||
| Self {} | ||
| } | ||
| } | ||
|
|
||
| impl Default for Boolector { | ||
| fn default() -> Self { | ||
| Self::new() | ||
| } | ||
| } | ||
|
|
||
| impl Solver for Boolector { | ||
| fn solve(&mut self, graph: &Formula, root: NodeIndex) -> Option<Assignment<BitVector>> { | ||
| debug!("try to solve with Boolector"); | ||
|
|
||
| time_debug!("finished solving formula", { solve(graph, root) }) | ||
| } | ||
| } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.