1 files changed, 44 insertions, 0 deletions

diff --git a/z3-solver/src/solving/z3/mod.rs b/z3-solver/src/solving/z3/mod.rs
new file mode 100644
index 0000000..2f29073
--- /dev/null
+++ b/z3-solver/src/solving/z3/mod.rs
@@ -0,0 +1,44 @@
+use super::{Solver, FloatHandle};
+
+use std::collections::HashMap;
+
+pub struct Z3Solver {
+    ctx: z3::Context,
+}
+
+pub struct Handles<'a> {
+    float: HashMap<u32, z3::ast::Real<'a>>,
+    float_max_id: u32,
+}
+
+impl<'a> Handles<'a> {
+    pub fn new() -> Self {
+        Self {
+            float: HashMap::new(),
+            float_max_id: 0,
+        }
+    }
+}
+
+impl Z3Solver {
+    pub fn new<'a>() -> (Self, Handles<'a>) {
+        let config = z3::Config::new();
+
+        (
+            Self {
+                ctx: z3::Context::new(&config),
+            },
+            Handles::new(),
+        )
+    }
+}
+
+impl Solver for Z3Solver {
+    fn new_float<'a>(&'a mut self, handles: &mut Handles<'a>) -> FloatHandle {
+        let id = handles.float_max_id;
+        let float = z3::ast::Real::new_const(&self.ctx, id);
+        handles.float_max_id += 1;
+        handles.float.insert(id, float);
+        FloatHandle(id)
+    }
+}