mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

fixes/debugging

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-11-02 14:48:19 -07:00
parent 4c81f8676c
commit 3f3bd5948f
5 changed files with 41 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -146,7 +146,7 @@ namespace polysat {
if (!c2->has_bvar() || l_undef == c2.bvalue(s))
core.keep(c2); // adds propagation of c to the search stack
core.reset();
LOG("reduced to " << c2);
LOG_H3("Polynomial superposition " << eq << " " << c << " reduced to " << c2);
if (c2.bvalue(s) == l_false) {
core.insert(eq);
core.insert(c);
@ -161,12 +161,10 @@ namespace polysat {
}
bool ex_polynomial_superposition::try_explain(pvar v, conflict& core) {
LOG_H3("Trying polynomial superposition...");
reduce_by(v, core);
lbool result = l_undef;
while (result == l_undef)
result = try_explain1(v, core);
LOG("success? " << result);
return result == l_true;
}

20
src/math/polysat/saturation.cpp
View file

@ -147,20 +147,26 @@ namespace polysat {
auto c2 = s.ule(y, pddm.mk_val(y_lo));
new_constraints.insert(c1);
new_constraints.insert(c2);
LOG("bounded " << bound << " : " << c1 << " " << c2);
LOG("bounded " << bound << " : " << x << " " << x_max << " " << y << " " << y_max << " " << c1 << " " << c2);
}
rational inf_saturate::max_value(pdd const& x) {
if (x.is_var())
return s.m_viable.max_viable(x.var());
else if (x.is_val())
return x.val();
else
return x.manager().max_value();
}
// determine worst case upper bounds for x, y
// then extract premises for a non-worst-case bound.
void inf_saturate::push_omega(vector<signed_constraint>& new_constraints, pdd const& x, pdd const& y) {
auto& pddm = x.manager();
rational x_max = pddm.max_value();
rational y_max = pddm.max_value();
rational x_max = max_value(x);
rational y_max = max_value(y);
if (x.is_var())
x_max = s.m_viable.max_viable(x.var());
if (y.is_var())
y_max = s.m_viable.max_viable(y.var());
LOG("pushing " << x << " " << y);
if (x_max * y_max > pddm.max_value())
push_omega_bisect(new_constraints, x, x_max, y, y_max);

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

@ -89,6 +89,8 @@ namespace polysat {
// p := coeff*x*y where coeff_x = coeff*x, x a variable
bool is_coeffxY(pdd const& coeff_x, pdd const& p, pdd& y);
rational max_value(pdd const& x);
public:
inf_saturate(solver& s) : inference_engine(s) {}
bool perform(pvar v, conflict& core) override;

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

@ -489,7 +489,7 @@ namespace polysat {
*/
void solver::resolve_bool(sat::literal lit) {
SASSERT(m_bvars.is_propagation(lit.var()));
clause other = *m_bvars.reason(lit.var());
clause const& other = *m_bvars.reason(lit.var());
LOG_H3("resolve_bool: " << lit << " " << other);
m_conflict.resolve(m_constraints, lit, other);
}
@ -518,7 +518,8 @@ namespace polysat {
SASSERT(!lemma.empty());
lemma.set_justified_var(v);
add_lemma(lemma);
decide_bool(lemma);
if (!is_conflict())
decide_bool(lemma);
}
// Guess a literal from the given clause; returns the guessed constraint

40
src/test/polysat.cpp
View file

@ -876,23 +876,27 @@ namespace polysat {
}
// x*y <= b & a <= x & !Omega(x*y) => a*y <= b
static void test_ineq_non_axiom4(unsigned bw = 32) {
static void test_ineq_non_axiom4(unsigned bw, unsigned i) {
auto const bound = rational::power_of_two(bw - 1);
for (unsigned i = 0; i < 24; ++i) {
scoped_solver s(__func__);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto a = s.var(s.add_var(bw));
auto b = s.var(s.add_var(bw));
permute_args(i, x, y, a, b);
s.add_ule(x * y, b);
s.add_ule(a, x);
s.add_ult(x, bound);
s.add_ult(y, bound);
s.add_ult(b, a * y);
s.check();
s.expect_sat();
}
scoped_solver s(__func__);
LOG("permutation: " << i);
auto x = s.var(s.add_var(bw));
auto y = s.var(s.add_var(bw));
auto a = s.var(s.add_var(bw));
auto b = s.var(s.add_var(bw));
permute_args(i, x, y, a, b);
s.add_ule(x * y, b);
s.add_ule(a, x);
s.add_ult(x, bound);
s.add_ult(y, bound);
s.add_ult(b, a * y);
s.check();
s.expect_sat();
}
static void test_ineq_non_axiom4(unsigned bw = 32) {
for (unsigned i = 0; i < 24; ++i)
test_ineq_non_axiom4(bw, i);
}
// a < xy & x <= b & !Omega(x*y) => a < b*y
@ -1063,8 +1067,8 @@ void tst_polysat() {
// polysat::test_ineq_axiom1();
// polysat::test_ineq_axiom2();
// polysat::test_ineq_axiom3();
polysat::test_ineq_non_axiom1();
polysat::test_ineq_non_axiom4();
// polysat::test_ineq_non_axiom1();
polysat::test_ineq_non_axiom4(32, 5);
polysat::test_ineq_axiom4();
polysat::test_ineq_axiom5();
polysat::test_ineq_axiom6();