From 92a02c34628343153b33602eae00cef46e28d191 Mon Sep 17 00:00:00 2001 From: Minijackson Date: Thu, 22 Dec 2022 12:19:59 +0100 Subject: WIP --- cli/src/main.rs | 188 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 188 insertions(+) create mode 100644 cli/src/main.rs (limited to 'cli/src') diff --git a/cli/src/main.rs b/cli/src/main.rs new file mode 100644 index 0000000..d2ec038 --- /dev/null +++ b/cli/src/main.rs @@ -0,0 +1,188 @@ +use diaphragm_cairo_renderer::CairoRenderer; +use diaphragm_core::{styles::*, types::*, *}; +use diaphragm_z3_solver::{z3, Z3Context}; + +// drawing::{cairo::CairoEngine, Engine}, +// z3::{self, ast::Ast}, + +fn main() { + let z3_cfg = z3::Config::new(); + let z3_ctx = z3::Context::new(&z3_cfg); + let ctx = Z3Context::new(&z3_ctx); + + let cairo_renderer = CairoRenderer::new(); + + let mut runtime = Runtime::new(Box::new(ctx), Box::new(cairo_renderer)); + + let ctx = runtime.solver_ctx(); + + let rect1_height = ctx.new_free_float(); + let rect1_width = ctx.new_free_float(); + + let rect1_ctx = ShapeContext { + bounds: Bounds { + top: ctx.new_fixed_float(10.), + left: ctx.new_fixed_float(10.), + height: rect1_height, + width: rect1_width, + }, + fill: FillStyle::default(), + stroke: StrokeStyle::default(), + }; + + let text_bounds = rect1_ctx.bounds.clone(); + + let rect1 = core_shapes::Rectangle {}; + + let rect2_top = ctx.new_free_float(); + let rect2_left = ctx.new_free_float(); + + let rect2_ctx = ShapeContext { + bounds: Bounds { + top: rect2_top, + left: rect2_left, + height: rect1_width, + width: rect1_height, + }, + fill: FillStyle::default(), + stroke: StrokeStyle::default(), + }; + + let rect2 = core_shapes::Rectangle {}; + + let _2 = ctx.new_fixed_float(2.); + let double_height = ctx.float_mul(&[rect1_height, _2]); + let width_constraint = ctx.float_eq(rect1_width, double_height); + ctx.constrain(width_constraint); + + let _42 = ctx.new_fixed_float(42.); + let width_constraint2 = ctx.float_eq(rect1_width, _42); + ctx.constrain(width_constraint2); + + let _10 = ctx.new_fixed_float(10.); + let top_constraint = ctx.float_eq(rect2_top, _10); + ctx.constrain(top_constraint); + + let bigger_width = ctx.float_add(&[rect1_width, _10]); + let left_constraint = ctx.float_eq(rect2_left, bigger_width); + ctx.constrain(left_constraint); + + let text = core_shapes::Text { + content: String::from("Hello, World!"), + font: text::FontDescription { + family: String::from("mono"), + style: Default::default(), + weight: Default::default(), + size: rect1_height, + }, + }; + + let text_ctx = ShapeContext { + bounds: text_bounds, + fill: FillStyle::default(), + stroke: StrokeStyle::default(), + }; + + runtime.add_shape(rect1, rect1_ctx); + runtime.add_shape(rect2, rect2_ctx); + runtime.add_shape(text, text_ctx); + + runtime.render(); +} + +/* +fn main() { + // simple_test() + + let z3_cfg = z3::Config::new(); + let z3_ctx = z3::Context::new(&z3_cfg); + + let mut ctx = Context::new(); + + let rect1_height = z3::ast::Real::new_const(&z3_ctx, "rect1_height"); + let rect1_width = z3::ast::Real::new_const(&z3_ctx, "rect1_width"); + + let rect1_bounds = Bounds { + top: Float::Defined(10.), + left: Float::Defined(10.), + height: Float::Constrained(rect1_height.clone()), + width: Float::Constrained(rect1_width.clone()), + }; + + let rect1 = Bounded::> { + bounds: rect1_bounds, + shape: Box::new(Shape::Rectangle(Rectangle {})), + }; + + let rect2_top = z3::ast::Real::new_const(&z3_ctx, "rect2_top"); + let rect2_left = z3::ast::Real::new_const(&z3_ctx, "rect2_left"); + + let rect2_bounds = Bounds { + top: Float::Constrained(rect2_top.clone()), + left: Float::Constrained(rect2_left.clone()), + height: Float::Constrained(rect1_width.clone()), + width: Float::Constrained(rect1_height.clone()), + }; + + let rect2 = Bounded::> { + bounds: rect2_bounds, + shape: Box::new(Shape::Rectangle(Rectangle {})), + }; + + let solver = z3::Solver::new(&z3_ctx); + + solver.assert(&rect1_width._eq(&(rect1_height * z3::ast::Real::from_real(&z3_ctx, 2, 1)))); + solver.assert(&rect1_width._eq(&z3::ast::Real::from_real(&z3_ctx, 42, 1))); + + solver.assert(&rect2_top._eq(&z3::ast::Real::from_real(&z3_ctx, 10, 1))); + solver.assert(&rect2_left._eq(&(rect1_width + z3::ast::Real::from_real(&z3_ctx, 10, 1)))); + + ctx.add_shape(rect1); + ctx.add_shape(rect2); + ctx.set_constraints(&z3_ctx, &solver); + + solver.check(); + let model = solver.get_model().expect("Failed to get model"); + + let shapes = ctx.draw(&model); + + let mut cairo = CairoEngine::new(); + + for shape in shapes { + cairo.draw(&shape); + } +} + +#[allow(dead_code)] +fn simple_test() { + let mut cairo = CairoEngine::new(); + + cairo.draw(&DefinitelyBounded { + bounds: DefinedBounds { + top: 10., + left: 10., + height: 40., + width: 40., + }, + shape: Shape::Rectangle(Rectangle {}), + }); + + cairo.draw(&DefinitelyBounded { + bounds: DefinedBounds { + top: 20., + left: 20., + height: 40., + width: 40., + }, + shape: Shape::Text(Text { + content: String::from("Hello, World!"), + font: FontDescription { + family: String::from("Fira Code"), + size: 21, + style: FontStyle::Normal, + weight: FontWeight::Normal, + }, + }), + }); +} +*/ -- cgit v1.2.3