mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'polysat' of https://github.com/Z3Prover/z3 into polysat

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-12-16 10:14:10 +01:00
commit d5bc4b84a7
9 changed files with 430 additions and 45 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -647,22 +647,29 @@ namespace polysat {
rational val;
justification j;
switch (m_viable.find_viable(v, val)) {
case dd::find_t::empty:
case find_t::empty:
// NOTE: all such cases should be discovered elsewhere (e.g., during propagation/narrowing)
// (fail here in debug mode so we notice if we miss some)
DEBUG_CODE( UNREACHABLE(); );
m_free_pvars.unassign_var_eh(v);
set_conflict(v, false);
return;
case dd::find_t::singleton:
case find_t::singleton:
// NOTE: this case may happen legitimately if all other possibilities were excluded by brute force search
// NOTE 2: probably not true anymore; viable::intersect should trigger all propagations now
DEBUG_CODE( UNREACHABLE(); );
j = justification::propagation(m_level);
break;
case dd::find_t::multiple:
case find_t::multiple:
j = justification::decision(m_level + 1);
break;
case find_t::resource_out:
// the value is not viable, so assign_verify will call the univariate solver.
j = justification::decision(m_level + 1);
break;
default:
UNREACHABLE();
break;
}
assign_verify(v, val, j);
}
@ -731,20 +738,24 @@ namespace polysat {
}
if (c) {
LOG_H2("Chosen assignment " << assignment_pp(*this, v, val) << " is not actually viable!");
LOG("Current assignment: " << assignments_pp(*this));
++m_stats.m_num_viable_fallback;
// Try to find a valid replacement value
switch (m_viable_fallback.find_viable(v, val)) {
case dd::find_t::singleton:
case dd::find_t::multiple:
case find_t::singleton:
case find_t::multiple:
LOG("Fallback solver: " << assignment_pp(*this, v, val));
SASSERT(!j.is_propagation()); // all excluded values are true negatives, so if j.is_propagation() the univariate solver must return unsat
j = justification::decision(m_level + 1);
break;
case dd::find_t::empty:
case find_t::empty:
LOG("Fallback solver: unsat");
m_free_pvars.unassign_var_eh(v);
set_conflict(v, true);
return;
case find_t::resource_out:
UNREACHABLE(); // TODO: abort solving
return;
}
}
if (j.is_decision())

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

@ -90,8 +90,6 @@ namespace polysat {
return;
if (narrow_bound(s, is_positive, q(), p(), q1, p1))
return;
}
void umul_ovfl_constraint::activate(solver& s, bool is_positive) {
@ -99,8 +97,10 @@ namespace polysat {
return;
if (!is_positive) {
signed_constraint sc(this, is_positive);
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(p(), p()*q()), false);
s.add_clause(~sc, s.eq(p()), s.eq(q()), s.ule(q(), p()*q()), false);
// ¬Omega(p, q) ==> q = 0 \/ p <= p*q
// ¬Omega(p, q) ==> p = 0 \/ q <= p*q
s.add_clause(~sc, /* s.eq(p()), */ s.eq(q()), s.ule(p(), p()*q()), false);
s.add_clause(~sc, s.eq(p()), /* s.eq(q()), */ s.ule(q(), p()*q()), false);
}
}

134
src/math/polysat/univariate/univariate_solver.cpp
View file

