cvlr_spec/
combinators.rs

1//! Combinators for composing boolean expressions.
2
3use crate::formula::CvlrFormula;
4
5/// A boolean expression representing the logical AND of two expressions.
6///
7/// This expression evaluates to `true` only when both sub-expressions evaluate to `true`.
8/// When asserting or assuming, both sub-expressions are processed.
9#[derive(Copy, Clone)]
10pub struct CvlrAnd<A, B>(A, B);
11
12impl<A, B> CvlrFormula for CvlrAnd<A, B>
13where
14    A: CvlrFormula,
15    B: CvlrFormula<Context = A::Context>,
16{
17    type Context = A::Context;
18    fn eval(&self, ctx: &Self::Context) -> bool {
19        self.0.eval(ctx) && self.1.eval(ctx)
20    }
21    fn assert(&self, ctx: &Self::Context) {
22        self.0.assert(ctx);
23        self.1.assert(ctx);
24    }
25    fn assume(&self, ctx: &Self::Context) {
26        self.0.assume(ctx);
27        self.1.assume(ctx);
28    }
29
30    fn eval_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) -> bool {
31        self.0.eval_with_states(ctx0, ctx1) && self.1.eval_with_states(ctx0, ctx1)
32    }
33    fn assert_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
34        self.0.assert_with_states(ctx0, ctx1);
35        self.1.assert_with_states(ctx0, ctx1);
36    }
37    fn assume_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
38        self.0.assume_with_states(ctx0, ctx1);
39        self.1.assume_with_states(ctx0, ctx1);
40    }
41}
42
43/// Combines two boolean expressions with logical AND.
44///
45/// Returns a new expression that evaluates to `true` only when both input
46/// expressions evaluate to `true`.
47///
48/// # Arguments
49///
50/// * `a` - The first boolean expression
51/// * `b` - The second boolean expression
52///
53/// # Examples
54///
55/// ```
56/// use cvlr_spec::{cvlr_and, cvlr_true, CvlrFormula};
57///
58/// let expr = cvlr_and(cvlr_true::<()>(), cvlr_true::<()>());
59/// assert!(expr.eval(&()));
60/// ```
61pub fn cvlr_and<A, B>(a: A, b: B) -> CvlrAnd<A, B>
62where
63    A: CvlrFormula,
64    B: CvlrFormula<Context = A::Context>,
65{
66    CvlrAnd(a, b)
67}
68
69/// A boolean expression representing logical implication (A → B).
70///
71/// This expression evaluates to `true` when either the antecedent `A` is `false`,
72/// or when both `A` and `B` are `true`. When asserting or assuming, the consequent
73/// `B` is only processed if the antecedent `A` evaluates to `true`.
74#[derive(Copy, Clone)]
75pub struct CvlrImplies<A, B>(A, B);
76
77impl<A, B> CvlrFormula for CvlrImplies<A, B>
78where
79    A: CvlrFormula,
80    B: CvlrFormula<Context = A::Context>,
81{
82    type Context = A::Context;
83    fn eval(&self, ctx: &Self::Context) -> bool {
84        if self.0.eval(ctx) {
85            self.1.eval(ctx)
86        } else {
87            true
88        }
89    }
90
91    fn assert(&self, ctx: &Self::Context) {
92        if self.0.eval(ctx) {
93            self.1.assert(ctx);
94        }
95    }
96    fn assume(&self, ctx: &Self::Context) {
97        if self.0.eval(ctx) {
98            self.1.assume(ctx);
99        }
100    }
101
102    fn eval_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) -> bool {
103        if self.0.eval_with_states(ctx0, ctx1) {
104            self.1.eval_with_states(ctx0, ctx1)
105        } else {
106            true
107        }
108    }
109
110    fn assert_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
111        if self.0.eval_with_states(ctx0, ctx1) {
112            self.1.assert_with_states(ctx0, ctx1)
113        }
114    }
115
116    fn assume_with_states(&self, ctx0: &Self::Context, ctx1: &Self::Context) {
117        if self.0.eval_with_states(ctx0, ctx1) {
118            self.1.assume_with_states(ctx0, ctx1)
119        }
120    }
121}
122
123/// Creates a boolean expression representing logical implication (A → B).
124///
125/// Returns a new expression that evaluates to `true` when either `a` is `false`
126/// or when both `a` and `b` are `true`.
127///
128/// # Arguments
129///
130/// * `a` - The antecedent (left-hand side) of the implication
131/// * `b` - The consequent (right-hand side) of the implication
132///
133/// # Examples
134///
135/// ```
136/// use cvlr_spec::{cvlr_implies, cvlr_true, CvlrFormula};
137///
138/// // true → true evaluates to true
139/// let expr = cvlr_implies(cvlr_true::<()>(), cvlr_true::<()>());
140/// assert!(expr.eval(&()));
141/// ```
142pub fn cvlr_implies<A, B>(a: A, b: B) -> CvlrImplies<A, B>
143where
144    A: CvlrFormula,
145    B: CvlrFormula<Context = A::Context>,
146{
147    CvlrImplies(a, b)
148}
cvlr_spec/combinators.rs

cvlr_spec/
combinators.rs
