Define models of SAT

sarsko · Jul 12, 2022 · 7d161d0 · 7d161d0
1 parent 3ac3efc
commit 7d161d0
Showing 1 changed file with 10 additions and 1 deletion.
diff --git a/CreuSAT/src/logic/logic.rs b/CreuSAT/src/logic/logic.rs
@@ -1,11 +1,20 @@
-extern crate creusot_contracts;
 use creusot_contracts::std::*;
 use creusot_contracts::*;
 
 use crate::{assignments::*, clause::*, formula::*, lit::*, trail::*};
 
 use crate::logic::{logic_assignments::*, logic_clause::*, logic_formula::*, logic_trail::*};
 
+
+#[cfg(feature="contracts")]
+mod inner {
+    struct Model(Mapping<Int, bool>);
+
+}
+
+#[cfg(feature="contracts")]
+pub use inner::*;
+
 #[logic]
 fn pos() -> AssignedState {
     1u8