mirror of
https://github.com/Z3Prover/z3
synced 2025-04-22 00:26:38 +00:00
univariate solver seems to work
This commit is contained in:
Jakob Rath
parent
1de51da67e
commit
c4370eb7e6
4 changed files with 143 additions and 34 deletions
|
|
@ -20,26 +20,32 @@ Author:
|
|||
#include "sat/sat_solver/inc_sat_solver.h"
|
||||
#include "solver/solver.h"
|
||||
#include "util/util.h"
|
||||
#include "ast/ast.h"
|
||||
#include "ast/reg_decl_plugins.h"
|
||||
#include "ast/ast_smt2_pp.h"
|
||||
|
||||
|
||||
namespace polysat {
|
||||
|
||||
class univariate_bitblast_solver : public univariate_solver {
|
||||
// TODO: does it make sense to share m and bv between different solver instances?
|
||||
ast_manager m;
|
||||
bv_util bv;
|
||||
scoped_ptr<bv_util> bv;
|
||||
scoped_ptr<solver> s;
|
||||
unsigned bit_width;
|
||||
func_decl* x_decl;
|
||||
expr* x;
|
||||
|
||||
public:
|
||||
univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
|
||||
bv(m),
|
||||
bit_width(bit_width)
|
||||
{
|
||||
// m.register_plugin(symbol("bv"), alloc(bv_decl_plugin)); // this alone doesn't work
|
||||
reg_decl_plugins(m);
|
||||
bv = alloc(bv_util, m);
|
||||
s = mk_solver(m, params_ref::get_empty(), false, true, true, symbol::null);
|
||||
// auto s = bv.mk_sort(bit_width);
|
||||
// auto n = bv.mk_numeral(rational(123), bit_width);
|
||||
x_decl = m.mk_const_decl("x", bv.mk_sort(bit_width));
|
||||
x_decl = m.mk_const_decl("x", bv->mk_sort(bit_width));
|
||||
x = m.mk_const(x_decl);
|
||||
}
|
||||
|
||||
~univariate_bitblast_solver() override = default;
|
||||
|
|
@ -52,57 +58,80 @@ namespace polysat {
|
|||
s->pop(n);
|
||||
}
|
||||
|
||||
expr* mk_poly(univariate p) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return nullptr;
|
||||
expr* mk_numeral(rational const& r) const {
|
||||
return bv->mk_numeral(r, bit_width);
|
||||
}
|
||||
|
||||
void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
|
||||
expr* e = bv.mk_ule(mk_poly(lhs), mk_poly(rhs));
|
||||
// [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());
|
||||
} else {
|
||||
expr* e = mk_numeral(p.back());
|
||||
for (unsigned i = p.size() - 1; i-- > 0; ) {
|
||||
e = bv->mk_bv_mul(e, x);
|
||||
if (!p[i].is_zero())
|
||||
e = bv->mk_bv_add(e, mk_numeral(p[i]));
|
||||
}
|
||||
return e;
|
||||
}
|
||||
}
|
||||
|
||||
void add(expr* e, bool sign, dep_t dep) {
|
||||
if (sign)
|
||||
e = m.mk_not(e);
|
||||
// TODO: record dep, and pass second argument to assert_expr (for tracking in the unsat core)
|
||||
s->assert_expr(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";
|
||||
}
|
||||
|
||||
void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
void add_ule(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
|
||||
add(bv->mk_ule(mk_poly(lhs), mk_poly(rhs)), sign, dep);
|
||||
}
|
||||
|
||||
void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
void add_umul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
|
||||
add(bv->mk_bvumul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep);
|
||||
}
|
||||
|
||||
void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
void add_smul_ovfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
|
||||
add(bv->mk_bvsmul_no_ovfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep);
|
||||
}
|
||||
|
||||
void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) override {
|
||||
add(bv->mk_bvsmul_no_udfl(mk_poly(lhs), mk_poly(rhs)), !sign, dep);
|
||||
}
|
||||
|
||||
lbool check() override {
|
||||
// TODO: need to pass assumptions to get an unsat core?
|
||||
return s->check_sat();
|
||||
}
|
||||
|
||||
dep_vector unsat_core() override {
|
||||
SASSERT(s->status() == l_false);
|
||||
dep_vector deps;
|
||||
expr_ref_vector core(m);
|
||||
s->get_unsat_core(core);
|
||||
NOT_IMPLEMENTED_YET();
|
||||
return {};
|
||||
for (expr* a : core) {
|
||||
unsigned dep = to_app(a)->get_decl()->get_name().get_num();
|
||||
deps.push_back(dep);
|
||||
}
|
||||
SASSERT(deps.size() > 0);
|
||||
return deps;
|
||||
}
|
||||
|
||||
rational model() override {
|
||||
SASSERT(s->status() == l_true);
|
||||
model_ref model;
|
||||
s->get_model(model);
|
||||
expr* val_expr = model->get_const_interp(x_decl);
|
||||
SASSERT(val_expr->get_kind() == AST_APP);
|
||||
app* val = static_cast<app*>(val_expr);
|
||||
SASSERT(val->get_kind() == OP_BV_NUM);
|
||||
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();
|
||||
}
|
||||
|
||||
std::ostream& display(std::ostream& out) const override {
|
||||
return out << *s;
|
||||
}
|
||||
};
|
||||
|
||||
class univariate_bitblast_factory : public univariate_solver_factory {
|
||||
|
|
|
|||
|
|
@ -17,6 +17,7 @@ Author:
|
|||
--*/
|
||||
#pragma once
|
||||
|
||||
#include <ostream>
|
||||
#include "util/lbool.h"
|
||||
#include "util/rational.h"
|
||||
#include "util/vector.h"
|
||||
|
|
@ -29,6 +30,9 @@ namespace polysat {
|
|||
public:
|
||||
using dep_t = unsigned;
|
||||
using dep_vector = svector<dep_t>;
|
||||
|
||||
/// Coefficients of univariate polynomial, index == degree,
|
||||
/// e.g., the vector [ c, b, a ] represents a*x^2 + b*x + c.
|
||||
using univariate = vector<rational>;
|
||||
|
||||
virtual ~univariate_solver() = default;
|
||||
|
|
@ -40,13 +44,19 @@ namespace polysat {
|
|||
virtual dep_vector unsat_core() = 0;
|
||||
virtual rational model() = 0;
|
||||
|
||||
virtual void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
|
||||
virtual void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
|
||||
virtual void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 0;
|
||||
virtual void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) = 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;
|
||||
virtual void add_smul_udfl(univariate const& lhs, univariate const& rhs, bool sign, dep_t dep) = 0;
|
||||
// op constraints?
|
||||
|
||||
virtual std::ostream& display(std::ostream& out) const = 0;
|
||||
};
|
||||
|
||||
inline std::ostream& operator<<(std::ostream& out, univariate_solver& s) {
|
||||
return s.display(out);
|
||||
}
|
||||
|
||||
class univariate_solver_factory {
|
||||
public:
|
||||
virtual ~univariate_solver_factory() = default;
|
||||
|
|
|
|||
|
|
@ -3,7 +3,7 @@ add_subdirectory(lp)
|
|||
################################################################################
|
||||
# z3-test executable
|
||||
################################################################################
|
||||
set(z3_test_deps api fuzzing simplex polysat)
|
||||
set(z3_test_deps api fuzzing simplex polysat polysat_univariate_solver)
|
||||
z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps})
|
||||
set (z3_test_extra_object_files "")
|
||||
foreach (component ${z3_test_expanded_deps})
|
||||
|
|
|
|||
|
|
@ -1,6 +1,7 @@
|
|||
#include "math/polysat/log.h"
|
||||
#include "math/polysat/solver.h"
|
||||
#include "math/polysat/viable.h"
|
||||
#include "math/polysat/univariate/univariate_solver.h"
|
||||
|
||||
namespace polysat {
|
||||
|
||||
|
|
@ -113,11 +114,80 @@ namespace polysat {
|
|||
vector<std::pair<unsigned, unsigned>> intervals;
|
||||
test_intervals(3, intervals);
|
||||
}
|
||||
|
||||
static void test_univariate() {
|
||||
std::cout << "\ntest_univariate\n";
|
||||
unsigned bw = 32;
|
||||
rational modulus = rational::power_of_two(bw);
|
||||
auto factory = mk_univariate_bitblast_factory();
|
||||
auto solver = (*factory)(bw);
|
||||
|
||||
vector<rational> lhs;
|
||||
vector<rational> rhs;
|
||||
|
||||
// c0: 2x+10 <= 123
|
||||
lhs.clear();
|
||||
lhs.push_back(rational(10));
|
||||
lhs.push_back(rational(2));
|
||||
rhs.clear();
|
||||
rhs.push_back(rational(123));
|
||||
solver->add_ule(lhs, rhs, false, 0);
|
||||
std::cout << "status: " << solver->check() << "\n";
|
||||
std::cout << "model: " << solver->model() << "\n";
|
||||
|
||||
solver->push();
|
||||
|
||||
// c1: x*x == 16
|
||||
lhs.clear();
|
||||
lhs.push_back(modulus - 16);
|
||||
lhs.push_back(rational(0));
|
||||
lhs.push_back(rational(1));
|
||||
rhs.clear();
|
||||
solver->add_ule(lhs, rhs, false, 1);
|
||||
std::cout << "status: " << solver->check() << "\n";
|
||||
std::cout << "model: " << solver->model() << "\n";
|
||||
|
||||
solver->push();
|
||||
|
||||
// c2: x <= 1000
|
||||
lhs.clear();
|
||||
lhs.push_back(rational(0));
|
||||
lhs.push_back(rational(1));
|
||||
rhs.clear();
|
||||
rhs.push_back(rational(1000));
|
||||
solver->add_ule(lhs, rhs, false, 2);
|
||||
// std::cout << *solver << '\n';
|
||||
std::cout << "status: " << solver->check() << "\n";
|
||||
std::cout << "model: " << solver->model() << "\n";
|
||||
|
||||
solver->pop(2);
|
||||
|
||||
// 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";
|
||||
|
||||
// c4: 1000 > x
|
||||
lhs.clear();
|
||||
lhs.push_back(rational(1000));
|
||||
rhs.clear();
|
||||
rhs.push_back(rational(0));
|
||||
rhs.push_back(rational(1));
|
||||
solver->add_ule(lhs, rhs, true, 4);
|
||||
std::cout << "status: " << solver->check() << "\n";
|
||||
std::cout << "core: " << solver->unsat_core() << "\n";
|
||||
}
|
||||
}
|
||||
|
||||
|
||||
|
||||
void tst_viable() {
|
||||
polysat::test1();
|
||||
polysat::test2();
|
||||
}
|
||||
// polysat::test2();
|
||||
polysat::test_univariate();
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue