Merge pull request #25 from sarsko/remove-inner

CreuSAT/Cargo.toml

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

CreuSAT/src/clause.rs

@@ -142,10 +142,10 @@ impl Clause {
         let old_c = ghost! { self };
         self.rest.swap(j, k);
         proof_assert!(^old_c.inner() == ^self);
-        proof_assert!((*old_c.inner()).equisat_extension(*_f));
+        proof_assert!(old_c.equisat_extension(*_f));
         proof_assert!(self.invariant(@_f.num_vars));
-        proof_assert!((@self).exchange(@old_c.inner(), @j, @k));
-        proof_assert!((@old_c.inner()).permut(@self, 0, (@self).len()));
+        proof_assert!((@self).exchange(@old_c, @j, @k));
+        proof_assert!((@old_c).permut(@self, 0, (@self).len()));
         proof_assert!(self.equisat(*old_c.inner()));
         proof_assert!(self.equisat2(*old_c.inner(), *_f));
         proof_assert!(^old_c.inner() == ^self);

CreuSAT/src/conflict_analysis.rs

@@ -71,20 +71,20 @@ fn resolve(
     proof_assert!(^seen == ^old_seen.inner());
     proof_assert!(c.clause_is_seen(*seen));
     let old_c2 = ghost!(c);
-    proof_assert!(!(@old_c.inner())[@c_idx].lit_in(*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.inner()).len()
-        && j != @c_idx ==> (@old_c.inner())[j].lit_in(*c));
+    proof_assert!(forall<j: Int> 0 <= j && j < (@old_c).len()
+        && j != @c_idx ==> (@old_c)[j].lit_in(*c));
 
     // Add all the literals from the other clause
     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(not_in, !(@old_c.inner())[@c_idx].lit_in(*c) && !(@o)[0].lit_in(*c))]
+    #[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_in2, forall<j: Int> 0 <= j && j < (@old_c.inner()).len()
-        && j != @c_idx ==> (@old_c.inner())[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() ==>
                     ((@c)[j].lit_in(*old_c.inner()) ||  (@c)[j].lit_in(*o))))]
     #[invariant(path_c_less, @path_c <= (@c).len())]
@@ -101,19 +101,19 @@ fn resolve(
         if idx_in(&c.rest, o.rest[i].index(), &seen) {
             //if seen[o.rest[i].index()] {
             proof_assert!((@o)[@i].lit_in(*c));
-            proof_assert!(@c == @old_c3.inner());
+            proof_assert!(@c == @old_c3);
         } else {
             seen[o.rest[i].index()] = true;
             to_bump.push(o.rest[i].index());
             c.rest.push(o.rest[i]);
             if trail.lit_to_level[o.rest[i].index()] >= trail.decision_level() {
                 *path_c += 1;
             }
-            proof_assert!(@c == (@old_c3.inner()).push((@o)[@i]));
+            proof_assert!(@c == (@old_c3).push((@o)[@i]));
             proof_assert!((@o)[@i].lit_in(*c));
         }
-        proof_assert!(forall<j: Int> 0 <= j && j < (@old_c3.inner()).len() ==>
-            ((@old_c3.inner())[j] == (@c)[j]));
+        proof_assert!(forall<j: Int> 0 <= j && j < (@old_c3).len() ==>
+            ((@old_c3)[j] == (@c)[j]));
         i += 1;
     }
     proof_assert!(c.resolvent_of(*old_c.inner(), *o, 0, @c_idx));

CreuSAT/src/decision.rs

