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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 116d2fe233cb87fa9f6f914eddb2fde915cfee5c..15b6e2fc9f0a3e59aec5bbbee59cecba77fb0c53 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1403,6 +1403,8 @@ void SmtEngine::setDefaults() {
     d_logic = d_logic.getUnlockedCopy();
     d_logic.enableTheory(THEORY_DATATYPES);
     d_logic.lock();
+    // since we are trying to recast as sygus, we assume the input is sygus
+    is_sygus = true;
   }
 
   if ((options::checkModels() || options::checkSynthSol())
@@ -2053,6 +2055,10 @@ void SmtEngine::setDefaults() {
     if( !options::miniscopeQuantFreeVar.wasSetByUser() ){
       options::miniscopeQuantFreeVar.set( false );
     }
+    if (!options::quantSplit.wasSetByUser())
+    {
+      options::quantSplit.set(false);
+    }
     //rewrite divk
     if( !options::rewriteDivk.wasSetByUser()) {
       options::rewriteDivk.set( true );

diff --git a/src/theory/quantifiers/sygus_inference.cpp b/src/theory/quantifiers/sygus_inference.cpp
index fe5761e03d7ffb724e1aabdc7c15359d723ba89c..6232de6fef1803b9e5b4d9b2c387017fb3a37eab 100644 (file)
--- 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);
     }
   }