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

Replace smt::kernel with smt_solver

Browse source 
Replace all ad-hoc uses of smt::kernel with ad-hoc uses of smt_solver
This commit is contained in:
Arie Gurfinkel 2018-05-23 14:27:32 -07:00
parent df2e9d8fe2
commit 4b09cefb97
2 changed files with 23 additions and 21 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/muz/spacer/spacer_context.cpp
View file

@ -2256,9 +2256,10 @@ bool context::validate()
fv.reverse ();
tmp = m.mk_exists(fv.size(), fv.c_ptr(), names.c_ptr(), tmp);
}
smt::kernel solver(m, m_pm.fparams2());
solver.assert_expr(tmp);
lbool res = solver.check();
ref<solver> sol =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
sol->assert_expr(tmp);
lbool res = sol->check_sat(0, nullptr);
if (res != l_false) {
msg << "rule validation failed when checking: "
<< mk_pp(tmp, m);
@ -2648,7 +2649,8 @@ expr_ref context::get_ground_sat_answer()
{ cex.push_back(m.mk_const(preds[0])); }
// smt context to obtain local cexes
scoped_ptr<smt::kernel> cex_ctx = alloc (smt::kernel, m, m_pm.fparams2 ());
ref<solver> cex_ctx =
mk_smt_solver(m, params_ref::get_empty(), symbol::null);
model_evaluator_util mev (m);
// preorder traversal of the query derivation tree
@ -2689,7 +2691,7 @@ expr_ref context::get_ground_sat_answer()
}
cex_ctx->assert_expr (pt->transition ());
cex_ctx->assert_expr (pt->rule2tag (r));
lbool res = cex_ctx->check ();
lbool res = cex_ctx->check_sat(0, nullptr);
CTRACE("cex", res == l_false,
tout << "Cex fact: " << mk_pp(cex_fact, m) << "\n";
for (unsigned i = 0; i < u_tail_sz; i++)
@ -3624,10 +3626,9 @@ void context::reset_statistics()
bool context::check_invariant(unsigned lvl)
{
decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
for (; it != end; ++it) {
for (auto &entry : m_rels) {
checkpoint();
if (!check_invariant(lvl, it->m_key)) {
if (!check_invariant(lvl, entry.m_key)) {
return false;
}
}
@ -3636,7 +3637,7 @@ bool context::check_invariant(unsigned lvl)
bool context::check_invariant(unsigned lvl, func_decl* fn)
{
smt::kernel ctx(m, m_pm.fparams2());
ref<solver> ctx = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
pred_transformer& pt = *m_rels.find(fn);
expr_ref_vector conj(m);
expr_ref inv = pt.get_formulas(next_level(lvl), false);
@ -3644,9 +3645,10 @@ bool context::check_invariant(unsigned lvl, func_decl* fn)
pt.add_premises(m_rels, lvl, conj);
conj.push_back(m.mk_not(inv));
expr_ref fml(m.mk_and(conj.size(), conj.c_ptr()), m);
ctx.assert_expr(fml);
lbool result = ctx.check();
TRACE("spacer", tout << "Check invariant level: " << lvl << " " << result << "\n" << mk_pp(fml, m) << "\n";);
ctx->assert_expr(fml);
lbool result = ctx->check_sat(0, nullptr);
TRACE("spacer", tout << "Check invariant level: " << lvl << " " << result
<< "\n" << mk_pp(fml, m) << "\n";);
return result == l_false;
}

18
src/muz/spacer/spacer_generalizers.cpp
View file

@ -29,7 +29,7 @@ Revision History:
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/substitution/matcher.h"
#include "ast/expr_functors.h"
#include "smt/smt_solver.h"
namespace spacer {
void lemma_sanity_checker::operator()(lemma_ref &lemma) {
@ -249,17 +249,17 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
{ eqs.push_back(m.mk_eq(m.mk_const(vsymbs.get(i)),
m.mk_const(vsymbs.get(j)))); }
smt::kernel solver(m, m_ctx.get_manager().fparams2());
ref<solver> sol = mk_smt_solver(m, params_ref::get_empty(), symbol::null);
expr_ref_vector lits(m);
for (unsigned i = 0, core_sz = core.size(); i < core_sz; ++i) {
SASSERT(lits.size() == i);
solver.push();
solver.assert_expr(core.get(i));
sol->push();
sol->assert_expr(core.get(i));
for (unsigned j = 0, eqs_sz = eqs.size(); j < eqs_sz; ++j) {
solver.push();
solver.assert_expr(eqs.get(j));
lbool res = solver.check();
solver.pop(1);
sol->push();
sol->assert_expr(eqs.get(j));
lbool res = sol->check_sat(0, nullptr);
sol->pop(1);
if (res == l_false) {
TRACE("core_array_eq",
@ -269,7 +269,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma)
break;
}
}
solver.pop(1);
sol->pop(1);
if (lits.size() == i) { lits.push_back(core.get(i)); }
}