Update Replay + cargo fmt.

sarsko · Jul 27, 2022 · 0841dbe · 0841dbe
1 parent 8af2d2f
commit 0841dbe
Show file tree

Hide file tree

Showing 7 changed files with 2,097 additions and 2,049 deletions.
diff --git a/.github/workflows/replay.yml b/.github/workflows/replay.yml
@@ -52,5 +52,5 @@ jobs:
     - name: Replay
       run: |
         eval $(opam env)
-        WHY3CONFIG= why3 replay -Lprelude --obsolete-only mlcfgs/CreuSAT
+        WHY3CONFIG= why3 replay -Lprelude --merging-only mlcfgs/CreuSAT
 
diff --git a/CreuSAT/src/decision.rs b/CreuSAT/src/decision.rs
@@ -134,7 +134,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: Ghost<&mut Decisions> = ghost! { self };
         let mut curr_score = self.linked_list.len();
         let mut i: usize = 0;
         let mut curr = self.start;

diff --git a/CreuSAT/src/formula.rs b/CreuSAT/src/formula.rs
@@ -156,7 +156,7 @@ impl Formula {
     #[ensures((@(^self).clauses)[@result] == clause)]
     #[ensures((@self.clauses).len() + 1 == (@(^self).clauses).len())]
     pub fn add_unwatched_clause(&mut self, clause: Clause, watches: &mut Watches, _t: &Trail) -> usize {
-        let old_self: Ghost<&mut Formula>= ghost! { self };
+        let old_self: Ghost<&mut Formula> = ghost! { self };
         let cref = self.clauses.len();
         self.clauses.push(clause);
         proof_assert!(old_self.equisat_compatible(*self));

diff --git a/CreuSAT/src/trail.rs b/CreuSAT/src/trail.rs
@@ -172,7 +172,7 @@ impl Trail {
         #[invariant(inv, self.invariant_no_decision(*f))]
         #[invariant(proph, ^old_t.inner() == ^self)]
         while self.decisions.len() > 0 && self.decisions[self.decisions.len() - 1] > self.trail.len() {
-            let old_t3: Ghost<& mut Trail> = ghost! { self };
+            let old_t3: Ghost<&mut Trail> = ghost! { self };
             proof_assert!(sorted(@self.decisions));
             proof_assert!((@self.decisions).len() > 0);
             proof_assert!(lemma_pop_maintains_sorted(@self.decisions); true);

diff --git a/CreuSAT/src/unit_prop.rs b/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::*, util, watches::*, clause::*};
+use crate::{clause::*, formula::*, lit::*, trail::*, util, watches::*};
 
 use crate::logic::{
     logic::*,

diff --git a/mlcfgs/CreuSAT/why3session.xml b/mlcfgs/CreuSAT/why3session.xml
diff --git a/mlcfgs/CreuSAT/why3shapes.gz b/mlcfgs/CreuSAT/why3shapes.gz