From c4370eb7e6a69c4f8b24dc3543aae6feef67cdd8 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Fri, 11 Mar 2022 18:06:32 +0100 Subject: [PATCH] univariate solver seems to work --- .../polysat/univariate/univariate_solver.cpp | 83 +++++++++++++------ .../polysat/univariate/univariate_solver.h | 18 +++- src/test/CMakeLists.txt | 2 +- src/test/viable.cpp | 74 ++++++++++++++++- 4 files changed, 143 insertions(+), 34 deletions(-) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp index 1f7588655..0c7b1a94f 100644 --- a/src/math/polysat/univariate/univariate_solver.cpp +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -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; scoped_ptr 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(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 { diff --git a/src/math/polysat/univariate/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h index 79398855a..962dacae5 100644 --- a/src/math/polysat/univariate/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -17,6 +17,7 @@ Author: --*/ #pragma once +#include #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; + + /// Coefficients of univariate polynomial, index == degree, + /// e.g., the vector [ c, b, a ] represents a*x^2 + b*x + c. using univariate = vector; 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; diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 56f9d53e2..61c58fb49 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -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}) diff --git a/src/test/viable.cpp b/src/test/viable.cpp index dceda0be6..c88f34902 100644 --- a/src/test/viable.cpp +++ b/src/test/viable.cpp @@ -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> 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 lhs; + vector 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(); -} \ No newline at end of file + // polysat::test2(); + polysat::test_univariate(); +}