mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-23 12:48:53 +00:00
Code Activity

Adding grounding of the current lemma

Browse source 
In addition to adding the necessary instance of a quantified lemma,
add its grounding over the global set of skolems.
This commit is contained in:
Arie Gurfinkel 2017-08-16 17:23:55 -04:00
parent e8befc072c
commit 135a4a765f
1 changed files with 8 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -379,8 +379,15 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child,
expr_ref_vector inst(m); expr_ref_vector inst(m);
expr* a = to_app(fmls.get(i))->get_arg(0); expr* a = to_app(fmls.get(i))->get_arg(0);
expr* l = to_app(fmls.get(i))->get_arg(1); expr* l = to_app(fmls.get(i))->get_arg(1);
if (get_context().use_instantiate()) { if (!lemma->is_ground() && get_context().use_instantiate()) {
expr_ref grnd_lemma(m);
app_ref_vector tmp(m);
lemma->mk_insts(inst, l); lemma->mk_insts(inst, l);
// -- take ground instance of the current lemma
ground_expr(to_quantifier(l)->get_expr(), grnd_lemma, tmp);
STRACE("spacer.expand-add",
tout << "Adding instance: " << mk_epp(grnd_lemma, m) << "\n";);
inst.push_back(grnd_lemma);
} }
for (unsigned j=0; j < inst.size(); j++) { for (unsigned j=0; j < inst.size(); j++) {
inst.set(j, m.mk_implies(a, inst.get(j))); inst.set(j, m.mk_implies(a, inst.get(j)));