Fix degenerate case of sygus grammar construction for 0-argument Bools (#2260)

3 files changed, 50 insertions, 33 deletions

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index deea1c261..d6a6d0944 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -392,6 +392,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     std::vector<CVC4::Datatype>& datatypes,
     std::set<Type>& unres)
 {
+  NodeManager* nm = NodeManager::currentNM();
   Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
                              << range << std::endl;
   // collect the variables
@@ -584,9 +585,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }else{
       std::stringstream sserr;
       sserr << "No implementation for default Sygus grammar of type " << types[i] << std::endl;
-      //AlwaysAssert( false, sserr.str() );
-      // FIXME
-      AlwaysAssert( false );
+      throw LogicException(sserr.str());
     }
     //add for all selectors to this type
     if( !sels[types[i]].empty() ){
@@ -628,7 +627,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     }
   }
 
-  //make Boolean type
+  //------ make Boolean type
   TypeNode btype = NodeManager::currentNM()->booleanType();
   datatypes.push_back(Datatype(dbname));
   ops.push_back(std::vector<Expr>());
@@ -667,35 +666,6 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
     pcs.push_back(nullptr);
     weights.push_back(-1);
   }
-  //add operators
-  for (unsigned i = 0; i < 4; i++)
-  {
-    CVC4::Kind k = i == 0
-                       ? kind::NOT
-                       : (i == 1 ? kind::AND : (i == 2 ? kind::OR : kind::ITE));
-    // TODO #1935 ITEs are added to Boolean grammars so that we can infer
-    // unification strategies. We can do away with this if we can infer
-    // unification strategies from and/or/not
-    if (k == ITE && !options::sygusUnif())
-    {
-      continue;
-    }
-    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
-    ops.back().push_back(NodeManager::currentNM()->operatorOf(k).toExpr());
-    cnames.push_back(kind::kindToString(k));
-    cargs.push_back( std::vector< CVC4::Type >() );
-    cargs.back().push_back(unres_bt);
-    if (k != kind::NOT)
-    {
-      cargs.back().push_back(unres_bt);
-      if (k == kind::ITE)
-      {
-        cargs.back().push_back(unres_bt);
-      }
-    }
-    pcs.push_back(nullptr);
-    weights.push_back(-1);
-  }
   //add predicates for types
   for( unsigned i=0; i<types.size(); i++ ){
     Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
@@ -738,6 +708,37 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       }
     }
   }
+  // add Boolean connectives, if not in a degenerate case of (recursively)
+  // having only constant constructors
+  if (ops.back().size() > consts.size())
+  {
+    for (unsigned i = 0; i < 4; i++)
+    {
+      Kind k = i == 0 ? NOT : (i == 1 ? AND : (i == 2 ? OR : ITE));
+      // TODO #1935 ITEs are added to Boolean grammars so that we can infer
+      // unification strategies. We can do away with this if we can infer
+      // unification strategies from and/or/not
+      if (k == ITE && !options::sygusUnif())
+      {
+        continue;
+      }
+      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
+      ops.back().push_back(nm->operatorOf(k).toExpr());
+      cnames.push_back(kindToString(k));
+      cargs.push_back(std::vector<CVC4::Type>());
+      cargs.back().push_back(unres_bt);
+      if (k != NOT)
+      {
+        cargs.back().push_back(unres_bt);
+        if (k == ITE)
+        {
+          cargs.back().push_back(unres_bt);
+        }
+      }
+      pcs.push_back(nullptr);
+      weights.push_back(-1);
+    }
+  }
   if( range==btype ){
     startIndex = datatypes.size()-1;
   }
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index 6cbdfee26..b8479475f 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1508,6 +1508,7 @@ REG1_TESTS = \
 	regress1/sygus/clock-inc-tuple.sy \
 	regress1/sygus/commutative.sy \
 	regress1/sygus/constant.sy \
+	regress1/sygus/constant-dec-tree-bug.sy \
 	regress1/sygus/constant-ite-bv.sy \
 	regress1/sygus/crci-ssb-unk.sy \
 	regress1/sygus/crcy-si-rcons.sy \
diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
new file mode 100644
index 000000000..15df2d507
--- /dev/null
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -0,0 +1,15 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status --sygus-unif
+
+(set-logic SAT)
+(synth-fun u ((x Int)) Int)
+(synth-fun f () Bool)
+(synth-fun g () Bool)
+(synth-fun h () Bool)
+
+(constraint (= (u 3) (+ (u 2) 2)))
+(constraint f)
+(constraint (not g))
+(constraint h)
+
+(check-synth)