mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 10:52:02 +00:00
Code Activity

fix iterator

Browse source
This commit is contained in:
Jakob Rath 2021-09-13 15:33:39 +02:00
parent e5289f84a0
commit b6c478c2ca
2 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -136,11 +136,11 @@ namespace polysat {
conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2): conflict_core_iterator(constraint_manager& cm, it1_t it1, it1_t end1, it2_t it2):
m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {} m_cm(&cm), m_it1(it1), m_end1(end1), m_it2(it2) {}
static conflict_core_iterator begin(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) { static conflict_core_iterator begin(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.begin(), cs.end(), lits.begin()}; return {cm, cs.begin(), cs.end(), lits.begin()};
} }
static conflict_core_iterator end(constraint_manager& cm, signed_constraints cs, indexed_uint_set lits) { static conflict_core_iterator end(constraint_manager& cm, signed_constraints const& cs, indexed_uint_set const& lits) {
return {cm, cs.end(), cs.end(), lits.end()}; return {cm, cs.end(), cs.end(), lits.end()};
} }

8
src/math/polysat/explain.cpp
View file

@ -47,8 +47,7 @@ namespace polysat {
// c2 ... constraint that is currently false // c2 ... constraint that is currently false
// Try to replace it with a new false constraint (derived from superposition with a true constraint) // Try to replace it with a new false constraint (derived from superposition with a true constraint)
signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) { signed_constraint ex_polynomial_superposition::find_replacement(signed_constraint c2, pvar v, conflict_core& core) {
for (auto it1 = core.begin(); it1 != core.end(); ++it1) { for (auto c1 : core) {
signed_constraint c1 = *it1;
if (!is_positive_equality_over(v, c1)) if (!is_positive_equality_over(v, c1))
continue; continue;
if (!c1.is_currently_true(s())) if (!c1.is_currently_true(s()))
@ -69,14 +68,13 @@ namespace polysat {
// TODO(later): check superposition into disequality again (see notes) // TODO(later): check superposition into disequality again (see notes)
// true = done, false = abort, undef = continue // true = done, false = abort, undef = continue
lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) { lbool ex_polynomial_superposition::try_explain1(pvar v, conflict_core& core) {
for (auto it2 = core.begin(); it2 != core.end(); ++it2) { for (auto c2 : core) {
signed_constraint c2 = *it2;
if (!is_positive_equality_over(v, c2)) if (!is_positive_equality_over(v, c2))
continue; continue;
if (!c2.is_currently_false(s())) if (!c2.is_currently_false(s()))
continue; continue;
// TODO: can try multiple replacements at once; then the it2 loop needs to be done only once... (requires some reorganization for storing the premises) // TODO: can try multiple replacements at once; then the c2 loop needs to be done only once... (requires some reorganization for storing the premises)
signed_constraint c = find_replacement(c2, v, core); signed_constraint c = find_replacement(c2, v, core);
if (!c) if (!c)
continue; continue;