From a8b3b927071f795596d12b0d77053280e8cc54e8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Sarek=20H=C3=B8verstad=20Skot=C3=A5m?= Date: Wed, 10 Apr 2024 23:56:48 +0200 Subject: [PATCH] Bump Clap version. Ghost to Snapshot in Scratch and NewDB --- Cargo.lock | 177 ++++++++++++++++++++++++++++++++-- NewDB/src/clause_allocator.rs | 2 +- NewDB/src/clause_manager.rs | 2 +- Scratch/Cargo.toml | 2 +- Scratch/src/clause.rs | 2 +- Scratch/src/scratch.rs | 2 +- mlcfgs/NewDB.mlcfg | 76 +++++++-------- mlcfgs/Scratch.mlcfg | 16 +-- 8 files changed, 219 insertions(+), 60 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index fcad812a..95604afd 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -6,7 +6,7 @@ version = 3 name = "CreuSAT" version = "0.1.0" dependencies = [ - "clap", + "clap 2.34.0", "creusot-contracts", "rand", "termcolor", @@ -32,7 +32,7 @@ dependencies = [ name = "JigSAT" version = "0.1.0" dependencies = [ - "clap", + "clap 2.34.0", "log", "rand", "termcolor", @@ -49,7 +49,7 @@ dependencies = [ name = "Robinson" version = "0.1.0" dependencies = [ - "clap", + "clap 2.34.0", "creusot-contracts", ] @@ -57,7 +57,7 @@ dependencies = [ name = "Scratch" version = "0.1.0" dependencies = [ - "clap", + "clap 4.5.4", "creusot-contracts", ] @@ -70,6 +70,54 @@ dependencies = [ "winapi", ] +[[package]] +name = "anstream" +version = "0.6.13" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d96bd03f33fe50a863e394ee9718a706f988b9079b20c3784fb726e7678b62fb" +dependencies = [ + "anstyle", + "anstyle-parse", + "anstyle-query", + "anstyle-wincon", + "colorchoice", + "utf8parse", +] + +[[package]] +name = "anstyle" +version = "1.0.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8901269c6307e8d93993578286ac0edf7f195079ffff5ebdeea6a59ffb7e36bc" + +[[package]] +name = "anstyle-parse" +version = "0.2.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c75ac65da39e5fe5ab759307499ddad880d724eed2f6ce5b5e8a26f4f387928c" +dependencies = [ + "utf8parse", +] + +[[package]] +name = "anstyle-query" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e28923312444cdd728e4738b3f9c9cac739500909bb3d3c94b43551b16517648" +dependencies = [ + "windows-sys", +] + +[[package]] +name = "anstyle-wincon" +version = "3.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1cd54b81ec8d6180e24654d0b371ad22fc3dd083b6ff8ba325b72e00c87660a7" +dependencies = [ + "anstyle", + "windows-sys", +] + [[package]] name = "atty" version = "0.2.14" @@ -108,12 +156,45 @@ dependencies = [ "ansi_term", "atty", "bitflags", - "strsim", + "strsim 0.8.0", "textwrap", "unicode-width", "vec_map", ] +[[package]] +name = "clap" +version = "4.5.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "90bc066a67923782aa8515dbaea16946c5bcc5addbd668bb80af688e53e548a0" +dependencies = [ + "clap_builder", +] + +[[package]] +name = "clap_builder" +version = "4.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ae129e2e766ae0ec03484e609954119f123cc1fe650337e155d03b022f24f7b4" +dependencies = [ + "anstream", + "anstyle", + "clap_lex", + "strsim 0.11.1", +] + +[[package]] +name = "clap_lex" +version = "0.7.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "98cc8fbded0c607b7ba9dd60cd98df59af97e84d24e49c8557331cfc26d301ce" + +[[package]] +name = "colorchoice" +version = "1.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "acbf1af155f9b9ef647e42cdc158db4b64a1b61f743629225fde6f3e0be2a7c7" + [[package]] name = "creusot-contracts" version = "0.2.0" @@ -146,9 +227,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.13" +version = "0.2.14" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a06fddc2749e0528d2813f95e050e87e52c8cbbae56223b9babf73b3e53b0cc6" +checksum = "94b22e06ecb0110981051723910cbf0b5f5e09a2062dd7663334ee79a9d1286c" dependencies = [ "cfg-if", "libc", @@ -244,9 +325,9 @@ dependencies = [ [[package]] name = "quote" -version = "1.0.35" +version = "1.0.36" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "291ec9ab5efd934aaf503a6466c5d5251535d108ee747472c3977cc5acc868ef" +checksum = "0fa76aaf39101c457836aec0ce2316dbdc3ab723cdda1c6bd4e6ad4208acaca7" dependencies = [ "proc-macro2", ] @@ -287,6 +368,12 @@ version = "0.8.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8ea5119cdb4c55b55d432abb513a0429384878c15dde60cc77b1c99de1a95a6a" +[[package]] +name = "strsim" +version = "0.11.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" + [[package]] name = "syn" version = "2.0.58" @@ -328,6 +415,12 @@ version = "0.1.11" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e51733f11c9c4f72aa0c160008246859e340b00807569a0da0e7a1079b27ba85" +[[package]] +name = "utf8parse" +version = "0.2.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "711b9620af191e0cdc7468a8d14e709c3dcdb115b36f838e601583af800a370a" + [[package]] name = "uuid" version = "1.8.0" @@ -379,3 +472,69 @@ name = "winapi-x86_64-pc-windows-gnu" version = "0.4.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "712e227841d057c1ee1cd2fb22fa7e5a5461ae8e48fa2ca79ec42cfc1931183f" + +[[package]] +name = "windows-sys" +version = "0.52.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "282be5f36a8ce781fad8c8ae18fa3f9beff57ec1b52cb3de0789201425d9a33d" +dependencies = [ + "windows-targets", +] + +[[package]] +name = "windows-targets" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7dd37b7e5ab9018759f893a1952c9420d060016fc19a472b4bb20d1bdd694d1b" +dependencies = [ + "windows_aarch64_gnullvm", + "windows_aarch64_msvc", + "windows_i686_gnu", + "windows_i686_msvc", + "windows_x86_64_gnu", + "windows_x86_64_gnullvm", + "windows_x86_64_msvc", +] + +[[package]] +name = "windows_aarch64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bcf46cf4c365c6f2d1cc93ce535f2c8b244591df96ceee75d8e83deb70a9cac9" + +[[package]] +name = "windows_aarch64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "da9f259dd3bcf6990b55bffd094c4f7235817ba4ceebde8e6d11cd0c5633b675" + +[[package]] +name = "windows_i686_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b474d8268f99e0995f25b9f095bc7434632601028cf86590aea5c8a5cb7801d3" + +[[package]] +name = "windows_i686_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1515e9a29e5bed743cb4415a9ecf5dfca648ce85ee42e15873c3cd8610ff8e02" + +[[package]] +name = "windows_x86_64_gnu" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5eee091590e89cc02ad514ffe3ead9eb6b660aedca2183455434b93546371a03" + +[[package]] +name = "windows_x86_64_gnullvm" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ca79f2451b49fa9e2af39f0747fe999fcda4f5e241b2898624dca97a1f2177" + +[[package]] +name = "windows_x86_64_msvc" +version = "0.52.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "32b752e52a2da0ddfbdbcc6fceadfeede4c939ed16d13e648833a61dfb611ed8" diff --git a/NewDB/src/clause_allocator.rs b/NewDB/src/clause_allocator.rs index 9b427a57..e2bf2b43 100644 --- 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 index eeeaf7bb..0ce90a3f 100644 --- 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 index 97245617..5398e5f1 100644 --- a/Scratch/Cargo.toml +++ b/Scratch/Cargo.toml @@ -5,7 +5,7 @@ authors = ["Sarek Høverstad Skotåm "] 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 index 6e922749..b99526cc 100644 --- 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 index 7b0b8c1d..4b8b5ffa 100644 --- 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); diff --git a/mlcfgs/NewDB.mlcfg b/mlcfgs/NewDB.mlcfg index 098e7747..76abafb1 100644 --- a/mlcfgs/NewDB.mlcfg +++ b/mlcfgs/NewDB.mlcfg @@ -760,7 +760,7 @@ module NewDb_ClauseAllocator_Impl1_GetClauseFsetInternal_Impl clone NewDb_ClauseAllocator_Impl2_ShallowModel as ShallowModel0 with function ShallowModel0.shallow_model = ShallowModel1.shallow_model, val Max0.mAX' = Max0.mAX' - let rec ghost function get_clause_fset_internal [#"../NewDB/src/clause_allocator.rs" 84 4 84 83] (self : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (cref : int) (idx : int) (upper : int) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) + let rec Snapshot function get_clause_fset_internal [#"../NewDB/src/clause_allocator.rs" 84 4 84 83] (self : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (cref : int) (idx : int) (upper : int) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) requires {[#"../NewDB/src/clause_allocator.rs" 83 15 83 47] idx >= 0 /\ upper <= Seq.length (ShallowModel0.shallow_model self)} variant {[#"../NewDB/src/clause_allocator.rs" 82 14 82 25] upper - idx} @@ -1193,31 +1193,31 @@ module CreusotContracts_Std1_Slice_Impl15_Produces ensures { result = produces self visited tl } end -module CreusotContracts_Ghost_Impl1_ShallowModel_Stub +module CreusotContracts_Snapshot_Impl1_ShallowModel_Stub type t - use prelude.Ghost + use prelude.Snapshot clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with type self = t - function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy + function shallow_model (self : Snapshot.Snapshot_ty t) : ShallowModelTy0.shallowModelTy end -module CreusotContracts_Ghost_Impl1_ShallowModel_Interface +module CreusotContracts_Snapshot_Impl1_ShallowModel_Interface type t - use prelude.Ghost + use prelude.Snapshot clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with type self = t - function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy + function shallow_model (self : Snapshot.Snapshot_ty t) : ShallowModelTy0.shallowModelTy end -module CreusotContracts_Ghost_Impl1_ShallowModel +module CreusotContracts_Snapshot_Impl1_ShallowModel type t - use prelude.Ghost + use prelude.Snapshot clone CreusotContracts_Model_ShallowModel_ShallowModelTy_Type as ShallowModelTy0 with type self = t clone CreusotContracts_Model_Impl1_ShallowModel_Stub as ShallowModel0 with type t = t, type ShallowModelTy0.shallowModelTy = ShallowModelTy0.shallowModelTy - function shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy = - ShallowModel0.shallow_model (Ghost.inner self) - val shallow_model (self : Ghost.ghost_ty t) : ShallowModelTy0.shallowModelTy + function shallow_model (self : Snapshot.Snapshot_ty t) : ShallowModelTy0.shallowModelTy = + ShallowModel0.shallow_model (Snapshot.inner self) + val shallow_model (self : Snapshot.Snapshot_ty t) : ShallowModelTy0.shallowModelTy ensures { result = shallow_model self } end @@ -1612,7 +1612,7 @@ module NewDb_ClauseAllocator_Impl3_AddClause use prelude.Borrow use prelude.Slice use prelude.UIntSize - use prelude.Ghost + use prelude.Snapshot use seq.Seq use prelude.IntSize use Core_Slice_Iter_Iter_Type as Core_Slice_Iter_Iter_Type @@ -1717,7 +1717,7 @@ module NewDb_ClauseAllocator_Impl3_AddClause predicate Produces0.produces = Produces0.produces clone NewDb_Lit_Impl1_VarInRange as VarInRange0 with function IndexLogic0.index_logic = IndexLogic1.index_logic - clone CreusotContracts_Ghost_Impl1_ShallowModel as ShallowModel3 with + clone CreusotContracts_Snapshot_Impl1_ShallowModel as ShallowModel3 with type t = borrowed (NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator), type ShallowModelTy0.shallowModelTy = Seq.seq (NewDb_Lit_Lit_Type.t_lit), function ShallowModel0.shallow_model = ShallowModel9.shallow_model @@ -1778,14 +1778,14 @@ module NewDb_ClauseAllocator_Impl3_AddClause var _21 : uint32; var _22 : usize; var _23 : slice (NewDb_Lit_Lit_Type.t_lit); - var old_self_24 : Ghost.ghost_ty (borrowed (NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator)); + var old_self_24 : Snapshot.Snapshot_ty (borrowed (NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator)); var _26 : (); var _27 : (); var iter_28 : Core_Slice_Iter_Iter_Type.t_iter (NewDb_Lit_Lit_Type.t_lit); var _29 : slice (NewDb_Lit_Lit_Type.t_lit); - var iter_old_30 : Ghost.ghost_ty (Core_Slice_Iter_Iter_Type.t_iter (NewDb_Lit_Lit_Type.t_lit)); + var iter_old_30 : Snapshot.Snapshot_ty (Core_Slice_Iter_Iter_Type.t_iter (NewDb_Lit_Lit_Type.t_lit)); var _32 : (); - var produced_33 : Ghost.ghost_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); + var produced_33 : Snapshot.Snapshot_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); var _36 : (); var _45 : (); var _46 : Core_Option_Option_Type.t_option (NewDb_Lit_Lit_Type.t_lit); @@ -1793,7 +1793,7 @@ module NewDb_ClauseAllocator_Impl3_AddClause var _48 : borrowed (Core_Slice_Iter_Iter_Type.t_iter (NewDb_Lit_Lit_Type.t_lit)); var _49 : isize; var __creusot_proc_iter_elem_50 : NewDb_Lit_Lit_Type.t_lit; - var _51 : Ghost.ghost_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); + var _51 : Snapshot.Snapshot_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); var _53 : (); var lit_54 : NewDb_Lit_Lit_Type.t_lit; var _55 : (); @@ -1829,7 +1829,7 @@ module NewDb_ClauseAllocator_Impl3_AddClause } BB4 { _26 <- (); - old_self_24 <- ([#"../NewDB/src/clause_allocator.rs" 125 52 125 64] Ghost.new self_1); + old_self_24 <- ([#"../NewDB/src/clause_allocator.rs" 125 52 125 64] Snapshot.new self_1); goto BB5 } BB5 { @@ -1839,12 +1839,12 @@ module NewDb_ClauseAllocator_Impl3_AddClause } BB6 { _32 <- (); - iter_old_30 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Ghost.new iter_28); + iter_old_30 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Snapshot.new iter_28); goto BB7 } BB7 { _36 <- (); - produced_33 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Ghost.new (Seq.empty )); + produced_33 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Snapshot.new (Seq.empty )); goto BB8 } BB8 { @@ -1852,10 +1852,10 @@ module NewDb_ClauseAllocator_Impl3_AddClause } BB9 { invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Invariant1.invariant' iter_28 }; - invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Produces0.produces (Ghost.inner iter_old_30) (Ghost.inner produced_33) iter_28 }; - invariant { [#"../NewDB/src/clause_allocator.rs" 127 20 127 54] NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ( * self_1) = NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ( * Ghost.inner old_self_24) }; - invariant { [#"../NewDB/src/clause_allocator.rs" 128 20 128 39] ^ Ghost.inner old_self_24 = ^ self_1 }; - invariant { [#"../NewDB/src/clause_allocator.rs" 129 20 129 67] Seq.length (ShallowModel1.shallow_model self_1) = Seq.length (ShallowModel3.shallow_model old_self_24) + Seq.length (Ghost.inner produced_33) }; + invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Produces0.produces (Snapshot.inner iter_old_30) (Snapshot.inner produced_33) iter_28 }; + invariant { [#"../NewDB/src/clause_allocator.rs" 127 20 127 54] NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ( * self_1) = NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ( * Snapshot.inner old_self_24) }; + invariant { [#"../NewDB/src/clause_allocator.rs" 128 20 128 39] ^ Snapshot.inner old_self_24 = ^ self_1 }; + invariant { [#"../NewDB/src/clause_allocator.rs" 129 20 129 67] Seq.length (ShallowModel1.shallow_model self_1) = Seq.length (ShallowModel3.shallow_model old_self_24) + Seq.length (Snapshot.inner produced_33) }; invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel3.shallow_model old_self_24) -> Seq.get (ShallowModel1.shallow_model self_1) i = Seq.get (ShallowModel3.shallow_model old_self_24) i }; invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel1.shallow_model self_1) - Seq.length (ShallowModel3.shallow_model old_self_24) -> Seq.get (ShallowModel1.shallow_model self_1) (UInt32.to_int cref_15 + UIntSize.to_int HeaderLen0.hEADER_LEN' + i) = Seq.get (ShallowModel0.shallow_model lits_2) i }; invariant { [#"../NewDB/src/clause_allocator.rs" 127 8 127 56] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel1.shallow_model self_1) - Seq.length (ShallowModel3.shallow_model old_self_24) -> VarInRange0.var_in_range (Seq.get (ShallowModel1.shallow_model self_1) (UInt32.to_int cref_15 + UIntSize.to_int HeaderLen0.hEADER_LEN' + i)) (UIntSize.to_int (NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ( * self_1))) }; @@ -1886,12 +1886,12 @@ module NewDb_ClauseAllocator_Impl3_AddClause BB13 { __creusot_proc_iter_elem_50 <- Core_Option_Option_Type.some_0 _46; _53 <- (); - _51 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Ghost.new (Seq.(++) (Ghost.inner produced_33) (Seq.singleton __creusot_proc_iter_elem_50))); + _51 <- ([#"../NewDB/src/clause_allocator.rs" 127 8 127 56] Snapshot.new (Seq.(++) (Snapshot.inner produced_33) (Seq.singleton __creusot_proc_iter_elem_50))); goto BB14 } BB14 { produced_33 <- _51; - _51 <- any Ghost.ghost_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); + _51 <- any Snapshot.Snapshot_ty (Seq.seq (NewDb_Lit_Lit_Type.t_lit)); lit_54 <- __creusot_proc_iter_elem_50; _56 <- borrow_mut (NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_buffer ( * self_1)); self_1 <- { self_1 with current = (let NewDb_ClauseAllocator_ClauseAllocator_Type.C_ClauseAllocator a b = * self_1 in NewDb_ClauseAllocator_ClauseAllocator_Type.C_ClauseAllocator ( ^ _56) b) }; @@ -2526,7 +2526,7 @@ module NewDb_Formula_Impl0_FromInternal_Impl clone NewDb_ClauseAllocator_Impl1_Invariant as Invariant0 with function ShallowModel0.shallow_model = ShallowModel0.shallow_model, val Max0.mAX' = Max0.mAX' - let rec ghost function from_internal [#"../NewDB/src/formula.rs" 60 4 60 118] (crefs : Seq.seq uint32) (clause_allocator : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (idx : int) (_num_vars : int) : Fset.fset (Fset.fset (NewDb_Lit_Lit_Type.t_lit)) + let rec Snapshot function from_internal [#"../NewDB/src/formula.rs" 60 4 60 118] (crefs : Seq.seq uint32) (clause_allocator : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (idx : int) (_num_vars : int) : Fset.fset (Fset.fset (NewDb_Lit_Lit_Type.t_lit)) requires {[#"../NewDB/src/formula.rs" 54 15 54 23] idx >= 0} requires {[#"../NewDB/src/formula.rs" 55 15 55 43] Invariant0.invariant' clause_allocator} requires {[#"../NewDB/src/formula.rs" 56 4 57 72] forall i : int . 0 <= i /\ i < Seq.length crefs -> CrefInvariant0.cref_invariant (UInt32.to_int (Seq.get crefs i)) clause_allocator _num_vars} @@ -2666,7 +2666,7 @@ module NewDb_Formula_Impl0_From_Impl function Insert0.insert = Insert0.insert, axiom . use NewDb_Formula_Formula_Type as NewDb_Formula_Formula_Type - let rec ghost function from [#"../NewDB/src/formula.rs" 42 4 42 101] (crefs : Seq.seq uint32) (clause_allocator : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (num_vars : int) : NewDb_Formula_Formula_Type.t_formula + let rec Snapshot function from [#"../NewDB/src/formula.rs" 42 4 42 101] (crefs : Seq.seq uint32) (clause_allocator : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (num_vars : int) : NewDb_Formula_Formula_Type.t_formula requires {[#"../NewDB/src/formula.rs" 36 15 36 43] Invariant0.invariant' clause_allocator} requires {[#"../NewDB/src/formula.rs" 37 4 38 71] forall i : int . 0 <= i /\ i < Seq.length crefs -> CrefInvariant0.cref_invariant (UInt32.to_int (Seq.get crefs i)) clause_allocator num_vars} ensures { [#"../NewDB/src/formula.rs" 39 14 39 41] NewDb_Formula_Formula_Type.formula_num_vars result = num_vars } @@ -3005,7 +3005,7 @@ module NewDb_ClauseManager_LemmaImpliedByStableOnPush_Impl predicate Invariant0.invariant' = Invariant0.invariant', predicate CrefInvariant0.cref_invariant = CrefInvariant0.cref_invariant, predicate Contains0.contains = Contains0.contains - let rec ghost function lemma_implied_by_stable_on_push [#"../NewDB/src/clause_manager.rs" 30 0 32 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (lit : NewDb_Lit_Lit_Type.t_lit) : () + let rec Snapshot function lemma_implied_by_stable_on_push [#"../NewDB/src/clause_manager.rs" 30 0 32 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (lit : NewDb_Lit_Lit_Type.t_lit) : () requires {[#"../NewDB/src/clause_manager.rs" 28 11 28 62] AreImpliedBy0.are_implied_by learnt_clauses original_clauses ca} ensures { [#"../NewDB/src/clause_manager.rs" 29 10 29 71] AreImpliedBy0.are_implied_by learnt_clauses original_clauses (Push0.push ca lit) } @@ -3156,7 +3156,7 @@ module NewDb_ClauseManager_LemmaImpliedByStableOnExtension_Impl predicate Invariant0.invariant' = Invariant0.invariant', predicate CrefInvariant0.cref_invariant = CrefInvariant0.cref_invariant, predicate Contains0.contains = Contains0.contains - let rec ghost function lemma_implied_by_stable_on_extension [#"../NewDB/src/clause_manager.rs" 40 0 42 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (ca2 : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) : () + let rec Snapshot function lemma_implied_by_stable_on_extension [#"../NewDB/src/clause_manager.rs" 40 0 42 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (ca2 : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) : () requires {[#"../NewDB/src/clause_manager.rs" 36 11 36 62] AreImpliedBy0.are_implied_by learnt_clauses original_clauses ca} requires {[#"../NewDB/src/clause_manager.rs" 37 11 37 27] Extended0.extended ca ca2} requires {[#"../NewDB/src/clause_manager.rs" 38 11 38 27] Extended0.extended ca2 ca} @@ -3342,7 +3342,7 @@ module NewDb_ClauseManager_LemmaImpliedByStableOnBlim_Impl predicate Invariant0.invariant' = Invariant0.invariant', predicate CrefInvariant0.cref_invariant = CrefInvariant0.cref_invariant, predicate Contains0.contains = Contains0.contains - let rec ghost function lemma_implied_by_stable_on_blim [#"../NewDB/src/clause_manager.rs" 52 0 54 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (ca2 : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) : () + let rec Snapshot function lemma_implied_by_stable_on_blim [#"../NewDB/src/clause_manager.rs" 52 0 54 1] (original_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (learnt_clauses : NewDb_CrefManager_CRefManager_Type.t_crefmanager) (ca : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) (ca2 : NewDb_ClauseAllocator_ClauseAllocator_Type.t_clauseallocator) : () requires {[#"../NewDB/src/clause_manager.rs" 46 11 46 62] AreImpliedBy0.are_implied_by learnt_clauses original_clauses ca} requires {[#"../NewDB/src/clause_manager.rs" 47 11 47 38] NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ca = NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_num_vars ca2} requires {[#"../NewDB/src/clause_manager.rs" 48 0 48 81] forall i : int . 0 <= i /\ i < Seq.length (ShallowModel0.shallow_model (NewDb_ClauseAllocator_ClauseAllocator_Type.clauseallocator_buffer ca)) -> Seq.get (ShallowModel1.shallow_model ca) i = Seq.get (ShallowModel1.shallow_model ca2) i} @@ -3405,7 +3405,7 @@ module NewDb_LogicUtil_SeqToFsetInternal_Impl type t = NewDb_Lit_Lit_Type.t_lit clone CreusotContracts_Logic_Fset_Impl0_Contains as Contains0 with type t = NewDb_Lit_Lit_Type.t_lit - let rec ghost function seq_to_fset_internal [#"../NewDB/src/logic_util.rs" 33 0 33 61] (seq : Seq.seq (NewDb_Lit_Lit_Type.t_lit)) (idx : int) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) + let rec Snapshot function seq_to_fset_internal [#"../NewDB/src/logic_util.rs" 33 0 33 61] (seq : Seq.seq (NewDb_Lit_Lit_Type.t_lit)) (idx : int) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) requires {[#"../NewDB/src/logic_util.rs" 30 11 30 19] idx >= 0} ensures { [#"../NewDB/src/logic_util.rs" 31 0 31 103] forall l : NewDb_Lit_Lit_Type.t_lit . Contains0.contains result l -> (exists i : int . idx <= i /\ i < Seq.length seq /\ Seq.get seq i = l) } ensures { [#"../NewDB/src/logic_util.rs" 32 0 32 81] forall i : int . idx <= i /\ i < Seq.length seq -> Contains0.contains result (Seq.get seq i) } @@ -3471,7 +3471,7 @@ module NewDb_LogicUtil_SeqToFset_Impl predicate Contains0.contains = Contains0.contains, function Insert0.insert = Insert0.insert, axiom . - let rec ghost function seq_to_fset [#"../NewDB/src/logic_util.rs" 22 0 22 53] (seq : Seq.seq (NewDb_Lit_Lit_Type.t_lit)) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) + let rec Snapshot function seq_to_fset [#"../NewDB/src/logic_util.rs" 22 0 22 53] (seq : Seq.seq (NewDb_Lit_Lit_Type.t_lit)) : Fset.fset (NewDb_Lit_Lit_Type.t_lit) ensures { [#"../NewDB/src/logic_util.rs" 20 0 20 78] forall i : int . 0 <= i /\ i < Seq.length seq -> Contains0.contains result (Seq.get seq i) } ensures { [#"../NewDB/src/logic_util.rs" 21 0 21 101] forall l : NewDb_Lit_Lit_Type.t_lit . Contains0.contains result l -> (exists i : int . 0 <= i /\ i < Seq.length seq /\ Seq.get seq i = l) } @@ -3660,7 +3660,7 @@ module NewDb_ClauseManager_Impl1_LearnClause use prelude.UInt32 use prelude.Borrow use prelude.Slice - use prelude.Ghost + use prelude.Snapshot use seq.Seq use prelude.UIntSize use set.Fset @@ -3829,7 +3829,7 @@ module NewDb_ClauseManager_Impl1_LearnClause var _0 : uint32; var self_1 : borrowed (NewDb_ClauseManager_ClauseManager_Type.t_clausemanager); var lits_2 : slice (NewDb_Lit_Lit_Type.t_lit); - var old_self_9 : Ghost.ghost_ty (borrowed (NewDb_ClauseManager_ClauseManager_Type.t_clausemanager)); + var old_self_9 : Snapshot.Snapshot_ty (borrowed (NewDb_ClauseManager_ClauseManager_Type.t_clausemanager)); var _11 : (); var _12 : (); var cref_14 : uint32; @@ -3850,7 +3850,7 @@ module NewDb_ClauseManager_Impl1_LearnClause } BB0 { _11 <- (); - old_self_9 <- ([#"../NewDB/src/clause_manager.rs" 67 50 67 62] Ghost.new self_1); + old_self_9 <- ([#"../NewDB/src/clause_manager.rs" 67 50 67 62] Snapshot.new self_1); goto BB1 } BB1 { @@ -3863,7 +3863,7 @@ module NewDb_ClauseManager_Impl1_LearnClause goto BB2 } BB2 { - assert { [#"../NewDB/src/clause_manager.rs" 70 22 70 41] ^ Ghost.inner old_self_9 = ^ self_1 }; + assert { [#"../NewDB/src/clause_manager.rs" 70 22 70 41] ^ Snapshot.inner old_self_9 = ^ self_1 }; _17 <- (); ca_19 <- NewDb_ClauseManager_ClauseManager_Type.clausemanager_clause_allocator ( * self_1); assert { [#"../NewDB/src/clause_manager.rs" 72 8 72 100] AreImpliedBy0.are_implied_by (NewDb_ClauseManager_ClauseManager_Type.clausemanager_learnt_core ( * self_1)) (NewDb_ClauseManager_ClauseManager_Type.clausemanager_original_clauses ( * self_1)) (NewDb_ClauseManager_ClauseManager_Type.clausemanager_clause_allocator ( * self_1)) }; diff --git a/mlcfgs/Scratch.mlcfg b/mlcfgs/Scratch.mlcfg index 88f60e16..3121930f 100644 --- a/mlcfgs/Scratch.mlcfg +++ b/mlcfgs/Scratch.mlcfg @@ -1761,7 +1761,7 @@ module Scratch_Formula_Impl1_Invariant_Impl predicate Invariant0.invariant' = Invariant0.invariant', function ShallowModel1.shallow_model = ShallowModel2.shallow_model, val Max0.mAX' = Max0.mAX' - let rec ghost predicate invariant' [#"../Scratch/src/formula.rs" 71 4 71 34] (self : Scratch_Formula_Formula_Type.t_formula) + let rec Snapshot predicate invariant' [#"../Scratch/src/formula.rs" 71 4 71 34] (self : Scratch_Formula_Formula_Type.t_formula) ensures { [#"../Scratch/src/formula.rs" 70 14 70 47] result = InvariantMirror0.invariant_mirror self } = [@vc:do_not_keep_trace] [@vc:sp] @@ -2336,7 +2336,7 @@ module Scratch_Scratch_LemmaClausePermutedMaintainsSat_Impl clone Scratch_Clause_Impl2_Sat as Sat0 with function ShallowModel0.shallow_model = ShallowModel1.shallow_model, predicate SatInner0.sat_inner = SatInner0.sat_inner - let rec ghost function lemma_clause_permuted_maintains_sat [#"../Scratch/src/scratch.rs" 26 0 26 69] (c : Scratch_Clause_Clause_Type.t_clause) (a : Scratch_Assignments_Assignments_Type.t_assignments) : () + let rec Snapshot function lemma_clause_permuted_maintains_sat [#"../Scratch/src/scratch.rs" 26 0 26 69] (c : Scratch_Clause_Clause_Type.t_clause) (a : Scratch_Assignments_Assignments_Type.t_assignments) : () requires {[#"../Scratch/src/scratch.rs" 24 11 24 19] Sat0.sat c a} ensures { [#"../Scratch/src/scratch.rs" 25 0 25 67] forall c2 : Scratch_Clause_Clause_Type.t_clause . PermutationOf0.permutation_of (ShallowModel0.shallow_model c2) (ShallowModel0.shallow_model c) -> Sat0.sat c2 a } @@ -2422,7 +2422,7 @@ module Scratch_Scratch_LemmaClausePermutedMaintainsUnsat_Impl clone Scratch_Clause_Impl2_Unsat as Unsat0 with function ShallowModel0.shallow_model = ShallowModel1.shallow_model, predicate UnsatInner0.unsat_inner = UnsatInner0.unsat_inner - let rec ghost function lemma_clause_permuted_maintains_unsat [#"../Scratch/src/scratch.rs" 31 0 31 71] (c : Scratch_Clause_Clause_Type.t_clause) (a : Scratch_Assignments_Assignments_Type.t_assignments) : () + let rec Snapshot function lemma_clause_permuted_maintains_unsat [#"../Scratch/src/scratch.rs" 31 0 31 71] (c : Scratch_Clause_Clause_Type.t_clause) (a : Scratch_Assignments_Assignments_Type.t_assignments) : () requires {[#"../Scratch/src/scratch.rs" 29 11 29 21] Unsat0.unsat c a} ensures { [#"../Scratch/src/scratch.rs" 30 0 30 69] forall c2 : Scratch_Clause_Clause_Type.t_clause . PermutationOf0.permutation_of (ShallowModel0.shallow_model c2) (ShallowModel0.shallow_model c) -> Unsat0.unsat c2 a } @@ -2835,7 +2835,7 @@ module Scratch_Scratch_Swap use prelude.Borrow use prelude.Int use prelude.UIntSize - use prelude.Ghost + use prelude.Snapshot use prelude.Slice use seq.Seq use seq.Permut @@ -2989,7 +2989,7 @@ module Scratch_Scratch_Swap var j_3 : usize; var k_4 : usize; var assignments_5 : Scratch_Assignments_Assignments_Type.t_assignments; - var old_f_17 : Ghost.ghost_ty (borrowed (Scratch_Formula_Formula_Type.t_formula)); + var old_f_17 : Snapshot.Snapshot_ty (borrowed (Scratch_Formula_Formula_Type.t_formula)); var _19 : (); var _20 : (); var _21 : borrowed (slice (Scratch_Lit_Lit_Type.t_lit)); @@ -3014,7 +3014,7 @@ module Scratch_Scratch_Swap } BB1 { _19 <- (); - old_f_17 <- ([#"../Scratch/src/scratch.rs" 44 37 44 49] Ghost.new f_1); + old_f_17 <- ([#"../Scratch/src/scratch.rs" 44 37 44 49] Snapshot.new f_1); goto BB2 } BB2 { @@ -3042,7 +3042,7 @@ module Scratch_Scratch_Swap goto BB5 } BB5 { - assert { [#"../Scratch/src/scratch.rs" 48 18 48 38] ^ f_1 = ^ Ghost.inner old_f_17 }; + assert { [#"../Scratch/src/scratch.rs" 48 18 48 38] ^ f_1 = ^ Snapshot.inner old_f_17 }; _29 <- (); _0 <- (); goto BB6 @@ -3114,7 +3114,7 @@ end module Scratch_Logic_BoolToAssignedstate_Impl use prelude.UInt8 use prelude.Int - let rec ghost function bool_to_assignedstate [#"../Scratch/src/logic.rs" 32 0 32 54] (b : bool) : uint8 + let rec Snapshot function bool_to_assignedstate [#"../Scratch/src/logic.rs" 32 0 32 54] (b : bool) : uint8 ensures { [#"../Scratch/src/logic.rs" 30 0 30 30] b -> UInt8.to_int result = 1 } ensures { [#"../Scratch/src/logic.rs" 31 0 31 31] not b -> UInt8.to_int result = 0 }