@@ -140,8 +140,8 @@ impl Decisions {
         #[invariant(curr_ok, curr == usize::MAX || @curr < (@self.linked_list).len())]
         #[invariant(proph, ^old_self.inner() == ^self)]
         #[invariant(unch, forall<j: Int> 0 <= j && j < (@self.linked_list).len() ==>
-            ((@self.linked_list)[j].next == (@(old_self.inner()).linked_list)[j].next
-            && (@self.linked_list)[j].prev == (@(old_self.inner()).linked_list)[j].prev)
+            ((@self.linked_list)[j].next == (@old_self.linked_list)[j].next
+            && (@self.linked_list)[j].prev == (@old_self.linked_list)[j].prev)
         )]
         #[invariant(inv, self.invariant(@_f.num_vars))]
         while curr != INVALID {

CreuSAT/src/formula.rs

@@ -100,8 +100,8 @@ impl Formula {
         watches.add_watcher(first_lit, cref, self, second_lit);
         watches.add_watcher(second_lit, cref, self, first_lit);
         proof_assert!(^old_self.inner() == ^self);
-        proof_assert!((old_self.inner()).equisat_compatible(*self));
-        proof_assert!((old_self.inner()).equisat(*self));
+        proof_assert!(old_self.equisat_compatible(*self));
+        proof_assert!(old_self.equisat(*self));
         proof_assert!(trail_invariant(@_t.trail, *self)); // This one needs some inlining/splits
         cref
     }
@@ -125,7 +125,7 @@ impl Formula {
         let old_self = ghost! { self };
         let cref = self.clauses.len();
         self.clauses.push(clause);
-        proof_assert!((old_self.inner()).equisat_compatible(*self));
+        proof_assert!(old_self.equisat_compatible(*self));
         proof_assert!(trail_invariant(@_t.trail, *self)); // This one needs some inlining/splits
         cref
     }
@@ -149,7 +149,7 @@ impl Formula {
         let old_self = ghost! { self };
         let cref = self.clauses.len();
         self.clauses.push(clause);
-        proof_assert!((old_self.inner()).equisat_compatible(*self));
+        proof_assert!(old_self.equisat_compatible(*self));
         // proof_assert!(trail_invariant(@_t.trail, *self)); // This one needs some inlining/splits
         cref
     }
@@ -185,8 +185,8 @@ impl Formula {
         watches.unwatch(self, t, cref, self.clauses[cref].rest[1]);
         self.clauses[cref].deleted = true;
         proof_assert!(forall<i: Int> 0 <= i && i < (@(@self.clauses)[@cref]).len() ==>
-            (@(@self.clauses)[@cref])[i] == (@(@(old_f.inner()).clauses)[@cref])[i]);
-        proof_assert!((old_f.inner()).equisat(*self)); // This assertion helps with the invariant, which otherwise takes a long time.
+            (@(@self.clauses)[@cref])[i] == (@(@old_f.clauses)[@cref])[i]);
+        proof_assert!(old_f.equisat(*self)); // This assertion helps with the invariant, which otherwise takes a long time.
         proof_assert!(^self == ^old_f.inner());
     }
 
