From 135a4a765fed0ccf7f391974e8303ee5751fd185 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 16 Aug 2017 17:23:55 -0400 Subject: [PATCH] Adding grounding of the current lemma In addition to adding the necessary instance of a quantified lemma, add its grounding over the global set of skolems. --- src/muz/spacer/spacer_context.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 7c4afa3f7..4968a44e4 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -379,8 +379,15 @@ void pred_transformer::add_lemma_from_child (pred_transformer& child, expr_ref_vector inst(m); expr* a = to_app(fmls.get(i))->get_arg(0); 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); + // -- 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++) { inst.set(j, m.mk_implies(a, inst.get(j)));