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

integrate intblast solver

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-10 13:00:43 -08:00
parent 9931c811ca
commit 09c2e0dd6e
4 changed files with 56 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

30
src/sat/smt/intblast_solver.cpp
View file

@ -78,6 +78,7 @@ namespace intblast {
literals.push_back(a);
}
m_core.reset();
m_solver = mk_smt2_solver(m, s.params(), symbol::null);
expr_ref_vector es(m);
@ -86,11 +87,23 @@ namespace intblast {
translate(es);
for (auto e : es)
m_solver->assert_expr(e);
for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi;
m_solver->assert_expr(a.mk_le(a.mk_int(0), v));
m_solver->assert_expr(a.mk_lt(v, a.mk_int(b)));
}
lbool r = m_solver->check_sat(0, nullptr);
lbool r = m_solver->check_sat(es);
if (r == l_false) {
expr_ref_vector core(m);
m_solver->get_unsat_core(core);
obj_map<expr, unsigned> e2index;
for (unsigned i = 0; i < es.size(); ++i)
e2index.insert(es.get(i), i);
for (auto e : core)
m_core.push_back(literals[e2index[e]]);
}
return r;
};
@ -290,11 +303,6 @@ namespace intblast {
}
for (unsigned i = 0; i < es.size(); ++i)
es[i] = translated[es.get(i)];
for (auto const& [src, vi] : m_vars) {
auto const& [v, b] = vi;
es.push_back(a.mk_le(a.mk_int(0), v));
es.push_back(a.mk_lt(v, a.mk_int(b)));
}
}
rational solver::get_value(expr* e) const {
@ -313,4 +321,8 @@ namespace intblast {
return val;
}
sat::literal_vector const& solver::unsat_core() {
return m_core;
}
}

3
src/sat/smt/intblast_solver.h
View file

@ -46,6 +46,7 @@ namespace intblast {
scoped_ptr<::solver> m_solver;
obj_map<expr, var_info> m_vars;
expr_ref_vector m_trail;
sat::literal_vector m_core;
@ -58,6 +59,8 @@ namespace intblast {
lbool check();
sat::literal_vector const& unsat_core();
rational get_value(expr* e) const;
};

30
src/sat/smt/polysat_solver.cpp
View file

@ -31,6 +31,8 @@ The result of polysat::core::check is one of:
#include "sat/smt/polysat/polysat_umul_ovfl.h"
namespace polysat {
solver::solver(euf::solver& ctx, theory_id id):
@ -38,6 +40,7 @@ namespace polysat {
bv(ctx.get_manager()),
m_autil(ctx.get_manager()),
m_core(*this),
m_intblast(ctx),
m_lemma(ctx.get_manager())
{
ctx.get_egraph().add_plugin(alloc(euf::bv_plugin, ctx.get_egraph()));
@ -56,7 +59,31 @@ namespace polysat {
}
sat::check_result solver::check() {
return m_core.check();
switch (m_core.check()) {
case sat::check_result::CR_DONE:
return sat::check_result::CR_DONE;
case sat::check_result::CR_CONTINUE:
return sat::check_result::CR_CONTINUE;
case sat::check_result::CR_GIVEUP: {
if (!m.inc())
return sat::check_result::CR_GIVEUP;
switch (m_intblast.check()) {
case l_true:
trail().push(value_trail(m_use_intblast_model));
m_use_intblast_model = true;
return sat::check_result::CR_DONE;
case l_false: {
auto core = m_intblast.unsat_core();
for (auto& lit : core)
lit.neg();
s().add_clause(core.size(), core.data(), sat::status::th(true, get_id(), nullptr));
return sat::check_result::CR_CONTINUE;
}
case l_undef:
return sat::check_result::CR_GIVEUP;
}
}
}
}
void solver::asserted(literal l) {
@ -136,6 +163,7 @@ namespace polysat {
unsigned num_scopes = s().scope_lvl() - m_lemma_level;
NOT_IMPLEMENTED_YET();
// s().pop_reinit(num_scopes);
sat::literal_vector lits;

4
src/sat/smt/polysat_solver.h
View file

@ -19,6 +19,7 @@ Author:
#include "sat/smt/sat_th.h"
#include "math/dd/dd_pdd.h"
#include "sat/smt/polysat/polysat_core.h"
#include "sat/smt/intblast_solver.h"
namespace euf {
class solver;
@ -57,7 +58,8 @@ namespace polysat {
arith_util m_autil;
stats m_stats;
core m_core;
polysat_proof m_proof;
intblast::solver m_intblast;
bool m_use_intblast_model = false;
vector<pdd> m_var2pdd; // theory_var 2 pdd
bool_vector m_var2pdd_valid; // valid flag