liquid_layout/layout/
builder.rs

1use anyhow::Result;
2
3use super::{
4  context::{LayoutContext, Z3BuildContext},
5  prop::Prop,
6  widget::RawWidget,
7};
8use thiserror::Error;
9
10pub struct LayoutBuilder<'a> {
11  layout_ctx: &'a LayoutContext,
12  widgets: Vec<Box<dyn RawWidget<'a> + 'a>>,
13  constraints: Vec<Prop<'a>>,
14}
15
16#[derive(Debug)]
17pub struct BuildReport<'a> {
18  pub satisfied_constraints: Vec<Prop<'a>>,
19  pub unsatisfied_constraints: Vec<Prop<'a>>,
20}
21
22#[derive(Error, Debug)]
23pub enum LayoutUnsatError {
24  #[error("provided constraints cannot be satisfied")]
25  Unsat,
26  #[error("failed to derive a layout under provided constraints")]
27  Unknown,
28}
29
30impl<'a> LayoutBuilder<'a> {
31  pub fn new(layout_ctx: &'a LayoutContext) -> Self {
32    Self {
33      layout_ctx,
34      widgets: vec![],
35      constraints: vec![],
36    }
37  }
38
39  pub fn ctx(&self) -> &'a LayoutContext {
40    self.layout_ctx
41  }
42
43  pub fn push_widget<W: RawWidget<'a> + 'a>(&mut self, widget: W) {
44    let widget: Box<dyn RawWidget<'a> + 'a> = Box::new(widget);
45    self.widgets.push(widget);
46  }
47
48  pub fn push_constraint(&mut self, prop: Prop<'a>) {
49    self.constraints.push(prop);
50  }
51
52  pub fn build(self) -> Result<BuildReport<'a>> {
53    let z3_ctx = z3::Context::new(&z3::Config::new());
54    let mut build_context = Z3BuildContext::new(&z3_ctx);
55
56    let opt = z3::Optimize::new(&z3_ctx);
57
58    let constraints = self
59      .widgets
60      .iter()
61      .map(|x| x.constraints().into_iter())
62      .flatten()
63      .chain(self.constraints.iter().copied())
64      .collect::<Vec<_>>();
65    for c in &constraints {
66      opt.assert_soft(&c.build_z3(&mut build_context)?, c.weight, None);
67    }
68
69    let check_res = opt.check(&[]);
70    match check_res {
71      z3::SatResult::Sat => {}
72      z3::SatResult::Unsat => return Err(LayoutUnsatError::Unsat.into()),
73      z3::SatResult::Unknown => return Err(LayoutUnsatError::Unknown.into()),
74    }
75
76    let model = opt
77      .get_model()
78      .expect("check returned sat but failed to get model");
79    for w in self.widgets {
80      let measures = w.measures();
81      let mut refined_values = Vec::with_capacity(measures.len());
82      for m in measures {
83        let value = model
84          .eval(&m.build_z3(&mut build_context)?)
85          .expect("check returned sat but model does not provided value for a measure");
86        let (num, den) = value
87          .as_real()
88          .expect("failed to get value from a evaluated Real");
89        refined_values.push(num as f64 / den as f64);
90      }
91      w.paint(&refined_values)?;
92    }
93
94    let mut unsatisfied_constraints = vec![];
95    let mut satisfied_constraints = vec![];
96
97    for c in &constraints {
98      let value = model
99        .eval(&c.build_z3(&mut build_context)?)
100        .expect("check returned sat but model does not provided value for a prop");
101      let value = value
102        .as_bool()
103        .expect("failed to get value from a evaluated Bool");
104      if !value {
105        unsatisfied_constraints.push(*c);
106      } else {
107        satisfied_constraints.push(*c);
108      }
109    }
110
111    Ok(BuildReport {
112      unsatisfied_constraints,
113      satisfied_constraints,
114    })
115  }
116}
liquid_layout/layout/builder.rs

liquid_layout/layout/
builder.rs
