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

propagate at the right level

Browse source
This commit is contained in:
Jakob Rath 2021-09-08 16:00:57 +02:00
parent 40d62af796
commit f2c79b851f
4 changed files with 23 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -44,12 +44,12 @@ 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) && !reason(var); }
// bool is_decision(bool_lit lit) const { return is_decision(lit.var()); }
bool is_decision(sat::literal lit) const { return is_decision(lit.var()); }
bool is_propagation(sat::bool_var var) const { return is_assigned(var) && reason(var); }
lbool value(sat::bool_var var) const { return value(sat::literal(var)); }
lbool value(sat::literal lit) const { return m_value[lit.index()]; }
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()); }
unsigned level(sat::literal lit) const { return level(lit.var()); }
clause* reason(sat::bool_var var) const { SASSERT(is_assigned(var)); return m_reason[var]; }
clause* lemma(sat::bool_var var) const { SASSERT(is_decision(var)); return m_lemma[var]; }

4
src/math/polysat/conflict_core.cpp
View file

@ -144,17 +144,19 @@ namespace polysat {
auto it = m_saturation_premises.find_iterator(c);
if (it == m_saturation_premises.end())
return;
unsigned active_level = 0;
auto& premises = it->m_value;
clause_builder c_lemma(*m_solver);
for (auto premise : premises) {
handle_saturation_premises(premise);
c_lemma.push_literal(~premise.blit());
active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit()));
}
c_lemma.push_literal(c.blit());
clause* cl = cm().store(c_lemma.build());
if (cl->size() == 1)
c->set_unit_clause(cl);
m_solver->assign_bool(c.blit(), cl, nullptr);
m_solver->propagate_bool_at(active_level, c.blit(), cl);
}
/** Create fallback lemma that excludes the current search state */

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

@ -247,7 +247,7 @@ namespace polysat {
void solver::pop_levels(unsigned num_levels) {
SASSERT(m_level >= num_levels);
unsigned const target_level = m_level - num_levels;
vector<signed_constraint> replay;
vector<sat::literal> replay;
LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
#if ENABLE_LINEAR_SOLVER
m_linear_solver.pop(num_levels);
@ -287,10 +287,9 @@ namespace polysat {
case trail_instr_t::assign_bool_i: {
sat::literal lit = m_search.back().lit();
LOG_V("Undo assign_bool_i: " << lit);
// TODO: we should use the level of the boolean literal here, but that isn't yet set correctly.
signed_constraint c = m_constraints.lookup(lit);
if (c.level() <= target_level)
replay.push_back(c);
unsigned active_level = m_bvars.level(lit);
if (active_level <= target_level)
replay.push_back(lit);
else
m_bvars.unassign(lit);
m_search.pop();
@ -313,9 +312,9 @@ namespace polysat {
m_constraints.release_level(m_level + 1);
SASSERT(m_level == target_level);
for (unsigned j = replay.size(); j-- > 0; ) {
auto c = replay[j];
auto lit = replay[j];
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(c.blit());
m_search.push_boolean(lit);
}
}
@ -737,21 +736,25 @@ namespace polysat {
void solver::decide_bool(sat::literal lit, clause& lemma) {
push_level();
LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
assign_bool(lit, nullptr, &lemma);
assign_bool(m_level, lit, nullptr, &lemma);
}
void solver::propagate_bool(sat::literal lit, clause* reason) {
LOG("Propagate boolean literal " << lit << " @ " << m_level << " by " << show_deref(reason));
propagate_bool_at(m_level, lit, reason);
}
void solver::propagate_bool_at(unsigned level, sat::literal lit, clause* reason) {
LOG("Propagate boolean literal " << lit << " @ " << level << " by " << show_deref(reason));
SASSERT(reason);
assign_bool(lit, reason, nullptr);
SASSERT(level <= m_level);
assign_bool(level, lit, reason, nullptr);
}
/// Assign a boolean literal and put it on the search stack,
/// and activate the corresponding constraint.
void solver::assign_bool(sat::literal lit, clause* reason, clause* lemma) {
void solver::assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma) {
LOG("Assigning boolean literal: " << lit);
m_bvars.assign(lit, m_level, reason, lemma);
m_bvars.assign(lit, level, reason, lemma);
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(lit);
}
@ -777,7 +780,6 @@ namespace polysat {
void solver::deactivate_constraint(signed_constraint c) {
LOG("Deactivating constraint: " << c);
erase_watch(c);
// c->set_unit_clause(nullptr);
}
void solver::backjump(unsigned new_level) {

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

@ -156,12 +156,13 @@ namespace polysat {
void pop_levels(unsigned num_levels);
void pop_constraints(signed_constraints& cs);
void assign_bool(sat::literal lit, clause* reason, clause* lemma);
void assign_bool(unsigned level, sat::literal lit, clause* reason, clause* lemma);
void activate_constraint(signed_constraint c);
void deactivate_constraint(signed_constraint c);
sat::literal decide_bool(clause& lemma);
void decide_bool(sat::literal lit, clause& lemma);
void propagate_bool(sat::literal lit, clause* reason);
void propagate_bool_at(unsigned level, sat::literal lit, clause* reason);
void assign_core(pvar v, rational const& val, justification const& j);
bool is_assigned(pvar v) const { return !m_justification[v].is_unassigned(); }