Skip to content

Commit

Permalink
Update CreuSAT to postfix @ and unnamed invariants
Browse files Browse the repository at this point in the history
  • Loading branch information
@sarsko
sarsko committed May 8, 2023
1 parent 3048f35 commit aa75b5e
Show file tree
Hide file tree
Showing 32 changed files with 3,795 additions and 3,491 deletions.
28 changes: 14 additions & 14 deletions CreuSAT/src/assignments.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -17,8 +17,8 @@ impl Index<usize> for Assignments {
type Output = AssignedState;
#[inline]
#[cfg_attr(feature = "trust_assignments", trusted)]
#[requires(i@x < self@.len())]
#[ensures(self@[i@x] == *result)]
#[requires(ix@ < self@.len())]
#[ensures(self@[ix@] == *result)]
fn index(&self, ix: usize) -> &AssignedState {
#[cfg(not(creusot))]
unsafe {
Expand All @@ -32,11 +32,11 @@ impl Index<usize> for Assignments {
impl IndexMut<usize> for Assignments {
#[inline]
#[cfg_attr(feature = "trust_assignments", trusted)]
#[requires(i@x < self@.len())]
#[ensures((@*self)[i@x] == *result)]
#[ensures((@^self)[i@x] == ^result)]
#[ensures(forall<i : Int> 0 <= i && i != i@x && i < self@.len() ==> self@[i] == (@^self)[i])]
#[ensures((@^self).len() == (@*self).len())]
#[requires(ix@ < self@.len())]
#[ensures((*self)@[ix@] == *result)]
#[ensures((^self)@[ix@] == ^result)]
#[ensures(forall<i : Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
#[ensures((^self)@.len() == (*self)@.len())]
fn index_mut(&mut self, ix: usize) -> &mut AssignedState {
#[cfg(not(creusot))]
unsafe {
Expand All @@ -59,16 +59,16 @@ impl Assignments {
#[inline(always)]
#[cfg_attr(feature = "trust_assignments", trusted)]
#[maintains((mut self).invariant(*_f))]
#[requires(lit.invariant(@_f.num_vars))]
#[requires(lit.invariant(_f.num_vars@))]
#[requires(_f.invariant())]
#[requires(trail_invariant(@_t, *_f))]
#[requires(trail_invariant(_t@, *_f))]
#[requires(unset(self@[lit.index_logic()]))]
#[requires(long_are_post_unit_inner(@_t, *_f, self@))]
#[ensures(long_are_post_unit_inner(@_t, *_f, @^self))]
#[ensures(!unset((@^self)[lit.index_logic()]))]
#[ensures((@^self).len() == self@.len())]
#[requires(long_are_post_unit_inner(_t@, *_f, self@))]
#[ensures(long_are_post_unit_inner(_t@, *_f, (^self)@))]
#[ensures(!unset((^self)@[lit.index_logic()]))]
#[ensures((^self)@.len() == self@.len())]
#[ensures((forall<j : Int> 0 <= j && j < self@.len()
&& j != lit.index_logic() ==> (@*self)[j] == (@^self)[j]))]
&& j != lit.index_logic() ==> (*self)@[j] == (^self)@[j]))]
#[ensures(lit.sat(^self))]
pub fn set_assignment(&mut self, lit: Lit, _f: &Formula, _t: &Vec<Step>) {
let old_self: Ghost<&mut Assignments> = ghost! { self };
Expand Down
70 changes: 35 additions & 35 deletions CreuSAT/src/clause.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ impl Index<usize> for Clause {
type Output = Lit;
#[inline]
#[cfg_attr(feature = "trust_clause", trusted)]
#[requires(i@x < self@.len())]
#[ensures(self@[i@x] == *result)]
#[requires(ix@ < self@.len())]
#[ensures(self@[ix@] == *result)]
fn index(&self, ix: usize) -> &Lit {
#[cfg(not(creusot))]
unsafe {
Expand All @@ -34,11 +34,11 @@ impl Index<usize> for Clause {
impl IndexMut<usize> for Clause {
#[inline]
#[cfg_attr(feature = "trust_clause", trusted)]
#[requires(i@x < self@.len())]
#[ensures((@*self)[i@x] == *result)]
#[ensures((@^self)[i@x] == ^result)]
#[ensures(forall<i : Int> 0 <= i && i != i@x && i < self@.len() ==> self@[i] == (@^self)[i])]
#[ensures((@^self).len() == (@*self).len())]
#[requires(ix@ < self@.len())]
#[ensures((*self)@[ix@] == *result)]
#[ensures((^self)@[ix@] == ^result)]
#[ensures(forall<i : Int> 0 <= i && i != ix@ && i < self@.len() ==> self@[i] == (^self)@[i])]
#[ensures((^self)@.len() == (*self)@.len())]
fn index_mut(&mut self, ix: usize) -> &mut Lit {
#[cfg(not(creusot))]
unsafe {
Expand All @@ -51,10 +51,10 @@ impl IndexMut<usize> for Clause {

impl Clause {
#[cfg_attr(feature = "trust_clause", trusted)]
#[ensures(result == self.invariant(@n))]
#[ensures(result == self.invariant(n@))]
pub fn check_clause_invariant(&self, n: usize) -> bool {
let mut i: usize = 0;
#[invariant(inv, forall<j: Int> 0 <= j && j < i@ ==> self@[j].invariant(@n))]
#[invariant(forall<j: Int> 0 <= j && j < i@ ==> self@[j].invariant(n@))]
while i < self.len() {
if !self[i].check_lit_invariant(n) {
return false;
Expand All @@ -71,13 +71,13 @@ impl Clause {
#[ensures(result == self.no_duplicate_indexes())]
pub fn no_duplicates(&self) -> bool {
let mut i: usize = 0;
#[invariant(no_dups,
#[invariant(
forall<j: Int, k: Int> 0 <= j && j < i@ &&
0 <= k && k < j ==> self@[j].index_logic() != self@[k].index_logic())]
while i < self.len() {
let lit1 = self[i];
let mut j: usize = 0;
#[invariant(inv, forall<k: Int> 0 <= k && k < @j ==> lit1.index_logic() != self@[k].index_logic())]
#[invariant(forall<k: Int> 0 <= k && k < j@ ==> lit1.index_logic() != self@[k].index_logic())]
while j < i {
let lit2 = self[j];
if lit1.index() == lit2.index() {
Expand Down Expand Up @@ -107,13 +107,13 @@ impl Clause {
// This does better without splitting
#[inline(always)]
#[cfg_attr(feature = "trust_clause", trusted)]
#[maintains((mut self).invariant(@_f.num_vars))]
#[maintains((mut self).invariant(_f.num_vars@))]
#[requires(self@.len() > 0)]
#[requires(i@dx < self@.len())]
#[ensures(forall<i: Int> 0 <= i && i < (@(^self)).len() ==>
(exists<j: Int> 0 <= j && j < self@.len() && (@(^self))[i] == self@[j]))]
#[ensures((@(^self))[(@^self).len() - 1] == self@[i@dx])]
#[ensures((@(^self)).len() == self@.len())]
#[requires(idx@ < self@.len())]
#[ensures(forall<i: Int> 0 <= i && i < (^self)@.len() ==>
(exists<j: Int> 0 <= j && j < self@.len() && (^self)@[i] == self@[j]))]
#[ensures((^self)@[(^self)@.len() - 1] == self@[idx@])]
#[ensures((^self)@.len() == self@.len())]
#[ensures(forall<j: Int> 0 <= j && j < self@.len()
==> self@[j].lit_in(^self))]
fn move_to_end(&mut self, idx: usize, _f: &Formula) {
Expand All @@ -124,30 +124,30 @@ impl Clause {
// This does better without splitting
#[inline(always)]
#[cfg_attr(feature = "trust_clause", trusted)]
#[maintains((mut self).invariant(@_f.num_vars))]
#[maintains((mut self).invariant(_f.num_vars@))]
#[requires(self@.len() > 0)]
#[requires(i@dx < self@.len())]
#[ensures(forall<i: Int> 0 <= i && i < (@(^self)).len() ==>
exists<j: Int> 0 <= j && j < self@.len() && (@(^self))[i] == self@[j])]
#[ensures((@(^self)).len() + 1 == self@.len())]
#[ensures(!self@[i@dx].lit_in(^self))]
#[requires(idx@ < self@.len())]
#[ensures(forall<i: Int> 0 <= i && i < (^self)@.len() ==>
exists<j: Int> 0 <= j && j < self@.len() && (^self)@[i] == self@[j])]
#[ensures((^self)@.len() + 1 == self@.len())]
#[ensures(!self@[idx@].lit_in(^self))]
#[ensures(forall<j: Int> 0 <= j && j < self@.len()
&& j != i@dx ==> self@[j].lit_in(^self))]
&& j != idx@ ==> self@[j].lit_in(^self))]
pub fn remove_from_clause(&mut self, idx: usize, _f: &Formula) {
self.move_to_end(idx, _f);
self.lits.pop();
}

// This is an ugly runtime check
#[cfg_attr(feature = "trust_clause", trusted)]
#[requires(invariant_internal(self@, @_f.num_vars))]
#[requires(invariant_internal(self@, _f.num_vars@))]
#[requires(a.invariant(*_f))]
#[requires(self@.len() > 1)]
#[ensures(result ==> self.unit(*a))]
#[ensures(result ==> self@[0].unset(*a))]
pub fn unit_and_unset(&self, a: &Assignments, _f: &Formula) -> bool {
let mut i: usize = 1;
#[invariant(unsat, forall<j: Int> 1 <= j && j < i@ ==> self@[j].unsat(*a))]
#[invariant(forall<j: Int> 1 <= j && j < i@ ==> self@[j].unsat(*a))]
while i < self.len() {
if !self[i].lit_unsat(a) {
return false;
Expand All @@ -159,25 +159,25 @@ impl Clause {

// ONLY VALID FOR CLAUSES NOT IN THE FORMULA
#[cfg_attr(feature = "trust_clause", trusted)]
#[requires(self@.len() > @j)]
#[requires(self@.len() > @k)]
#[maintains((mut self).invariant(@_f.num_vars))]
#[requires(self@.len() > j@)]
#[requires(self@.len() > k@)]
#[maintains((mut self).invariant(_f.num_vars@))]
#[maintains((mut self).equisat_extension(*_f))]
#[ensures(self@.len() == (@(^self)).len())]
#[ensures(self@.len() == (^self)@.len())]
pub fn swap_lits_in_clause(&mut self, _f: &Formula, j: usize, k: usize) {
let old_c: Ghost<&mut Clause> = ghost! { self };
self.lits.swap(j, k);
proof_assert!(eventually_sat_complete((((@_f).0).push(*self), (@_f).1)) ==>
eventually_sat_complete((((@_f).0).push(*old_c.inner()), (@_f).1)));
proof_assert!(eventually_sat_complete(((_f@.0).push(*self), _f@.1)) ==>
eventually_sat_complete(((_f@.0).push(*old_c.inner()), _f@.1)));
}

#[cfg_attr(feature = "trust_clause", trusted)]
#[requires((@t.lit_to_level).len() == (@_f.num_vars))]
#[requires(self.invariant(@_f.num_vars))]
#[requires(t.lit_to_level@.len() == _f.num_vars@)]
#[requires(self.invariant(_f.num_vars@))]
pub fn calc_lbd(&self, _f: &Formula, s: &mut Solver, t: &Trail) -> usize {
let mut i: usize = 0;
let mut lbd: usize = 0;
#[invariant(lbd_bound, @lbd <= i@)]
#[invariant(lbd@ <= i@)]
while i < self.len() {
let level = t.lit_to_level[self[i].index()];
if level < s.perm_diff.len() && // TODO: Add this as an invariant to Solver
Expand Down
Loading

0 comments on commit aa75b5e

Please sign in to comment.