From 30f7d39ca2ed4590b5d356b1a4c024d11156a383 Mon Sep 17 00:00:00 2001
From: Minijackson <minijackson@riseup.net>
Date: Sun, 25 Dec 2022 15:46:31 +0100
Subject: WIP before core rewrite

---
 z3-solver/Cargo.toml |  2 +-
 z3-solver/src/lib.rs | 20 ++++++++++----------
 2 files changed, 11 insertions(+), 11 deletions(-)

(limited to 'z3-solver')

diff --git a/z3-solver/Cargo.toml b/z3-solver/Cargo.toml
index 6f63e1c..f598f53 100644
--- a/z3-solver/Cargo.toml
+++ b/z3-solver/Cargo.toml
@@ -9,4 +9,4 @@ edition = "2021"
 [dependencies]
 diaphragm-core = { path = "../core" }
 
-z3 = "0.9"
+z3 = "0.11"
diff --git a/z3-solver/src/lib.rs b/z3-solver/src/lib.rs
index 04d77eb..35a17a8 100644
--- a/z3-solver/src/lib.rs
+++ b/z3-solver/src/lib.rs
@@ -45,7 +45,7 @@ impl<'z3> Z3Context<'z3> {
     pub fn new(ctx: &'z3 z3::Context) -> Self {
         Self {
             ctx,
-            solver: z3::Solver::new(&ctx),
+            solver: z3::Solver::new(ctx),
             floats: HashMap::new(),
             max_float_id: 0,
             bools: HashMap::new(),
@@ -85,7 +85,7 @@ impl<'z3> Z3Context<'z3> {
         let handle = match f {
             Float::Fixed(value) => {
                 let (num, den) = value_to_num_den(value);
-                return z3::ast::Real::from_real(&self.ctx, num, den);
+                return z3::ast::Real::from_real(self.ctx, num, den);
             }
             Float::Variable(handle) => handle,
         };
@@ -128,7 +128,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let id = self.max_float_id;
         let handle = VariableHandle::new(id as usize);
         self.floats
-            .insert(handle, z3::ast::Real::new_const(&self.ctx, id));
+            .insert(handle, z3::ast::Real::new_const(self.ctx, id));
         Float::from_handle(handle)
     }
 
@@ -140,7 +140,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let (num, den) = value_to_num_den(value);
 
         self.floats
-            .insert(handle, z3::ast::Real::from_real(&self.ctx, num, den));
+            .insert(handle, z3::ast::Real::from_real(self.ctx, num, den));
         Float::from_handle(handle)
     }
 
@@ -236,7 +236,7 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let id = self.max_bool_id;
         let handle = VariableHandle::new(id as usize);
         self.bools
-            .insert(handle, z3::ast::Bool::new_const(&self.ctx, id));
+            .insert(handle, z3::ast::Bool::new_const(self.ctx, id));
         Bool::new(handle)
     }
 
@@ -246,21 +246,21 @@ impl<'z3> SolverContext for Z3Context<'z3> {
         let handle = VariableHandle::new(id as usize);
 
         self.bools
-            .insert(handle, z3::ast::Bool::from_bool(&self.ctx, value));
+            .insert(handle, z3::ast::Bool::from_bool(self.ctx, value));
         Bool::new(handle)
     }
 
     fn bool_eq(&mut self, lhs: Bool, rhs: Bool) -> Bool {
         let lhs = self.bool(lhs);
         let rhs = self.bool(rhs);
-        let result = lhs._eq(&rhs);
+        let result = lhs._eq(rhs);
         self.anon_bool(result)
     }
 
     fn bool_ne(&mut self, lhs: Bool, rhs: Bool) -> Bool {
         let lhs = self.bool(lhs);
         let rhs = self.bool(rhs);
-        let result = lhs._eq(&rhs).not();
+        let result = lhs._eq(rhs).not();
         self.anon_bool(result)
     }
 
@@ -308,7 +308,7 @@ impl SolverModel for Z3Model<'_> {
 
         let (num, den) = self
             .model
-            .eval::<z3::ast::Real>(self.ctx.floats.get(&handle).expect("Couldn't find float"))
+            .eval::<z3::ast::Real>(self.ctx.floats.get(&handle).expect("Couldn't find float"), true)
             .unwrap()
             .as_real()
             .unwrap();
@@ -319,7 +319,7 @@ impl SolverModel for Z3Model<'_> {
     fn eval_bool(&self, f: Bool) -> Option<bool> {
         Some(
             self.model
-                .eval::<z3::ast::Bool>(&self.ctx.bool(f))
+                .eval::<z3::ast::Bool>(self.ctx.bool(f), true)
                 .unwrap()
                 .as_bool()
                 .unwrap(),
-- 
cgit v1.2.3