From 38e1a8bd1d8ad2e4fab4c89c46bfab88223762eb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 15 Aug 2019 10:00:51 -0500 Subject: [PATCH] Fix for when to apply single invocation techniques (#3193) --- .../sygus/ce_guided_single_inv.cpp | 26 ++++++++++++------- 1 file changed, 16 insertions(+), 10 deletions(-) diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 59c463b96..fcec12d39 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -297,17 +297,8 @@ void CegSingleInv::finishInit(bool syntaxRestricted) if (!func_vars.empty()) { Node pbvl = nm->mkNode(BOUND_VAR_LIST, func_vars); - // mark as quantifier elimination to ensure its structure is preserved - Node n_attr = - nm->mkSkolem("qe_si", - nm->booleanType(), - "Auxiliary variable for qe attr for single invocation."); - QuantElimAttribute qea; - n_attr.setAttribute(qea, true); - n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); - n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); // make the single invocation conjecture - d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv, n_attr); + d_single_inv = nm->mkNode(FORALL, pbvl, d_single_inv); } // now, introduce the skolems std::vector sivars; @@ -326,6 +317,7 @@ void CegSingleInv::finishInit(bool syntaxRestricted) << std::endl; // check whether we can handle this quantified formula CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv); + Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl; if (status < CEG_HANDLED) { Trace("cegqi-si") << "...do not invoke single invocation techniques since " @@ -335,6 +327,20 @@ void CegSingleInv::finishInit(bool syntaxRestricted) d_single_invocation = false; d_single_inv = Node::null(); } + // If we succeeded, mark the quantified formula with the quantifier + // elimination attribute to ensure its structure is preserved + if (!d_single_inv.isNull() && d_single_inv.getKind() == FORALL) + { + Node n_attr = + nm->mkSkolem("qe_si", + nm->booleanType(), + "Auxiliary variable for qe attr for single invocation."); + QuantElimAttribute qea; + n_attr.setAttribute(qea, true); + n_attr = nm->mkNode(INST_ATTRIBUTE, n_attr); + n_attr = nm->mkNode(INST_PATTERN_LIST, n_attr); + d_single_inv = nm->mkNode(FORALL, d_single_inv[0], d_single_inv[1], n_attr); + } } bool CegSingleInv::solve() { -- 2.30.2