From d98a93bcc8bbc345fc1331d181a723851b7c610a Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 11 Apr 2022 15:30:28 +0200 Subject: [PATCH] Remove bdecide --- src/math/polysat/boolean.cpp | 13 ------------- src/math/polysat/boolean.h | 14 +------------- src/math/polysat/solver.cpp | 15 +-------------- src/math/polysat/solver.h | 3 +-- 4 files changed, 3 insertions(+), 42 deletions(-) diff --git a/src/math/polysat/boolean.cpp b/src/math/polysat/boolean.cpp index 51724a319..c3ffa5ae3 100644 --- a/src/math/polysat/boolean.cpp +++ b/src/math/polysat/boolean.cpp @@ -28,7 +28,6 @@ namespace polysat { m_clause.push_back(nullptr); m_watch.push_back({}); m_watch.push_back({}); - m_activity.push_back(0); } else { var = m_unused.back(); @@ -54,8 +53,6 @@ namespace polysat { m_deps[var] = null_dependency; m_watch[lit.index()].reset(); m_watch[(~lit).index()].reset(); - if (m_tracked.get(var, false)) - m_free_vars.del_var_eh(var); // TODO: this is disabled for now, since re-using variables for different constraints may be confusing during debugging. Should be enabled later. // m_unused.push_back(var); } @@ -72,12 +69,6 @@ namespace polysat { SASSERT(is_decision(lit)); } - void bool_var_manager::decide(sat::literal lit, unsigned lvl) { - LOG("Decide literal " << lit << " @ " << lvl); - assign(kind_t::decision, lit, lvl, nullptr); - 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); @@ -99,8 +90,6 @@ namespace polysat { m_kind[lit.var()] = k; m_clause[lit.var()] = reason; m_deps[lit.var()] = dep; - if (m_tracked.get(lit.var(), false)) - m_free_vars.del_var_eh(lit.var()); } void bool_var_manager::unassign(sat::literal lit) { @@ -111,8 +100,6 @@ namespace polysat { m_kind[lit.var()] = kind_t::unassigned; m_clause[lit.var()] = nullptr; m_deps[lit.var()] = null_dependency; - if (m_tracked.get(lit.var(), false)) - m_free_vars.unassign_var_eh(lit.var()); } std::ostream& bool_var_manager::display(std::ostream& out) const { diff --git a/src/math/polysat/boolean.h b/src/math/polysat/boolean.h index 68aa34ee6..28752ab20 100644 --- a/src/math/polysat/boolean.h +++ b/src/math/polysat/boolean.h @@ -32,22 +32,19 @@ namespace polysat { 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 - bool_vector m_tracked; // is the variable tracked - unsigned_vector m_activity; // 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; - var_queue m_free_vars; // free Boolean variables 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(): m_free_vars(m_activity) {} + bool_var_manager() {} // allocated size (not the number of active variables) unsigned size() const { return m_level.size(); } @@ -78,19 +75,10 @@ namespace polysat { 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()]; } - unsigned_vector& activity() { return m_activity; } - bool can_decide() const { return !m_free_vars.empty(); } - sat::bool_var next_var() { return m_free_vars.next_var(); } - void track_var(sat::literal lit) { m_tracked.setx(lit.var(), true, false); m_free_vars.mk_var_eh(lit.var()); } - - // TODO connect activity updates with solver - void inc_activity(sat::literal lit) { m_activity[lit.var()]++; } - void dec_activity(sat::literal lit) { m_activity[lit.var()] /= 2; } /// 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 decide(sat::literal lit, unsigned lvl); void eval(sat::literal lit, unsigned lvl); void assumption(sat::literal lit, unsigned lvl, dependency dep); void unassign(sat::literal lit); diff --git a/src/math/polysat/solver.cpp b/src/math/polysat/solver.cpp index f8fc32e9b..868a57526 100644 --- a/src/math/polysat/solver.cpp +++ b/src/math/polysat/solver.cpp @@ -157,9 +157,6 @@ namespace polysat { add_clause(c_eq, ult(r, b), false); add_clause(~c_eq, eq(q + 1), false); - // force decisions on whether b == 0 - m_bvars.track_var(c_eq.blit()); - return std::tuple(q, r); } @@ -479,10 +476,7 @@ namespace polysat { void solver::decide() { LOG_H2("Decide"); SASSERT(can_decide()); - if (!m_free_pvars.empty()) - pdecide(m_free_pvars.next_var()); - else - bdecide(m_bvars.next_var()); + pdecide(m_free_pvars.next_var()); } void solver::pdecide(pvar v) { @@ -538,13 +532,6 @@ namespace polysat { assign_core(v, val, j); } - void solver::bdecide(sat::bool_var b) { - sat::literal lit(b); - m_bvars.decide(lit, m_level); - m_trail.push_back(trail_instr_t::assign_bool_i); - m_search.push_boolean(lit); - } - void solver::assign_core(pvar v, rational const& val, justification const& j) { if (j.is_decision()) ++m_stats.m_num_decisions; diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index f17008f05..2daf0e15d 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -186,10 +186,9 @@ namespace polysat { void set_conflict(clause& cl) { m_conflict.set(cl); } void set_conflict(pvar v) { m_conflict.set(v); } - bool can_decide() const { return !m_free_pvars.empty() || m_bvars.can_decide(); } + bool can_decide() const { return !m_free_pvars.empty(); } void decide(); void pdecide(pvar v); - void bdecide(sat::bool_var b); void narrow(pvar v); void linear_propagate();