1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
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::<Box<dyn Drawable>> {
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::<Box<dyn Drawable>> {
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,
},
}),
});
}
*/
|
