mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 08:28:44 +00:00
Code Activity

Don't call assign_eh for internal constraints

Browse source
This commit is contained in:
Jakob Rath 2022-11-28 18:43:19 +01:00
parent c1f9a26f09
commit 0c44391b9e
3 changed files with 22 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/constraint_manager.cpp
View file

@ -311,17 +311,17 @@ namespace polysat {
// addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r // addition does not overflow in (b*q) + r; for now expressed as: r <= bq+r
// b ≠ 0 ==> r < b // b ≠ 0 ==> r < b
// b = 0 ==> q = -1 // b = 0 ==> q = -1
s.add_eq(a, b * q + r); s.add_clause(eq(b * q + r - a), false);
s.add_umul_noovfl(b, q); s.add_clause(~umul_ovfl(b, q), false);
// r <= b*q+r // r <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 } // { apply equivalence: p <= q <=> q-p <= -p-1 }
// b*q <= -r-1 // b*q <= -r-1
s.add_ule(b*q, -r-1); s.add_clause(ule(b*q, -r-1), false);
#if 0 #if 0
// b*q <= b*q+r // b*q <= b*q+r
// { apply equivalence: p <= q <=> q-p <= -p-1 } // { apply equivalence: p <= q <=> q-p <= -p-1 }
// r <= - b*q - 1 // r <= - b*q - 1
s.add_ule(r, -b*q-1); // redundant, but may help propagation s.add_clause(ule(r, -b*q-1), false); // redundant, but may help propagation
#endif #endif
auto c_eq = eq(b); auto c_eq = eq(b);
@ -347,7 +347,7 @@ namespace polysat {
pdd r = m.mk_var(s.add_var(sz)); pdd r = m.mk_var(s.add_var(sz));
m_dedup.op_constraint_expr.insert(args, r.var()); m_dedup.op_constraint_expr.insert(args, r.var());
s.assign_eh(mk_op_constraint(op, p, q, r), null_dependency); s.add_clause(mk_op_constraint(op, p, q, r), false);
return r; return r;
} }

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

@ -62,6 +62,10 @@ namespace polysat {
} }
lbool solver::check_sat() { lbool solver::check_sat() {
#ifndef NDEBUG
SASSERT(!m_is_solving);
flet<bool> save_(m_is_solving, true);
#endif
LOG("Starting"); LOG("Starting");
while (should_search()) { while (should_search()) {
m_stats.m_num_iterations++; m_stats.m_num_iterations++;
@ -136,6 +140,8 @@ namespace polysat {
} }
void solver::assign_eh(signed_constraint c, dependency dep) { void solver::assign_eh(signed_constraint c, dependency dep) {
// This method is part of the external interface and should not be used to create internal constraints during solving.
SASSERT(!m_is_solving);
backjump(base_level()); backjump(base_level());
SASSERT(at_base_level()); SASSERT(at_base_level());
SASSERT(c); SASSERT(c);
@ -184,8 +190,8 @@ namespace polysat {
if (!can_propagate()) if (!can_propagate())
return; return;
#ifndef NDEBUG #ifndef NDEBUG
SASSERT(!m_propagating); SASSERT(!m_is_propagating);
flet<bool> save_(m_propagating, true); flet<bool> save_(m_is_propagating, true);
#endif #endif
push_qhead(); push_qhead();
while (can_propagate()) { while (can_propagate()) {
@ -1152,6 +1158,11 @@ namespace polysat {
} }
} }
void solver::add_clause(signed_constraint c1, bool is_redundant) {
signed_constraint cs[1] = { c1 };
add_clause(1, cs, is_redundant);
}
void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) { void solver::add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant) {
signed_constraint cs[2] = { c1, c2 }; signed_constraint cs[2] = { c1, c2 };
add_clause(2, cs, is_redundant); add_clause(2, cs, is_redundant);

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

@ -165,7 +165,8 @@ namespace polysat {
vector<constraints> m_pwatch; // watch list datastructure into constraints. vector<constraints> m_pwatch; // watch list datastructure into constraints.
#ifndef NDEBUG #ifndef NDEBUG
std::optional<pvar> m_locked_wlist; // restrict watch list modification while it is being propagated std::optional<pvar> m_locked_wlist; // restrict watch list modification while it is being propagated
bool m_propagating = false; // set to true during propagation bool m_is_propagating = false; // set to true during propagation
bool m_is_solving = false; // set to true during solving
#endif #endif
unsigned_vector m_activity; unsigned_vector m_activity;
@ -274,6 +275,7 @@ namespace polysat {
void learn_lemma(clause& lemma); void learn_lemma(clause& lemma);
void backjump(unsigned new_level); void backjump(unsigned new_level);
void add_clause(clause& clause); void add_clause(clause& clause);
void add_clause(signed_constraint c1, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant); void add_clause(signed_constraint c1, signed_constraint c2, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant); void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, bool is_redundant);
void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant); void add_clause(signed_constraint c1, signed_constraint c2, signed_constraint c3, signed_constraint c4, bool is_redundant);
@ -417,7 +419,7 @@ namespace polysat {
signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); } signed_constraint smul_udfl(pdd const& p, pdd const& q) { return m_constraints.smul_udfl(p, q); }
signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); } signed_constraint bit(pdd const& p, unsigned i) { return m_constraints.bit(p, i); }
/** Create and activate polynomial constraints. */ /** Create and activate constraints */
void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); } void add_eq(pdd const& p, dependency dep = null_dependency) { assign_eh(eq(p), dep); }
void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } void add_eq(pdd const& p, pdd const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }
void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); } void add_eq(pdd const& p, rational const& q, dependency dep = null_dependency) { assign_eh(eq(p, q), dep); }