From eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 23 Aug 2019 16:59:41 -0500 Subject: [PATCH] Fixes for sygus regressions (#3219) --- src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 1 + src/theory/quantifiers/quant_split.cpp | 8 ++++++++ src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 6 +++++- 3 files changed, 14 insertions(+), 1 deletion(-) diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 6427b52d5..bc21cce81 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -353,6 +353,7 @@ CegHandledStatus CegInstantiator::isCbqiQuantPrefix(Node q, CegHandledStatus CegInstantiator::isCbqiQuant(Node q, QuantifiersEngine* qe) { + Assert(q.getKind() == FORALL); // compute attributes QAttributes qa; QuantAttributes::computeQuantAttributes(q, qa); diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 4e9441279..54708f6cb 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -33,6 +33,14 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){ void QuantDSplit::checkOwnership(Node q) { + // If q is non-standard (marked as sygus, quantifier elimination, etc.), then + // do no split it. + QAttributes qa; + QuantAttributes::computeQuantAttributes(q, qa); + if (!qa.isStandard()) + { + return; + } int max_index = -1; int max_score = -1; Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; diff --git a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp index 4289fc815..c3b9fc28b 100644 --- a/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp +++ b/src/theory/quantifiers/sygus/ce_guided_single_inv.cpp @@ -314,7 +314,11 @@ void CegSingleInv::finishInit(bool syntaxRestricted) Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv << std::endl; // check whether we can handle this quantified formula - CegHandledStatus status = CegInstantiator::isCbqiQuant(d_single_inv); + CegHandledStatus status = CEG_HANDLED; + if (d_single_inv.getKind() == FORALL) + { + status = CegInstantiator::isCbqiQuant(d_single_inv); + } Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl; if (status < CEG_HANDLED) { -- 2.30.2