From 92a02c34628343153b33602eae00cef46e28d191 Mon Sep 17 00:00:00 2001
From: Minijackson <minijackson@riseup.net>
Date: Thu, 22 Dec 2022 12:19:59 +0100
Subject: WIP

---
 z3-solver/src/solving/mod.rs    |  9 +++++++++
 z3-solver/src/solving/z3/mod.rs | 44 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 53 insertions(+)
 create mode 100644 z3-solver/src/solving/mod.rs
 create mode 100644 z3-solver/src/solving/z3/mod.rs

(limited to 'z3-solver/src/solving')

diff --git a/z3-solver/src/solving/mod.rs b/z3-solver/src/solving/mod.rs
new file mode 100644
index 0000000..f3f6673
--- /dev/null
+++ b/z3-solver/src/solving/mod.rs
@@ -0,0 +1,9 @@
+pub mod z3;
+
+#[derive(Debug, Eq, PartialEq, Ord, PartialOrd, Hash, Clone, Copy)]
+pub struct FloatHandle(u32);
+
+pub trait Solver {
+    // TODO: make handles generic?
+    fn new_float<'a>(&'a mut self, handles: &mut z3::Handles<'a>) -> FloatHandle;
+}
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)
+    }
+}
-- 
cgit v1.2.3