Update for Creusot 0.7.0

CreuSAT/Cargo.toml

@@ -10,7 +10,7 @@ unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }
 [dependencies]
 clap = { version = "4.5", features = ["cargo"] }
 rand = "0.8.5"
-creusot-contracts = "0.5"
+creusot-contracts = "0.7.0"
 
 [dev-dependencies]
 termcolor = "1.1"

CreuSAT/src/assignments.rs

@@ -1,7 +1,6 @@
-use creusot_contracts::{std::*, *};
-
 use crate::{formula::*, lit::*, trail::*};
 use ::std::ops::{Index, IndexMut};
+use creusot_contracts::prelude::*;
 
 #[allow(unused_features)]
 #[cfg(creusot)]
@@ -83,6 +82,6 @@ impl Assignments {
     #[requires(f.inv())]
     #[ensures(result.inv(*f))]
     pub fn new(f: &Formula) -> Self {
-        Assignments(vec::from_elem(2, f.num_vars))
+        Assignments(std::vec::from_elem(2, f.num_vars))
     }
 }

CreuSAT/src/clause.rs

@@ -1,4 +1,4 @@
-use creusot_contracts::{std::*, Clone, Snapshot, *};
+use creusot_contracts::prelude::{Clone, *};
 
 use crate::{assignments::*, formula::*, lit::*, solver::*, trail::*};
 use ::std::ops::{Index, IndexMut};

CreuSAT/src/conflict_analysis.rs

@@ -1,4 +1,4 @@
-use creusot_contracts::{std::*, vec, Snapshot, *};
+use creusot_contracts::{prelude::*, std::vec::vec};
 
 use crate::{assignments::*, clause::*, decision::*, formula::*, lit::*, trail::*};
 

CreuSAT/src/decision.rs

@@ -1,6 +1,8 @@
-use creusot_contracts::{ensures, invariant, maintains, proof_assert, requires, std::vec, Clone, Int, Snapshot, *};
-
 use crate::{assignments::*, formula::*, util::*};
+use creusot_contracts::{
+    prelude::{Clone, *},
+    std::vec::vec,
+};
 
 #[cfg(creusot)]
 use crate::logic::{logic::unset, logic_decision::*, logic_util::*};
@@ -23,14 +25,6 @@ impl ::std::default::Default for Node {
     }
 }
 