@@ -209,7 +209,7 @@ impl Formula {
         #[invariant(f_inv, self.invariant())]
         #[invariant(proph_w, ^watches == ^old_w.inner())]
         #[invariant(proph_f, ^self == ^old_f.inner())]
-        #[invariant(num_vars_unch, @self.num_vars == @(old_f.inner()).num_vars)]
+        #[invariant(num_vars_unch, @self.num_vars == @old_f.num_vars)]
         #[invariant(equi, self.equisat(*old_f.inner()))]
         while i < self.clauses.len() {
             if !self.clauses[i].deleted {
@@ -264,7 +264,7 @@ impl Formula {
         #[invariant(f_inv, self.invariant())]
         #[invariant(proph_w, ^watches == ^old_w.inner())]
         #[invariant(proph_f, ^self == ^old_f.inner())]
-        #[invariant(num_vars_unch, @self.num_vars == @(old_f.inner()).num_vars)]
+        #[invariant(num_vars_unch, @self.num_vars == @old_f.num_vars)]
         #[invariant(equi, self.equisat(*old_f.inner()))]
         while i < self.clauses.len() {
             if !self.clauses[i].deleted {

CreuSAT/src/solver.rs

@@ -237,7 +237,7 @@ impl Solver {
         #[invariant(maintains_w, w.invariant(*f))]
         #[invariant(maintains_d, d.invariant(@f.num_vars))]
         #[invariant(equi, old_f.inner().equisat(*f))]
-        #[invariant(num_vars, @f.num_vars == @old_f.inner().num_vars)]
+        #[invariant(num_vars, @f.num_vars == @old_f.num_vars)]
         #[invariant(prophf, ^f == ^old_f.inner())]
         #[invariant(propht, ^t == ^old_t.inner())]
         #[invariant(prophw, ^w == ^old_w.inner())]
@@ -327,7 +327,7 @@ impl Solver {
     ) -> SatResult {
         let old_f = ghost! { formula };
         #[invariant(equi, old_f.inner().equisat(*formula))]
-        #[invariant(num_vars, @formula.num_vars == @old_f.inner().num_vars)]
+        #[invariant(num_vars, @formula.num_vars == @old_f.num_vars)]
         #[invariant(maintains_f, formula.invariant())]
         #[invariant(maintains_t, trail.invariant(*formula))]
         #[invariant(maintains_w, watches.invariant(*formula))]

CreuSAT/src/trail.rs

@@ -71,7 +71,7 @@ impl Trail {
                 // TODO: Wrap in abstraction
                 self.assignments.0[step.lit.index()] += 2;
 
-                proof_assert!(@self.trail == pop(@(old_t.inner()).trail));
+                proof_assert!(@self.trail == pop(@old_t.trail));
                 proof_assert!(^old_t.inner() == ^self);
 
                 self.lit_to_level[step.lit.index()] = usize::MAX;
@@ -126,12 +126,12 @@ impl Trail {
         let mut i: usize = 0;
         let mut curr = d.search;
         let mut timestamp = if curr != usize::MAX { d.linked_list[curr].ts } else { 0 }; // revisit this later
-        #[invariant(i_less2, @i <= (@(old_t.inner()).trail).len())]
+        #[invariant(i_less2, @i <= (@old_t.trail).len())]
         #[invariant(i_less, i <= how_many)]
         #[invariant(post_unit, long_are_post_unit_inner(@self.trail, *f, @self.assignments))]
         #[invariant(inv, self.invariant_no_decision(*f))]
         #[invariant(d_inv, d.invariant(@f.num_vars))]
-        //#[invariant(len_is, (@self.trail).len() == (@(old_t.inner()).trail).len() - @i)] // we don't care anymore
+        //#[invariant(len_is, (@self.trail).len() == (@old_t.trail).len() - @i)] // we don't care anymore
         #[invariant(proph, ^old_t.inner() == ^self)]
         #[invariant(proph_d, ^old_d.inner() == ^d)]
         #[invariant(curr_less, @curr < (@d.linked_list).len() || @curr == @usize::MAX)]
@@ -158,7 +158,7 @@ impl Trail {
             proof_assert!(lemma_pop_maintains_sorted(@self.decisions); true);
             match self.decisions.pop() {
                 Some(_) => {
-                    proof_assert!(@self.decisions == pop(@(old_t2.inner()).decisions));
+                    proof_assert!(@self.decisions == pop(@old_t2.decisions));
                     proof_assert!((^old_t2.inner()) == ^self);
                 }
                 None => {
@@ -179,14 +179,14 @@ impl Trail {
             //proof_assert!((@self.decisions) == (@(@old_trail).decisions));
             match self.decisions.pop() {
                 Some(_) => {
-                    proof_assert!((@self.decisions) == pop(@(old_t3.inner()).decisions));
+                    proof_assert!((@self.decisions) == pop(@old_t3.decisions));
                     proof_assert!((^old_t3.inner()) == ^self);
                 }
                 None => {
                     unreachable!();
                 }
             }
-            proof_assert!(lemma_pop_maintains_sorted(@(old_t3.inner()).decisions); true);
+            proof_assert!(lemma_pop_maintains_sorted(@old_t3.decisions); true);
             proof_assert!(sorted(@self.decisions));
         }
         proof_assert!(

CreuSAT/src/unit_prop.rs

@@ -68,7 +68,7 @@ fn swap(f: &mut Formula, trail: &Trail, watches: &Watches, cref: usize, j: usize
     proof_assert!(no_duplicate_indexes_inner(@(@f.clauses)[@cref]));
     proof_assert!(long_are_post_unit_inner(@trail.trail, *f, @trail.assignments) && true);
     f.clauses[cref].rest.swap(j, k);
-    proof_assert!((@(@f.clauses)[@cref]).exchange(@(@(old_f.inner()).clauses)[@cref], @j, @k));
+    proof_assert!((@(@f.clauses)[@cref]).exchange(@(@old_f.clauses)[@cref], @j, @k));
     proof_assert!(forall<i: Int> 0 <= i && i < (@trail.trail).len() ==>
     match (@trail.trail)[i].reason {
     Reason::Long(cref2) => { @cref != @cref2 },
@@ -213,7 +213,7 @@ fn propagate_lit_with_regard_to_clause(
         let old_c = ghost! { f.clauses[cref] };
         proof_assert!((@(@f.clauses)[@cref])[1].unset(trail.assignments));
         swap(f, trail, watches, cref, 0, 1);
-        proof_assert!((@(@f.clauses)[@cref]).exchange(@old_c.inner(), 0, 1));
+        proof_assert!((@(@f.clauses)[@cref]).exchange(@old_c, 0, 1));
         proof_assert!((@(@f.clauses)[@cref])[0].unset(trail.assignments));
         trail.enq_assignment(step, f);
         proof_assert!(((@f.clauses)[@cref]).post_unit(trail.assignments));
@@ -245,12 +245,12 @@ fn propagate_literal(f: &mut Formula, trail: &mut Trail, watches: &mut Watches,
     let old_f = ghost! { f };
     let old_w = ghost! { watches };
     #[invariant(trail_inv, trail.invariant(*f))]
-    #[invariant(watch_len, (@watches.watches).len() == (@(old_w.inner()).watches).len())]
+    #[invariant(watch_len, (@watches.watches).len() == (@old_w.watches).len())]
     #[invariant(watch_inv, watches.invariant(*f))]
-    #[invariant(f_equi, (old_f.inner()).equisat(*f))]
+    #[invariant(f_equi, old_f.equisat(*f))]
     #[invariant(f_inv, f.invariant())]
-    #[invariant(dec_unch, (@trail.decisions) == (@(old_trail.inner()).decisions))]
-    #[invariant(nvars_unch, @f.num_vars == @(old_f.inner()).num_vars)]
+    #[invariant(dec_unch, (@trail.decisions) == (@old_trail.decisions))]
+    #[invariant(nvars_unch, @f.num_vars == @old_f.num_vars)]
     #[invariant(proph_t, ^trail == ^old_trail.inner())]
     #[invariant(proph_f, ^f == ^old_f.inner())]
     #[invariant(proph_w, ^watches == ^old_w.inner())]
@@ -292,10 +292,10 @@ pub fn unit_propagate(f: &mut Formula, trail: &mut Trail, watches: &mut Watches)
     let old_w = ghost! { watches };
     #[invariant(f_inv, f.invariant())]
     #[invariant(trail_inv, trail.invariant(*f))]
-    #[invariant(watch_len, (@watches.watches).len() == (@(old_w.inner()).watches).len())]
+    #[invariant(watch_len, (@watches.watches).len() == (@old_w.watches).len())]
     #[invariant(watch_inv, watches.invariant(*f))]
-    #[invariant(f_equi, (old_f.inner()).equisat(*f))]
-    #[invariant(nvars_unch, @f.num_vars == @(old_f.inner()).num_vars)]
+    #[invariant(f_equi, old_f.equisat(*f))]
+    #[invariant(nvars_unch, @f.num_vars == @old_f.num_vars)]
     #[invariant(proph_t, ^trail == ^old_trail.inner())]
     #[invariant(proph_f, ^f == ^old_f.inner())]
     #[invariant(proph_w, ^watches == ^old_w.inner())]