Option to force return values of Bool functions to be constant in CegisUnif (#1930)

1 files changed, 4 insertions, 19 deletions

diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 9ae598f83..692055b87 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -37,7 +37,6 @@ bool CegisUnif::processInitialize(Node n,
                                   const std::vector<Node>& candidates,
                                   std::vector<Node>& lemmas)
 {
-  Trace("cegis-unif") << "Initialize CegisUnif : " << n << std::endl;
   // list of strategy points for unification candidates
   std::vector<Node> unif_candidate_pts;
   // map from strategy points to their conditions
@@ -453,24 +452,10 @@ void CegisUnifEnumManager::incrementNumEnumerators()
                                  << " to strategy point " << ci.second.d_pt
                                  << "\n";
         d_tds->registerEnumerator(e, ci.second.d_pt, d_parent);
-        // if the sygus datatype is interpreted as an infinite type
-        // (this should be the case for almost all examples)
-        TypeNode et = e.getType();
-        if (!et.isInterpretedFinite())
-        {
-          // it is disequal from all previous ones
-          for (const Node& ei : ci.second.d_enums[index])
-          {
-            if (ei == e)
-            {
-              continue;
-            }
-            Node deq = e.eqNode(ei).negate();
-            Trace("cegis-unif-enum-lemma")
-                << "CegisUnifEnum::lemma, enum deq:" << deq << "\n";
-            d_qe->getOutputChannel().lemma(deq);
-          }
-        }
+        // TODO symmetry breaking for making
+        //   e distinct from ei : (ci.second.d_enums[index] \ {e})
+        // if its respective type has had at least
+        // ci.second.d_enums[index].size() distinct values enumerated
       }
     }
     // register the evaluation points at the new value