diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index c3ffa5ae3..c18f4a36e 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -25,19 +25,22 @@ namespace polysat { m_level.push_back(UINT_MAX); m_deps.push_back(null_dependency); m_kind.push_back(kind_t::unassigned); - m_clause.push_back(nullptr); + m_reason.push_back(nullptr); m_watch.push_back({}); m_watch.push_back({}); } else { var = m_unused.back(); m_unused.pop_back(); + auto lit = sat::literal(var); + SASSERT_EQ(m_value[lit.index()], l_undef); + SASSERT_EQ(m_value[(~lit).index()], l_undef); SASSERT_EQ(m_level[var], UINT_MAX); - SASSERT_EQ(m_value[2*var], l_undef); - SASSERT_EQ(m_value[2*var+1], l_undef); - SASSERT_EQ(m_kind[var], kind_t::unassigned); - SASSERT_EQ(m_clause[var], nullptr); SASSERT_EQ(m_deps[var], null_dependency); + SASSERT_EQ(m_kind[var], kind_t::unassigned); + SASSERT_EQ(m_reason[var], nullptr); + SASSERT(m_watch[lit.index()].empty()); + SASSERT(m_watch[(~lit).index()].empty()); } return var; } @@ -49,7 +52,7 @@ namespace polysat { m_value[(~lit).index()] = l_undef; m_level[var] = UINT_MAX; m_kind[var] = kind_t::unassigned; - m_clause[var] = nullptr; + m_reason[var] = nullptr; m_deps[var] = null_dependency; m_watch[lit.index()].reset(); m_watch[(~lit).index()].reset(); @@ -63,12 +66,6 @@ namespace polysat { SASSERT(is_bool_propagation(lit)); } - void bool_var_manager::decide(sat::literal lit, unsigned lvl, clause& lemma) { - LOG("Decide literal " << lit << " @ " << lvl); - assign(kind_t::decision, lit, lvl, &lemma); - SASSERT(is_decision(lit)); - } - void bool_var_manager::eval(sat::literal lit, unsigned lvl) { LOG("Eval literal " << lit << " @ " << lvl); assign(kind_t::value_propagation, lit, lvl, nullptr); @@ -78,7 +75,7 @@ namespace polysat { void bool_var_manager::assumption(sat::literal lit, unsigned lvl, dependency dep) { LOG("Asserted " << lit << " @ " << lvl); assign(kind_t::assumption, lit, lvl, nullptr, dep); - SASSERT(is_decision(lit) || is_assumption(lit)); + SASSERT(is_assumption(lit)); } void bool_var_manager::assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep) { @@ -88,7 +85,7 @@ namespace polysat { m_value[(~lit).index()] = l_false; m_level[lit.var()] = lvl; m_kind[lit.var()] = k; - m_clause[lit.var()] = reason; + m_reason[lit.var()] = reason; m_deps[lit.var()] = dep; } @@ -98,7 +95,7 @@ namespace polysat { m_value[(~lit).index()] = l_undef; m_level[lit.var()] = UINT_MAX; m_kind[lit.var()] = kind_t::unassigned; - m_clause[lit.var()] = nullptr; + m_reason[lit.var()] = nullptr; m_deps[lit.var()] = null_dependency; } diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index 28752ab20..a3a83d349 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -25,25 +25,19 @@ namespace polysat { bool_propagation, value_propagation, assumption, - decision, }; - svector m_unused; // previously deleted variables that can be reused by new_var(); - svector m_value; // current value (indexed by literal) - unsigned_vector m_level; // level of assignment (indexed by variable) - dependency_vector m_deps; // dependencies of external asserts - svector m_kind; // decision or propagation? - // Clause associated with the assignment (indexed by variable): - // - for propagations: the reason (or NULL for eval'd literals) - // - for decisions: the lemma (or NULL for externally asserted literals) - ptr_vector m_clause; - - vector> m_watch; // watch list for literals into clauses + svector m_unused; // previously deleted variables that can be reused by new_var(); + svector m_value; // current value (indexed by literal) + unsigned_vector m_level; // level of assignment (indexed by variable) + dependency_vector m_deps; // dependencies of external asserts + svector m_kind; // decision or propagation? + ptr_vector m_reason; // reasons for bool-propagated literals + vector> m_watch; // watch list for literals into clauses void assign(kind_t k, sat::literal lit, unsigned lvl, clause* reason, dependency dep = null_dependency); public: - bool_var_manager() {} // allocated size (not the number of active variables) @@ -54,8 +48,6 @@ namespace polysat { bool is_assigned(sat::bool_var var) const { return value(var) != l_undef; } bool is_assigned(sat::literal lit) const { return value(lit) != l_undef; } - bool is_decision(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::decision; } - bool is_decision(sat::literal lit) const { return is_decision(lit.var()); } bool is_assumption(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::assumption; } bool is_assumption(sat::literal lit) const { return is_assumption(lit.var()); } bool is_bool_propagation(sat::bool_var var) const { return is_assigned(var) && m_kind[var] == kind_t::bool_propagation; } @@ -68,17 +60,14 @@ namespace polysat { bool is_false(sat::literal lit) const { return value(lit) == l_false; } unsigned level(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_level[var]; } unsigned level(sat::literal lit) const { return level(lit.var()); } - clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return is_bool_propagation(var) ? m_clause[var] : nullptr; } + clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); SASSERT(is_bool_propagation(var) == !!m_reason[var]); return m_reason[var]; } clause* reason(sat::literal lit) const { return reason(lit.var()); } dependency dep(sat::literal lit) const { return lit == sat::null_literal ? null_dependency : m_deps[lit.var()]; } - clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_clause[var]; } - ptr_vector& watch(sat::literal lit) { return m_watch[lit.index()]; } /// Set the given literal to true void propagate(sat::literal lit, unsigned lvl, clause& reason); - void decide(sat::literal lit, unsigned lvl, clause& lemma); void eval(sat::literal lit, unsigned lvl); void assumption(sat::literal lit, unsigned lvl, dependency dep); void unassign(sat::literal lit); @@ -91,7 +80,6 @@ namespace polysat { case kind_t::unassigned: return out << "unassigned"; case kind_t::bool_propagation: return out << "bool propagation"; case kind_t::value_propagation: return out << "value propagation"; - case kind_t::decision: return out << "decision"; case kind_t::assumption: return out << "assumption"; default: UNREACHABLE(); return out; }