mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 17:45:32 +00:00
Code Activity

merge 'keep' and 'handle_saturation_premises'

Browse source
This commit is contained in:
Jakob Rath 2021-09-12 16:05:34 +02:00
parent deeb6c7784
commit a8c132f769
2 changed files with 5 additions and 13 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -111,14 +111,6 @@ namespace polysat {
m_constraints.shrink(j);
}
void conflict_core::keep(signed_constraint c) {
SASSERT(!c->has_bvar());
cm().ensure_bvar(c.get());
LOG("new constraint: " << c);
// Insert the temporary constraint from saturation into \Gamma.
handle_saturation_premises(c);
}
void conflict_core::resolve(constraint_manager const& m, sat::bool_var var, clause const& cl) {
// Note: core: x, y, z; corresponds to clause ~x \/ ~y \/ ~z
// clause: x \/ u \/ v
@ -147,7 +139,9 @@ namespace polysat {
}
/** If the constraint c is a temporary constraint derived by core saturation, insert it (and recursively, its premises) into \Gamma */
void conflict_core::handle_saturation_premises(signed_constraint c) {
void conflict_core::keep(signed_constraint c) {
cm().ensure_bvar(c.get());
LOG_H3("keeping: " << c);
// NOTE: maybe we should skip intermediate steps and just collect the leaf premises for c?
auto it = m_saturation_premises.find_iterator(c);
if (it == m_saturation_premises.end())
@ -156,9 +150,7 @@ namespace polysat {
auto& premises = it->m_value;
clause_builder c_lemma(*m_solver);
for (auto premise : premises) {
cm().ensure_bvar(premise.get());
// keep(premise);
handle_saturation_premises(premise);
keep(premise);
SASSERT(premise->has_bvar());
c_lemma.push(~premise.blit());
active_level = std::max(active_level, m_solver->m_bvars.level(premise.blit()));

2
src/math/polysat/ule_constraint.h
View file

@ -44,7 +44,7 @@ namespace polysat {
inequality as_inequality(bool is_positive) const override;
unsigned hash() const override;
bool operator==(constraint const& other) const override;
bool is_eq() const { return m_rhs.is_zero(); }
bool is_eq() const override { return m_rhs.is_zero(); }
pdd const& p() const { SASSERT(is_eq()); return m_lhs; }
};