From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 19 Aug 2021 22:40:05 +0000 (-0500)
Subject: Catch cases where recursive functions reference functions-to-synthesize (#6993)
X-Git-Tag: cvc5-1.0.0~1366
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=09719301db1532093117bc60546e01dca77b59b8;p=cvc5.git

Catch cases where recursive functions reference functions-to-synthesize (#6993)

We previously incorrectly allowed this, leading to problems that were unsolvable but where we would not warn the user this combination is not supported.

FYI @polgreen
---

diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp
index b7688d833..6292b5982 100644
--- a/src/smt/assertions.cpp
+++ b/src/smt/assertions.cpp
@@ -178,12 +178,19 @@ void Assertions::addFormula(TNode n,
     if (expr::hasFreeVar(n))
     {
       std::stringstream se;
-      se << "Cannot process assertion with free variable.";
-      if (language::isInputLangSygus(options::inputLanguage()))
+      if (isFunDef)
       {
-        // Common misuse of SyGuS is to use top-level assert instead of
-        // constraint when defining the synthesis conjecture.
-        se << " Perhaps you meant `constraint` instead of `assert`?";
+        se << "Cannot process function definition with free variable.";
+      }
+      else
+      {
+        se << "Cannot process assertion with free variable.";
+        if (language::isInputLangSygus(options::inputLanguage()))
+        {
+          // Common misuse of SyGuS is to use top-level assert instead of
+          // constraint when defining the synthesis conjecture.
+          se << " Perhaps you meant `constraint` instead of `assert`?";
+        }
       }
       throw ModalException(se.str().c_str());
     }
@@ -205,9 +212,11 @@ void Assertions::addDefineFunDefinition(Node n, bool global)
   }
   else
   {
-    // we don't check for free variables here, since even if we are sygus,
-    // we could contain functions-to-synthesize within definitions.
-    addFormula(n, true, false, true, false);
+    // We don't permit functions-to-synthesize within recursive function
+    // definitions currently. Thus, we should check for free variables if the
+    // input language is SyGuS.
+    bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
+    addFormula(n, true, false, true, maybeHasFv);
   }
 }
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 21c22586b..12d3fccfe 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -303,7 +303,16 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       // the atom should not have free variables
       Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
                       << std::endl;
-      Assert(!expr::hasFreeVar(preprocessed));
+      if (Configuration::isAssertionBuild())
+      {
+        std::unordered_set<Node> fvs;
+        expr::getFreeVariables(preprocessed, fvs);
+        if (!fvs.empty())
+        {
+          Unhandled() << "Preregistered term with free variable: "
+                      << preprocessed << ", fv=" << *fvs.begin();
+        }
+      }
       // should not have witness
       Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));