Update any-constant and normalization policies for sygus grammars (#3583)

10 files changed, 36 insertions, 29 deletions

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index 78ea5b22f..2d27878fd 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -79,7 +79,6 @@ bool Cegis::processInitialize(Node conj,
     Trace("cegis") << "...register enumerator " << candidates[i];
     // We use symbolic constants if we are doing repair constants or if the
     // grammar construction was not simple.
-    bool useSymCons = false;
     if (options::sygusRepairConst()
         || options::sygusGrammarConsMode()
                != options::SygusGrammarConsMode::SIMPLE)
@@ -89,15 +88,13 @@ bool Cegis::processInitialize(Node conj,
       SygusTypeInfo& cti = d_tds->getTypeInfo(ctn);
       if (cti.hasSubtermSymbolicCons())
       {
-        useSymCons = true;
         // remember that we are using symbolic constructors
         d_usingSymCons = true;
         Trace("cegis") << " (using symbolic constructors)";
       }
     }
     Trace("cegis") << std::endl;
-    d_tds->registerEnumerator(
-        candidates[i], candidates[i], d_parent, erole, useSymCons);
+    d_tds->registerEnumerator(candidates[i], candidates[i], d_parent, erole);
   }
   return true;
 }
diff --git a/src/theory/quantifiers/sygus/cegis_unif.cpp b/src/theory/quantifiers/sygus/cegis_unif.cpp
index 8812032ba..a76159b90 100644
--- a/src/theory/quantifiers/sygus/cegis_unif.cpp
+++ b/src/theory/quantifiers/sygus/cegis_unif.cpp
@@ -639,9 +639,7 @@ void CegisUnifEnumDecisionStrategy::setUpEnumerator(Node e,
   }
   Trace("cegis-unif-enum") << "* Registering new enumerator " << e
                            << " to strategy point " << si.d_pt << "\n";
