From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Feb 2020 17:47:05 +0000 (-0600)
Subject: Use default consts when not using any const during grammar normalization (#3807)
X-Git-Tag: cvc5-1.0.0~3598
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2a274c84867a2974abc0b626349b934d520339b0;p=cvc5.git

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 b2e7d2681..f00fd0092 100644
--- 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 00faecedd..3fe4321d0 100644
--- 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
index 000000000..10daee6ec
--- /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)