mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

add propagation after lemma addition

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-09-19 08:09:53 -04:00
parent dac2f1c026
commit 663b61b612
1 changed files with 8 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -163,6 +163,8 @@ namespace polysat {
} }
void solver::propagate() { void solver::propagate() {
if (!can_propagate())
return;
push_qhead(); push_qhead();
while (can_propagate()) { while (can_propagate()) {
auto const& item = m_search[m_qhead++]; auto const& item = m_search[m_qhead++];
@ -677,6 +679,8 @@ namespace polysat {
} }
void solver::decide_bool(sat::literal lit, clause* lemma) { void solver::decide_bool(sat::literal lit, clause* lemma) {
SASSERT(!can_propagate());
SASSERT(!is_conflict());
push_level(); push_level();
LOG_H2("Decide boolean literal " << lit << " @ " << m_level); LOG_H2("Decide boolean literal " << lit << " @ " << m_level);
assign_bool(m_level, lit, nullptr, lemma); assign_bool(m_level, lit, nullptr, lemma);
@ -747,25 +751,21 @@ namespace polysat {
} }
// Add lemma to storage but do not activate it // Add lemma to storage
void solver::add_lemma(clause& lemma) { void solver::add_lemma(clause& lemma) {
LOG("Lemma: " << lemma); LOG("Lemma: " << lemma);
for (sat::literal lit : lemma) { for (sat::literal lit : lemma) {
LOG(" Literal " << lit << " is: " << lit2cnstr(lit)); LOG(" Literal " << lit << " is: " << lit2cnstr(lit));
// Check that fully evaluated constraints are on the stack
SASSERT(!lit2cnstr(lit).is_currently_true(*this)); SASSERT(!lit2cnstr(lit).is_currently_true(*this));
// literals that are added from m_conflict.m_vars have not been assigned. SASSERT(m_bvars.value(lit) != l_true);
// they are false in the current model.
// SASSERT(m_bvars.is_assigned(lit) || !c.is_currently_false(*this));
// TODO: work out invariant for the lemma. It should be impossible to extend the model in a way that makes the lemma true.
} }
SASSERT(lemma.size() > 0); SASSERT(!lemma.empty());
m_constraints.store(&lemma, *this); m_constraints.store(&lemma, *this);
if (lemma.size() == 1) { if (lemma.size() == 1) {
signed_constraint c = lit2cnstr(lemma[0]); signed_constraint c = lit2cnstr(lemma[0]);
c->set_unit_clause(&lemma); c->set_unit_clause(&lemma);
} }
propagate();
} }
void solver::insert_constraint(signed_constraints& cs, signed_constraint c) { void solver::insert_constraint(signed_constraints& cs, signed_constraint c) {