From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 23 Aug 2019 21:59:41 +0000 (-0500)
Subject:  Fixes for sygus regressions (#3219)
X-Git-Tag: cvc5-1.0.0~3995
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5;p=cvc5.git

 Fixes for sygus regressions (#3219)
---

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)
   {