-impl creusot_contracts::Default for Node {
-    #[predicate]
-    #[open]
-    fn is_default(self) -> bool {
-        pearlite! { self.next@ == usize::MAX@ && self.prev@ == usize::MAX@ && self.ts@ == 0 }
-    }
-}
-
 pub struct Decisions {
     pub linked_list: Vec<Node>,
     timestamp: usize,
@@ -48,7 +42,7 @@ impl Decisions {
                 lit_order@[i]@ < f.num_vars@)]
     #[ensures(result.inv(f.num_vars@))]
     pub fn make_linked_list(f: &Formula, lit_order: Vec<usize>) -> Decisions {
-        let mut linked_list: Vec<Node> = vec::from_elem(Node::default(), f.num_vars);
+        let mut linked_list: Vec<Node> = std::vec::from_elem(Node::default(), f.num_vars);
         let mut i: usize = 0;
         let mut head: usize = 0;
         #[invariant([email protected]() == f.num_vars@)]
@@ -84,9 +78,9 @@ impl Decisions {
     #[requires(0 < f.num_vars@ && f.num_vars@ < usize::MAX@/2)]
     #[ensures(result.inv(f.num_vars@))]
     pub fn new(f: &Formula) -> Decisions {
-        let mut lit_order: Vec<usize> = vec::from_elem(0, f.num_vars);
-        let mut counts: Vec<usize> = vec::from_elem(0, f.num_vars);
-        let mut counts_with_index: Vec<(usize, usize)> = vec::from_elem((0, 0), f.num_vars);
+        let mut lit_order: Vec<usize> = std::vec::from_elem(0, f.num_vars);
+        let mut counts: Vec<usize> = std::vec::from_elem(0, f.num_vars);
+        let mut counts_with_index: Vec<(usize, usize)> = std::vec::from_elem((0, 0), f.num_vars);
         let mut i: usize = 0;
         #[invariant(i@ <= [email protected]())]
         #[invariant([email protected]() == f.num_vars@)]

CreuSAT/src/formula.rs

@@ -1,6 +1,6 @@
 // Formula is Mac OK with an inline_full + split on VC #12 for add_clause 11.04 22.18
 
-use creusot_contracts::{std::*, Snapshot, *};
+use creusot_contracts::prelude::*;
 
 use crate::{assignments::*, clause::*, solver::*, trail::*, watches::*};
 use ::std::ops::{Index, IndexMut};

CreuSAT/src/lib.rs

@@ -1,13 +1,9 @@
-//#![feature(type_ascription)]
-//#![cfg_attr(not(creusot), feature(stmt_expr_attributes, proc_macro_hygiene))]
 #![allow(unused_imports)]
 #![allow(unused)]
 #![allow(dead_code)]
 #![allow(non_snake_case)]
 #![recursion_limit = "512"]
 
-use creusot_contracts::{std::*, Snapshot, *};
-
 mod assignments;
 mod clause;
 mod conflict_analysis;

CreuSAT/src/lit.rs

@@ -1,7 +1,5 @@
 use ::std::ops;
-use creusot_contracts::{model::*, std::*, *};
-
-use creusot_contracts::Clone;
+use creusot_contracts::prelude::{Clone, *};
 
 use crate::assignments::*;
 
@@ -18,8 +16,7 @@ pub struct Lit {
 impl View for Lit {
     type ViewTy = Lit;
 
-    #[logic]
-    #[open]
+    #[logic(open)]
     fn view(self) -> Self {
         self
     }
@@ -29,8 +26,7 @@ impl View for Lit {
 impl DeepModel for Lit {
     type DeepModelTy = Lit;
 
-    #[logic]
-    #[open]
+    #[logic(open)]
     fn deep_model(self) -> Self {
         self
     }

CreuSAT/src/logic/logic.rs

@@ -1,24 +1,20 @@
-use creusot_contracts::std::*;
-use creusot_contracts::*;
+use creusot_contracts::prelude::*;
 
 use crate::{assignments::*, clause::*, formula::*, lit::*, trail::*};
 
 use crate::logic::{logic_assignments::*, logic_clause::*, logic_formula::*, logic_trail::*};
 
-#[logic]
-#[open]
+#[logic(open)]
 pub fn pos() -> AssignedState {
     1u8
 }
 
-#[logic]
-#[open]
+#[logic(open)]
 pub fn neg() -> AssignedState {
     0u8
 }
 
-#[predicate]
-#[open]
+#[logic(open)]
 pub fn unset(v: AssignedState) -> bool {
     pearlite! {
         if v@ >= 2 {
@@ -30,8 +26,7 @@ pub fn unset(v: AssignedState) -> bool {
 }
 
 #[cfg_attr(feature = "trust_logic_logic", trusted)]
-#[logic]
-#[open]
+#[logic(open)]
 #[ensures(b ==> result@ == 1)]
 #[ensures(!b ==> result@ == 0)]
 pub fn bool_to_assignedstate(b: bool) -> AssignedState {
@@ -42,8 +37,7 @@ pub fn bool_to_assignedstate(b: bool) -> AssignedState {
     }
 }
 
-#[logic]
-#[open]
+#[logic(open)]
 pub fn flip_v(v: AssignedState) -> AssignedState {
     pearlite! {
         if v@ == 0 {

CreuSAT/src/logic/logic_assignments.rs

@@ -1,4 +1,4 @@
-use creusot_contracts::{model::*, std::*, *};
+use creusot_contracts::{model::*, prelude::*};
 
 use crate::{
     assignments::*,
@@ -13,49 +13,43 @@ use crate::logic::{logic::*, logic_formula::*};
 impl View for Assignments {
     type ViewTy = Seq<AssignedState>;
 
-    #[logic]
-    #[open]
+    #[logic(open)]
     fn view(self) -> Self::ViewTy {
         self.0.view()
     }
 }
 
-#[predicate]
-#[open]
+#[logic(open)]
 pub fn compatible_inner(a: Seq<AssignedState>, a2: Seq<AssignedState>) -> bool {
     pearlite! {
         a.len() == a2.len() && (forall<i: Int> 0 <= i && i < a.len() ==>
             (unset(a[i]) || a[i] == a2[i]))
     }
 }
 
-#[predicate]
-#[open]
+#[logic(open)]
 pub fn complete_inner(a: Seq<AssignedState>) -> bool {
     pearlite! {
         forall<i: Int> 0 <= i && i < a.len() ==> !unset(a[i])
     }
 }
 
-#[predicate]
-#[open]
+#[logic(open)]
 pub fn compatible_complete_inner(a: Seq<AssignedState>, a2: Seq<AssignedState>) -> bool {
     compatible_inner(a, a2) && complete_inner(a2)
 }
 
 // Predicates
 impl Assignments {
-    #[predicate]
-    #[open]
+    #[logic(open)]
     pub fn inv(self, f: Formula) -> bool {
         pearlite! {
             f.num_vars@ == [email protected]()
             && forall<i: Int> 0 <= i && i < [email protected]() ==> self@[i]@ <= 3
         }
     }
 
-    #[predicate]
-    #[open]
+    #[logic(open)]
     pub fn complete(self) -> bool {
         pearlite! {
             forall<i: Int> 0 <= i && i < [email protected]() ==> !unset(self@[i])