mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-20 21:03:39 +00:00
Code Activity

Try to evaluate constraints whenever one of its variables is changed

Browse source
This commit is contained in:
Jakob Rath 2023-03-17 22:19:46 +01:00
parent f82f18efda
commit 526a55f116
2 changed files with 40 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -219,6 +219,7 @@ namespace polysat {
flet<bool> save_(m_is_propagating, true); flet<bool> save_(m_is_propagating, true);
#endif #endif
push_qhead(); push_qhead();
unsigned const qhead_init = m_qhead;
unsigned bool_qhead = m_qhead; unsigned bool_qhead = m_qhead;
unsigned eval_qhead = m_qhead; unsigned eval_qhead = m_qhead;
while (can_propagate_search()) { while (can_propagate_search()) {
@ -245,7 +246,27 @@ namespace polysat {
auto const& item = m_search[eval_qhead++]; auto const& item = m_search[eval_qhead++];
if (item.is_assignment()) { if (item.is_assignment()) {
// LOG_H1("P2: eval pvar v" << item.var()); // LOG_H1("P2: eval pvar v" << item.var());
propagate(item.var(), false); // propagate(item.var(), false);
for (int i = 0; i < qhead_init; ++i) {
if (!m_search[i].is_boolean())
continue;
sat::literal lit = m_search[i].lit();
if (m_ptrue_lits.contains(lit))
continue;
signed_constraint c = lit2cnstr(lit);
if (!c.contains_var(item.var()))
continue;
SASSERT(m_bvars.is_true(lit));
lbool const pvalue = c.eval(*this);
if (pvalue == l_true) {
m_ptrue_lits.insert(lit);
m_ptrue_lits_trail.push_back(lit);
}
else if (pvalue == l_false) {
set_conflict(c);
break;
}
}
} }
else { else {
SASSERT(item.is_boolean()); SASSERT(item.is_boolean());

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

@ -196,14 +196,32 @@ namespace polysat {
unsigned_vector m_base_levels; // External clients can push/pop scope. unsigned_vector m_base_levels; // External clients can push/pop scope.
// Cache literals that evaluate to true in the current assignment.
// TODO: convert to proper pvalue caching. decouple trail from qhead. push size on trail when a pvar is assigned, because that's the point where evaluations can change.
sat::literal_set m_ptrue_lits;
sat::literal_vector m_ptrue_lits_trail;
unsigned_vector m_ptrue_lits_size_trail;
void push_qhead() { void push_qhead() {
m_trail.push_back(trail_instr_t::qhead_i); m_trail.push_back(trail_instr_t::qhead_i);
m_qhead_trail.push_back(m_qhead); m_qhead_trail.push_back(m_qhead);
//
SASSERT(m_ptrue_lits.size() == m_ptrue_lits_trail.size());
m_ptrue_lits_size_trail.push_back(m_ptrue_lits_trail.size());
} }
void pop_qhead() { void pop_qhead() {
m_qhead = m_qhead_trail.back(); m_qhead = m_qhead_trail.back();
m_qhead_trail.pop_back(); m_qhead_trail.pop_back();
//
unsigned sz = m_ptrue_lits_size_trail.back();
m_ptrue_lits_size_trail.pop_back();
while (m_ptrue_lits_trail.size() > sz) {
sat::literal lit = m_ptrue_lits_trail.back();
m_ptrue_lits.remove(lit);
m_ptrue_lits_trail.pop_back();
}
SASSERT(m_ptrue_lits.size() == m_ptrue_lits_trail.size());
} }
unsigned size(pvar v) const { return m_size[v]; } unsigned size(pvar v) const { return m_size[v]; }