WIP

1 files changed, 279 insertions, 0 deletions

diff --git a/core/src/solving.rs b/core/src/solving.rs
new file mode 100644
index 0000000..c7e94ba
--- /dev/null
+++ b/core/src/solving.rs
@@ -0,0 +1,279 @@
+use super::core_shapes::*;
+use super::styles::*;
+use super::text::*;
+use super::types::{Bool, Float};
+
+#[derive(Copy, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
+pub struct VariableHandle(usize);
+
+impl VariableHandle {
+    pub fn new(id: usize) -> Self {
+        Self(id)
+    }
+
+    pub fn id(&self) -> usize {
+        self.0
+    }
+}
+
+/*
+pub trait VariableFloat<'a> {
+    fn id(&self) -> usize;
+    fn dyn_clone(&self) -> Box<dyn VariableFloat<'a> + 'a>;
+
+    fn eq(&self, other: &dyn VariableFloat) -> Bool<'a>;
+    fn neq(&self, other: &dyn VariableFloat) -> Bool<'a>;
+    fn gt(&self, other: &dyn VariableFloat) -> Bool<'a>;
+    fn ge(&self, other: &dyn VariableFloat) -> Bool<'a>;
+    fn lt(&self, other: &dyn VariableFloat) -> Bool<'a>;
+    fn le(&self, other: &dyn VariableFloat) -> Bool<'a>;
+
+    fn add(&self, other: &dyn VariableFloat) -> Float<'a>;
+    fn sub(&self, other: &dyn VariableFloat) -> Float<'a>;
+    fn mul(&self, other: &dyn VariableFloat) -> Float<'a>;
+    fn div(&self, other: &dyn VariableFloat) -> Float<'a>;
+
+    fn neg(&self) -> Float<'a>;
+}
+
+pub trait VariableBool<'a> {
+    fn id(&self) -> usize;
+    fn dyn_clone(&self) -> Box<dyn VariableBool<'a> + 'a>;
+
+    fn eq(&self, other: &dyn VariableBool) -> Bool<'a>;
+    fn neq(&self, other: &dyn VariableBool) -> Bool<'a>;
+
+    fn and(&self, other: &dyn VariableBool) -> Bool<'a>;
+    fn or(&self, other: &dyn VariableBool) -> Bool<'a>;
+
+    fn not(&self) -> Bool<'a>;
+}
+*/
+
+pub trait SolverContext {
+    fn solve<'a>(&'a self) -> Box<dyn SolverModel + 'a>;
+    fn constrain(&mut self, assertion: Bool);
+
+    // Floats
+
+    fn new_free_float(&mut self) -> Float;
+    fn new_fixed_float(&mut self, value: f64) -> Float;
+
+    fn float_add(&mut self, values: &[Float]) -> Float;
+    fn float_sub(&mut self, values: &[Float]) -> Float;
+    fn float_mul(&mut self, values: &[Float]) -> Float;
+    fn float_div(&mut self, lhs: Float, rhs: Float) -> Float;
+    fn float_neg(&mut self, value: Float) -> Float;
+
+    fn float_eq(&mut self, lhs: Float, rhs: Float) -> Bool;
+    fn float_ne(&mut self, lhs: Float, rhs: Float) -> Bool;
+    fn float_gt(&mut self, lhs: Float, rhs: Float) -> Bool;
+    fn float_ge(&mut self, lhs: Float, rhs: Float) -> Bool;
+    fn float_lt(&mut self, lhs: Float, rhs: Float) -> Bool;
+    fn float_le(&mut self, lhs: Float, rhs: Float) -> Bool;
+
+    fn float_max(&mut self, values: &[Float]) -> Float {
+        let result = self.new_free_float();
+
+        for (index, &candidate) in values.iter().enumerate() {
+            let comparisons: Vec<_> = values
+                .iter()
+                .enumerate()
+                .filter(|(other_index, _)| *other_index != index)
+                .map(|(_, &other)| self.float_ge(candidate, other))
+                .collect();
+
+            let premise = self.bool_and(&comparisons);
+            let conclusion = self.float_eq(candidate, result);
+            let implication = self.bool_implies(premise, conclusion);
+            self.constrain(implication);
+        }
+
+        result
+    }
+
+    fn float_min(&mut self, values: &[Float]) -> Float {
+        let result = self.new_free_float();
+
+        for (index, &candidate) in values.iter().enumerate() {
+            let comparisons: Vec<_> = values
+                .iter()
+                .enumerate()
+                .filter(|(other_index, _)| *other_index != index)
+                .map(|(_, &other)| self.float_le(candidate, other))
+                .collect();
+
+            let premise = self.bool_and(&comparisons);
+            let conclusion = self.float_eq(candidate, result);
+            let implication = self.bool_implies(premise, conclusion);
+            self.constrain(implication);
+        }
+
+        result
+    }
+
+    // Bools
+
+    fn new_free_bool(&mut self) -> Bool;
+    fn new_fixed_bool(&mut self, value: bool) -> Bool;
+
+    fn bool_eq(&mut self, lhs: Bool, rhs: Bool) -> Bool;
+    fn bool_ne(&mut self, lhs: Bool, rhs: Bool) -> Bool;
+
+    fn bool_and(&mut self, values: &[Bool]) -> Bool;
+    fn bool_or(&mut self, values: &[Bool]) -> Bool;
+    fn bool_not(&mut self, value: Bool) -> Bool;
+
+    fn bool_implies(&mut self, lhs: Bool, rhs: Bool) -> Bool;
+}
+
+pub trait SolverModel {
+    fn eval_float(&self, f: Float) -> Option<f64>;
+    fn eval_bool(&self, b: Bool) -> Option<bool>;
+}
+
+/*
+pub trait Solver {
+    fn constrain(&mut self, assertion: &Bool);
+    fn solve(&self) -> Box<dyn SolverModel>;
+}
+*/
+
+use super::types::*;
+
+pub trait Constrainable {
+    type Fixated;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated>;
+}
+
+impl Constrainable for Float {
+    type Fixated = f64;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        model.eval_float(*self)
+    }
+
+    /*
+    fn fixate(&self, model: &Model) -> Self::Fixated {
+        match self {
+            Float::Defined(float) => *float,
+            Float::Constrained(variable) => {
+                let (num, den) = model
+                    .eval::<z3::ast::Real>(variable)
+                    .expect("Couldn't eval variable")
+                    .as_real()
+                    .expect("Couldn't get value from variable");
+
+                num as f64 / den as f64
+            }
+            Float::Undefined => panic!("Undefined float"),
+        }
+    }
+    */
+}
+
+impl Constrainable for Bounds {
+    type Fixated = DefinedBounds;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedBounds {
+            top: self.top.fixate(model)?,
+            left: self.left.fixate(model)?,
+            width: self.width.fixate(model)?,
+            height: self.height.fixate(model)?,
+        })
+    }
+}
+
+impl Constrainable for StrokeStyle {
+    type Fixated = DefinedStrokeStyle;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        let dash = match &self.dash {
+            Some(dash) => Some(dash.fixate(model)?),
+            None => None,
+        };
+
+        Some(DefinedStrokeStyle {
+            pattern: self.pattern.clone(),
+            dash,
+            line_width: self.line_width.fixate(model)?,
+        })
+    }
+}
+
+impl Constrainable for DashStyle {
+    type Fixated = DefinedDashStyle;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedDashStyle {
+            dashes: self
+                .dashes
+                .iter()
+                .map(|value| value.fixate(model))
+                .collect::<Option<_>>()?,
+            offset: self.offset.fixate(model)?,
+        })
+    }
+}
+
+impl Constrainable for ShapeContext {
+    type Fixated = DefinedShapeContext;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedShapeContext {
+            bounds: self.bounds.fixate(model)?,
+            fill: self.fill.clone(),
+            stroke: self.stroke.fixate(model)?,
+        })
+    }
+}
+
+impl Constrainable for Point2D {
+    type Fixated = DefinedPoint2D;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedPoint2D {
+            x: self.x.fixate(model)?,
+            y: self.y.fixate(model)?,
+        })
+    }
+}
+
+impl Constrainable for FontDescription {
+    type Fixated = DefinedFontDescription;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedFontDescription {
+            family: self.family.clone(),
+            style: self.style,
+            weight: self.weight,
+            size: self.size.fixate(&*model)?,
+        })
+    }
+}
+
+impl Constrainable for Text {
+    type Fixated = DefinedText;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        Some(DefinedText {
+            content: self.content.clone(),
+            font: self.font.fixate(&*model)?,
+        })
+    }
+}
+
+impl Constrainable for StraightPath {
+    type Fixated = DefinedStraightPath;
+
+    fn fixate(&self, model: &dyn SolverModel) -> Option<Self::Fixated> {
+        let points: Option<_> = self
+            .points
+            .iter()
+            .map(|point| point.fixate(model))
+            .collect();
+        Some(DefinedStraightPath { points: points? })
+    }
+}