Implement option to turn off symmetry breaking for basic enumerators (#2686)

Improves the existing implementation for sygus-active-gen=basic.

diff --git a/src/theory/quantifiers/sygus/sygus_enumerator.cpp b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
index 61ab9007a11ada6486d1a446ff31b27afba14043..a39c9e958341a3e36e5e491d4723f13b4b35f015 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_enumerator.cpp
+++ b/src/theory/quantifiers/sygus/sygus_enumerator.cpp
@@ -241,33 +241,36 @@ bool SygusEnumerator::TermCache::addTerm(Node n)
     d_terms.push_back(n);
     return true;
   }
-  Node bn = d_tds->sygusToBuiltin(n);
-  Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
-  // must be unique up to rewriting
-  if (d_bterms.find(bnr) != d_bterms.end())
+  if (options::sygusSymBreakDynamic())
   {
-    Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
-    return false;
-  }
-  // if we are doing PBE symmetry breaking
-  if (d_pbe != nullptr)
-  {
-    // Is it equivalent under examples?
-    Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
-    if (!bne.isNull())
+    Node bn = d_tds->sygusToBuiltin(n);
+    Node bnr = d_tds->getExtRewriter()->extendedRewrite(bn);
+    // must be unique up to rewriting
+    if (d_bterms.find(bnr) != d_bterms.end())
+    {
+      Trace("sygus-enum-exc") << "Exclude: " << bn << std::endl;
+      return false;
+    }
+    // if we are doing PBE symmetry breaking
+    if (d_pbe != nullptr)
     {
-      if (bnr != bne)
+      // Is it equivalent under examples?
+      Node bne = d_pbe->addSearchVal(d_tn, d_enum, bnr);
+      if (!bne.isNull())
       {
-        Trace("sygus-enum-exc") << "Exclude (by examples): " << bn
-                                << ", since we already have " << bne
-                                << "!=" << bnr << std::endl;
-        return false;
+        if (bnr != bne)
+        {
+          Trace("sygus-enum-exc") << "Exclude (by examples): " << bn
+                                  << ", since we already have " << bne
+                                  << "!=" << bnr << std::endl;
+          return false;
+        }
       }
     }
+    Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
+    d_bterms.insert(bnr);
   }
-  Trace("sygus-enum-terms") << "tc(" << d_tn << "): term " << bn << std::endl;
   d_terms.push_back(n);
-  d_bterms.insert(bnr);
   return true;
 }
 void SygusEnumerator::TermCache::pushEnumSizeIndex()

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.cpp b/src/theory/quantifiers/sygus/synth_conjecture.cpp
index 21079aedc235f5115ceb2319641f657236382f13..e668b22061f7964a30b7e42b946353d68647ea79 100644 (file)
--- a/src/theory/quantifiers/sygus/synth_conjecture.cpp
+++ b/src/theory/quantifiers/sygus/synth_conjecture.cpp
@@ -705,17 +705,17 @@ class EnumValGeneratorBasic : public EnumValGenerator
     }
     Node next = *d_te;
     ++d_te;
-    Node nextb = d_tds->sygusToBuiltin(next);
     if (options::sygusSymBreakDynamic())
     {
+      Node nextb = d_tds->sygusToBuiltin(next);
       nextb = d_tds->getExtRewriter()->extendedRewrite(nextb);
-    }
-    if (d_cache.find(nextb) == d_cache.end())
-    {
+      if (d_cache.find(nextb) != d_cache.end())
+      {
+        return getNext();
+      }
       d_cache.insert(nextb);
-      return next;
     }
-    return getNext();
+    return next;
   }
 
  private: