Merge pull request #24 from sarsko/Search-idx-clause-CreuSAT2

CreuSAT/Cargo.toml

@@ -25,10 +25,8 @@ opt-level = 3
 [dependencies]
 clap = "2.33.3"
 rand = "*"
-#creusot-contracts = { git = "https://github.com/sarsko/creusot", version = "^0" }
 creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0" }
 #creusot-contracts = { git = "https://github.com/xldenis/creusot", rev="f9e56a5" , version = "^0" }
-#creusot-contracts = { path = "../../../creusot/creusot-contracts", version = "^0" }
 #creusot = { path = "../../../creusot/", version = "^0" }
 
 

CreuSAT/src/clause.rs

@@ -10,14 +10,16 @@ use crate::logic::{logic_clause::*, logic_formula::*};
 
 pub struct Clause {
     pub deleted: bool,
+    pub lbd: u32,
+    pub search: usize,
     pub rest: Vec<Lit>,
 }
 
 impl Clone for Clause {
     #[trusted] // TODO
     #[ensures(result == *self)]
     fn clone(&self) -> Self {
-        Clause { deleted: self.deleted, rest: self.rest.clone() }
+        Clause { deleted: self.deleted, lbd: self.lbd, search: self.search, rest: self.rest.clone() }
     }
 }
 
@@ -73,7 +75,7 @@ impl Clause {
     #[inline]
     #[trusted]
     pub fn clause_from_vec(vec: &[Lit]) -> Clause {
-        Clause { deleted: false, rest: vec.to_owned() }
+        Clause { deleted: false, lbd: 0, search: 2, rest: vec.to_owned() }
     }
 
     // This does better without splitting

CreuSAT/src/conflict_analysis.rs

@@ -236,12 +236,14 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
         proof_assert!(clause.same_idx_same_polarity_except(*ante, @idx));
         resolve(f, &mut clause, ante, idx, c_idx, &trail, &mut seen, &mut path_c, &mut to_bump);
     }
