Set axiom handling

bounded/src/bdd.rs

@@ -70,20 +70,9 @@ fn check_internal<'a>(
     let indices = Indices::new(&module.signature, universe, 2);
 
     let translate = |term| {
-        fn enumerated_to_bdd(term: Enumerated, indices: &Indices) -> Bdd {
-            let go = |term| enumerated_to_bdd(term, indices);
-            match term {
-                Enumerated::And(xs) => indices.bdd_and(xs.into_iter().map(go)),
-                Enumerated::Or(xs) => indices.bdd_or(xs.into_iter().map(go)),
-                Enumerated::Not(x) => go(*x).not(),
-                Enumerated::Eq(x, y) => go(*x).iff(&go(*y)),
-                Enumerated::App(name, primes, args) => indices.bdd_var(&name, primes, &args),
-            }
-        }
-
         let term = enumerate_quantifiers(&term, &module.signature, universe)
             .map_err(CheckerError::EnumerationError)?;
-        Ok(enumerated_to_bdd(term, &indices))
+        Ok(indices.bdd_from_enumerated(term))
     };
 
     println!("starting translation...");

bounded/src/checker.rs

@@ -46,6 +46,9 @@ pub enum CheckerError {
     /// `Formula`s are single-vocabulary
     #[error("a transition contained a disjunction that contained a prime")]
     PrimeInFormula,
+    /// We can't support unproven mutable axioms without post-guards
+    #[error("an axiom that mentioned mutable relations couldn't be proven")]
+    UnprovenMutableAxiom,
 
     // smt.rs
     /// See solver::SolveError

bounded/src/indices.rs

@@ -132,6 +132,18 @@ impl Indices<'_> {
             .fold(self.bdd_context.mk_false(), |acc, term| acc.or(&term))
     }
 
