mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Remove bdecide

Browse source
This commit is contained in:
Jakob Rath 2022-04-11 15:30:28 +02:00
parent 63031548cb
commit d98a93bcc8
4 changed files with 3 additions and 42 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/math/polysat/boolean.cpp
View file

@ -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 {

14
src/math/polysat/boolean.h
View file

@ -32,22 +32,19 @@ namespace polysat {
svector<lbool> 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<kind_t> 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<clause> m_clause;
var_queue m_free_vars; // free Boolean variables
vector<ptr_vector<clause>> 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<clause>& 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);

15
src/math/polysat/solver.cpp
View file

@ -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<pdd, pdd>(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;

3
src/math/polysat/solver.h
View file

@ -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();