diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 16:59:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-23 16:59:41 -0500 |
| commit | eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 (patch) | |
| tree | 06a70eee6db68dd0cf293e5973133f30947f3a14 /src | |
| parent | c11154240248592b5446f1de4743d78ed2fb97bd (diff) | |
Fixes for sygus regressions (#3219)
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/quantifiers/cegqi/ceg_instantiator.cpp | 1 | ||||
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 8 | ||||
| -rw-r--r-- | src/theory/quantifiers/sygus/ce_guided_single_inv.cpp | 6 |
3 files changed, 14 insertions, 1 deletions
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) { |