mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 00:26:38 +00:00
Code Activity

use solver_factory

Browse source
This commit is contained in:
Jakob Rath 2022-03-10 16:57:08 +01:00
parent 4a86c3fb67
commit 78028bedae
2 changed files with 28 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -29,11 +29,8 @@ namespace polysat {
scoped_ptr<solver> 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_inc_sat_solver(m, params_ref::get_empty());
univariate_bitblast_solver(solver_factory& mk_solver) {
s = mk_solver(m, params_ref::get_empty(), false, true, true, symbol::null);
}
~univariate_bitblast_solver() override = default;
@ -85,7 +82,24 @@ namespace polysat {
}
};
scoped_ptr<univariate_solver> mk_univariate_bitblast_solver() {
return alloc(univariate_bitblast_solver);
class univariate_bitblast_factory : public univariate_solver_factory {
symbol qf_bv;
scoped_ptr<solver_factory> sf;
public:
univariate_bitblast_factory() :
qf_bv("QF_BV") {
sf = mk_smt_strategic_solver_factory(qf_bv);
}
~univariate_bitblast_factory() override = default;
scoped_ptr<univariate_solver> operator()() override {
return alloc(univariate_bitblast_solver, *sf);
}
};
scoped_ptr<univariate_solver_factory> mk_univariate_bitblast_factory() {
return alloc(univariate_bitblast_factory);
}
}

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

@ -47,6 +47,12 @@ namespace polysat {
// op constraints?
};
scoped_ptr<univariate_solver> mk_univariate_bitblast_solver();
class univariate_solver_factory {
public:
virtual ~univariate_solver_factory();
virtual scoped_ptr<univariate_solver> operator()() = 0;
};
scoped_ptr<univariate_solver_factory> mk_univariate_bitblast_factory();
}