From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 10 May 2018 16:38:03 +0000 (-0500)
Subject: Fix priority of decisions for cegis unif (#1897)
X-Git-Tag: cvc5-1.0.0~5069
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=aef0e5ed90b1b8913b5c8c743cbcd012d5916ba7;p=cvc5.git

Fix priority of decisions for cegis unif (#1897)
---

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index a99e726b6..a5ab27bf3 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -266,7 +266,7 @@ Node CegisUnifEnumManager::getNextDecisionRequest(unsigned& priority)
   bool value;
   if (!d_qe->getValuation().hasSatValue(lit, value))
   {
-    priority = 0;
+    priority = 1;
     return lit;
   }
   else if (!value)
@@ -306,7 +306,22 @@ void CegisUnifEnumManager::incrementNumEnumerators()
         Node size_eu = nm->mkNode(DT_SIZE, eu);
         Node size_eu_prev = nm->mkNode(DT_SIZE, eu_prev);
         Node sym_break = nm->mkNode(GEQ, size_eu, size_eu_prev);
+        Trace("cegis-unif-enum-lemma")
+            << "CegisUnifEnum::lemma, enum sym break:" << sym_break << "\n";
         d_qe->getOutputChannel().lemma(sym_break);
+        // if the sygus datatype is interpreted as an infinite type
+        // (this should be the case for almost all examples)
+        if (!ct.isInterpretedFinite())
+        {
+          // it is disequal from all previous ones
+          for (const Node eui : ci.second.d_enums)
+          {
+            Node deq = eu.eqNode(eui).negate();
+            Trace("cegis-unif-enum-lemma")
+                << "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
+            d_qe->getOutputChannel().lemma(deq);
+          }
+        }
       }
       ci.second.d_enums.push_back(eu);
       d_tds->registerEnumerator(eu, d_null, d_parent);
@@ -353,7 +368,8 @@ void CegisUnifEnumManager::registerEvalPtAtSize(TypeNode ct,
     disj.push_back(ei.eqNode(itc->second.d_enums[i]));
   }
   Node lem = NodeManager::currentNM()->mkNode(OR, disj);
-  Trace("cegis-unif-enum") << "Adding lemma " << lem << "\n";
+  Trace("cegis-unif-enum-lemma")
+      << "CegisUnifEnum::lemma, domain:" << lem << "\n";
   d_qe->getOutputChannel().lemma(lem);
 }