Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.

9 files changed, 312 insertions, 67 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 4657449f8..d9c38ec65 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -776,6 +776,8 @@ libcvc4_add_sources(
   theory/quantifiers/sygus/sygus_unif_rl.h
   theory/quantifiers/sygus/sygus_unif_strat.cpp
   theory/quantifiers/sygus/sygus_unif_strat.h
+  theory/quantifiers/sygus/sygus_utils.cpp
+  theory/quantifiers/sygus/sygus_utils.h
   theory/quantifiers/sygus/synth_conjecture.cpp
   theory/quantifiers/sygus/synth_conjecture.h
   theory/quantifiers/sygus/synth_engine.cpp
diff --git a/src/preprocessing/passes/sygus_inference.cpp b/src/preprocessing/passes/sygus_inference.cpp
index ea767e771..caf63b0ec 100644
--- a/src/preprocessing/passes/sygus_inference.cpp
+++ b/src/preprocessing/passes/sygus_inference.cpp
@@ -20,6 +20,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/smt_engine_subsolver.h"
 
 using namespace std;
@@ -293,15 +294,8 @@ bool SygusInference::solveSygus(const std::vector<Node>& assertions,
 
   // sygus attribute to mark the conjecture as a sygus conjecture
   Trace("sygus-infer") << "Make outer sygus conjecture..." << std::endl;
-  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
-  theory::SygusAttribute ca;
-  sygusVar.setAttribute(ca, true);
-  Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
-  Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr);
 
-  Node fbvl = nm->mkNode(BOUND_VAR_LIST, ff_vars);
-
-  body = nm->mkNode(FORALL, fbvl, body, instAttrList);
+  body = quantifiers::SygusUtils::mkSygusConjecture(ff_vars, body);
 
   Trace("sygus-infer") << "*** Return sygus inference : " << body << std::endl;
 
diff --git a/src/preprocessing/passes/synth_rew_rules.cpp b/src/preprocessing/passes/synth_rew_rules.cpp
index 8465a63a0..ecf1e281d 100644
--- a/src/preprocessing/passes/synth_rew_rules.cpp
+++ b/src/preprocessing/passes/synth_rew_rules.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/candidate_rewrite_database.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace std;
@@ -429,12 +430,6 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
 
   // sygus attribute to mark the conjecture as a sygus conjecture
   Trace("srs-input") << "Make sygus conjecture..." << std::endl;
-  Node iaVar = nm->mkSkolem("sygus", nm->booleanType());
-  // the attribute to mark the conjecture as being a sygus conjecture
-  theory::SygusAttribute ca;
-  iaVar.setAttribute(ca, true);
-  Node instAttr = nm->mkNode(INST_ATTRIBUTE, iaVar);
-  Node instAttrList = nm->mkNode(INST_PATTERN_LIST, instAttr);
   // we are "synthesizing" functions for each type of subterm
   std::vector<Node> synthConj;
   unsigned fCounter = 1;
@@ -451,10 +446,9 @@ PreprocessingPassResult SynthRewRulesPass::applyInternal(
     // this marks that the grammar used for solutions for sfun is the type of
     // gvar, which is the sygus datatype type constructed above.
     sfun.setAttribute(ssg, gvar);
-    Node fvarBvl = nm->mkNode(BOUND_VAR_LIST, sfun);
 
     Node body = nm->mkConst(false);
-    body = nm->mkNode(FORALL, fvarBvl, body, instAttrList);
+    body = theory::quantifiers::SygusUtils::mkSygusConjecture({sfun}, body);
     synthConj.push_back(body);
   }
   Node trueNode = nm->mkConst(true);
diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp
index fa369b467..67f02b558 100644
--- a/src/theory/quantifiers/sygus/sygus_abduct.cpp
+++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp
@@ -22,6 +22,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 
@@ -155,12 +156,6 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
     res = nm->mkNode(EXISTS, bvl, res);
   }
   // sygus attribute
