Fixes for sygus regressions (#3219)

diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp
index 6427b52d51919ca2904e4d33eeb90afc5c746d0d..bc21cce81e525ede34928aae50a350a719bf4abc 100644 (file)
--- 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 4e9441279d509e7acbe566921607b0b8c5432150..54708f6cb45179e70a756a77f73dc1c996477f9a 100644 (file)
--- 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 4289fc815b81ef4069f45373588e90b4a8ede66f..c3b9fc28b50e7953398ac01ed4a45ab4090990dd 100644 (file)
--- 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)
   {