Update Robinson to postfix @ and unnamed invariants

CreuSAT/src/assignments.rs

@@ -17,8 +17,8 @@ impl Index<usize> for Assignments {
     type Output = AssignedState;
     #[inline]
     #[cfg_attr(feature = "trust_assignments", trusted)]
-    #[requires(@ix < (@self).len())]
-    #[ensures((@self)[@ix] == *result)]
+    #[requires(i@x < self@.len())]
+    #[ensures(self@[i@x] == *result)]
     fn index(&self, ix: usize) -> &AssignedState {
         #[cfg(not(creusot))]
         unsafe {
@@ -32,10 +32,10 @@ impl Index<usize> for Assignments {
 impl IndexMut<usize> for Assignments {
     #[inline]
     #[cfg_attr(feature = "trust_assignments", trusted)]
-    #[requires(@ix < (@self).len())]
-    #[ensures((@*self)[@ix] == *result)]
-    #[ensures((@^self)[@ix] == ^result)]
-    #[ensures(forall<i : Int> 0 <= i && i != @ix && i < (@self).len() ==> (@self)[i] == (@^self)[i])]
+    #[requires(i@x < self@.len())]
+    #[ensures((@*self)[i@x] == *result)]
+    #[ensures((@^self)[i@x] == ^result)]
+    #[ensures(forall<i : Int> 0 <= i && i != i@x && i < self@.len() ==> self@[i] == (@^self)[i])]
     #[ensures((@^self).len() == (@*self).len())]
     fn index_mut(&mut self, ix: usize) -> &mut AssignedState {
         #[cfg(not(creusot))]
@@ -51,7 +51,7 @@ impl Assignments {
     // Ok
     #[inline(always)]
     #[cfg_attr(feature = "trust_assignments", trusted)]
-    #[ensures(@result == (@self).len())]
+    #[ensures(result@ == self@.len())]
     pub fn len(&self) -> usize {
         self.0.len()
     }
@@ -62,12 +62,12 @@ impl Assignments {
     #[requires(lit.invariant(@_f.num_vars))]
     #[requires(_f.invariant())]
     #[requires(trail_invariant(@_t, *_f))]
-    #[requires(unset((@self)[lit.index_logic()]))]
-    #[requires(long_are_post_unit_inner(@_t, *_f, @self))]
+    #[requires(unset(self@[lit.index_logic()]))]
+    #[requires(long_are_post_unit_inner(@_t, *_f, self@))]
     #[ensures(long_are_post_unit_inner(@_t, *_f, @^self))]
     #[ensures(!unset((@^self)[lit.index_logic()]))]
-    #[ensures((@^self).len() == (@self).len())]
-    #[ensures((forall<j : Int> 0 <= j && j < (@self).len()
+    #[ensures((@^self).len() == self@.len())]
+    #[ensures((forall<j : Int> 0 <= j && j < self@.len()
             && j != lit.index_logic() ==> (@*self)[j] == (@^self)[j]))]
     #[ensures(lit.sat(^self))]
     pub fn set_assignment(&mut self, lit: Lit, _f: &Formula, _t: &Vec<Step>) {

CreuSAT/src/clause.rs

@@ -19,8 +19,8 @@ impl Index<usize> for Clause {
     type Output = Lit;
     #[inline]
     #[cfg_attr(feature = "trust_clause", trusted)]
-    #[requires(@ix < (@self).len())]
-    #[ensures((@self)[@ix] == *result)]
+    #[requires(i@x < self@.len())]
+    #[ensures(self@[i@x] == *result)]
     fn index(&self, ix: usize) -> &Lit {
         #[cfg(not(creusot))]
         unsafe {
@@ -34,10 +34,10 @@ impl Index<usize> for Clause {
 impl IndexMut<usize> for Clause {
     #[inline]
     #[cfg_attr(feature = "trust_clause", trusted)]
-    #[requires(@ix < (@self).len())]
-    #[ensures((@*self)[@ix] == *result)]
-    #[ensures((@^self)[@ix] == ^result)]
-    #[ensures(forall<i : Int> 0 <= i && i != @ix && i < (@self).len() ==> (@self)[i] == (@^self)[i])]
+    #[requires(i@x < self@.len())]
+    #[ensures((@*self)[i@x] == *result)]
+    #[ensures((@^self)[i@x] == ^result)]
+    #[ensures(forall<i : Int> 0 <= i && i != i@x && i < self@.len() ==> self@[i] == (@^self)[i])]
     #[ensures((@^self).len() == (@*self).len())]
     fn index_mut(&mut self, ix: usize) -> &mut Lit {
         #[cfg(not(creusot))]
@@ -54,7 +54,7 @@ impl Clause {
     #[ensures(result == self.invariant(@n))]
     pub fn check_clause_invariant(&self, n: usize) -> bool {
         let mut i: usize = 0;
-        #[invariant(inv, forall<j: Int> 0 <= j && j < @i ==> (@self)[j].invariant(@n))]
+        #[invariant(inv, forall<j: Int> 0 <= j && j < i@ ==> self@[j].invariant(@n))]
         while i < self.len() {
             if !self[i].check_lit_invariant(n) {
                 return false;
@@ -72,12 +72,12 @@ impl Clause {
     pub fn no_duplicates(&self) -> bool {
         let mut i: usize = 0;
         #[invariant(no_dups,
-            forall<j: Int, k: Int> 0 <= j && j < @i &&
-             0 <= k && k < j ==> (@self)[j].index_logic() != (@self)[k].index_logic())]
+            forall<j: Int, k: Int> 0 <= j && j < i@ &&
+             0 <= k && k < j ==> self@[j].index_logic() != self@[k].index_logic())]
         while i < self.len() {
             let lit1 = self[i];
             let mut j: usize = 0;
-            #[invariant(inv, forall<k: Int> 0 <= k && k < @j ==> lit1.index_logic() != (@self)[k].index_logic())]
+            #[invariant(inv, forall<k: Int> 0 <= k && k < @j ==> lit1.index_logic() != self@[k].index_logic())]
             while j < i {
                 let lit2 = self[j];
                 if lit1.index() == lit2.index() {
@@ -92,7 +92,7 @@ impl Clause {
 
     #[inline(always)]
     #[cfg_attr(feature = "trust_clause", trusted)]
-    #[ensures(@result == (@self).len())]
+    #[ensures(result@ == self@.len())]
     pub fn len(&self) -> usize {
         self.lits.len()
     }
@@ -108,14 +108,14 @@ impl Clause {
     #[inline(always)]
     #[cfg_attr(feature = "trust_clause", trusted)]
     #[maintains((mut self).invariant(@_f.num_vars))]
-    #[requires((@self).len() > 0)]
-    #[requires(@idx < (@self).len())]
+    #[requires(self@.len() > 0)]
+    #[requires(i@dx < self@.len())]
     #[ensures(forall<i: Int> 0 <= i && i < (@(^self)).len() ==>
-        (exists<j: Int> 0 <= j && j < (@self).len() && (@(^self))[i] == (@self)[j]))]
-    #[ensures((@(^self))[(@^self).len() - 1] == (@self)[@idx])]
-    #[ensures((@(^self)).len() == (@self).len())]
-    #[ensures(forall<j: Int> 0 <= j && j < (@self).len()
-        ==> (@self)[j].lit_in(^self))]
+        (exists<j: Int> 0 <= j && j < self@.len() && (@(^self))[i] == self@[j]))]
+    #[ensures((@(^self))[(@^self).len() - 1] == self@[i@dx])]
+    #[ensures((@(^self)).len() == self@.len())]
+    #[ensures(forall<j: Int> 0 <= j && j < self@.len()
+        ==> self@[j].lit_in(^self))]
     fn move_to_end(&mut self, idx: usize, _f: &Formula) {
         let end = self.len() - 1;
         self.lits.swap(idx, end);
@@ -125,29 +125,29 @@ impl Clause {
     #[inline(always)]
     #[cfg_attr(feature = "trust_clause", trusted)]
     #[maintains((mut self).invariant(@_f.num_vars))]
-    #[requires((@self).len() > 0)]
-    #[requires(@idx < (@self).len())]
+    #[requires(self@.len() > 0)]
+    #[requires(i@dx < self@.len())]
     #[ensures(forall<i: Int> 0 <= i && i < (@(^self)).len() ==>
-        exists<j: Int> 0 <= j && j < (@self).len() && (@(^self))[i] == (@self)[j])]
-    #[ensures((@(^self)).len() + 1 == (@self).len())]
-    #[ensures(!(@self)[@idx].lit_in(^self))]
-    #[ensures(forall<j: Int> 0 <= j && j < (@self).len()
-        && j != @idx ==> (@self)[j].lit_in(^self))]
+        exists<j: Int> 0 <= j && j < self@.len() && (@(^self))[i] == self@[j])]
+    #[ensures((@(^self)).len() + 1 == self@.len())]
+    #[ensures(!self@[i@dx].lit_in(^self))]
+    #[ensures(forall<j: Int> 0 <= j && j < self@.len()
+        && j != i@dx ==> self@[j].lit_in(^self))]
     pub fn remove_from_clause(&mut self, idx: usize, _f: &Formula) {
         self.move_to_end(idx, _f);
         self.lits.pop();
     }
 
     // This is an ugly runtime check
     #[cfg_attr(feature = "trust_clause", trusted)]
-    #[requires(invariant_internal(@self, @_f.num_vars))]
+    #[requires(invariant_internal(self@, @_f.num_vars))]
     #[requires(a.invariant(*_f))]
-    #[requires((@self).len() > 1)]
+    #[requires(self@.len() > 1)]
     #[ensures(result ==> self.unit(*a))]
-    #[ensures(result ==> (@self)[0].unset(*a))]
+    #[ensures(result ==> self@[0].unset(*a))]
     pub fn unit_and_unset(&self, a: &Assignments, _f: &Formula) -> bool {
         let mut i: usize = 1;
-        #[invariant(unsat, forall<j: Int> 1 <= j && j < @i ==> (@self)[j].unsat(*a))]
+        #[invariant(unsat, forall<j: Int> 1 <= j && j < i@ ==> self@[j].unsat(*a))]
         while i < self.len() {
             if !self[i].lit_unsat(a) {
                 return false;
@@ -159,11 +159,11 @@ impl Clause {
 
     // ONLY VALID FOR CLAUSES NOT IN THE FORMULA
     #[cfg_attr(feature = "trust_clause", trusted)]
-    #[requires((@self).len() > @j)]
-    #[requires((@self).len() > @k)]
+    #[requires(self@.len() > @j)]
+    #[requires(self@.len() > @k)]
     #[maintains((mut self).invariant(@_f.num_vars))]
     #[maintains((mut self).equisat_extension(*_f))]
-    #[ensures((@self).len() == (@(^self)).len())]
+    #[ensures(self@.len() == (@(^self)).len())]
     pub fn swap_lits_in_clause(&mut self, _f: &Formula, j: usize, k: usize) {
         let old_c: Ghost<&mut Clause> = ghost! { self };
         self.lits.swap(j, k);
@@ -177,7 +177,7 @@ impl Clause {
     pub fn calc_lbd(&self, _f: &Formula, s: &mut Solver, t: &Trail) -> usize {
         let mut i: usize = 0;
         let mut lbd: usize = 0;
-        #[invariant(lbd_bound, @lbd <= @i)]
+        #[invariant(lbd_bound, @lbd <= i@)]
         while i < self.len() {
             let level = t.lit_to_level[self[i].index()];
             if level < s.perm_diff.len() && // TODO: Add this as an invariant to Solver

CreuSAT/src/conflict_analysis.rs

@@ -19,23 +19,23 @@ pub enum Conflict {
 #[inline(always)]
 #[cfg_attr(feature = "trust_conflict", trusted)]
 #[requires(vars_in_range_inner(@c, (@seen).len()))]
-#[requires(@idx < (@seen).len())]
-#[requires((@seen)[@idx] == idx_in_logic(@idx, @c))]
-#[ensures(result == (exists<i: Int> 0 <= i && i < (@c).len() && (@c)[i].index_logic() == @idx))]
+#[requires(i@dx < (@seen).len())]
+#[requires((@seen)[i@dx] == idx_in_logic(i@dx, @c))]
+#[ensures(result == (exists<i: Int> 0 <= i && i < (@c).len() && (@c)[i].index_logic() == i@dx))]
 fn idx_in(c: &Vec<Lit>, idx: usize, seen: &Vec<bool>) -> bool {
     seen[idx]
 }
 
 #[cfg_attr(feature = "trust_conflict", trusted)]
 #[requires(_f.invariant())]
 #[requires(trail.invariant(*_f))]
-#[requires(@idx < @_f.num_vars)]
+#[requires(i@dx < @_f.num_vars)]
 #[requires(o.in_formula(*_f))]
 #[requires(@c_idx < (@c).len()
-    && (@c)[@c_idx].index_logic() == @idx
+    && (@c)[@c_idx].index_logic() == i@dx
     && (@o)[0].is_opp((@c)[@c_idx])
 )]
-#[requires(c.same_idx_same_polarity_except(*o, @idx))]
+#[requires(c.same_idx_same_polarity_except(*o, i@dx))]
 // New post unit -> abstract away
 #[requires(forall<j: Int> 1 <= j && j < (@o).len() ==> (@o)[j].unsat_inner(@trail.assignments))]
 #[requires((@o)[0].sat_inner(@trail.assignments))]
@@ -78,9 +78,9 @@ fn resolve(
     let mut i: usize = 1;
     #[invariant(inv, c.invariant(@_f.num_vars))]
     #[invariant(all_unsat, c.unsat(trail.assignments))] // TODO: Should be stated with regards to seq
-    #[invariant(i_bound, 1 <= @i && @i <= (@o).len())]
+    #[invariant(i_bound, 1 <= i@ && i@ <= (@o).len())]
     #[invariant(not_in, !(@old_c)[@c_idx].lit_in(*c) && !(@o)[0].lit_in(*c))]
-    #[invariant(all_in, forall<j: Int> 1 <= j && j < @i ==> (@o)[j].lit_in(*c))]
+    #[invariant(all_in, forall<j: Int> 1 <= j && j < i@ ==> (@o)[j].lit_in(*c))]
     #[invariant(all_in2, forall<j: Int> 0 <= j && j < (@old_c).len()
         && j != @c_idx ==> (@old_c)[j].lit_in(*c))]
     #[invariant(from_c_or_o, (forall<j: Int> 0 <= j && j < (@c).len() ==>
@@ -104,9 +104,9 @@ fn resolve(
             if trail.lit_to_level[o[i].index()] >= trail.decision_level() {
                 *path_c += 1;
             }
-            proof_assert!(@c == (@old_c3).push((@o)[@i]));
+            proof_assert!(@c == (@old_c3).push((@o)[i@]));
             proof_assert!((@c).len() == (@old_c3).len() + 1);
-            proof_assert!((@o)[@i].lit_in(*c));
+            proof_assert!((@o)[i@].lit_in(*c));
         }
 
         proof_assert!(forall<j: Int> 0 <= j && j < (@old_c3).len() ==>
@@ -120,7 +120,7 @@ fn resolve(
 #[cfg_attr(feature = "trust_conflict", trusted)]
 #[requires(trail.invariant(*_f))]
 #[requires(c.unsat(trail.assignments))]
-#[requires(@i <= (@trail.trail).len())]
+#[requires(i@ <= (@trail.trail).len())]
 #[requires((@seen).len() == @_f.num_vars)]
 #[ensures(match result {
     Some(r) =>  @r < (@c).len()
@@ -133,13 +133,13 @@ fn resolve(
 })]
 fn choose_literal(c: &Clause, trail: &Trail, i: &mut usize, _f: &Formula, seen: &Vec<bool>) -> Option<usize> {
     let old_i: Ghost<&mut usize> = ghost! {i};
-    #[invariant(i_bound, 0 <= @i && @i <= (@trail.trail).len())]
+    #[invariant(i_bound, 0 <= i@ && i@ <= (@trail.trail).len())]
     #[invariant(proph_i, ^i == ^old_i.inner())]
     while *i > 0 {
         *i -= 1;
         if seen[trail.trail[*i].lit.index()] {
             let mut k: usize = 0;
-            #[invariant(i_bound2, 0 <= @i && @i < (@trail.trail).len())]
+            #[invariant(i_bound2, 0 <= i@ && i@ < (@trail.trail).len())]
             #[invariant(k_bound, 0 <= @k && @k <= (@c).len())]
             #[invariant(proph_i2, ^i == ^old_i.inner())]
             while k < c.len() {
@@ -155,36 +155,36 @@ fn choose_literal(c: &Clause, trail: &Trail, i: &mut usize, _f: &Formula, seen:
 
 #[cfg_attr(feature = "trust_conflict", trusted)]
 #[requires(f.invariant())]
-#[requires(@f.num_vars < @usize::MAX)]
+#[requires(f.num_vars@ < usize::MAX@)]
 #[requires(trail.invariant(*f))]
-#[requires(@cref < (@f.clauses).len())]
-#[requires((@f.clauses)[@cref].unsat(trail.assignments))]
+#[requires(@cref < f.clauses@.len())]
+#[requires(f.clauses@[@cref].unsat(trail.assignments))]
 #[ensures(match result {
     Conflict::Ground => f.not_satisfiable(),
     Conflict::Unit(clause) => {
-        clause.invariant(@f.num_vars)
+        clause.invariant(f.num_vars@)
         && (@clause).len() == 1
-        && vars_in_range_inner(@clause, @f.num_vars)
+        && vars_in_range_inner(@clause, f.num_vars@)
         && no_duplicate_indexes_inner(@clause)
         && equisat_extension_inner(clause, @f)
     },
     Conflict::Learned(s_idx, clause) => {
-        clause.invariant(@f.num_vars)
+        clause.invariant(f.num_vars@)
         && (@clause).len() > 1
-        && vars_in_range_inner(@clause, @f.num_vars)
+        && vars_in_range_inner(@clause, f.num_vars@)
         && no_duplicate_indexes_inner(@clause)
         && equisat_extension_inner(clause, @f)
         && @s_idx < (@clause).len()
     },
     Conflict::Restart(clause) => {
-        clause.invariant(@f.num_vars)
+        clause.invariant(f.num_vars@)
         && (@clause).len() > 1
-        && vars_in_range_inner(@clause, @f.num_vars)
+        && vars_in_range_inner(@clause, f.num_vars@)
         && no_duplicate_indexes_inner(@clause)
         && equisat_extension_inner(clause, @f)
     },
 })]
-#[maintains((mut d).invariant(@f.num_vars))]
+#[maintains((mut d).invariant(f.num_vars@))]
 pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisions) -> Conflict {
     let decisionlevel = trail.decision_level();
     let mut to_bump = Vec::new();
@@ -196,10 +196,10 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
     let mut j: usize = 0;
     #[invariant(seen_is_clause, forall<idx: Int> 0 <= idx && idx < (@seen).len() ==>
         ((@seen)[idx] == (exists<i: Int> 0 <= i && i < @j && (@clause)[i].index_logic() == idx)))]
-    #[invariant(seen_len, (@seen).len() == @f.num_vars)]
+    #[invariant(seen_len, (@seen).len() == f.num_vars@)]
     #[invariant(path_c_less, @path_c <= @j)]
     #[invariant(j_is_len, @j <= (@clause).len())] // This is needed to establish the loop invariant for the next loop
-    #[invariant(elems_less, elems_less_than(@to_bump, @f.num_vars))]
+    #[invariant(elems_less, elems_less_than(@to_bump, f.num_vars@))]
     while j < clause.len() {
         seen[clause[j].index()] = true;
         to_bump.push(clause[j].index());
@@ -209,15 +209,15 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
         j += 1;
     }
     let mut clause = clause;
-    #[invariant(seen_len, (@seen).len() == @f.num_vars)]
+    #[invariant(seen_len, (@seen).len() == f.num_vars@)]
     #[invariant(seen_is_clause, forall<idx: Int> 0 <= idx && idx < (@seen).len() ==>
         ((@seen)[idx] == idx_in_logic(idx, @clause)))]
-    #[invariant(clause_vars, clause.invariant(@f.num_vars))]
+    #[invariant(clause_vars, clause.invariant(f.num_vars@))]
     #[invariant(clause_equi, equisat_extension_inner(clause, @f))]
     #[invariant(clause_unsat, clause.unsat(trail.assignments))]
-    #[invariant(i_bound, 0 <= @i && @i <= (@trail.trail).len())]
+    #[invariant(i_bound, 0 <= i@ && i@ <= (@trail.trail).len())]
     #[invariant(path_c_less, @path_c <= (@clause).len())]
-    #[invariant(elems_less, elems_less_than(@to_bump, @f.num_vars))]
+    #[invariant(elems_less, elems_less_than(@to_bump, f.num_vars@))]
     while path_c > break_cond {
         let c_idx = match choose_literal(&clause, trail, &mut i, f, &seen) {
             Some(c_idx) => c_idx,
@@ -229,7 +229,7 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
             _ => break,
         };
         let idx = trail.trail[i].lit.index();
-        proof_assert!(clause.same_idx_same_polarity_except(*ante, @idx));
+        proof_assert!(clause.same_idx_same_polarity_except(*ante, i@dx));
         resolve(f, &mut clause, ante, idx, c_idx, &trail, &mut seen, &mut path_c, &mut to_bump);
     }
     //let clause = clause;
@@ -261,8 +261,8 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
 #[cfg_attr(all(feature = "trust_conflict", not(feature = "problem_child")), trusted)]
 #[requires(f.invariant())]
 #[requires(trail.invariant(*f))]
-#[requires(@cref < (@f.clauses).len())]
-#[requires((@f.clauses)[@cref].unsat(trail.assignments))]
+#[requires(@cref < f.clauses@.len())]
+#[requires(f.clauses@[@cref].unsat(trail.assignments))]
 #[ensures(result ==> f.not_satisfiable())]
 pub fn resolve_empty_clause(f: &Formula, trail: &Trail, cref: usize) -> bool {
     let decisionlevel = trail.decision_level();
@@ -273,7 +273,7 @@ pub fn resolve_empty_clause(f: &Formula, trail: &Trail, cref: usize) -> bool {
     let mut j: usize = 0;
     #[invariant(seen_is_clause, forall<idx: Int> 0 <= idx && idx < (@seen).len() ==>
         ((@seen)[idx] == (exists<i: Int> 0 <= i && i < @j && (@clause)[i].index_logic() == idx)))]
-    #[invariant(seen_len, (@seen).len() == @f.num_vars)]
+    #[invariant(seen_len, (@seen).len() == f.num_vars@)]
     #[invariant(j_is_len, @j <= (@clause).len())]
     // This is needed to establish the loop invariant for the next loop
     while j < clause.len() {