+    /// Construct a `Bdd` from an `Enumerated`.
+    pub fn bdd_from_enumerated(&self, term: Enumerated) -> Bdd {
+        let go = |term| self.bdd_from_enumerated(term);
+        match term {
+            Enumerated::And(xs) => self.bdd_and(xs.into_iter().map(go)),
+            Enumerated::Or(xs) => self.bdd_or(xs.into_iter().map(go)),
+            Enumerated::Not(x) => go(*x).not(),
+            Enumerated::Eq(x, y) => go(*x).iff(&go(*y)),
+            Enumerated::App(name, primes, args) => self.bdd_var(&name, primes, &args),
+        }
+    }
+
     /// Construct a [`Model`] given a function over its indices at some time.
     pub fn model(&self, primes: usize, f: impl Fn(usize) -> usize) -> Model {
         Model::new(

bounded/src/set.rs

@@ -239,46 +239,29 @@ fn translate<'a>(
         enumerated_to_formula(term, &indices)
     };
 
-    // get cube
-    let mut init = BoundedState::ZERO;
-    let mut constrained = HashSet::default();
-    let inits = formula(Term::and(&d.inits))?;
-    for constraint in inits.get_and() {
-        if let Formula::Guard(Guard { index, value }) = constraint {
-            init.set(index, value);
-            constrained.insert(index);
-        } else {
-            return Err(CheckerError::InitNotConj);
-        }
-    }
-    // enumerate cube
-    let mut inits = vec![init];
-    println!(
-        "enumerating {} initial states",
-        2_usize.pow((indices.num_vars - constrained.len()) as u32)
+    // compute initial states
+    let inits = Term::and(d.inits.iter().chain(&d.axioms));
+    let inits = indices.bdd_from_enumerated(
+        enumerate_quantifiers(&inits, &module.signature, universe)
+            .map_err(CheckerError::EnumerationError)?,
     );
-    for index in 0..indices.num_vars {
-        if !constrained.contains(&index) {
-            let mut with_unconstrained = inits.clone();
-            for init in &mut with_unconstrained {
-                init.set(index, true);
+    println!("enumerating {} initial states", inits.exact_cardinality());
+    let inits: Vec<BoundedState> = inits
+        .sat_valuations()
+        .map(|valuation| {
+            let mut init = BoundedState::ZERO;
+            for (r, rest) in indices.iter() {
+                for (xs, (i, _)) in rest {
+                    init.set(
+                        *i,
+                        valuation.value(indices.bdd_variables[indices.get(r, 0, xs)]),
+                    );
+                }
             }
-            inits.append(&mut with_unconstrained);
-        }
-    }
-    // filter by axioms
-    let axiom = formula(Term::and(&d.axioms))?;
-    let inits = inits
-        .into_iter()
-        .filter(|init| axiom.evaluate(init))
+            init
+        })
         .collect();
 
-    assert!(
-        d.mutable_axioms(&module.signature.relations)
-            .next()
-            .is_none(),
-        "currently, the set checker does not support axioms that mention mutable relations"
-    );
     // compute imperative transitions
     let trs = match d.transitions.as_slice() {
         [] => vec![],
@@ -316,7 +299,7 @@ fn translate<'a>(
             .map(|(_, unconstrained)| 2_usize.pow(unconstrained.len() as u32))
             .sum::<usize>()
     );
-    let trs: Vec<_> = trs
+    let mut trs: Vec<_> = trs
         .into_iter()
         .flat_map(|(tr, unconstrained)| {
             // enumerate cube
@@ -361,6 +344,60 @@ fn translate<'a>(
         })
         .collect();
 
+    // filter transitions using the mutable axioms
+    let mutable_axioms = formula(Term::and(d.mutable_axioms(&module.signature.relations)))?;
+    let guard_indices = mutable_axioms.guard_indices();
+    let mut should_keep = vec![true; trs.len()];
+    for (i, should_keep) in should_keep.iter_mut().enumerate() {
+        // if the axiom was true in the pre-state, it will still be true in the post-state
+        if guard_indices
+            .iter()
+            .all(|index| !trs[i].updates.iter().any(|u| *index == u.index))
+        {
+            continue;
+        }
+        // else, try to statically determine the post-state and evaluate it
+        let guards_with_no_updates: Vec<_> = trs[i]
+            .guards
+            .iter()
+            .cloned()
+            .filter(|guard| {
+                !trs[i]
+                    .updates
+                    .iter()
+                    .any(|update| update.index == guard.index)
+            })
+            .collect();
+        let true_or_false_updates: Vec<_> = trs[i]
+            .updates
+            .iter()
+            .filter_map(|update| match &update.formula {
+                f if *f == Formula::always_true() => Some(Guard {
+                    index: update.index,
+                    value: true,
+                }),
+                f if *f == Formula::always_false() => Some(Guard {
+                    index: update.index,
+                    value: false,
+                }),
+                _ => None,
+            })
+            .collect();
+        match mutable_axioms.evaluate_partial(
+            guards_with_no_updates
+                .into_iter()
+                .chain(true_or_false_updates),
+        ) {
+            Some(b) => *should_keep = b,
+            None => return Err(CheckerError::UnprovenMutableAxiom),
+        }
+    }
+    let mut i = 0;
+    trs.retain(|_| {
+        i += 1;
+        should_keep[i - 1]
+    });
+
     // compute safety property
     let safes = d.proofs.iter().map(|proof| proof.safety.x.clone());
     let safe = formula(Term::and(safes))?;
@@ -523,6 +560,44 @@ impl Formula {
             Formula::Guard(Guard { index, value }) => state.get(*index) == *value,
         }
     }
+
+    // returns Some(true) for true, Some(false) for false, and None for unknown
+    fn evaluate_partial(&self, state: impl IntoIterator<Item = Guard>) -> Option<bool> {
+        fn evaluate_partial(formula: &Formula, state: &HashMap<usize, bool>) -> Option<bool> {
+            match formula {
+                Formula::And(terms) => terms.iter().try_fold(true, |b, term| {
+                    match (b, evaluate_partial(term, state)) {
+                        (false, _) | (_, Some(false)) => Some(false),
+                        (true, Some(true)) => Some(true),
+                        _ => None,
+                    }
+                }),
+                Formula::Or(terms) => terms.iter().try_fold(false, |b, term| {
+                    match (b, evaluate_partial(term, state)) {
+                        (true, _) | (_, Some(true)) => Some(true),
+                        (false, Some(false)) => Some(false),
+                        _ => None,
+                    }
+                }),
+                Formula::Guard(Guard { index, value }) => state.get(index).map(|v| v == value),
+            }
+        }
+        let mut map = HashMap::default();
+        for guard in state {
+            map.insert(guard.index, guard.value);
+        }
+        evaluate_partial(self, &map)
+    }
+
+    // returns a vector of the indices in the guards in this formula
+    fn guard_indices(&self) -> Vec<usize> {
+        match self {
+            Formula::And(terms) | Formula::Or(terms) => {
+                terms.iter().flat_map(Formula::guard_indices).collect()
+            }
+            Formula::Guard(Guard { index, .. }) => vec![*index],
+        }
+    }
 }
 
 // Converts a Term to exactly one Transition (we aren't doing DNF, so this function cannot
@@ -1306,6 +1381,24 @@ mod tests {
         Ok(())
     }
 
+    #[test]
+    fn checker_set_consensus_forall() -> Result<(), CheckerError> {
+        let source = include_str!("../../temporal-verifier/examples/consensus_forall.fly");
+
+        let mut m = fly::parser::parse(source).unwrap();
+        sort_check_module(&mut m).unwrap();
+        let _ = m.convert_non_bool_relations().unwrap();
+        let universe = std::collections::HashMap::from([
+            ("node".to_string(), 2),
+            ("quorum".to_string(), 2),
+            ("value".to_string(), 2),
+        ]);
+        let output = check(&m, &universe, Some(10), TraceCompression::No, false)?;
+        assert_eq!(output, CheckerAnswer::Unknown);
+
+        Ok(())
+    }
+
     #[test]
     fn checker_set_immutability() {
         let source =