Limit cases of sygus inference based on type (#3370)

This makes `--sygus-inference` a no-op for inputs where there is a free function whose sort cannot be handled in a sygus grammar.

It also fixes an issue where skolem variables were not being treated as functions-to-synthesize.

Fixes #3250 and fixes #3356.

1 files changed, 20 insertions, 1 deletions

diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index 471d68ff8..930edf869 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -19,6 +19,7 @@
 #include "smt/smt_statistics_registry.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
 
 using namespace std;
 using namespace CVC4::kind;
@@ -194,7 +195,7 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
             free_functions.push_back(op);
           }
         }
-        else if (cur.getKind() == VARIABLE)
+        else if (cur.isVar() && cur.getKind() != BOUND_VARIABLE)
         {
           // a free variable is a 0-argument function to synthesize
           Assert(std::find(free_functions.begin(), free_functions.end(), cur)
@@ -223,6 +224,24 @@ bool SygusInference::solveSygus(std::vector<Node>& assertions,
     return false;
   }
 
+  // Ensure the type of all free functions is handled by the sygus grammar
+  // constructor utility.
+  bool typeSuccess = true;
+  for (const Node& f : free_functions)
+  {
+    TypeNode tn = f.getType();
+    if (!theory::quantifiers::CegGrammarConstructor::isHandledType(tn))
+    {
+      Trace("sygus-infer") << "...fail: unhandled type " << tn << std::endl;
+      typeSuccess = false;
+      break;
+    }
+  }
+  if (!typeSuccess)
+  {
+    return false;
+  }
+
   Assert(!processed_assertions.empty());
   // conjunction of the assertions
   Trace("sygus-infer") << "Construct body..." << std::endl;