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

add replay

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-09-07 14:58:56 +02:00
parent 733c21bb20
commit 4c7ec75868
3 changed files with 20 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -126,7 +126,7 @@ namespace polysat {
c->set_unit_clause(cl);
// TODO: this should be backtrackable (unless clause is unit).
// => add at the end and update pop_levels to replay appropriately
m_solver->assign_bool_core(c.blit(), cl, nullptr);
m_solver->assign_bool_backtrackable(c.blit(), cl, nullptr);
m_solver->activate_constraint(c);
}

1
src/math/polysat/constraint.h
View file

@ -214,6 +214,7 @@ namespace polysat {
sat::bool_var bvar() const { return m_constraint->bvar(); }
sat::literal blit() const { return sat::literal(bvar(), is_negative()); }
unsigned level() const { return m_constraint->level(); }
constraint* get() const { return m_constraint; }
explicit operator bool() const { return !!m_constraint; }

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

@ -244,11 +244,9 @@ namespace polysat {
}
void solver::pop_levels(unsigned num_levels) {
// TODO: replay mechanism for saturation results
// NOTE: we only need to replay boolean literal propagations (might be unit clauses but not necessarily... no, unit clauses do not need to go on the stack. but we still have to pop them if the solver level is popped.)
SASSERT(m_level >= num_levels);
unsigned const target_level = m_level - num_levels;
(void)target_level;
vector<signed_constraint> replay;
LOG("Pop " << num_levels << " levels (lvl " << m_level << " -> " << target_level << ")");
#if ENABLE_LINEAR_SOLVER
m_linear_solver.pop(num_levels);
@ -284,8 +282,13 @@ namespace polysat {
sat::literal lit = m_search.back().lit();
LOG_V("Undo assign_bool_i: " << lit);
signed_constraint c = m_constraints.lookup(lit);
deactivate_constraint(c);
m_bvars.unassign(lit);
if (c.level() <= target_level)
replay.push_back(c);
else {
deactivate_constraint(c);
m_bvars.unassign(lit);
}
m_search.pop();
break;
}
@ -305,6 +308,11 @@ namespace polysat {
pop_constraints(m_redundant);
m_constraints.release_level(m_level + 1);
SASSERT(m_level == target_level);
for (auto c : replay) {
m_trail.push_back(trail_instr_t::assign_bool_i);
m_search.push_boolean(c.blit());
c.narrow(*this);
}
}
void solver::pop_constraints(signed_constraints& cs) {
@ -679,6 +687,11 @@ namespace polysat {
}
/** Create fallback lemma that excludes the current search state */
/**
* revisit: can prune literals further by slicing base on cone of influence
* based on marked literals/variables on the stack. Only decisions that affect
* marked items need to be included.
*/
clause_ref solver::mk_fallback_lemma(unsigned lvl) {
LOG_H3("Creating fallback lemma for level " << lvl);
LOG_V("m_search: " << m_search);