Fixes for sygus inference (#2238)

This includes:
- Enabling sygus-specific options in SmtEngine::setDefaults,
- Disabling a variant of miniscoping (triggered by many chc-comp18 benchmarks),
- Treating free constants as functions to synthesize

1 files changed, 17 insertions, 4 deletions

diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp
index fe5761e03..6232de6fe 100644
--- a/src/theory/quantifiers/sygus_inference.cpp
+++ b/src/theory/quantifiers/sygus_inference.cpp
@@ -144,6 +144,13 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
             free_functions.push_back(op);
           }
         }
+        else if (cur.getKind() == VARIABLE)
+        {
+          // a free variable is a 0-argument function to synthesize
+          Assert(std::find(free_functions.begin(), free_functions.end(), cur)
+                 == free_functions.end());
+          free_functions.push_back(cur);
+        }
         else if (cur.getKind() == FORALL)
         {
           Trace("sygus-infer")
@@ -159,7 +166,7 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
     processed_assertions.push_back(pas);
   }
 
-  // if no free function symbols, there is no use changing into SyGuS
+  // no functions to synthesize
   if (free_functions.empty())
   {
     Trace("sygus-infer") << "...fail: no free function symbols." << std::endl;
@@ -252,16 +259,22 @@ bool SygusInference::simplify(std::vector<Node>& assertions)
     if (itffv != ff_var_to_ff.end())
     {
       Node ff = itffv->second;
+      Expr body = it->second;
       std::vector<Expr> args;
-      for (const Node& v : lambda[0])
+      // if it is a non-constant function
+      if (lambda.getKind() == LAMBDA)
       {
-        args.push_back(v.toExpr());
+        for (const Node& v : lambda[0])
+        {
+          args.push_back(v.toExpr());
+        }
+        body = it->second[1];
       }
       Trace("sygus-infer") << "Define " << ff << " as " << it->second
                            << std::endl;
       final_ff.push_back(ff);
       final_ff_sol.push_back(it->second);
-      master_smte->defineFunction(ff.toExpr(), args, it->second[1]);
+      master_smte->defineFunction(ff.toExpr(), args, body);
     }
   }