Solve constraints and return result
(&self)
| 81 | impl Z3Solver { |
| 82 | /// Solve constraints and return result |
| 83 | pub fn solve(&self) -> SmtResult { |
| 84 | unsafe { |
| 85 | let _guard = Z3_MUTEX.lock().unwrap(); |
| 86 | match z3_sys::Z3_solver_check(self.z3_context, self.z3_solver) { |
| 87 | z3_sys::Z3_L_TRUE => SmtResult::Sat, |
| 88 | z3_sys::Z3_L_FALSE => SmtResult::Unsat, |
| 89 | _ => SmtResult::Unknown, |
| 90 | } |
| 91 | } |
| 92 | } |
| 93 | |
| 94 | /// Solve a Z3 ast without changing the internal state of the solver |
| 95 | pub fn solve_expression(&self, expression: &Z3Expression) -> SmtResult { |