diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 355277aef..f4c1c7219 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -42,6 +42,7 @@ add_subdirectory(math/simplex) add_subdirectory(math/interval) add_subdirectory(math/bigfix) add_subdirectory(math/polysat) +add_subdirectory(math/polysat/univariate) add_subdirectory(math/automata) add_subdirectory(math/realclosure) add_subdirectory(math/subpaving) diff --git a/src/math/polysat/solver.h b/src/math/polysat/solver.h index 4b4832cc2..468a77b97 100644 --- a/src/math/polysat/solver.h +++ b/src/math/polysat/solver.h @@ -35,7 +35,6 @@ Author: #include "math/polysat/trail.h" #include "math/polysat/viable.h" #include "math/polysat/log.h" -#include "math/polysat/univariate_solver.h" diff --git a/src/math/polysat/univariate/CMakeLists.txt b/src/math/polysat/univariate/CMakeLists.txt new file mode 100644 index 000000000..29f25f2c6 --- /dev/null +++ b/src/math/polysat/univariate/CMakeLists.txt @@ -0,0 +1,4 @@ +z3_add_component(polysat_univariate_solver + SOURCES + univariate_solver.cpp +) diff --git a/src/math/polysat/univariate/univariate_solver.cpp b/src/math/polysat/univariate/univariate_solver.cpp new file mode 100644 index 000000000..1f5fa5410 --- /dev/null +++ b/src/math/polysat/univariate/univariate_solver.cpp @@ -0,0 +1,90 @@ +/*++ +Copyright (c) 2022 Microsoft Corporation + +Module Name: + + polysat univariate solver + +Abstract: + + Solve univariate constraints for polysat using bitblasting + +Author: + + Nikolaj Bjorner (nbjorner) 2022-03-10 + Jakob Rath 2022-03-10 + +--*/ + +#include "math/polysat/univariate/univariate_solver.h" +#include "solver/solver.h" +#include "util/util.h" + + +namespace polysat { + + class univariate_bitblast_solver : public univariate_solver { + ast_manager m; + scoped_ptr s; + + public: + univariate_bitblast_solver() { + NOT_IMPLEMENTED_YET(); + // which concrete solver do we want here? + // need to set params to enable model and unsat core generation; and bit blasting? + s = mk_smt2_solver(m, params_ref::get_empty()); + } + + ~univariate_bitblast_solver() override = default; + + void push() override { + s->push(); + } + + void pop(unsigned n) override { + s->pop(n); + } + + void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override { + // s->assert_expr(); + NOT_IMPLEMENTED_YET(); + } + + void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override { + NOT_IMPLEMENTED_YET(); + } + + void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override { + NOT_IMPLEMENTED_YET(); + } + + void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override { + NOT_IMPLEMENTED_YET(); + } + + 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); + expr_ref_vector core(m); + s->get_unsat_core(core); + NOT_IMPLEMENTED_YET(); + return {}; + } + + rational model() override { + SASSERT(s->status() == l_true); + model_ref model; + s->get_model(model); + NOT_IMPLEMENTED_YET(); + return {}; + } + }; + + scoped_ptr mk_univariate_bitblast_solver() { + return alloc(univariate_bitblast_solver); + } +} diff --git a/src/math/polysat/univariate_solver.h b/src/math/polysat/univariate/univariate_solver.h similarity index 84% rename from src/math/polysat/univariate_solver.h rename to src/math/polysat/univariate/univariate_solver.h index 87d1fe94f..e94815935 100644 --- a/src/math/polysat/univariate_solver.h +++ b/src/math/polysat/univariate/univariate_solver.h @@ -1,5 +1,5 @@ /*++ -Copyright (c) 2021 Microsoft Corporation +Copyright (c) 2022 Microsoft Corporation Module Name: @@ -47,10 +47,6 @@ namespace polysat { // op constraints? }; - class univariate_solver_factory { - public: - virtual ~univariate_solver_factory() = default; - virtual scoped_ptr create() = 0; - }; + scoped_ptr mk_univariate_bitblast_solver(); } diff --git a/src/math/polysat/viable.h b/src/math/polysat/viable.h index 9cc01a214..ecee866f7 100644 --- a/src/math/polysat/viable.h +++ b/src/math/polysat/viable.h @@ -23,7 +23,7 @@ Author: #include "math/polysat/types.h" #include "math/polysat/conflict.h" #include "math/polysat/constraint.h" -#include "math/polysat/univariate_solver.h" +#include "math/polysat/univariate/univariate_solver.h" namespace polysat { @@ -33,7 +33,6 @@ namespace polysat { friend class test_fi; solver& s; - scoped_ptr m_univariate_solver_factory; struct entry : public dll_base, public fi_record { entry() : fi_record({ eval_interval::full(), {}, {}, rational::one()}) {} diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 405d4e55c..7d05d97ab 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -25,34 +25,9 @@ Notes: #include "sat/smt/bv_solver.h" #include "sat/smt/euf_solver.h" #include "math/polysat/solver.h" -#include "math/polysat/univariate_solver.h" namespace bv { - class univariate_bitblast_solver : public polysat::univariate_solver { - public: - univariate_bitblast_solver() {}; - ~univariate_bitblast_solver() override = default; - void push() override {} - void pop(unsigned n) override {} - lbool check() override { return l_undef; } - dep_vector unsat_core() override { return {}; } - rational model() override { return {}; } - void add_ule(univariate lhs, univariate rhs, bool sign, dep_t dep) override {} - void add_umul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {} - void add_smul_ovfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {} - void add_smul_udfl(univariate lhs, univariate rhs, bool sign, dep_t dep) override {} - }; - - class univariate_bitblast_factory : public polysat::univariate_solver_factory { - public: - ~univariate_bitblast_factory() override = default; - scoped_ptr create() override { - return alloc(univariate_bitblast_solver); - } - }; - - typedef polysat::pdd pdd; void solver::internalize_polysat(app* a) {