-  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
-  theory::SygusAttribute ca;
-  sygusVar.setAttribute(ca, true);
-  Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusVar);
-  std::vector<Node> iplc;
-  iplc.push_back(instAttr);
   Node aconj = axioms.size() == 0
                    ? nm->mkConst(true)
                    : (axioms.size() == 1 ? axioms[0] : nm->mkNode(AND, axioms));
@@ -171,18 +166,14 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name,
   sc = nm->mkNode(EXISTS, vbvl, sc);
   Node sygusScVar = nm->mkSkolem("sygus_sc", nm->booleanType());
   sygusScVar.setAttribute(theory::SygusSideConditionAttribute(), sc);
-  instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
+  Node instAttr = nm->mkNode(INST_ATTRIBUTE, sygusScVar);
   // build in the side condition
   //   exists x. A( x ) ^ input_axioms( x )
   // as an additional annotation on the sygus conjecture. In other words,
   // the abducts A we procedure must be consistent with our axioms.
-  iplc.push_back(instAttr);
-  Node instAttrList = nm->mkNode(INST_PATTERN_LIST, iplc);
-
-  Node fbvl = nm->mkNode(BOUND_VAR_LIST, abd);
 
   // forall A. exists x. ~( A( x ) => ~input( x ) )
-  res = nm->mkNode(FORALL, fbvl, res, instAttrList);
+  res = SygusUtils::mkSygusConjecture({abd}, res, {instAttr});
   Trace("sygus-abduct-debug") << "...finish" << std::endl;
 
   res = theory::Rewriter::rewrite(res);
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 79fc1a36e..23d924581 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -21,6 +21,7 @@
 #include "theory/datatypes/sygus_datatype_utils.h"
 #include "theory/quantifiers/sygus/sygus_grammar_norm.h"
 #include "theory/quantifiers/sygus/sygus_process_conj.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/sygus/synth_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_util.h"
@@ -44,14 +45,10 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
   Assert(q.getKind() == FORALL);
   for (const Node& f : q[0])
   {
-    Node gv = f.getAttribute(SygusSynthGrammarAttribute());
-    if (!gv.isNull())
+    TypeNode tn = SygusUtils::getSygusTypeForSynthFun(f);
+    if (tn.isDatatype() && tn.getDType().isSygus())
     {
-      TypeNode tn = gv.getType();
-      if (tn.isDatatype() && tn.getDType().isSygus())
-      {
-        return true;
-      }
+      return true;
     }
   }
   return false;