-  bool useSymCons =
-      options::sygusGrammarConsMode() != options::SygusGrammarConsMode::SIMPLE;
-  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole, useSymCons);
+  d_tds->registerEnumerator(e, si.d_pt, d_parent, erole);
 }
 
 void CegisUnifEnumDecisionStrategy::registerEvalPts(
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 78fbc48f3..389cf34de 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -141,6 +141,9 @@ Node CegGrammarConstructor::process(Node q,
     {
       sfvl = preGrammarType.getDType().getSygusVarList();
       tn = preGrammarType;
+      // normalize type, if user-provided
+      SygusGrammarNorm sygus_norm(d_qe);
+      tn = sygus_norm.normalizeSygusType(tn, sfvl);
     }else{
       sfvl = getSygusVarList(sf);
       // check which arguments are irrelevant
@@ -167,10 +170,6 @@ Node CegGrammarConstructor::process(Node q,
     Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is "
                          << sfvl << std::endl;
 
-    // normalize type
-    SygusGrammarNorm sygus_norm(d_qe);
-    tn = sygus_norm.normalizeSygusType(tn, sfvl);
-
     std::map<Node, Node>::const_iterator itt = templates.find(sf);
     if( itt!=templates.end() ){
       Node templ = itt->second;
diff --git a/src/theory/quantifiers/sygus/sygus_pbe.cpp b/src/theory/quantifiers/sygus/sygus_pbe.cpp
index 474fdb5d8..5c0985f7e 100644
--- a/src/theory/quantifiers/sygus/sygus_pbe.cpp
+++ b/src/theory/quantifiers/sygus/sygus_pbe.cpp
@@ -235,7 +235,7 @@ bool SygusPbe::initialize(Node conj,
     for (const Node& e : d_candidate_to_enum[c])
     {
       TypeNode etn = e.getType();
-      d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL, false);
+      d_tds->registerEnumerator(e, c, d_parent, ROLE_ENUM_POOL);
       d_enum_to_candidate[e] = c;
       TNode te = e;
       // initialize static symmetry breaking lemmas for it
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.cpp b/src/theory/quantifiers/sygus/term_database_sygus.cpp
index 1fda55172..b096b2430 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.cpp
+++ b/src/theory/quantifiers/sygus/term_database_sygus.cpp
@@ -373,8 +373,7 @@ bool TermDbSygus::registerSygusType(TypeNode tn)
 void TermDbSygus::registerEnumerator(Node e,
                                      Node f,
                                      SynthConjecture* conj,
-                                     EnumeratorRole erole,
-                                     bool useSymbolicCons)
+                                     EnumeratorRole erole)
 {
   if (d_enum_to_conjecture.find(e) != d_enum_to_conjecture.end())
   {
@@ -391,7 +390,6 @@ void TermDbSygus::registerEnumerator(Node e,
 
   Trace("sygus-db") << "  registering symmetry breaking clauses..."
                     << std::endl;
-  d_enum_to_using_sym_cons[e] = useSymbolicCons;
   // depending on if we are using symbolic constructors, introduce symmetry
   // breaking lemma templates for each relevant subtype of the grammar
   SygusTypeInfo& eti = getTypeInfo(et);
@@ -409,13 +407,7 @@ void TermDbSygus::registerEnumerator(Node e,
     for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       bool isAnyC = static_cast<int>(i) == anyC;
-      if (isAnyC && !useSymbolicCons)
-      {
-        // if we are not using the any constant constructor
-        // do not use the symbolic constructor
-        rm_indices.push_back(i);
-      }
-      else if (anyC != -1 && !isAnyC && useSymbolicCons)
+      if (anyC != -1 && !isAnyC)
       {
         // if we are using the any constant constructor, do not use any
         // concrete constant
diff --git a/src/theory/quantifiers/sygus/term_database_sygus.h b/src/theory/quantifiers/sygus/term_database_sygus.h
index 6d328ddca..b9f8bf987 100644
--- a/src/theory/quantifiers/sygus/term_database_sygus.h
+++ b/src/theory/quantifiers/sygus/term_database_sygus.h
@@ -103,17 +103,13 @@ class TermDbSygus {
    * and not x2-x1 will be generated, assuming x1 and x2 are in the same
    * "subclass", see getSubclassForVar).
    *
-   * useSymbolicCons : whether we want model values for e to include symbolic
-   * constructors like the "any constant" variable.
-   *
    * An "active guard" may be allocated by this method for e based on erole
    * and the policies for active generation.
    */
   void registerEnumerator(Node e,
                           Node f,
                           SynthConjecture* conj,
-                          EnumeratorRole erole,
-                          bool useSymbolicCons = false);
+                          EnumeratorRole erole);
   /** is e an enumerator registered with this class? */
   bool isEnumerator(Node e) const;
   /** return the conjecture e is associated with */
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index b42d586c8..a53201e3e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1762,6 +1762,7 @@ set(regress_1_tests
   regress1/sygus/issue3498.smt2
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
+  regress1/sygus/issue3580.sy
   regress1/sygus/large-const-simp.sy
   regress1/sygus/let-bug-simp.sy
   regress1/sygus/list-head-x.sy
diff --git a/test/regress/regress1/sygus/coeff-solve-inv.sy b/test/regress/regress1/sygus/coeff-solve-inv.sy
index edfcd6089..ed4689fe9 100644
--- a/test/regress/regress1/sygus/coeff-solve-inv.sy
+++ b/test/regress/regress1/sygus/coeff-solve-inv.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const --lang=sygus2 --sygus-grammar-cons=any-const
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (y Int)) )
diff --git a/test/regress/regress1/sygus/issue3580.sy b/test/regress/regress1/sygus/issue3580.sy
new file mode 100644
index 000000000..9da07407a
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3580.sy
@@ -0,0 +1,24 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-active-gen=none --lang=sygus2
+(set-logic ALL)
+(synth-fun f 
+	() Bool 
+	((B Bool)) 
+	(
+		(B Bool (true))
+	)
+)
+(synth-fun g 
+	((r Int)) Bool 
+	((B Bool) (I Int) (IConst Int)) 
+	(
+		(B Bool ((= I I) (=> B B)))
+		(I Int (r 0 (mod I IConst)))
+		(IConst Int ((Constant Int)))
+	)
+) 
+(constraint (g 0))
+(constraint (not (g 1)))
+(constraint (g 2))
+(constraint f)
+(check-synth)
diff --git a/test/regress/regress2/sygus/ex23.sy b/test/regress/regress2/sygus/ex23.sy
index c19b2ff42..29e8527dc 100644
--- a/test/regress/regress2/sygus/ex23.sy
+++ b/test/regress/regress2/sygus/ex23.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-repair-const
+; COMMAND-LINE: --sygus-out=status --sygus-repair-const --sygus-grammar-cons=any-const
 (set-logic LIA)
 
 (synth-inv inv-f ((y Int) (z Int) (c Int)))