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
|
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
}
}
|
