Add cfg_attrs and derive Clone for Clause

sarsko · Jul 29, 2022 · 32a6a89 · 32a6a89
1 parent 4871a8f
commit 32a6a89
Show file tree

Hide file tree

Showing 10 changed files with 1,589 additions and 1,466 deletions.
diff --git a/CreuSAT/src/assignments.rs b/CreuSAT/src/assignments.rs
@@ -18,6 +18,7 @@ pub struct Assignments(pub Vec<AssignedState>);
 impl Index<usize> for Assignments {
     type Output = AssignedState;
     #[inline]
+    #[cfg_attr(feature = "trust_assignments", trusted)]
     #[requires(@ix < (@self).len())]
     #[ensures((@self)[@ix] == *result)]
     fn index(&self, ix: usize) -> &AssignedState {
@@ -32,6 +33,7 @@ impl Index<usize> for Assignments {
 
 impl IndexMut<usize> for Assignments {
     #[inline]
+    #[cfg_attr(feature = "trust_assignments", trusted)]
     #[requires(@ix < (@self).len())]
     #[ensures((@*self)[@ix] == *result)]
     #[ensures((@^self)[@ix] == ^result)]

diff --git a/CreuSAT/src/clause.rs b/CreuSAT/src/clause.rs
@@ -6,9 +6,12 @@ use creusot_contracts::*;
 use crate::{assignments::*, formula::*, lit::*, solver::*, trail::*};
 use ::std::ops::{Index, IndexMut};
 
+use creusot_contracts::derive::Clone;
+
 #[cfg(feature = "contracts")]
 use crate::logic::{logic_clause::*, logic_formula::*};
 
+#[derive(Clone)]
 pub struct Clause {
     pub deleted: bool,
     pub lbd: u32,
@@ -19,6 +22,7 @@ pub struct Clause {
 impl Index<usize> for Clause {
     type Output = Lit;
     #[inline]
+    #[cfg_attr(feature = "trust_clause", trusted)]
     #[requires(@ix < (@self).len())]
     #[ensures((@self)[@ix] == *result)]
     fn index(&self, ix: usize) -> &Lit {
@@ -33,6 +37,7 @@ impl Index<usize> for Clause {
 
 impl IndexMut<usize> for Clause {
     #[inline]
+    #[cfg_attr(feature = "trust_clause", trusted)]
     #[requires(@ix < (@self).len())]
     #[ensures((@*self)[@ix] == *result)]
     #[ensures((@^self)[@ix] == ^result)]
@@ -48,14 +53,6 @@ impl IndexMut<usize> for Clause {
     }
 }
 
-impl Clone for Clause {
-    #[trusted] // TODO
-    #[ensures(result == *self)]
-    fn clone(&self) -> Self {
-        Clause { deleted: self.deleted, lbd: self.lbd, search: self.search, lits: self.lits.clone() }
-    }
-}
-
 impl Clause {
     #[cfg_attr(feature = "trust_clause", trusted)]
     #[ensures(result == self.invariant(@n))]

diff --git a/CreuSAT/src/conflict_analysis.rs b/CreuSAT/src/conflict_analysis.rs
@@ -19,7 +19,7 @@ pub enum Conflict {
 }
 
 #[inline(always)]
-//#[cfg_attr(feature = "trust_conflict", trusted)]
+#[cfg_attr(feature = "trust_conflict", trusted)]
 #[requires(vars_in_range_inner(@c, (@seen).len()))]
 #[requires(@idx < (@seen).len())]
 #[requires((@seen)[@idx] == idx_in_logic(@idx, @c))]

diff --git a/CreuSAT/src/formula.rs b/CreuSAT/src/formula.rs
@@ -26,6 +26,7 @@ pub struct Formula {
 impl Index<usize> for Formula {
     type Output = Clause;
     #[inline]
+    #[cfg_attr(feature = "trust_formula", trusted)]
     #[requires(@ix < (@self).0.len())]
     #[ensures((@self).0[@ix] == *result)]
     fn index(&self, ix: usize) -> &Clause {
@@ -40,6 +41,7 @@ impl Index<usize> for Formula {
 
 impl IndexMut<usize> for Formula {
     #[inline]
+    #[cfg_attr(feature = "trust_formula", trusted)]
     #[requires(@ix < (@self).0.len())]
     #[ensures((@*self).0[@ix] == *result)]
     #[ensures((@^self).0[@ix] == ^result)]
@@ -160,7 +162,7 @@ impl Formula {
         cref
     }
 
-    //#[cfg_attr(feature = "trust_formula", trusted)]
+    #[cfg_attr(feature = "trust_formula", trusted)]
     #[maintains((mut self).invariant())]
     #[maintains(_t.invariant(mut self))]
     #[requires((@clause).len() == 1)]
@@ -172,7 +174,7 @@ impl Formula {
     #[ensures(@self.num_vars == @(^self).num_vars)]
     //#[ensures(self.equisat_compatible(^self))]
     #[ensures(forall<i: Int> 0 <= i && i < (@self.clauses).len() ==>
-        (@self.clauses)[i] == (@(^self).clauses)[i])] // Needed for the watch invariant
+        (@self.clauses)[i] == (@(^self).clauses)[i])] // This or equisat_compatible is needed for the watch invariant.
     #[ensures(self.equisat(^self))] // Added/changed
     #[ensures(@result == (@self.clauses).len())]
     #[ensures((@(@(^self).clauses)[@result]).len() == 1)]

diff --git a/CreuSAT/src/solver.rs b/CreuSAT/src/solver.rs
@@ -145,7 +145,7 @@ impl Solver {
         self.increase_num_conflicts();
     }
 
-    //#[cfg_attr(feature = "trust_solver", trusted)]
+    #[cfg_attr(feature = "trust_solver", trusted)]
     #[maintains((mut f).invariant())]
     #[maintains((mut t).invariant(mut f))]
     #[maintains((mut w).invariant(mut f))]
@@ -310,7 +310,7 @@ impl Solver {
     }
 
     // OK
-    //#[cfg_attr(feature = "trust_solver", trusted)]
+    #[cfg_attr(feature = "trust_solver", trusted)]
     #[requires(@formula.num_vars < @usize::MAX/2)]
     #[requires(formula.invariant())]
     #[requires(decisions.invariant(@formula.num_vars))]

diff --git a/CreuSAT/src/util.rs b/CreuSAT/src/util.rs
@@ -93,6 +93,7 @@ fn min_log(a: Int, b: Int) -> Int {
     }
 }
 
+#[cfg_attr(feature = "trust_util", trusted)]
 #[ensures(@result == min_log(@a, @b))]
 #[ensures(@a <= @b ==> @result == @a)]
 #[ensures(@b < @a ==> @result == @b)]
@@ -114,6 +115,7 @@ fn max_log(a: Int, b: Int) -> Int {
     }
 }
 
+#[cfg_attr(feature = "trust_util", trusted)]
 #[ensures(@result == max_log(@a, @b))]
 pub fn max(a: usize, b: usize) -> usize {
     if a >= b {

diff --git a/CreuSAT/src/watches.rs b/CreuSAT/src/watches.rs
@@ -151,7 +151,7 @@ impl Watches {
     }
 
     // This is just the first half of update_watch.
-    //#[cfg_attr(feature = "trust_watches", trusted)]
+    #[cfg_attr(feature = "trust_watches", trusted)]
     #[maintains((mut self).invariant(*f))]
     #[requires(@f.num_vars < @usize::MAX/2)]
     #[requires(lit.index_logic() < @f.num_vars)]