mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

univariate::find_min

Browse source
This commit is contained in:
Jakob Rath 2022-12-15 15:34:50 +01:00
parent 37536425f4
commit 31e0add966
3 changed files with 118 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -98,14 +98,14 @@ namespace polysat {
return mk_numeral(rational::zero());
}
else {
expr* e = mk_numeral(p.back());
expr* e = mk_numeral(p[0]);
expr* xpow = x;
for (unsigned i = p.size() - 1; i-- > 0; ) {
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)
if (i + 1 < p.size())
xpow = bv->mk_bv_mul(xpow, x);
}
return e;
@ -205,6 +205,34 @@ namespace polysat {
return p.get_rational();
}
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;
}
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;
}
std::ostream& display(std::ostream& out) const override {
return out << *s;
}

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

@ -41,9 +41,17 @@ 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;
// Precondition: check() returned l_true
// Returns false on resource out.
virtual bool find_min(rational& out_min) = 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 +73,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;
};

79
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,80 @@ namespace polysat {
std::cout << "status: " << solver->check() << "\n";
std::cout << "core: " << solver->unsat_core() << "\n";
}
static void test_univariate_min() {
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;
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
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);
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->add_ule_const(min - 1, false, 3);
VERIFY(solver->check() == l_false);
solver->pop(1);
// c4: 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, 4);
std::cout << "status: " << solver->check() << "\n";
std::cout << "model: " << solver->model() << "\n";
VERIFY(solver->find_min(min));
std::cout << "find_min: " << min << "\n";
solver->add_ule_const(min - 1, false, 5);
VERIFY(solver->check() == l_false);
}
}
@ -189,5 +263,6 @@ namespace polysat {
void tst_viable() {
polysat::test1();
polysat::test_univariate();
polysat::test_univariate_min();
polysat::test2(); // takes long
}