1 files changed, 90 insertions, 0 deletions

diff --git a/core/src/mod.rs b/core/src/mod.rs
new file mode 100644
index 0000000..40fe74f
--- /dev/null
+++ b/core/src/mod.rs
@@ -0,0 +1,90 @@
+pub mod constraints;
+pub mod drawable;
+pub mod shapes;
+pub mod text;
+pub mod types;
+
+pub use self::drawable::Drawable;
+pub use self::shapes::Shape as CoreShape;
+pub use self::types::{Bounded, Bounds, DefinitelyBounded};
+
+use self::constraints::Constrainable;
+
+const RECURSION_LIMIT: u64 = 10_000;
+
+pub struct Context<'z3> {
+    drawables: Vec<Bounded<'z3, Box<dyn Drawable>>>,
+}
+
+impl<'z3> Context<'z3> {
+    pub fn new() -> Self {
+        Self { drawables: vec![] }
+    }
+
+    pub fn add_shape(&mut self, shape: Bounded<'z3, Box<dyn Drawable>>) {
+        self.drawables.push(shape);
+    }
+
+    pub fn set_constraints(&self, z3_ctx: &z3::Context, solver: &z3::Solver) {
+        for drawable in &self.drawables {
+            for constraint in drawable.shape.constraints(&drawable.bounds, &z3_ctx) {
+                solver.assert(&constraint);
+            }
+        }
+    }
+
+    // TODO: simplify until not possible?
+
+    pub fn draw(&self, model: &z3::Model) -> Vec<DefinitelyBounded<CoreShape>> {
+        let mut acc_core_drawables = Vec::new();
+        let mut acc_complex_drawables = Vec::new();
+
+        for drawable in &self.drawables {
+            let bounds = &drawable.bounds;
+            let shape = &drawable.shape;
+
+            let (core_drawables, mut complex_drawables) = shape.draw(bounds);
+
+            acc_core_drawables.extend(core_drawables.iter().map(|Bounded { bounds, shape }| {
+                DefinitelyBounded {
+                    bounds: bounds.fixate(model),
+                    shape: shape.clone(),
+                }
+            }));
+
+            acc_complex_drawables.append(&mut complex_drawables);
+        }
+
+        let mut recursion_count = 0;
+
+        while !acc_complex_drawables.is_empty() {
+            recursion_count += 1;
+
+            let mut tmp_complex_drawables = Vec::new();
+
+            for drawable in acc_complex_drawables.drain(..) {
+                let bounds = drawable.bounds;
+                let shape = drawable.shape;
+
+                let (core_drawables, mut complex_drawables) = shape.draw(&bounds);
+
+                acc_core_drawables.extend(core_drawables.into_iter().map(
+                    |Bounded { bounds, shape }| DefinitelyBounded {
+                        bounds: bounds.fixate(model),
+                        shape,
+                    },
+                ));
+
+                tmp_complex_drawables.append(&mut complex_drawables);
+            }
+
+            acc_complex_drawables = tmp_complex_drawables;
+
+            if recursion_count > RECURSION_LIMIT {
+                panic!("Recursion limit reached");
+            }
+        }
+
+        acc_core_drawables
+    }
+}