Avoid non-well-founded sygus grammars (#3434)

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 0cce030b0b7cef626394854a8339e23da692f1e4..a5033278df2af4689a5d38f0dba7d5a2953f1e1c 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -1054,21 +1054,21 @@ sygusGrammar[CVC4::Type & ret,
       // grammar. This results in the error below.
       // We can also be in a case where the only rule specified was
       // (Constant T), in which case we have not yet added a constructor. We
-      // ensure an arbitrary constant is added in this case.
-      if (datatypes[i].getNumConstructors() == 0)
+      // ensure an arbitrary constant is added in this case. We additionally
+      // add a constant if the grammar allows it regardless of whether the
+      // datatype has other constructors, since this ensures the datatype is
+      // well-founded (see 3423).
+      if (aci)
       {
-        if (aci)
-        {
-          Expr c = btt.mkGroundTerm();
-          PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres);
-        }
-        else
-        {
-          std::stringstream se;
-          se << "Grouped rule listing for " << datatypes[i].getName()
-             << " produced an empty rule list.";
-          PARSER_STATE->parseError(se.str());
-        }
+        Expr c = btt.mkGroundTerm();
+        PARSER_STATE->addSygusConstructorTerm(datatypes[i], c, ntsToUnres);
+      }
+      else if (datatypes[i].getNumConstructors() == 0)
+      {
+        std::stringstream se;
+        se << "Grouped rule listing for " << datatypes[i].getName()
+           << " produced an empty rule list.";
+        PARSER_STATE->parseError(se.str());
       }
     }
     // pop scope from the pre-declaration

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 7e52501c265ca27f2e260f4fcf65c85101616126..7765591f87d594c47e05193f1d699e7caa5f34cc 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -920,6 +920,8 @@ set(regress_0_tests
   regress0/sygus/parity-AIG-d0.sy
   regress0/sygus/parse-bv-let.sy
   regress0/sygus/real-si-all.sy
+  regress0/sygus/sygus-no-wf.sy
+  regress0/sygus/sygus-uf.sy
   regress0/sygus/strings-unconstrained.sy
   regress0/sygus/uminus_one.sy
   regress0/sygus/univ_3-long-repeat-conflict.sy
@@ -2067,7 +2069,6 @@ set(regression_disabled_tests
   regress0/sets/sets-new.smt2
   regress0/sets/sets-testlemma-ints.smt2
   regress0/sets/sets-testlemma-reals.smt2
-  regress0/sygus/sygus-uf.sy
   regress0/symmetric.smtv1.smt2
   regress0/tptp/BOO003-4.p
   regress0/tptp/BOO027-1.p

diff --git a/test/regress/regress0/sygus/sygus-no-wf.sy b/test/regress/regress0/sygus/sygus-no-wf.sy
new file mode 100644 (file)
index 0000000..40a3d55
--- /dev/null
+++ b/test/regress/regress0/sygus/sygus-no-wf.sy
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
+(set-logic ALL)
+(synth-fun f ((x0 Bool)) Bool
+       (
+               (B Bool ((Variable Bool) (Constant Bool) (= I I) )) 
+               (I Int ((Constant Int) (+ I I)))
+       )
+)
+(constraint (= (f false) false))
+(check-synth)

diff --git a/test/regress/regress0/sygus/sygus-uf.sy b/test/regress/regress0/sygus/sygus-uf.sy
index 95cd8771e02d35e31a41a8d61f86587f1e176ab8..1b060637ae789469b54be8de8d38df524a5fd74c 100644 (file)
--- a/test/regress/regress0/sygus/sygus-uf.sy
+++ b/test/regress/regress0/sygus/sygus-uf.sy
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sygus-out=status
+; EXPECT: unsat
 (set-logic LIA)
 
 (declare-fun uf (Int) Int)