mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

ground lemmas during propagation when qlemmas are disabled

Browse source 
When asserting quantified lemmas are disabled, ground a lemma
explicitly during propagate to make sure that it is ground using our
local set of skolem constants.
This commit is contained in:
Arie Gurfinkel 2017-08-04 16:12:32 -04:00
parent 5da0753269
commit 9f0eb367b1
2 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -769,7 +769,7 @@ bool pred_transformer::is_invariant(unsigned level, expr* lemma,
expr_ref_vector conj(m), aux(m);
expr_ref glemma(m);
if (false && is_quantifier(lemma)) {
if (!get_context().use_qlemmas() && is_quantifier(lemma)) {
SASSERT(is_forall(lemma));
app_ref_vector tmp(m);
ground_expr(to_quantifier(lemma)->get_expr (), glemma, tmp);

28
src/muz/spacer/spacer_util.cpp
View file

@ -1166,21 +1166,21 @@ void mk_epp::rw(expr *e, expr_ref &out)
arw(e, out);
}
void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars)
{
expr_free_vars fv;
ast_manager &m = out.get_manager ();
fv (e);
if (vars.size () < fv.size ())
{ vars.resize(fv.size()); }
for (unsigned i = 0, sz = fv.size (); i < sz; ++i) {
SASSERT (fv[i]);
std::string str = "zk!" + datalog::to_string(sz - 1 - i);
vars [i] = m.mk_const (symbol(str.c_str()), fv [i]);
}
var_subst vs(m);
vs (e, vars.size (), (expr**) vars.c_ptr (), out);
void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
expr_free_vars fv;
ast_manager &m = out.get_manager();
fv(e);
if (vars.size() < fv.size()) {
vars.resize(fv.size());
}
for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
vars[i] = mk_zk_const(m, i, s);
var_subst vs(m, false);
vs(e, vars.size(), (expr * *) vars.c_ptr(), out);
}
}
struct index_term_finder {