Use default consts when not using any const during grammar normalization (#3807)

Fixes #3802.

If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
index b2e7d268184765262bc2b5cfb803f29a6309ce5f..f00fd0092fa2014de60a20eadb378a0b3a7d30d7 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_norm.cpp
@@ -23,6 +23,7 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/datatypes/theory_datatypes_utils.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 #include "theory/quantifiers/sygus/sygus_grammar_red.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -557,6 +558,19 @@ TypeNode SygusGrammarNorm::normalizeSygusRec(TypeNode tn,
       // same level as constants.
       to.d_sdt.addAnyConstantConstructor(dtn);
     }
+    else
+    {
+      // add default constant constructors
+      std::vector<Node> ops;
+      CegGrammarConstructor::mkSygusConstantsForType(sygus_type, ops);
+      for (const Node& op : ops)
+      {
+        std::stringstream ss;
+        ss << op;
+        std::vector<TypeNode> ctypes;
+        to.d_sdt.addConstructor(op, ss.str(), ctypes);
+      }
+    }
   }
 
   /* Determine normalization transformation based on sygus type and given

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 00faecedd0ac376138ca37c8273a6e46dd5d49d6..3fe4321d085812647c4800251b11756c37d6d8ce 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1823,6 +1823,7 @@ set(regress_1_tests
   regress1/sygus/issue3644.smt2
   regress1/sygus/issue3648.smt2
   regress1/sygus/issue3649.sy
+  regress1/sygus/issue3802-default-consts.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/issue3802-default-consts.sy b/test/regress/regress1/sygus/issue3802-default-consts.sy
new file mode 100644 (file)
index 0000000..10daee6
--- /dev/null
+++ b/test/regress/regress1/sygus/issue3802-default-consts.sy
@@ -0,0 +1,21 @@
+; EXPECT: unsat
+; COMMAND-LINE: --sygus-out=status
+(set-logic ALL)
+(synth-fun f 
+       () Bool
+       ((B Bool))
+       (
+               (B Bool ((Constant Bool)))
+       )
+)
+(synth-fun g 
+       ((x0 Int) (r Int)) Bool 
+       ((B Bool) (I Int)) 
+       (
+               (B Bool ((= I I))) 
+               (I Int (x0 r))
+       )
+)
+(constraint (=> f (g 2 2)))
+(constraint (not (=> f (g 0 1))))
+(check-synth)