liquid_layout/layout/
prop.rs

1use anyhow::Result;
2use std::fmt::{Debug, Display};
3use std::ops::{BitAnd, BitOr, Not};
4use z3::ast::{Ast, Bool};
5
6use super::measure::MeasureVariant;
7use super::{
8  context::{LayoutContext, Z3BuildContext},
9  measure::Measure,
10};
11
12/// A proposition on measurements or other propositions.
13#[derive(Copy, Clone)]
14pub struct Prop<'a> {
15  pub ctx: &'a LayoutContext,
16  pub(super) variant: &'a PropVariant<'a>,
17  pub(super) weight: u32,
18}
19
20impl<'a> Debug for Prop<'a> {
21  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
22    write!(f, "Prop({}) {{ {:?} }}", self.weight, self.variant)
23  }
24}
25
26#[derive(Copy, Clone, Debug)]
27pub enum PropVariant<'a> {
28  Eq(Measure<'a>, Measure<'a>),
29  Lt(Measure<'a>, Measure<'a>),
30  Le(Measure<'a>, Measure<'a>),
31  Gt(Measure<'a>, Measure<'a>),
32  Ge(Measure<'a>, Measure<'a>),
33  Or(Prop<'a>, Prop<'a>),
34  And(Prop<'a>, Prop<'a>),
35  Not(Prop<'a>),
36}
37
38#[allow(dead_code)]
39impl<'a> Prop<'a> {
40  pub fn with_weight(mut self, weight: u32) -> Self {
41    self.weight = weight;
42    self
43  }
44
45  pub fn select(self, left: Measure<'a>, right: Measure<'a>) -> Measure<'a> {
46    Measure {
47      ctx: self.ctx,
48      variant: self
49        .ctx
50        .alloc
51        .alloc(MeasureVariant::Select(self, left, right)),
52    }
53  }
54
55  pub fn build_z3<'ctx>(self, build_ctx: &mut Z3BuildContext<'ctx>) -> Result<Bool<'ctx>> {
56    let key = self.variant as *const _ as usize;
57    if let Some(x) = build_ctx.prop_cache.get(&key) {
58      return Ok(x.clone());
59    }
60    let res = self.do_build_z3(build_ctx)?;
61    build_ctx.prop_cache.insert(key, res.clone());
62    Ok(res)
63  }
64
65  fn do_build_z3<'ctx>(self, build_ctx: &mut Z3BuildContext<'ctx>) -> Result<Bool<'ctx>> {
66    use PropVariant as V;
67    let z3_ctx = build_ctx.z3_ctx;
68    Ok(match *self.variant {
69      V::Eq(left, right) => left.build_z3(build_ctx)?._eq(&right.build_z3(build_ctx)?),
70      V::Lt(left, right) => left.build_z3(build_ctx)?.lt(&right.build_z3(build_ctx)?),
71      V::Le(left, right) => left.build_z3(build_ctx)?.le(&right.build_z3(build_ctx)?),
72      V::Gt(left, right) => left.build_z3(build_ctx)?.gt(&right.build_z3(build_ctx)?),
73      V::Ge(left, right) => left.build_z3(build_ctx)?.ge(&right.build_z3(build_ctx)?),
74      V::Or(left, right) => Bool::or(
75        z3_ctx,
76        &[&left.build_z3(build_ctx)?, &right.build_z3(build_ctx)?],
77      ),
78      V::And(left, right) => Bool::and(
79        z3_ctx,
80        &[&left.build_z3(build_ctx)?, &right.build_z3(build_ctx)?],
81      ),
82      V::Not(that) => that.build_z3(build_ctx)?.not(),
83    })
84  }
85}
86
87impl<'a> Display for Prop<'a> {
88  fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
89    match self.variant {
90      PropVariant::Eq(l, r) => write!(f, "{} == {}", l, r),
91      PropVariant::Lt(l, r) => write!(f, "{} < {}", l, r),
92      PropVariant::Le(l, r) => write!(f, "{} <= {}", l, r),
93      PropVariant::Gt(l, r) => write!(f, "{} > {}", l, r),
94      PropVariant::Ge(l, r) => write!(f, "{} >= {}", l, r),
95      PropVariant::Or(l, r) => write!(f, "({}) or ({})", l, r),
96      PropVariant::And(l, r) => write!(f, "({}) and ({})", l, r),
97      PropVariant::Not(x) => write!(f, "not ({})", x),
98    }
99  }
100}
101
102impl<'a> BitOr for Prop<'a> {
103  type Output = Self;
104  fn bitor(self, that: Prop<'a>) -> Self {
105    Self {
106      ctx: self.ctx,
107      variant: self.ctx.alloc.alloc(PropVariant::Or(self, that)),
108      weight: 10,
109    }
110  }
111}
112
113impl<'a> BitAnd for Prop<'a> {
114  type Output = Self;
115  fn bitand(self, that: Prop<'a>) -> Self {
116    Self {
117      ctx: self.ctx,
118      variant: self.ctx.alloc.alloc(PropVariant::And(self, that)),
119      weight: 10,
120    }
121  }
122}
123
124impl<'a> Not for Prop<'a> {
125  type Output = Self;
126  fn not(self) -> Self {
127    Self {
128      ctx: self.ctx,
129      variant: self.ctx.alloc.alloc(PropVariant::Not(self)),
130      weight: 10,
131    }
132  }
133}
liquid_layout/layout/prop.rs

liquid_layout/layout/
prop.rs
