From 9ca190a3a2f7f952e1452efb69c78803ec302dd6 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 4 Nov 2019 14:24:02 -0600
Subject: [PATCH] Avoid non-well-founded sygus grammars (#3434)

---
 src/parser/smt2/Smt2.g                     | 28 +++++++++++-----------
 test/regress/CMakeLists.txt                |  3 ++-
 test/regress/regress0/sygus/sygus-no-wf.sy | 11 +++++++++
 test/regress/regress0/sygus/sygus-uf.sy    |  2 ++
 4 files changed, 29 insertions(+), 15 deletions(-)
 create mode 100644 test/regress/regress0/sygus/sygus-no-wf.sy

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 0cce030b0..a5033278d 100644
--- 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 7e52501c2..7765591f8 100644
--- 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
index 000000000..40a3d5547
--- /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 95cd8771e..1b060637a 100644
--- 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)
-- 
2.30.2