Bump Clap version. Ghost to Snapshot in Scratch and NewDB

sarsko · Apr 10, 2024 · a8b3b92 · a8b3b92
1 parent 4d653b9
commit a8b3b92
Show file tree

Hide file tree

Showing 8 changed files with 219 additions and 60 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/NewDB/src/clause_allocator.rs b/NewDB/src/clause_allocator.rs
@@ -131,7 +131,7 @@ impl ClauseAllocator {
         let cref = self.buffer.len() as CRef;
         self.buffer.push(Lit::raw(lits.len() as u32));
 
-        let old_self: Ghost<&mut ClauseAllocator> = ghost!(self);
+        let old_self: Snapshot<&mut ClauseAllocator> = snapshot!(self);
 
         #[invariant(self.num_vars == old_self.num_vars)] // TODO: Don't like this
         #[invariant(^*old_self == ^self)]

diff --git a/NewDB/src/clause_manager.rs b/NewDB/src/clause_manager.rs
@@ -68,7 +68,7 @@ impl ClauseManager {
     //#[requires(self@.len() + (@lits).len() + @HEADER_LEN <= @u32::MAX)] // TODO: May have to move this to a runtime check
     #[requires(clause_invariant_seq(lits@, self.clause_allocator.num_vars@))]
     pub(crate) fn learn_clause(&mut self, lits: &[Lit]) -> CRef {
-        let old_self: Ghost<&mut ClauseManager> = ghost!(self);
+        let old_self: Snapshot<&mut ClauseManager> = snapshot!(self);
         proof_assert!(self.learnt_core.are_implied_by(self.original_clauses, self.clause_allocator));
         let cref = self.clause_allocator.add_clause(lits);
         proof_assert!(^*old_self == ^self);

diff --git a/Scratch/Cargo.toml b/Scratch/Cargo.toml
@@ -5,7 +5,7 @@ authors = ["Sarek Høverstad Skotåm <sarek.skotam@gmail.com>"]
 edition = "2021"
 
 [dependencies]
-clap = "2.33.3"
+clap = "4.5.4"
 creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "1357cc97" }
 
 # This is just copied verbatim from CreuSAT.

diff --git a/Scratch/src/clause.rs b/Scratch/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::*};
 

diff --git a/Scratch/src/scratch.rs b/Scratch/src/scratch.rs
@@ -44,7 +44,7 @@ pub fn lemma_clause_permuted_maintains_unsat(c: Clause, a: Assignments) {}
 #[ensures(f.clauses@.len() == (^f).clauses@.len())]
 #[ensures(f.equisat(^f))] // This one is hard (both ways equisat)
 fn swap(f: &mut Formula, cref: usize, j: usize, k: usize, assignments: Assignments) {
-    let old_f: Ghost<&mut Formula> = ghost! { f };
+    let old_f: Snapshot<&mut Formula> = snapshot! { f };
 
     f.clauses[cref].lits.swap(j, k);