+    //let clause = clause;
     d.increment_and_move(f, to_bump);
     if clause.len() == 0 {
         Conflict::Ground
     } else if clause.len() == 1 {
         Conflict::Unit(clause)
     } else {
+        //clause.search = 2; // Setting this breaks equisat extension
         if path_c > break_cond {
             return Conflict::Restart(clause);
         }

CreuSAT/src/formula.rs

@@ -78,8 +78,9 @@ impl Formula {
     #[maintains((mut watches).invariant(mut self))]
     #[requires((@clause).len() >= 2)]
     #[requires(@self.num_vars < @usize::MAX/2)]
-    #[requires(vars_in_range_inner(@clause, @self.num_vars))]
-    #[requires(no_duplicate_indexes_inner(@clause))]
+    //#[requires(vars_in_range_inner(@clause, @self.num_vars))]
+    //#[requires(no_duplicate_indexes_inner(@clause))]
+    #[requires(clause.invariant(@self.num_vars))]
     #[requires(equisat_extension_inner(clause, @self))]
     #[ensures(@self.num_vars == @(^self).num_vars)]
     #[ensures(self.equisat(^self))]
@@ -111,8 +112,9 @@ impl Formula {
     #[maintains((mut watches).invariant(mut self))]
     #[requires((@clause).len() >= 2)]
     #[requires(@self.num_vars < @usize::MAX/2)]
-    #[requires(vars_in_range_inner(@clause, @self.num_vars))]
-    #[requires(no_duplicate_indexes_inner(@clause))]
+    //#[requires(vars_in_range_inner(@clause, @self.num_vars))]
+    //#[requires(no_duplicate_indexes_inner(@clause))]
+    #[requires(clause.invariant(@self.num_vars))]
     #[requires(equisat_extension_inner(clause, @self))]
     #[ensures(@self.num_vars == @(^self).num_vars)]
     #[ensures(self.equisat(^self))]

CreuSAT/src/logic/logic_clause.rs

@@ -57,6 +57,7 @@ impl Clause {
         pearlite! {
             exists<i: Int> 0 <= i && i < (@self).len() && (@self)[i].sat_inner(a)
             && forall<j: Int> 0 <= j && j < (@self).len() && j != i ==> (@self)[j].unsat_inner(a)
+
         }
     }
 
@@ -183,12 +184,28 @@ impl Clause {
         pearlite! { no_duplicate_indexes_inner(@self) }
     }
 
+    #[predicate]
+    pub fn search_idx_in_range(self) -> bool {
+        pearlite! {
+            2 <= @self.search && @self.search <= (@self).len()
+        }
+    }
+
     #[predicate]
     pub fn invariant(self, n: Int) -> bool {
-        pearlite! { invariant_internal(@self, n) }
+        pearlite! {
+            invariant_internal(@self, n)
+        }
+    }
+
+    // TODO: remove
+    #[predicate]
+    pub fn invariant_unary_ok(self, n: Int) -> bool {
+        // Should remove the possibility of empty clauses
+        pearlite! { self.vars_in_range(n) && self.no_duplicate_indexes() && self.search_idx_in_range() }
     }
 
-    // Neded in the equals lemma
+    // TODO: Revisit and see if it is needed
     #[predicate]
     pub fn equals(self, o: Clause) -> bool {
         pearlite! {

CreuSAT/src/logic/logic_watches.rs

@@ -16,6 +16,7 @@ pub fn watches_invariant_internal(w: Seq<Vec<Watcher>>, n: Int, f: Formula) -> b
                    ((@(@w[i])[j].cref < (@f.clauses).len()
                 && (@(@f.clauses)[@(@w[i])[j].cref]).len() > 1)
                 && (@w[i])[j].blocker.index_logic() < @f.num_vars)
+                //&& (@f.clauses)[@(@w[i])[j].cref].search_idx_in_range()
     }
 }
 

CreuSAT/src/trail.rs

@@ -82,7 +82,7 @@ impl Trail {
             None => {
                 // Could add a req on trail len and prove that this doesn't happen, but
                 // not sure if it really is needed.
-                proof_assert!(long_are_post_unit_inner(@self.trail, *f, @self.assignments));
+                proof_assert!(long_are_post_unit_inner(@self.trail, *f, @self.assignments)&& true);
             }
         }
         proof_assert!(self.assignments.invariant(*f));

CreuSAT/src/unit_prop.rs

@@ -4,7 +4,7 @@ use creusot_contracts::logic::Ghost;
 use creusot_contracts::std::*;
 use creusot_contracts::*;
 
-use crate::{formula::*, lit::*, trail::*, watches::*};
+use crate::{formula::*, lit::*, trail::*, util, watches::*};
 
 use crate::logic::{
     logic::*,
@@ -18,11 +18,9 @@ use crate::logic::{
 #[maintains((mut watches).invariant(mut f))]
 #[requires(@f.num_vars < @usize::MAX/2)]
 #[requires(lit.index_logic() < @f.num_vars)]
-//#[requires((@trail.trail).len() > 0)]
 #[requires(!(@(@f.clauses)[@cref])[0].sat_inner(@trail.assignments))]
 #[requires(@cref < (@f.clauses).len())]
 #[requires(2 <= @k && @k < (@(@f.clauses)[@cref]).len())]
-#[requires((@(@f.clauses)[@cref]).len() > 2)]
 #[requires((@(@watches.watches)[lit.to_watchidx_logic()]).len() > @j)]
 #[ensures(@f.num_vars == @(^f).num_vars)]
 #[ensures(f.equisat(^f))]
@@ -86,11 +84,10 @@ fn swap(f: &mut Formula, trail: &Trail, watches: &Watches, cref: usize, j: usize
 #[maintains((mut f).invariant())]
 #[maintains((trail).invariant(mut f))]
 #[maintains((mut watches).invariant(mut f))]
+#[requires(@f.num_vars < @usize::MAX/2)]
 #[requires(lit.to_watchidx_logic() < (@watches.watches).len())]
 #[requires((@(@watches.watches)[lit.to_watchidx_logic()]).len() > @j)]
-#[requires(@f.num_vars < @usize::MAX/2)]
 #[requires(lit.index_logic() < @f.num_vars)]
-#[requires(watches.invariant(*f))]
 #[requires(@cref < (@f.clauses).len())]
 #[requires((@(@f.clauses)[@cref]).len() >= 2)]
 #[requires(!(@(@f.clauses)[@cref])[0].sat_inner(@trail.assignments))]
@@ -104,20 +101,44 @@ fn exists_new_watchable_lit(
 ) -> bool {
     let old_w = ghost! { watches };
     let old_f = ghost! { f };
-    let mut k: usize = 2;
     let clause_len: usize = f.clauses[cref].rest.len();
-    #[invariant(k_bound, 2 <= @k && @k <= @clause_len)]
-    #[invariant(f_unchanged, f == old_f.inner())]
-    #[invariant(w_unchanged, *watches == *old_w.inner())]
-    #[invariant(proph_f, ^f == ^old_f.inner())]
-    #[invariant(proph_w, ^watches == ^old_w.inner())]
-    #[invariant(uns, forall<m: Int> 2 <= m && m < @k ==> ((@(@f.clauses)[@cref])[m]).unsat(trail.assignments))]
+    let init_search = util::max(util::min(f.clauses[cref].search, clause_len), 2); // TODO: Lame check
+    let mut search = init_search;
+    #[invariant(search, @search >= 2)]
+    #[invariant(f_unchanged, f == *old_f)]
+    #[invariant(w_unchanged, watches == *old_w)]
+    #[invariant(uns, forall<m: Int> @init_search <= m && m < @search ==> (@(@f.clauses)[@cref])[m].unsat(trail.assignments))]
+    // Here to help the trail invariant
+    #[invariant(first_not_sat, !(@(@f.clauses)[@cref])[0].sat_inner(@trail.assignments))]
+    while search < clause_len {
+        if check_and_move_watch(f, trail, watches, cref, j, search, lit) {
+            let old_f2 = ghost! { f };
+            f.clauses[cref].search = search;
+            proof_assert!(forall<j: Int> 0 <= j && j < (@f.clauses).len() ==> @(@f.clauses)[j] == @(@(old_f2.inner()).clauses)[j]);
+            proof_assert!(old_f2.inner().equisat(*f));
+            proof_assert!(crefs_in_range(@trail.trail, *f)); // I am here to help the trail invariant pass
+            return true;
+        }
+        search += 1;
+    }
+    search = 2;
+    #[invariant(search_bound, 2 <= @search && @search <= @clause_len)]
+    #[invariant(f_unchanged, f == *old_f)]
+    #[invariant(w_unchanged, watches == *old_w)]
+    #[invariant(uns, forall<m: Int> @init_search <= m && m < @clause_len ==> ((@(@f.clauses)[@cref])[m]).unsat(trail.assignments))]
+    #[invariant(uns2, forall<m: Int> 2 <= m && m < @search ==> ((@(@f.clauses)[@cref])[m]).unsat(trail.assignments))]
+    // Here to help the trail invariant
     #[invariant(first_not_sat, !(@(@f.clauses)[@cref])[0].sat_inner(@trail.assignments))]
-    while k < clause_len {
-        if check_and_move_watch(f, trail, watches, cref, j, k, lit) {
+    while search < init_search {
+        if check_and_move_watch(f, trail, watches, cref, j, search, lit) {
+            let old_f2 = ghost! { f };
+            f.clauses[cref].search = search;
+            proof_assert!(forall<j: Int> 0 <= j && j < (@f.clauses).len() ==> @(@f.clauses)[j] == @(@(old_f2.inner()).clauses)[j]);
+            proof_assert!(old_f2.inner().equisat(*f));
+            proof_assert!(crefs_in_range(@trail.trail, *f)); // I am here to help the trail invariant pass
             return true;
         }
-        k += 1;
+        search += 1;
     }
     false
 }

CreuSAT/src/util.rs

@@ -83,3 +83,42 @@ pub fn sort(v: &mut Vec<(usize, usize)>) {
         i += 1;
     }
 }
+
+#[logic]
+fn min_log(a: Int, b: Int) -> Int {
+    if a <= b {
+        a
+    } else {
+        b
+    }
+}
+
+#[ensures(@result == min_log(@a, @b))]
+#[ensures(@a <= @b ==> @result == @a)]
+#[ensures(@b < @a ==> @result == @b)]
+#[ensures(@result <= @b && @result <= @a)]
+pub fn min(a: usize, b: usize) -> usize {
+    if a <= b {
+        a
+    } else {
+        b
+    }
+}
+
+#[logic]
+fn max_log(a: Int, b: Int) -> Int {
+    if a >= b {
+        a
+    } else {
+        b
+    }
+}
+
+#[ensures(@result == max_log(@a, @b))]
+pub fn max(a: usize, b: usize) -> usize {
+    if a >= b {
+        a
+    } else {
+        b
+    }
+}