From 547df7cd146091674562dfa4812f10bae7765934 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 16 Oct 2020 12:20:53 -0500
Subject: Catch more cases of nested recursion in datatypes (#5285)

Fixes #5280.

Previously we were checking for nested recursive datatypes in expandDefinitions. This does not catch cases where the only terms of a malformed nested recursive datatype are variables. The proper place to check is in preRegisterTerm. The benchmark from that issue now gives an error.
---
 src/theory/datatypes/theory_datatypes.cpp          | 48 ++++++++++++----------
 test/regress/CMakeLists.txt                        |  1 +
 .../regress0/datatypes/issue5280-no-nrec.smt2      |  8 ++++
 3 files changed, 35 insertions(+), 22 deletions(-)
 create mode 100644 test/regress/regress0/datatypes/issue5280-no-nrec.smt2

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 08f3e1626..1b557b3cb 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -419,8 +419,33 @@ void TheoryDatatypes::notifyFact(TNode atom,
 
 void TheoryDatatypes::preRegisterTerm(TNode n)
 {
-  Debug("datatypes-prereg")
+  Trace("datatypes-prereg")
       << "TheoryDatatypes::preRegisterTerm() " << n << endl;
+  // must ensure the type is well founded and has no nested recursion if
+  // the option dtNestedRec is not set to true.
+  TypeNode tn = n.getType();
+  if (tn.isDatatype())
+  {
+    const DType& dt = tn.getDType();
+    Trace("dt-expand") << "Check properties of " << dt.getName() << std::endl;
+    if (!dt.isWellFounded())
+    {
+      std::stringstream ss;
+      ss << "Cannot handle non-well-founded datatype " << dt.getName();
+      throw LogicException(ss.str());
+    }
+    Trace("dt-expand") << "...well-founded ok" << std::endl;
+    if (!options::dtNestedRec())
+    {
+      if (dt.hasNestedRecursion())
+      {
+        std::stringstream ss;
+        ss << "Cannot handle nested-recursive datatype " << dt.getName();
+        throw LogicException(ss.str());
+      }
+      Trace("dt-expand") << "...nested recursion ok" << std::endl;
+    }
+  }
   collectTerms( n );
   switch (n.getKind()) {
   case kind::EQUAL:
@@ -446,28 +471,7 @@ void TheoryDatatypes::preRegisterTerm(TNode n)
 TrustNode TheoryDatatypes::expandDefinition(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
-  // must ensure the type is well founded and has no nested recursion if
-  // the option dtNestedRec is not set to true.
   TypeNode tn = n.getType();
-  if (tn.isDatatype())
-  {
-    const DType& dt = tn.getDType();
-    if (!dt.isWellFounded())
-    {
-      std::stringstream ss;
-      ss << "Cannot handle non-well-founded datatype " << dt.getName();
-      throw LogicException(ss.str());
-    }
-    if (!options::dtNestedRec())
-    {
-      if (dt.hasNestedRecursion())
-      {
-        std::stringstream ss;
-        ss << "Cannot handle nested-recursive datatype " << dt.getName();
-        throw LogicException(ss.str());
-      }
-    }
-  }
   Node ret;
   switch (n.getKind())
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index e8b85ac31..cb3c9d9f8 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -431,6 +431,7 @@ set(regress_0_tests
   regress0/datatypes/is_test.smt2
   regress0/datatypes/issue1433.smt2
   regress0/datatypes/issue2838.cvc
+  regress0/datatypes/issue5280-no-nrec.smt2
   regress0/datatypes/jsat-2.6.smt2
   regress0/datatypes/list-bool.smt2
   regress0/datatypes/model-subterms-min.smt2
diff --git a/test/regress/regress0/datatypes/issue5280-no-nrec.smt2 b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2
new file mode 100644
index 000000000..f80a6796a
--- /dev/null
+++ b/test/regress/regress0/datatypes/issue5280-no-nrec.smt2
@@ -0,0 +1,8 @@
+; EXPECT: (error "Cannot handle nested-recursive datatype ty0")
+; EXIT: 1
+(set-logic ALL)
+(declare-datatype ty0 ((Emp) (Container (v2 (Set ty0)))))
+(declare-fun v1 () ty0)
+(assert (not ((_ is Emp) v1)))
+(assert (= (v2 v1) (singleton v1)))
+(check-sat)
-- 
cgit v1.2.3