solving: add minimize/maximize

1 files changed, 11 insertions, 3 deletions

diff --git a/z3-solver/src/lib.rs b/z3-solver/src/lib.rs
index 6ad7ffc..2085768 100644
--- a/z3-solver/src/lib.rs
+++ b/z3-solver/src/lib.rs
@@ -13,7 +13,7 @@ use std::collections::HashMap;
 #[derive(Debug)]
 pub struct Z3Context<'z3> {
     ctx: &'z3 z3::Context,
-    solver: z3::Solver<'z3>,
+    solver: z3::Optimize<'z3>,
 
     floats: HashMap<VariableHandle, z3::ast::Real<'z3>>,
     max_float_id: u32,
@@ -57,7 +57,7 @@ impl<'z3> Z3Context<'z3> {
     pub fn new(ctx: &'z3 z3::Context) -> Self {
         Self {
             ctx,
-            solver: z3::Solver::new(ctx),
+            solver: z3::Optimize::new(ctx),
             floats: HashMap::new(),
             max_float_id: 0,
             bools: HashMap::new(),
@@ -115,7 +115,7 @@ impl<'z3> Z3Context<'z3> {
 
 impl<'z3> SolverContext for Z3Context<'z3> {
     fn solve<'a>(&'a self) -> Box<dyn SolverModel + 'a> {
-        match self.solver.check() {
+        match self.solver.check(&[]) {
             z3::SatResult::Unsat | z3::SatResult::Unknown => panic!("Failed solving"),
             z3::SatResult::Sat => {}
         }
@@ -241,6 +241,14 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         self.anon_bool(result)
     }
 
+    fn float_maximize(&mut self, value: Float) {
+        self.solver.maximize(&self.float(value));
+    }
+
+    fn float_minimize(&mut self, value: Float) {
+        self.solver.minimize(&self.float(value));
+    }
+
     // Bools
 
     fn new_free_bool(&mut self) -> Bool {