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

begin univariate solver impl

Browse source
This commit is contained in:
Jakob Rath 2022-03-10 17:58:37 +01:00
parent 78028bedae
commit 8b1f1d0e11
2 changed files with 31 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -26,11 +26,20 @@ namespace polysat {
class univariate_bitblast_solver : public univariate_solver { class univariate_bitblast_solver : public univariate_solver {
ast_manager m; ast_manager m;
bv_util bv;
scoped_ptr<solver> s; scoped_ptr<solver> s;
unsigned bit_width;
func_decl* x_decl;
public: public:
univariate_bitblast_solver(solver_factory& mk_solver) { univariate_bitblast_solver(solver_factory& mk_solver, unsigned bit_width) :
bv(m),
bit_width(bit_width)
{
s = mk_solver(m, params_ref::get_empty(), false, true, true, symbol::null); 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));
} }
~univariate_bitblast_solver() override = default; ~univariate_bitblast_solver() override = default;
@ -43,9 +52,17 @@ namespace polysat {
s->pop(n); s->pop(n);
} }
void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override { expr* mk_poly(univariate p) {
// s->assert_expr();
NOT_IMPLEMENTED_YET(); NOT_IMPLEMENTED_YET();
return nullptr;
}
void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
expr* e = bv.mk_ule(mk_poly(lhs), mk_poly(rhs));
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);
} }
void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override { void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {
@ -77,8 +94,14 @@ namespace polysat {
SASSERT(s->status() == l_true); SASSERT(s->status() == l_true);
model_ref model; model_ref model;
s->get_model(model); s->get_model(model);
NOT_IMPLEMENTED_YET(); expr* val_expr = model->get_const_interp(x_decl);
return {}; SASSERT(val_expr->get_kind() == AST_APP);
app* val = static_cast<app*>(val_expr);
SASSERT(val->get_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();
} }
}; };
@ -94,8 +117,8 @@ namespace polysat {
~univariate_bitblast_factory() override = default; ~univariate_bitblast_factory() override = default;
scoped_ptr<univariate_solver> operator()() override { scoped_ptr<univariate_solver> operator()(unsigned bit_width) override {
return alloc(univariate_bitblast_solver, *sf); return alloc(univariate_bitblast_solver, *sf, bit_width);
} }
}; };

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

@ -50,7 +50,7 @@ namespace polysat {
class univariate_solver_factory { class univariate_solver_factory {
public: public:
virtual ~univariate_solver_factory(); virtual ~univariate_solver_factory();
virtual scoped_ptr<univariate_solver> operator()() = 0; virtual scoped_ptr<univariate_solver> operator()(unsigned bit_width) = 0;
}; };
scoped_ptr<univariate_solver_factory> mk_univariate_bitblast_factory(); scoped_ptr<univariate_solver_factory> mk_univariate_bitblast_factory();