@ -35,6 +35,7 @@ namespace polysat {
unsigned bit_width;
func_decl_ref x_decl;
expr_ref x;
vector<rational> model_cache;
public:
univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
@ -48,15 +49,30 @@ namespace polysat {
s = mk_solver(m, p, false, true, true, symbol::null);
x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width));
x = m.mk_const(x_decl);
model_cache.push_back(rational(-1));
}
~univariate_bitblast_solver() override = default;
void reset_cache() {
model_cache.back() = -1;
}
void push_cache() {
model_cache.push_back(model_cache.back());
}
void pop_cache() {
model_cache.pop_back();
}
void push() override {
push_cache();
s->push();
}
void pop(unsigned n) override {
pop_cache();
s->pop(n);
}
@ -64,7 +80,8 @@ namespace polysat {
return bv->mk_numeral(r, bit_width);
}
// [d,c,b,a] ==> ((a*x + b)*x + c)*x + d
#if 0
// [d,c,b,a] --> ((a*x + b)*x + c)*x + d
expr* mk_poly(univariate const& p) const {
if (p.empty()) {
return mk_numeral(rational::zero());
@ -79,13 +96,46 @@ namespace polysat {
return e;
}
}
#else
// TODO: shouldn't the simplification step of the underlying solver already support this transformation? how to enable?
// 2^k*x --> x << k
// n*x --> n * x
expr* mk_poly_term(rational const& coeff, expr* xpow) const {
unsigned pow;
if (coeff.is_power_of_two(pow))
return bv->mk_bv_shl(xpow, mk_numeral(rational(pow)));
else
return bv->mk_bv_mul(mk_numeral(coeff), xpow);
}
// [d,c,b,a] --> d + c*x + b*(x*x) + a*(x*x*x)
expr* mk_poly(univariate const& p) const {
if (p.empty()) {
return mk_numeral(rational::zero());
}
else {
expr* e = mk_numeral(p[0]);
expr* xpow = x;
for (unsigned i = 1; i < p.size(); ++i) {
if (!p[i].is_zero()) {
expr* t = mk_poly_term(p[i], xpow);
e = bv->mk_bv_add(e, t);
}
if (i + 1 < p.size())
xpow = bv->mk_bv_mul(xpow, x);
}
return e;
}
}
#endif
void add(expr* e, bool sign, dep_t dep) {
reset_cache();
if (sign)
e = m.mk_not(e);
expr* a = m.mk_const(m.mk_const_decl(symbol(dep), m.mk_bool_sort()));
s->assert_expr(e, a);
// std::cout << "add: " << expr_ref(e, m) << " <== " << expr_ref(a, m) << "\n";
IF_VERBOSE(10, verbose_stream() << "(assert (! " << expr_ref(e, m) << " :named " << expr_ref(a, m) << "))\n");
}
void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
@ -161,15 +211,77 @@ namespace polysat {
}
rational model() override {
model_ref model;
s->get_model(model);
SASSERT(model);
app* val = to_app(model->get_const_interp(x_decl));
SASSERT(val->get_decl_kind() == OP_BV_NUM);
SASSERT(val->get_num_parameters() == 2);
auto const& p = val->get_parameter(0);
SASSERT(p.is_rational());
return p.get_rational();
rational& cached_model = model_cache.back();
if (cached_model.is_neg()) {
model_ref model;
s->get_model(model);
SASSERT(model);
app* val = to_app(model->get_const_interp(x_decl));
SASSERT(val->get_decl_kind() == OP_BV_NUM);
SASSERT(val->get_num_parameters() == 2);
auto const& p = val->get_parameter(0);
SASSERT(p.is_rational());
cached_model = p.get_rational();
}
return cached_model;
}
bool find_min(rational& val) override {
val = model();
push();
// try reducing val by setting bits to 0, starting at the msb.
for (unsigned k = bit_width; k-- > 0; ) {
if (!val.get_bit(k)) {
add_bit0(k, 0);
continue;
}
// try decreasing k-th bit
push();
add_bit0(k, 0);
lbool result = check();
if (result == l_true) {
SASSERT(model() < val);
val = model();
}
pop(1);
if (result == l_true)
add_bit0(k, 0);
else if (result == l_false)
add_bit1(k, 0);
else
return false;
}
pop(1);
return true;
}
bool find_max(rational& val) override {
val = model();
push();
// try increasing val by setting bits to 1, starting at the msb.
for (unsigned k = bit_width; k-- > 0; ) {
if (val.get_bit(k)) {
add_bit1(k, 0);
continue;
}
// try increasing k-th bit
push();
add_bit1(k, 0);
lbool result = check();
if (result == l_true) {
SASSERT(model() > val);
val = model();
}
pop(1);
if (result == l_true)
add_bit1(k, 0);
else if (result == l_false)
add_bit0(k, 0);
else
return false;
}
pop(1);
return true;
}
std::ostream& display(std::ostream& out) const override {

26
src/math/polysat/univariate/univariate_solver.h
View file

@ -41,9 +41,33 @@ namespace polysat {
virtual void pop(unsigned n) = 0;
virtual lbool check() = 0;
/**
* Precondition: check() returned l_false
*/
virtual dep_vector unsat_core() = 0;
/**
* Precondition: check() returned l_true
*/
virtual rational model() = 0;
/**
* Find minimal model.
*
* Precondition: check() returned l_true
* Returns: true on success, false on resource out.
*/
virtual bool find_min(rational& out_min) = 0;
/**
* Find maximal model.
*
* Precondition: check() returned l_true
* Returns: true on success, false on resource out.
*/
virtual bool find_max(rational& out_max) = 0;
virtual void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
virtual void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
@ -65,6 +89,8 @@ namespace polysat {
/// Assert i-th bit of x
virtual void add_bit(unsigned idx, bool sign, dep_t dep) = 0;
void add_bit0(unsigned idx, dep_t dep) { add_bit(idx, true, dep); }
void add_bit1(unsigned idx, dep_t dep) { add_bit(idx, false, dep); }
virtual std::ostream& display(std::ostream& out) const = 0;
};

142
src/math/polysat/viable.cpp
View file

@ -70,6 +70,7 @@ namespace polysat {
auto* e = m_alloc.back();
e->side_cond.reset();
e->coeff = 1;
e->refined = nullptr;
m_alloc.pop_back();
return e;
}
@ -131,11 +132,11 @@ namespace polysat {
if (intersect(v, sc)) {
rational val;
switch (find_viable(v, val)) {
case dd::find_t::singleton:
case find_t::singleton:
propagate(v, val);
prop = true;
break;
case dd::find_t::empty:
case find_t::empty:
s.set_conflict(v, false);
return true;
default:
@ -348,6 +349,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
@ -384,6 +386,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
@ -471,6 +474,7 @@ namespace polysat {
pdd lop = s.var2pdd(v).mk_val(lo);
pdd hip = s.var2pdd(v).mk_val(hi);
entry* ne = alloc_entry();
ne->refined = e;
ne->src = e->src;
ne->side_cond = e->side_cond;
ne->coeff = 1;
@ -588,25 +592,45 @@ namespace polysat {
return hi;
}
dd::find_t viable::find_viable(pvar v, rational& lo) {
refined:
// template <viable::query_t mode>
find_t viable::query(query_t mode, pvar v, rational& lo, rational& hi) {
SASSERT(mode == query_t::find_viable); // other modes are TODO
auto const& max_value = s.var2pdd(v).max_value();
// max number of interval refinements before falling back to the univariate solver
unsigned const refinement_budget = 1000;
unsigned refinements = refinement_budget;
refined:
if (!refinements) {
LOG("Refinement budget exhausted! Fall back to univariate solver.");
return find_t::resource_out;
}
refinements--;
// After a refinement, any of the existing entries may have been replaced
// (if it is subsumed by the new entry created during refinement).
// For this reason, we start chasing the intervals from the start again.
lo = 0;
auto* e = m_units[v];
if (!e && !refine_viable(v, lo))
goto refined;
if (!e && !refine_viable(v, rational::one()))
goto refined;
if (!e)
return dd::find_t::multiple;
return find_t::multiple;
if (e->interval.is_full())
return dd::find_t::empty;
return find_t::empty;
entry* first = e;
entry* last = first->prev();
// quick check: last interval does not wrap around
// and has space for 2 unassigned values.
auto& max_value = s.var2pdd(v).max_value();
if (last->interval.lo_val() < last->interval.hi_val() &&
last->interval.hi_val() < max_value) {
lo = last->interval.hi_val();
@ -614,7 +638,7 @@ namespace polysat {
goto refined;
if (!refine_viable(v, max_value))
goto refined;
return dd::find_t::multiple;
return find_t::multiple;
}
// find lower bound
@ -629,7 +653,76 @@ namespace polysat {
while (e != first);
if (e->interval.currently_contains(lo))
return dd::find_t::empty;
return find_t::empty;
// find upper bound
hi = max_value;
e = last;
do {
if (!e->interval.currently_contains(hi))
break;
hi = e->interval.lo_val() - 1;
e = e->prev();
}
while (e != last);
if (!refine_viable(v, lo))
goto refined;
if (!refine_viable(v, hi))
goto refined;
if (lo == hi)
return find_t::singleton;
else
return find_t::multiple;
}
find_t viable::find_viable(pvar v, rational& lo) {
#if 1
rational hi;
// return query<query_t::find_viable>(v, lo, hi);
return query(query_t::find_viable, v, lo, hi);
#else
refined:
lo = 0;
auto* e = m_units[v];
if (!e && !refine_viable(v, lo))
goto refined;
if (!e && !refine_viable(v, rational::one()))
goto refined;
if (!e)
return find_t::multiple;
if (e->interval.is_full())
return find_t::empty;
entry* first = e;
entry* last = first->prev();
// quick check: last interval does not wrap around
// and has space for 2 unassigned values.
auto& max_value = s.var2pdd(v).max_value();
if (last->interval.lo_val() < last->interval.hi_val() &&
last->interval.hi_val() < max_value) {
lo = last->interval.hi_val();
if (!refine_viable(v, lo))
goto refined;
if (!refine_viable(v, max_value))
goto refined;
return find_t::multiple;
}
// find lower bound
if (last->interval.currently_contains(lo))
lo = last->interval.hi_val();
do {
if (!e->interval.currently_contains(lo))
break;
lo = e->interval.hi_val();
e = e->next();
}
while (e != first);
if (e->interval.currently_contains(lo))
return find_t::empty;
// find upper bound
rational hi = max_value;
@ -646,9 +739,10 @@ namespace polysat {
if (!refine_viable(v, hi))
goto refined;
if (lo == hi)
return dd::find_t::singleton;
return find_t::singleton;
else
return dd::find_t::multiple;
return find_t::multiple;
#endif
}
bool viable::resolve(pvar v, conflict& core) {
@ -853,7 +947,7 @@ namespace polysat {
return {};
}
dd::find_t viable_fallback::find_viable(pvar v, rational& out_val) {
find_t viable_fallback::find_viable(pvar v, rational& out_val) {
unsigned bit_width = s.m_size[v];
univariate_solver* us;
@ -880,14 +974,11 @@ namespace polysat {
case l_true:
out_val = us->model();
// we don't know whether the SMT instance has a unique solution
return dd::find_t::multiple;
return find_t::multiple;
case l_false:
return dd::find_t::empty;
return find_t::empty;
default:
// TODO: what should we do here? (SMT solver had resource-out ==> polysat should abort too?)
// can we pass polysat's resource limit to the univariate solver?
UNREACHABLE();
return dd::find_t::empty;
return find_t::resource_out;
}
}
@ -901,5 +992,20 @@ namespace polysat {
return cs;
}
std::ostream& operator<<(std::ostream& out, find_t x) {
switch (x) {
case find_t::empty:
return out << "empty";
case find_t::singleton:
return out << "singleton";
case find_t::multiple:
return out << "multiple";
case find_t::resource_out:
return out << "resource_out";
}
UNREACHABLE();
return out;
}
}

27
src/math/polysat/viable.h
View file

@ -32,13 +32,24 @@ namespace polysat {
class univariate_solver;
class univariate_solver_factory;
enum class find_t {
empty,
singleton,
multiple,
resource_out,
};
std::ostream& operator<<(std::ostream& out, find_t x);
class viable {
friend class test_fi;
solver& s;
forbidden_intervals m_forbidden_intervals;
struct entry final : public dll_base<entry>, public fi_record {};
struct entry final : public dll_base<entry>, public fi_record {
entry const* refined = nullptr;
};
enum class entry_kind { unit_e, equal_e, diseq_e };
ptr_vector<entry> m_alloc;
@ -65,6 +76,16 @@ namespace polysat {
void propagate(pvar v, rational const& val);
enum class query_t {
has_viable, // currently only used internally in resolve_viable
min_viable, // currently unused
max_viable, // currently unused
find_viable,
};
// template <query_t mode>
find_t query(query_t mode, pvar v, rational& out_lo, rational& out_hi);
public:
viable(solver& s);
@ -110,7 +131,7 @@ namespace polysat {
/**
* Find a next viable value for variable.
*/
dd::find_t find_viable(pvar v, rational & val);
find_t find_viable(pvar v, rational& out_val);
/**
* Retrieve the unsat core for v,
@ -253,7 +274,7 @@ namespace polysat {
bool check_constraints(assignment const& a, pvar v) { return !find_violated_constraint(a, v); }
signed_constraint find_violated_constraint(assignment const& a, pvar v);
dd::find_t find_viable(pvar v, rational& out_val);
find_t find_viable(pvar v, rational& out_val);
signed_constraints unsat_core(pvar v);
};

2
src/sat/smt/bv_polysat.cpp
View file

@ -218,6 +218,8 @@ namespace bv {
}
bool solver::polysat_diseq_eh(euf::th_eq const& ne) {
if (!use_polysat())
return false;
euf::theory_var v1 = ne.v1(), v2 = ne.v2();
pdd p = var2pdd(v1);
pdd q = var2pdd(v2);

3
src/test/polysat.cpp
View file

@ -1859,7 +1859,8 @@ void tst_polysat() {
// test_polysat::test_parity1b();
// test_polysat::test_parity2();
// test_polysat::test_parity3();
test_polysat::test_parity4();
// test_polysat::test_parity4();
// test_polysat::test_parity4(32);
test_polysat::test_parity4(256);
// test_polysat::test_ineq2();
// test_polysat::test_ineq_non_axiom4(32, 3); // stuck in viable refinement loop

110
src/test/viable.cpp
View file

@ -117,8 +117,8 @@ namespace polysat {
static void test_univariate() {
std::cout << "\ntest_univariate\n";
unsigned bw = 32;
rational modulus = rational::power_of_two(bw);
unsigned const bw = 32;
rational const modulus = rational::power_of_two(bw);
auto factory = mk_univariate_bitblast_factory();
auto solver = (*factory)(bw);
@ -182,6 +182,111 @@ namespace polysat {
std::cout << "status: " << solver->check() << "\n";
std::cout << "core: " << solver->unsat_core() << "\n";
}
static void test_univariate_minmax() {
std::cout << "\ntest_univariate_min\n";
unsigned const bw = 32;
auto factory = mk_univariate_bitblast_factory();
auto solver = (*factory)(bw);
vector<rational> lhs;
vector<rational> rhs;
rational min;
rational max;
solver->push();
// c0: 123 <= 2x + 10
lhs.clear();
lhs.push_back(rational(123));
rhs.clear();
rhs.push_back(rational(10));
rhs.push_back(rational(2));
solver->add_ule(lhs, rhs, false, 0);
std::cout << "status: " << solver->check() << "\n";
std::cout << "model: " << solver->model() << "\n";
VERIFY(solver->find_min(min));
std::cout << "find_min: " << min << "\n";
VERIFY(min == 57); // 57*2 + 10 = 124; 56*2 + 10 = 122
VERIFY(solver->find_max(max));
std::cout << "find_max: " << max << "\n";
solver->push();
solver->add_ugt_const(max, false, 5);
VERIFY(solver->check() == l_false);
solver->pop(1);
solver->push();
// c1: 127 <= x
lhs.clear();
lhs.push_back(rational(127));
rhs.clear();
rhs.push_back(rational(0));
rhs.push_back(rational(1));
solver->add_ule(lhs, rhs, false, 1);
std::cout << "status: " << solver->check() << "\n";
std::cout << "model: " << solver->model() << "\n";
VERIFY(solver->find_min(min));
std::cout << "find_min: " << min << "\n";
VERIFY(min == 127);
VERIFY(solver->find_max(max));
std::cout << "find_max: " << max << "\n";
solver->add_ugt_const(max, false, 5);
VERIFY(solver->check() == l_false);
solver->pop(1);
// c2: umul_ovfl(2, x)
lhs.clear();
lhs.push_back(rational(2));
rhs.clear();
rhs.push_back(rational(0));
rhs.push_back(rational(1));
solver->add_umul_ovfl(lhs, rhs, false, 2);
std::cout << "status: " << solver->check() << "\n";
std::cout << "model: " << solver->model() << "\n";
VERIFY(solver->find_min(min));
std::cout << "find_min: " << min << "\n";
solver->push();
solver->add_ult_const(min, false, 5);
VERIFY(solver->check() == l_false);
solver->pop(1);
VERIFY(solver->find_max(max));
std::cout << "find_max: " << max << "\n";
solver->add_ugt_const(max, false, 5);
VERIFY(solver->check() == l_false);
solver->pop(1);
// c3: umul_ovfl(2, x)
lhs.clear();
lhs.push_back(rational(2));
rhs.clear();
rhs.push_back(rational(0));
rhs.push_back(rational(1));
solver->add_umul_ovfl(lhs, rhs, false, 3);
std::cout << "status: " << solver->check() << "\n";
std::cout << "model: " << solver->model() << "\n";
VERIFY(solver->find_min(min));
std::cout << "find_min: " << min << "\n";
solver->push();
solver->add_ult_const(min, false, 5);
VERIFY(solver->check() == l_false);
solver->pop(1);
VERIFY(solver->find_max(max));
std::cout << "find_max: " << max << "\n";
solver->add_ugt_const(max, false, 5);
VERIFY(solver->check() == l_false);
}
}
@ -189,5 +294,6 @@ namespace polysat {
void tst_viable() {
polysat::test1();
polysat::test_univariate();
polysat::test_univariate_minmax();
polysat::test2(); // takes long
}