Merge pull request #42 from sarsko/update-creusot

Update Creusot

.gitignore

@@ -4,3 +4,4 @@ tests/2018/
 *.bak
 /playground
 tests/probs
+/mir_dump/

CreuSAT/Cargo.toml

@@ -8,7 +8,7 @@ edition = "2021"
 #clap = "4.0.18"
 clap = "2.33.3"
 rand = "*"
-creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "5cc6cdd6" }
+creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "1357cc97" }
 
 [dev-dependencies]
 termcolor = "1.1"

CreuSAT/src/assignments.rs

@@ -70,8 +70,8 @@ impl Assignments {
     #[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>) {
-        let old_self: Ghost<&mut Assignments> = ghost! { self };
-        //self.0[lit.index()] = lit.is_positive() as u8;
+        let old_self: Snapshot<&mut Assignments> = snapshot! { self };
+        //self.clauses[lit.index()] = lit.is_positive() as u8;
         if lit.is_positive() {
             self.0[lit.index()] = 1;
         } else {

CreuSAT/src/clause.rs

@@ -1,5 +1,5 @@
 extern crate creusot_contracts;
-use creusot_contracts::{std::*, Clone, Ghost, *};
+use creusot_contracts::{std::*, Clone, Snapshot, *};
 
 use crate::{assignments::*, formula::*, lit::*, solver::*, trail::*};
 use ::std::ops::{Index, IndexMut};
@@ -61,10 +61,7 @@ impl Clause {
             }
             i += 1;
         }
-        if self.no_duplicates() {
-            return true;
-        }
-        false
+        return self.no_duplicates();
     }
 
     #[cfg_attr(feature = "trust_clause", trusted)]
@@ -161,14 +158,16 @@ impl Clause {
     #[cfg_attr(feature = "trust_clause", trusted)]
     #[requires(self@.len() > j@)]
     #[requires(self@.len() > k@)]
+    #[requires(_f.invariant())]
     #[maintains((mut self).invariant(_f.num_vars@))]
     #[maintains((mut self).equisat_extension(*_f))]
     #[ensures(self@.len() == (^self)@.len())]
+    #[ensures((^self)@.exchange(self@, j@, k@))]
     pub fn swap_lits_in_clause(&mut self, _f: &Formula, j: usize, k: usize) {
-        let old_c: Ghost<&mut Clause> = ghost! { self };
+        let old_c: Snapshot<&mut Clause> = snapshot! { self };
         self.lits.swap(j, k);
-        proof_assert!(eventually_sat_complete(((_f@.0).push(*self), _f@.1)) ==>
-                      eventually_sat_complete(((_f@.0).push(*old_c.inner()), _f@.1)));
+        proof_assert!(lemma_permuted_clause_maintains_equisat(_f@, *old_c.inner(), *self); true);
+        proof_assert!(dup_stable_on_permut(*old_c.inner(), *self); true);
     }
 
     #[cfg_attr(feature = "trust_clause", trusted)]

CreuSAT/src/conflict_analysis.rs

@@ -1,5 +1,5 @@
 extern crate creusot_contracts;
-use creusot_contracts::{std::*, vec, Ghost, *};
+use creusot_contracts::{std::*, vec, Snapshot, *};
 
 use crate::{assignments::*, clause::*, decision::*, formula::*, lit::*, trail::*};
 
@@ -54,10 +54,10 @@ fn resolve(
     _f: &Formula, c: &mut Clause, o: &Clause, idx: usize, c_idx: usize, trail: &Trail, seen: &mut Vec<bool>,
     path_c: &mut usize, to_bump: &mut Vec<usize>,
 ) {
-    let old_c: Ghost<&mut Clause> = ghost!(c);
-    let old_seen: Ghost<&mut Vec<bool>> = ghost!(seen);
-    let old_path_c: Ghost<&mut usize> = ghost!(path_c);
-    let old_to_bump: Ghost<&mut Vec<usize>> = ghost!(to_bump);
+    let old_c: Snapshot<&mut Clause> = snapshot!(c);
+    let old_seen: Snapshot<&mut Vec<bool>> = snapshot!(seen);
+    let old_path_c: Snapshot<&mut usize> = snapshot!(path_c);
+    let old_to_bump: Snapshot<&mut Vec<usize>> = snapshot!(to_bump);
 
     proof_assert!(c.clause_is_seen(*seen));
 
@@ -68,7 +68,7 @@ fn resolve(
 
     proof_assert!(^seen == ^old_seen.inner());
     proof_assert!(c.clause_is_seen(*seen));
-    let old_c2: Ghost<&mut Clause> = ghost!(c);
+    let old_c2: Snapshot<&mut Clause> = snapshot!(c);
     proof_assert!(!old_c@[c_idx@].lit_in(*c));
     proof_assert!(^c == ^old_c.inner());
     proof_assert!(forall<j: Int> 0 <= j && j < old_c@.len()
@@ -89,7 +89,7 @@ fn resolve(
     #[invariant(seen@.len() == _f.num_vars@)]
     #[invariant(elems_less_than(to_bump@, _f.num_vars@))]
     while i < o.len() {
-        let old_c3: Ghost<&mut Clause> = ghost!(c);
+        let old_c3: Snapshot<&mut Clause> = snapshot!(c);
         proof_assert!(^c == ^old_c3.inner());
 
         if !idx_in(&c.lits, o[i].index(), &seen) {
@@ -127,7 +127,7 @@ fn resolve(
     None => (^i)@ == 0
 })]
 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};
+    let old_i: Snapshot<&mut usize> = snapshot! {i};
     #[invariant(0 <= i@ && i@ <= trail.trail@.len())]
     while *i > 0 {
         *i -= 1;

CreuSAT/src/decision.rs

@@ -1,5 +1,5 @@
 extern crate creusot_contracts;
-use creusot_contracts::{ensures, ghost, invariant, maintains, proof_assert, requires, std::vec, Clone, Ghost, Int, *};
+use creusot_contracts::{ensures, invariant, maintains, proof_assert, requires, std::vec, Clone, Int, Snapshot, *};
 
 use crate::{assignments::*, formula::*, util::*};
 
@@ -26,6 +26,7 @@ impl ::std::default::Default for Node {
 
 impl creusot_contracts::Default for Node {
     #[predicate]
+    #[open]
     fn is_default(self) -> bool {
         pearlite! { self.next@ == usize::MAX@ && self.prev@ == usize::MAX@ && self.ts@ == 0 }
     }
@@ -135,7 +136,7 @@ impl Decisions {
     #[ensures((^self).linked_list@.len() == self.linked_list@.len())]
     fn rescore(&mut self, _f: &Formula) {
         let INVALID: usize = usize::MAX;
-        let old_self: Ghost<&mut Decisions> = ghost! { self };
+        let old_self: Snapshot<&mut Decisions> = snapshot! { self };
         let mut curr_score = self.linked_list.len();
         let mut i: usize = 0;
         let mut curr = self.start;
@@ -203,7 +204,7 @@ impl Decisions {
     #[maintains((mut self).invariant(f.num_vars@))]
     pub fn increment_and_move(&mut self, f: &Formula, v: Vec<usize>) {
         let mut counts_with_index: Vec<(usize, usize)> = vec![(0, 0); v.len()];
-        let old_self: Ghost<&mut Decisions> = ghost! { self };
+        let old_self: Snapshot<&mut Decisions> = snapshot! { self };
         let mut i: usize = 0;
         #[invariant(old_self.inner() == self)]
         #[invariant(v@.len() == counts_with_index@.len())]