solving: add minimize/maximize

3 files changed, 26 insertions, 3 deletions

diff --git a/core/src/solving.rs b/core/src/solving.rs
index da053e7..bfe3ff3 100644
--- a/core/src/solving.rs
+++ b/core/src/solving.rs
@@ -135,6 +135,9 @@ pub trait SolverContext {
         result
     }
 
+    fn float_maximize(&mut self, value: Float);
+    fn float_minimize(&mut self, value: Float);
+
     // Bools
 
     fn new_free_bool(&mut self) -> Bool;
diff --git a/lua-bindings/src/lib.rs b/lua-bindings/src/lib.rs
index fb56b5a..86a759d 100644
--- a/lua-bindings/src/lib.rs
+++ b/lua-bindings/src/lib.rs
@@ -61,6 +61,18 @@ impl LuaUserData for Float {
                 r.solver_ctx().float_abs(f.0)
             }))))
         });
+
+        methods.add_method("maximize", |_lua, f: &Float, _: ()| {
+            let f = *f;
+            runtime_thread_do(Box::new(move |r| r.solver_ctx().float_maximize(f.0)));
+            Ok(())
+        });
+
+        methods.add_method("minimize", |_lua, f: &Float, _: ()| {
+            let f = *f;
+            runtime_thread_do(Box::new(move |r| r.solver_ctx().float_minimize(f.0)));
+            Ok(())
+        });
     }
 }
 
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 {