@@ -144,7 +141,7 @@ Node CegGrammarConstructor::process(Node q,
       SygusGrammarNorm sygus_norm(d_qe);
       tn = sygus_norm.normalizeSygusType(tn, sfvl);
     }else{
-      sfvl = getSygusVarList(sf);
+      sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
       // check which arguments are irrelevant
       std::unordered_set<unsigned> arg_irrelevant;
       d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
@@ -213,7 +210,7 @@ Node CegGrammarConstructor::process(Node q,
   {
     Node sf = q[0][i];
     d_synth_fun_vars[sf] = ebvl[i];
-    Node sfvl = getSygusVarList(sf);
+    Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
     TypeNode tn = ebvl[i].getType();
     // check if there is a template
     std::map<Node, Node>::const_iterator itt = templates.find(sf);
@@ -1581,27 +1578,6 @@ TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg,
   return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
 }
 
-Node CegGrammarConstructor::getSygusVarList(Node f)
-{
-  Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
-  if (sfvl.isNull() && f.getType().isFunction())
-  {
-    NodeManager* nm = NodeManager::currentNM();
-    std::vector<TypeNode> argTypes = f.getType().getArgTypes();
-    // make default variable list if none was specified by input
-    std::vector<Node> bvs;
-    for (unsigned j = 0, size = argTypes.size(); j < size; j++)
-    {
-      std::stringstream ss;
-      ss << "arg" << j;
-      bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
-    }
-    sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
-    f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
-  }
-  return sfvl;
-}
-
 CegGrammarConstructor::SygusDatatypeGenerator::SygusDatatypeGenerator(
     const std::string& name)
     : d_sdt(name)
diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.h b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
index 872bed060..6edfbebd5 100644
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.h
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.h
@@ -146,14 +146,6 @@ public:
   */
   static TypeNode mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl, const std::string& fun );
   /**
-   * Returns the sygus variable list for function-to-synthesize variable f.
-   * These are the names of the arguments of f, which should be included in the
-   * grammar for f. This returns either the variable list set explicitly via the
-   * attribute SygusSynthFunVarListAttribute, or a fresh variable list of the
-   * proper type otherwise. It will return null if f is not a function.
-   */
-  static Node getSygusVarList(Node f);
-  /**
    * Returns true iff there are syntax restrictions on the
    * functions-to-synthesize of sygus conjecture q.
    */
diff --git a/src/theory/quantifiers/sygus/sygus_utils.cpp b/src/theory/quantifiers/sygus/sygus_utils.cpp
new file mode 100644
index 000000000..ca87e1049
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_utils.cpp
@@ -0,0 +1,180 @@
+/*********************                                                        */
+/*! \file sygus_utils.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief generic sygus utilities
+ **/
+
+#include "theory/quantifiers/sygus/sygus_utils.h"
+
+#include "expr/node_algorithm.h"
+#include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+/**
+ * Attribute for specifying a solution for a function-to-synthesize. This is
+ * used for marking certain functions that we have solved for, e.g. during
+ * preprocessing.
+ */
+struct SygusSolutionAttributeId
+{
+};
+typedef expr::Attribute<SygusSolutionAttributeId, Node> SygusSolutionAttribute;
+
+Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
+                                   Node conj,
+                                   const std::vector<Node>& iattrs)
+{
+  Assert(!fs.empty());
+  NodeManager* nm = NodeManager::currentNM();
+  SygusAttribute ca;
+  Node sygusVar = nm->mkSkolem("sygus", nm->booleanType());
+  sygusVar.setAttribute(ca, true);
+  std::vector<Node> ipls{nm->mkNode(INST_ATTRIBUTE, sygusVar)};
+  // insert the remaining instantiation attributes
+  ipls.insert(ipls.end(), iattrs.begin(), iattrs.end());
+  Node ipl = nm->mkNode(INST_PATTERN_LIST, ipls);
+  Node bvl = nm->mkNode(BOUND_VAR_LIST, fs);
+  return nm->mkNode(FORALL, bvl, conj, ipl);
+}
+
+Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs, Node conj)
+{
+  std::vector<Node> iattrs;
+  return mkSygusConjecture(fs, conj, iattrs);
+}
+
+Node SygusUtils::mkSygusConjecture(const std::vector<Node>& fs,
+                                   Node conj,
+                                   const Subs& solvedf)
+{
+  Assert(!fs.empty());
+  NodeManager* nm = NodeManager::currentNM();
+  std::vector<Node> iattrs;
+  // take existing properties, without the previous solves
+  SygusSolutionAttribute ssa;
+  // add the current solves, which should be a superset of the previous ones
+  for (size_t i = 0, nsolved = solvedf.size(); i < nsolved; i++)
+  {
+    Node eq = solvedf.getEquality(i);
+    Node var = nm->mkSkolem("solved", nm->booleanType());
+    var.setAttribute(ssa, eq);
+    Node ipv = nm->mkNode(INST_ATTRIBUTE, var);
+    iattrs.push_back(ipv);
+  }
+  return mkSygusConjecture(fs, conj, iattrs);
+}
+
+void SygusUtils::decomposeSygusConjecture(Node q,
+                                          std::vector<Node>& fs,
+                                          std::vector<Node>& unsf,
+                                          Subs& solvedf)
+{
+  Assert(q.getKind() == FORALL);
+  Assert(q.getNumChildren() == 3);
+  Node ipl = q[2];
+  Assert(ipl.getKind() == INST_PATTERN_LIST);
+  fs.insert(fs.end(), q[0].begin(), q[0].end());
+  SygusSolutionAttribute ssa;
+  for (const Node& ip : ipl)
+  {
+    if (ip.getKind() == INST_ATTRIBUTE)
+    {
+      Node ipv = ip[0];
+      // does it specify a sygus solution?
+      if (ipv.hasAttribute(ssa))
+      {
+        Node eq = ipv.getAttribute(ssa);
+        Assert(std::find(fs.begin(), fs.end(), eq[0]) != fs.end());
+        solvedf.addEquality(eq);
+      }
+    }
+  }
+  // add to unsolved functions
+  for (const Node& f : fs)
+  {
+    if (!solvedf.contains(f))
+    {
+      unsf.push_back(f);
+    }
+  }
+}
+
+Node SygusUtils::decomposeSygusBody(Node conj, std::vector<Node>& vs)
+{
+  if (conj.getKind() == NOT && conj[0].getKind() == FORALL)
+  {
+    vs.insert(vs.end(), conj[0][0].begin(), conj[0][0].end());
+    return conj[0][1].negate();
+  }
+  return conj;
+}
+
+Node SygusUtils::getSygusArgumentListForSynthFun(Node f)
+{
+  Node sfvl = f.getAttribute(SygusSynthFunVarListAttribute());
+  if (sfvl.isNull() && f.getType().isFunction())
+  {
+    NodeManager* nm = NodeManager::currentNM();
+    std::vector<TypeNode> argTypes = f.getType().getArgTypes();
+    // make default variable list if none was specified by input
+    std::vector<Node> bvs;
+    for (unsigned j = 0, size = argTypes.size(); j < size; j++)
+    {
+      std::stringstream ss;
+      ss << "arg" << j;
+      bvs.push_back(nm->mkBoundVar(ss.str(), argTypes[j]));
+    }
+    sfvl = nm->mkNode(BOUND_VAR_LIST, bvs);
+    f.setAttribute(SygusSynthFunVarListAttribute(), sfvl);
+  }
+  return sfvl;
+}
+
+void SygusUtils::getSygusArgumentListForSynthFun(Node f,
+                                                 std::vector<Node>& formals)
+{
+  Node sfvl = getSygusArgumentListForSynthFun(f);
+  if (!sfvl.isNull())
+  {
+    formals.insert(formals.end(), sfvl.begin(), sfvl.end());
+  }
+}
+
+Node SygusUtils::wrapSolutionForSynthFun(Node f, Node sol)
+{
+  Node al = getSygusArgumentListForSynthFun(f);
+  if (!al.isNull())
+  {
+    sol = NodeManager::currentNM()->mkNode(LAMBDA, al, sol);
+  }
+  Assert(!expr::hasFreeVar(sol));
+  return sol;
+}
+
+TypeNode SygusUtils::getSygusTypeForSynthFun(Node f)
+{
+  Node gv = f.getAttribute(SygusSynthGrammarAttribute());
+  if (!gv.isNull())
+  {
+    return gv.getType();
+  }
+  return TypeNode::null();
+}
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
diff --git a/src/theory/quantifiers/sygus/sygus_utils.h b/src/theory/quantifiers/sygus/sygus_utils.h
new file mode 100644
index 000000000..c8b798097
--- /dev/null
+++ b/src/theory/quantifiers/sygus/sygus_utils.h
@@ -0,0 +1,115 @@
+/*********************                                                        */
+/*! \file sygus_utils.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+ ** in the top-level source directory and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief generic sygus utilities
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+#define CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/subs.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class SygusUtils
+{
+ public:
+  /**
+   * Make (negated) sygus conjecture of the form
+   *   forall fs. conj
+   * with instantiation attributes in iattrs. Notice that the marker for
+   * sygus conjecture is automatically prepended to this list.
+   *
+   * @param fs The functions
+   * @param conj The (negated) conjecture body
+   * @param iattrs The attributes of the conjecture. Notice this does not
+   * require the "sygus attribute" marker, which is automatically generated
+   * by this method.
+   */
+  static Node mkSygusConjecture(const std::vector<Node>& fs,
+                                Node conj,
+                                const std::vector<Node>& iattrs);
+  /** Same as above, without auxiliary instantiation attributes */
+  static Node mkSygusConjecture(const std::vector<Node>& fs, Node conj);
+
+  /**
+   * Make conjecture, with a set of solved functions. In particular,
+   * solvedf is a substitution of the form { f1 -> t1, ... fn -> tn } where
+   * each f1 ... fn are in fs.
+   *
+   * In the implementation, solutions for solved functions are stored
+   * in the instantiation attribute list of the returned conjecture.
+   */
+  static Node mkSygusConjecture(const std::vector<Node>& fs,
+                                Node conj,
+                                const Subs& solvedf);
+  /**
+   * Decompose (negated) sygus conjecture.
+   *
+   * @param q The (negated) sygus conjecture to decompose, of kind FORALL
+   * @param fs The functions-to-synthesize
+   * @param unsf The functions that have not been marked as solved.
+   * @param solvedf The substitution corresponding to the solved functions.
+   *
+   * The vector unsf and the domain of solved are a parition of fs.
+   */
+  static void decomposeSygusConjecture(Node q,
+                                       std::vector<Node>& fs,
+                                       std::vector<Node>& unsf,
+                                       Subs& solvedf);
+  /**
+   * Decompose the negated body. This takes as input the body of the negated
+   * sygus conjecture, which is of the form (NOT (FORALL V G)) or
+   * quantifier-free formula G. It returns the conjecture without quantified
+   * variables (G), and adds the quantified variables (V) to vs.
+   */
+  static Node decomposeSygusBody(Node conj, std::vector<Node>& vs);
+
+  /**
+   * Get the formal argument list for a function-to-synthesize. This returns
+   * a node of kind BOUND_VAR_LIST that corresponds to the formal argument list
+   * of the function to synthesize.
+   *
+   * Note that if f is constant, then this returns null, since f has no
+   * arguments in this case.
+   */
+  static Node getSygusArgumentListForSynthFun(Node f);
+  /**
+   * Same as above, but adds the variables to formals.
+   */
+  static void getSygusArgumentListForSynthFun(Node f,
+                                              std::vector<Node>& formals);
+  /**
+   * Wrap a solution sol for f in the proper lambda, return the lambda
+   * expression. Notice the returned expression is sol itself if f has no
+   * formal arguments.
+   */
+  static Node wrapSolutionForSynthFun(Node f, Node sol);
+
+  /**
+   * Get the sygus datatype type that encodes the syntax restrictions for
+   * function-to-synthesize f.
+   */
+  static TypeNode getSygusTypeForSynthFun(Node f);
+};
+
+}  // namespace quantifiers
+}  // namespace theory
+}  // namespace CVC4
+
+#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS__SYGUS_UTILS_H */
diff --git a/src/theory/quantifiers/sygus/template_infer.cpp b/src/theory/quantifiers/sygus/template_infer.cpp
index 0ac984aa3..904bec78c 100644
--- a/src/theory/quantifiers/sygus/template_infer.cpp
+++ b/src/theory/quantifiers/sygus/template_infer.cpp
@@ -16,6 +16,7 @@
 
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/sygus_grammar_cons.h"
+#include "theory/quantifiers/sygus/sygus_utils.h"
 #include "theory/quantifiers/term_util.h"
 
 using namespace CVC4::kind;
@@ -163,7 +164,7 @@ void SygusTemplateInfer::initialize(Node q)
   Assert(!templ.isNull());
 
   // get the variables
-  Node sfvl = CegGrammarConstructor::getSygusVarList(prog);
+  Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(prog);
   if (!sfvl.isNull())
   {
     std::vector<Node> prog_vars(sfvl.begin(), sfvl.end());