mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-23 06:13:40 +00:00
Code Activity

improved implementation of is_qblocked()

Browse source 
Disabled by default. Has no effect if ran with the default set of
options where qlemmas=true  and instantiate=true
This commit is contained in:
Arie Gurfinkel 2017-08-17 17:51:54 -04:00
parent 371ba4fbc0
commit b8b3703511
1 changed files with 38 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -51,6 +51,7 @@ Notes:
#include "ast/rewriter/expr_safe_replace.h" #include "ast/rewriter/expr_safe_replace.h"
#include "ast/expr_abstract.h" #include "ast/expr_abstract.h"
#include "smt/smt_solver.h"
namespace spacer { namespace spacer {
// ---------------- // ----------------
@ -648,20 +649,44 @@ bool pred_transformer::is_blocked (pob &n, unsigned &uses_level)
return res == l_false; return res == l_false;
} }
bool pred_transformer::is_qblocked (pob &n)
{ bool pred_transformer::is_qblocked (pob &n) {
// XXX Trivial implementation to get us started // XXX currently disabled
smt::kernel solver (m, get_manager ().fparams2()); return false;
params_ref p;
p.set_bool("arith.ignore_int", true);
p.set_bool("array.weak", true);
p.set_bool("mbqi", false);
scoped_ptr<solver> s;
s = mk_smt_solver(m, p, symbol::null);
s->updt_params(p);
// XXX force parameters to be set
s->push();
s->pop(1);
expr_ref_vector frame_lemmas(m); expr_ref_vector frame_lemmas(m);
m_frames.get_frame_geq_lemmas (n.level (), frame_lemmas); m_frames.get_frame_geq_lemmas (n.level (), frame_lemmas);
// assert all lemmas // assert all lemmas
bool has_quant = false;
for (unsigned i = 0, sz = frame_lemmas.size (); i < sz; ++i) for (unsigned i = 0, sz = frame_lemmas.size (); i < sz; ++i)
{ solver.assert_expr(frame_lemmas.get(i)); } {
// assert cti has_quant = has_quant || is_quantifier(frame_lemmas.get(i));
solver.assert_expr (n.post ()); s->assert_expr(frame_lemmas.get(i));
lbool res = solver.check (); }
if (!has_quant) return false;
// assert cti
s->assert_expr(n.post());
lbool res = s->check_sat(0, 0);
// if (res == l_false) {
// expr_ref_vector core(m);
// solver->get_itp_core(core);
// expr_ref c(m);
// c = mk_and(core);
// STRACE("spacer.expand-add", tout << "core: " << mk_epp(c,m) << "\n";);
// }
return res == l_false; return res == l_false;
} }
@ -2939,6 +2964,11 @@ lbool context::expand_node(pob& n)
return l_false; return l_false;
} }
if (n.pt().is_qblocked(n)) {
STRACE("spacer.expand-add",
tout << "This pob can be blocked by instantiation\n";);
}
smt_params &fparams = m_pm.fparams(); smt_params &fparams = m_pm.fparams();
flet<bool> _arith_ignore_int_(fparams.m_arith_ignore_int, flet<bool> _arith_ignore_int_(fparams.m_arith_ignore_int,
m_weak_abs && n.weakness() < 1); m_weak_abs && n.weakness() < 1);