Modify the smt2 parser to use the Sygus grammar. (#4829)

9 files changed, 388 insertions, 386 deletions

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index a1effec91..64f9dbd35 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -1413,16 +1413,14 @@ size_t OpHashFunction::operator()(const Op& t) const
 
 Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
 
-Term::Term(const Solver* slv, const CVC4::Expr& e)
-    : d_solver(slv)
+Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv)
 {
   // Ensure that we create the node in the correct node manager.
   NodeManagerScope scope(d_solver->getNodeManager());
   d_node.reset(new CVC4::Node(e));
 }
 
-Term::Term(const Solver* slv, const CVC4::Node& n)
-    : d_solver(slv)
+Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
 {
   // Ensure that we create the node in the correct node manager.
   NodeManagerScope scope(d_solver->getNodeManager());
@@ -2568,6 +2566,78 @@ void Grammar::addAnyVariable(Term ntSymbol)
   d_allowVars.insert(ntSymbol);
 }
 
+/**
+ * this function concatinates the outputs of calling f on each element between
+ * first and last, seperated by sep.
+ * @param first the beginning of the range
+ * @param last the end of the range
+ * @param f the function to call on each element in the range, its output must
+ *          be overloaded for operator<<
+ * @param sep the string to add between successive calls to f
+ */
+template <typename Iterator, typename Function>
+std::string join(Iterator first, Iterator last, Function f, std::string sep)
+{
+  std::stringstream ss;
+  Iterator i = first;
+
+  if (i != last)
+  {
+    ss << f(*i);
+    ++i;
+  }
+
+  while (i != last)
+  {
+    ss << sep << f(*i);
+    ++i;
+  }
+
+  return ss.str();
+}
+
+std::string Grammar::toString() const
+{
+  std::stringstream ss;
+  ss << "  ("  // pre-declaration
+     << join(
+            d_ntSyms.cbegin(),
+            d_ntSyms.cend(),
+            [](const Term& t) {
+              std::stringstream s;
+              s << '(' << t << ' ' << t.getSort() << ')';
+              return s.str();
+            },
+            " ")
+     << ")\n  ("  // grouped rule listing
+     << join(
+            d_ntSyms.cbegin(),
+            d_ntSyms.cend(),
+            [this](const Term& t) {
+              bool allowConst = d_allowConst.find(t) != d_allowConst.cend(),
+                   allowVars = d_allowVars.find(t) != d_allowVars.cend();
+              const std::vector<Term>& rules = d_ntsToTerms.at(t);
+              std::stringstream s;
+              s << '(' << t << ' ' << t.getSort() << " ("
+                << (allowConst ? "(Constant " + t.getSort().toString() + ")"
+                               : "")
+                << (allowConst && allowVars ? " " : "")
+                << (allowVars ? "(Var " + t.getSort().toString() + ")" : "")
+                << ((allowConst || allowVars) && !rules.empty() ? " " : "")
+                << join(
+                       rules.cbegin(),
+                       rules.cend(),
+                       [](const Term& rule) { return rule.toString(); },
+                       " ")
+                << "))";
+              return s.str();
+            },
+            "\n   ")
+     << ')';
+
+  return ss.str();
+}
+
 Sort Grammar::resolve()
 {
   d_isResolved = true;
@@ -2737,6 +2807,11 @@ void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
   }
 }
 
+std::ostream& operator<<(std::ostream& out, const Grammar& g)
+{
+  return out << g.toString();
+}
+
 /* -------------------------------------------------------------------------- */
 /* Rounding Mode for Floating Points                                          */
 /* -------------------------------------------------------------------------- */
@@ -4982,18 +5057,47 @@ bool Solver::getInterpolant(Term conj, Term& output) const
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   Expr result;
   bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), result);
-  if (success) {
+  if (success)
+  {
     output = Term(output.d_solver, result);
   }
   return success;
   CVC4_API_SOLVER_TRY_CATCH_END;
 }
 
-bool Solver::getInterpolant(Term conj, const Type& gtype, Term& output) const
+bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   Expr result;
-  bool success = d_smtEngine->getInterpol(conj.d_node->toExpr(), gtype, result);
+  bool success = d_smtEngine->getInterpol(
+      conj.d_node->toExpr(), *g.resolve().d_type, result);
+  if (success)
+  {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getAbduct(Term conj, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Node result;
+  bool success = d_smtEngine->getAbduct(*conj.d_node, result);
+  if (success)
+  {
+    output = Term(output.d_solver, result);
+  }
+  return success;
+  CVC4_API_SOLVER_TRY_CATCH_END;
+}
+
+bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
+{
+  CVC4_API_SOLVER_TRY_CATCH_BEGIN;
+  Node result;
+  bool success = d_smtEngine->getAbduct(
+      *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
   if (success)
   {
     output = Term(output.d_solver, result);
@@ -5149,7 +5253,7 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
 {
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
   CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)
-      << "non-empty vector";
+      << "a non-empty vector";
 
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
   {
@@ -5157,30 +5261,30 @@ Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
         this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+        << "a non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         boundVars[i],
         i)
         << "a bound variable";
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !boundVars[i].isNull(), "parameter term", boundVars[i], i)
-        << "non-null term";
   }
 
   for (size_t i = 0, n = ntSymbols.size(); i < n; ++i)
   {
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        this == ntSymbols[i].d_solver, "term", ntSymbols[i], i)
+        this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i)
         << "term associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i)
+        << "a non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
-        "bound variable",
+        "non-terminal",
         ntSymbols[i],
         i)
         << "a bound variable";
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !ntSymbols[i].isNull(), "parameter term", ntSymbols[i], i)
-        << "non-null term";
   }
 
   return Grammar(this, boundVars, ntSymbols);
@@ -5227,7 +5331,7 @@ Term Solver::synthFunHelper(const std::string& symbol,
   CVC4_API_ARG_CHECK_NOT_NULL(sort);
 
   CVC4_API_ARG_CHECK_EXPECTED(sort.d_type->isFirstClass(), sort)
-      << "first-class sort as codomain sort for function sort";
+      << "first-class codomain sort for function";
 
   std::vector<Type> varTypes;
   for (size_t i = 0, n = boundVars.size(); i < n; ++i)
@@ -5236,14 +5340,14 @@ Term Solver::synthFunHelper(const std::string& symbol,
         this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
         << "bound variable associated to this solver object";
     CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
+        !boundVars[i].isNull(), "bound variable", boundVars[i], i)
+        << "a non-null term";
+    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
         boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
         "bound variable",
         boundVars[i],
         i)
         << "a bound variable";
-    CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
-        !boundVars[i].isNull(), "parameter term", boundVars[i], i)
-        << "non-null term";
     varTypes.push_back(boundVars[i].d_node->getType().toType());
   }
   CVC4_API_SOLVER_CHECK_SORT(sort);
diff --git a/src/api/cvc4cpp.h b/src/api/cvc4cpp.h
index 30a0ad0a7..5d14e76a1 100644
--- a/src/api/cvc4cpp.h
+++ b/src/api/cvc4cpp.h
@@ -46,6 +46,7 @@ class DatatypeConstructorArg;
 class ExprManager;
 class NodeManager;
 class SmtEngine;
+class SynthFunCommand;
 class Type;
 class Options;
 class Random;
@@ -1950,6 +1951,7 @@ std::ostream& operator<<(std::ostream& out,
 class CVC4_PUBLIC Grammar
 {
   friend class Solver;
+  friend class CVC4::SynthFunCommand;
 
  public:
   /**
@@ -1960,6 +1962,13 @@ class CVC4_PUBLIC Grammar
   void addRule(Term ntSymbol, Term rule);
 
   /**
+   * Add <rules> to the set of rules corresponding to <ntSymbol>.
+   * @param ntSymbol the non-terminal to which the rules are added
+   * @param rule the rules to add
+   */
+  void addRules(Term ntSymbol, std::vector<Term> rules);
+
+  /**
    * Allow <ntSymbol> to be an arbitrary constant.
    * @param ntSymbol the non-terminal allowed to be any constant
    */
@@ -1973,11 +1982,9 @@ class CVC4_PUBLIC Grammar
   void addAnyVariable(Term ntSymbol);
 
   /**
-   * Add <rules> to the set of rules corresponding to <ntSymbol>.
-   * @param ntSymbol the non-terminal to which the rules are added
-   * @param rule the rules to add
+   * @return a string representation of this grammar.
    */
-  void addRules(Term ntSymbol, std::vector<Term> rules);
+  std::string toString() const;
 
   /**
    * Nullary constructor. Needed for the Cython API.
@@ -2072,6 +2079,14 @@ class CVC4_PUBLIC Grammar
   bool d_isResolved;
 };
 
+/**
+ * Serialize a grammar to given stream.
+ * @param out the output stream
+ * @param g the grammar to be serialized to the given output stream
+ * @return the output stream
+ */
+std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC4_PUBLIC;
+
 /* -------------------------------------------------------------------------- */
 /* Rounding Mode for Floating Points                                          */
 /* -------------------------------------------------------------------------- */
@@ -3125,7 +3140,7 @@ class CVC4_PUBLIC Solver
 
   /**
    * Get an interpolant
-   * SMT-LIB: ( get-interpol <term> )
+   * SMT-LIB: ( get-interpol <conj> )
    * Requires to enable option 'produce-interpols'.
    * @param conj the conjecture term
    * @param output a Term I such that A->I and I->B are valid, where A is the
@@ -3136,15 +3151,40 @@ class CVC4_PUBLIC Solver
 
   /**
    * Get an interpolant
-   * SMT-LIB: ( get-interpol <term> )
+   * SMT-LIB: ( get-interpol <conj> <g> )
    * Requires to enable option 'produce-interpols'.
    * @param conj the conjecture term
-   * @param gtype the grammar for the interpolant I
+   * @param g the grammar for the interpolant I
    * @param output a Term I such that A->I and I->B are valid, where A is the
    *        current set of assertions and B is given in the input by conj.
    * @return true if it gets I successfully, false otherwise.
    */
-  bool getInterpolant(Term conj, const Type& gtype, Term& output) const;
+  bool getInterpolant(Term conj, Grammar& g, Term& output) const;
+
+  /**
+   * Get an abduct.
+   * SMT-LIB: ( get-abduct <conj> )
+   * Requires enabling option 'produce-abducts'
+   * @param conj the conjecture term
+   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   *        unsatisfiable, where A is the current set of assertions and B is
+   *        given in the input by conj
+   * @return true if it gets C successfully, false otherwise
+   */
+  bool getAbduct(Term conj, Term& output) const;
+
+  /**
+   * Get an abduct.
+   * SMT-LIB: ( get-abduct <conj> <g> )
+   * Requires enabling option 'produce-abducts'
+   * @param conj the conjecture term
+   * @param g the grammar for the abduct C
+   * @param output a term C such that A^C is satisfiable, and A^~B^C is
+   *        unsatisfiable, where A is the current set of assertions and B is
+   *        given in the input by conj
+   * @return true if it gets C successfully, false otherwise
+   */
+  bool getAbduct(Term conj, Grammar& g, Term& output) const;
 
   /**
    * Print the model of a satisfiable query to the given output stream.
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index b88dc70b6..354f2d472 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -549,7 +549,7 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
   std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
   std::string name, fun;
   bool isInv;
-  CVC4::api::Sort grammar;
+  CVC4::api::Grammar* grammar = nullptr;
 }
   : /* declare-var */
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -560,7 +560,6 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
       api::Term var = PARSER_STATE->bindBoundVar(name, t);
       cmd.reset(new DeclareSygusVarCommand(name, var.getExpr(), t.getType()));
     }
-
   | /* synth-fun */
     ( SYNTH_FUN_TOK { isInv = false; }
       | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
@@ -618,23 +617,19 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
  * The argument fun is a unique identifier to avoid naming clashes for the
  * datatypes constructed by this call.
  */
-sygusGrammar[CVC4::api::Sort & ret,
+sygusGrammar[CVC4::api::Grammar*& ret,
              const std::vector<CVC4::api::Term>& sygusVars,
              const std::string& fun]
 @declarations
 {
   // the pre-declaration
-  std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
+  std::vector<std::pair<std::string, CVC4::api::Sort>> sortedVarNames;
   // non-terminal symbols of the grammar
   std::vector<CVC4::api::Term> ntSyms;
   CVC4::api::Sort t;
   std::string name;
   CVC4::api::Term e, e2;
-  std::vector<api::DatatypeDecl> datatypes;
-  std::set<api::Sort> unresTypes;
-  std::map<CVC4::api::Term, CVC4::api::Sort> ntsToUnres;
   unsigned dtProcessed = 0;
-  std::unordered_set<unsigned> allowConst;
 }
   :
   // predeclaration
@@ -675,21 +670,13 @@ sygusGrammar[CVC4::api::Sort & ret,
     PARSER_STATE->pushScope(true);
     for (std::pair<std::string, api::Sort>& i : sortedVarNames)
     {
-      Trace("parser-sygus2") << "Declare datatype " << i.first << std::endl;
-      // make the datatype, which encodes terms generated by this non-terminal
-      std::string dname = i.first;
-      datatypes.push_back(SOLVER->mkDatatypeDecl(dname));
-      // make its unresolved type, used for referencing the final version of
-      // the datatype
-      PARSER_STATE->checkDeclaration(dname, CHECK_UNDECLARED, SYM_SORT);
-      api::Sort urt = PARSER_STATE->mkUnresolvedType(dname);
-      unresTypes.insert(urt);
+      PARSER_STATE->checkDeclaration(name, CHECK_UNDECLARED, SYM_SORT);
       // make the non-terminal symbol, which will be parsed as an ordinary
       // free variable.
       api::Term nts = PARSER_STATE->bindBoundVar(i.first, i.second);
       ntSyms.push_back(nts);
-      ntsToUnres[nts] = urt;
     }
+    ret = PARSER_STATE->mkGrammar(sygusVars, ntSyms);
   }
   // the grouped rule listing
   LPAREN_TOK
@@ -719,17 +706,15 @@ sygusGrammar[CVC4::api::Sort & ret,
     (
       term[e,e2] {
         // add term as constructor to datatype
-        PARSER_STATE->addSygusConstructorTerm(
-            datatypes[dtProcessed], e, ntsToUnres);
+        ret->addRule(ntSyms[dtProcessed], e);
       }
       | LPAREN_TOK SYGUS_CONSTANT_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
-        // allow constants in datatypes[dtProcessed]
-        allowConst.insert(dtProcessed);
+        // allow constants in datatype for ntSyms[dtProcessed]
+        ret->addAnyConstant(ntSyms[dtProcessed]);
       }
       | LPAREN_TOK SYGUS_VARIABLE_TOK sortSymbol[t, CHECK_DECLARED] RPAREN_TOK {
         // add variable constructors to datatype
-        PARSER_STATE->addSygusConstructorVariables(
-            datatypes[dtProcessed], sygusVars, t);
+        ret->addAnyVariable(ntSyms[dtProcessed]);
       }
     )+
     RPAREN_TOK
@@ -740,45 +725,8 @@ sygusGrammar[CVC4::api::Sort & ret,
   )+
   RPAREN_TOK
   {
-    if (dtProcessed != sortedVarNames.size())
-    {
-      PARSER_STATE->parseError(
-          "Number of grouped rule listings does not match "
-          "number of symbols in predeclaration.");
-    }
-    api::Term bvl;
-    if (!sygusVars.empty())
-    {
-      bvl = MK_TERM(api::BOUND_VAR_LIST, sygusVars);
-    }
-    Trace("parser-sygus2") << "Process " << dtProcessed << " sygus datatypes..." << std::endl;
-    for (unsigned i = 0; i < dtProcessed; i++)
-    {
-      bool aci = allowConst.find(i)!=allowConst.end();
-      api::Sort btt = sortedVarNames[i].second;
-      datatypes[i].getDatatype().setSygus(btt.getType(), bvl.getExpr(), aci, false);
-      Trace("parser-sygus2") << "- " << datatypes[i].getName()
-                             << ", #cons= " << datatypes[i].getNumConstructors()
-                             << ", aci= " << aci << std::endl;
-      // We can be in a case where the only rule specified was (Variable T)
-      // and there are no variables of type T, in which case this is a bogus
-      // grammar. This results in the error below.
-      if (datatypes[i].getNumConstructors() == 0)
-      {
-        std::stringstream se;
-        se << "Grouped rule listing for " << datatypes[i].getName()
-           << " produced an empty rule list.";
-        PARSER_STATE->parseError(se.str());
-      }
-    }
     // pop scope from the pre-declaration
     PARSER_STATE->popScope();
-    // now, make the sygus datatype
-    Trace("parser-sygus2") << "Make the sygus datatypes..." << std::endl;
-    std::vector<api::Sort> datatypeTypes =
-      SOLVER->mkDatatypeSorts(datatypes, unresTypes);
-    // return is the first datatype
-    ret = api::Sort(datatypeTypes[0]);
   }
 ;
 
@@ -966,6 +914,7 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
   std::vector<api::Sort> sorts;
   std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
   std::unique_ptr<CVC4::CommandSequence> seq;
+  api::Grammar* g = nullptr;
 }
     /* Extended SMT-LIB set of commands syntax, not permitted in
      * --smtlib2 compliance mode. */
@@ -1131,10 +1080,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     term[e,e2]
     (
-      sygusGrammar[t, terms, name]
+      sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetAbductCommand(name,e.getExpr(), t.getType()));
+      cmd->reset(new GetAbductCommand(SOLVER, name, e, g));
     }
   | GET_INTERPOL_TOK {
       PARSER_STATE->checkThatLogicIsSet();
@@ -1142,10 +1091,10 @@ extendedCommand[std::unique_ptr<CVC4::Command>* cmd]
     symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     term[e,e2]
     (
-      sygusGrammar[t, terms, name]
+      sygusGrammar[g, terms, name]
     )?
     {
-      cmd->reset(new GetInterpolCommand(SOLVER, name, e, t.getType()));
+      cmd->reset(new GetInterpolCommand(SOLVER, name, e, g));
     }
   | DECLARE_HEAP LPAREN_TOK
     sortSymbol[t, CHECK_DECLARED]
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index eef23edfd..fa0f8af43 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -487,11 +487,11 @@ void Smt2::resetAssertions() {
 
 Smt2::SynthFunFactory::SynthFunFactory(
     Smt2* smt2,
-    const std::string& fun,
+    const std::string& id,
     bool isInv,
     api::Sort range,
     std::vector<std::pair<std::string, api::Sort>>& sortedVarNames)
-    : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
+    : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv)
 {
   if (range.isNull())
   {
@@ -501,37 +501,32 @@ Smt2::SynthFunFactory::SynthFunFactory(
   {
     smt2->parseError("Cannot use synth-fun with function return type.");
   }
+
   std::vector<api::Sort> varSorts;
   for (const std::pair<std::string, api::Sort>& p : sortedVarNames)
   {
     varSorts.push_back(p.second);
   }
-  Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
-  api::Sort synthFunType =
-      varSorts.size() > 0 ? d_smt2->getSolver()->mkFunctionSort(varSorts, range)
-                          : range;
+
+  api::Sort funSort = varSorts.empty()
+                          ? range
+                          : d_smt2->d_solver->mkFunctionSort(varSorts, range);
 
   // we do not allow overloading for synth fun
-  d_synthFun = d_smt2->bindBoundVar(fun, synthFunType);
-  // set the sygus type to be range by default, which is overwritten below
-  // if a grammar is provided
-  d_sygusType = range;
+  d_fun = d_smt2->bindBoundVar(id, funSort);
+
+  Debug("parser-sygus") << "Define synth fun : " << id << std::endl;
 
   d_smt2->pushScope(true);
   d_sygusVars = d_smt2->bindBoundVars(sortedVarNames);
 }
 
-Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
-
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Sort grammar)
+std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
 {
-  Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
+  Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
+  d_smt2->popScope();
   return std::unique_ptr<Command>(new SynthFunCommand(
-      d_fun,
-      d_synthFun.getExpr(),
-      grammar.isNull() ? d_sygusType.getType() : grammar.getType(),
-      d_isInv,
-      api::termVectorToExprs(d_sygusVars)));
+      d_smt2->d_solver, d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
 }
 
 std::unique_ptr<Command> Smt2::invConstraint(
@@ -762,6 +757,14 @@ Command* Smt2::setLogic(std::string name, bool fromCommand)
   return cmd;
 } /* Smt2::setLogic() */
 
+api::Grammar* Smt2::mkGrammar(const std::vector<api::Term>& boundVars,
+                              const std::vector<api::Term>& ntSymbols)
+{
+  d_allocGrammars.emplace_back(new api::Grammar(
+      std::move(d_solver->mkSygusGrammar(boundVars, ntSymbols))));
+  return d_allocGrammars.back().get();
+}
+
 bool Smt2::sygus() const
 {
   InputLanguage ilang = getLanguage();
@@ -906,99 +909,6 @@ api::Term Smt2::mkAbstractValue(const std::string& name)
   return d_solver->mkAbstractValue(name.substr(1));
 }
 
-
-void Smt2::addSygusConstructorTerm(
-    api::DatatypeDecl& dt,
-    api::Term term,
-    std::map<api::Term, api::Sort>& ntsToUnres) const
-{
-  Trace("parser-sygus2") << "Add sygus cons term " << term << std::endl;
-  // At this point, we should know that dt is well founded, and that its
-  // builtin sygus operators are well-typed.
-  // Now, purify each occurrence of a non-terminal symbol in term, replace by
-  // free variables. These become arguments to constructors. Notice we must do
-  // a tree traversal in this function, since unique paths to the same term
-  // should be treated as distinct terms.
-  // Notice that let expressions are forbidden in the input syntax of term, so
-  // this does not lead to exponential behavior with respect to input size.
-  std::vector<api::Term> args;
-  std::vector<api::Sort> cargs;
-  api::Term op = purifySygusGTerm(term, ntsToUnres, args, cargs);
-  std::stringstream ssCName;
-  ssCName << op.getKind();
-  Trace("parser-sygus2") << "Purified operator " << op
-                         << ", #args/cargs=" << args.size() << "/"
-                         << cargs.size() << std::endl;
-  if (!args.empty())
-  {
-    api::Term lbvl = d_solver->mkTerm(api::BOUND_VAR_LIST, args);
-    // its operator is a lambda
-    op = d_solver->mkTerm(api::LAMBDA, lbvl, op);
-  }
-  Trace("parser-sygus2") << "addSygusConstructor:  operator " << op
-                         << std::endl;
-  dt.getDatatype().addSygusConstructor(
-      op.getExpr(), ssCName.str(), api::sortVectorToTypes(cargs));
-}
-
-api::Term Smt2::purifySygusGTerm(api::Term term,
-                                 std::map<api::Term, api::Sort>& ntsToUnres,
-                                 std::vector<api::Term>& args,
-                                 std::vector<api::Sort>& cargs) const
-{
-  Trace("parser-sygus2-debug")
-      << "purifySygusGTerm: " << term
-      << " #nchild=" << term.getExpr().getNumChildren() << std::endl;
-  std::map<api::Term, api::Sort>::iterator itn = ntsToUnres.find(term);
-  if (itn != ntsToUnres.end())
-  {
-    api::Term ret = d_solver->mkVar(term.getSort());
-    Trace("parser-sygus2-debug")
-        << "...unresolved non-terminal, intro " << ret << std::endl;
-    args.push_back(api::Term(d_solver, ret.getExpr()));
-    cargs.push_back(itn->second);
-    return ret;
-  }
-  std::vector<api::Term> pchildren;
-  bool childChanged = false;
-  for (unsigned i = 0, nchild = term.getNumChildren(); i < nchild; i++)
-  {
-    Trace("parser-sygus2-debug")
-        << "......purify child " << i << " : " << term[i] << std::endl;
-    api::Term ptermc = purifySygusGTerm(term[i], ntsToUnres, args, cargs);
-    pchildren.push_back(ptermc);
-    childChanged = childChanged || ptermc != term[i];
-  }
-  if (!childChanged)
-  {
-    Trace("parser-sygus2-debug") << "...no child changed" << std::endl;
-    return term;
-  }
-  api::Term nret = d_solver->mkTerm(term.getOp(), pchildren);
-  Trace("parser-sygus2-debug")
-      << "...child changed, return " << nret << std::endl;
-  return nret;
-}
-
-void Smt2::addSygusConstructorVariables(api::DatatypeDecl& dt,
-                                        const std::vector<api::Term>& sygusVars,
-                                        api::Sort type) const
-{
-  // each variable of appropriate type becomes a sygus constructor in dt.
-  for (unsigned i = 0, size = sygusVars.size(); i < size; i++)
-  {
-    api::Term v = sygusVars[i];
-    if (v.getSort() == type)
-    {
-      std::stringstream ss;
-      ss << v;
-      std::vector<api::Sort> cargs;
-      dt.getDatatype().addSygusConstructor(
-          v.getExpr(), ss.str(), api::sortVectorToTypes(cargs));
-    }
-  }
-}
-
 InputLanguage Smt2::getLanguage() const
 {
   return d_solver->getOptions().getInputLanguage();
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 579fa90ce..2e725f9bf 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -60,6 +60,11 @@ class Smt2 : public Parser
    */
   std::unordered_map<std::string, api::Kind> d_indexedOpKindMap;
   std::pair<api::Term, std::string> d_lastNamedTerm;
+  /**
+   * A list of sygus grammar objects. We keep track of them here to ensure that
+   * they don't get deleted before the commands using them get invoked.
+   */
+  std::vector<std::unique_ptr<api::Grammar>> d_allocGrammars;
 
  protected:
   Smt2(api::Solver* solver,
@@ -198,7 +203,7 @@ class Smt2 : public Parser
      * Creates an instance of `SynthFunFactory`.
      *
      * @param smt2 Pointer to the parser state
-     * @param fun Name of the function to synthesize
+     * @param id Name of the function to synthesize
      * @param isInv True if the goal is to synthesize an invariant, false
      * otherwise
      * @param range The return type of the function-to-synthesize
@@ -206,11 +211,10 @@ class Smt2 : public Parser
      */
     SynthFunFactory(
         Smt2* smt2,
-        const std::string& fun,
+        const std::string& id,
         bool isInv,
         api::Sort range,
         std::vector<std::pair<std::string, api::Sort>>& sortedVarNames);
-    ~SynthFunFactory();
 
     const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; }
 
@@ -220,13 +224,13 @@ class Smt2 : public Parser
      * @param grammar Optional grammar associated with the synth-fun command
      * @return The instance of `SynthFunCommand`
      */
-    std::unique_ptr<Command> mkCommand(api::Sort grammar);
+    std::unique_ptr<Command> mkCommand(api::Grammar* grammar);
 
    private:
     Smt2* d_smt2;
-    std::string d_fun;
-    api::Term d_synthFun;
-    api::Sort d_sygusType;
+    std::string d_id;
+    api::Term d_fun;
+    api::Sort d_sort;
     bool d_isInv;
     std::vector<api::Term> d_sygusVars;
   };
@@ -257,6 +261,15 @@ class Smt2 : public Parser
    */
   const LogicInfo& getLogic() const { return d_logic; }
 
+  /**
+   * Create a Sygus grammar.
+   * @param boundVars the parameters to corresponding synth-fun/synth-inv
+   * @param ntSymbols the pre-declaration of the non-terminal symbols
+   * @return a pointer to the grammar
+   */
+  api::Grammar* mkGrammar(const std::vector<api::Term>& boundVars,
+                          const std::vector<api::Term>& ntSymbols);
+
   bool v2_0() const
   {
     return getLanguage() == language::input::LANG_SMTLIB_V2_0;
@@ -308,10 +321,13 @@ class Smt2 : public Parser
    */
   void checkLogicAllowsFunctions();
 
-  void checkUserSymbol(const std::string& name) {
-    if(name.length() > 0 && (name[0] == '.' || name[0] == '@')) {
+  void checkUserSymbol(const std::string& name)
+  {
+    if (name.length() > 0 && (name[0] == '.' || name[0] == '@'))
+    {
       std::stringstream ss;
-      ss << "cannot declare or define symbol `" << name << "'; symbols starting with . and @ are reserved in SMT-LIB";
+      ss << "cannot declare or define symbol `" << name
+         << "'; symbols starting with . and @ are reserved in SMT-LIB";
       parseError(ss.str());
     }
     else if (isOperatorEnabled(name))
@@ -329,7 +345,8 @@ class Smt2 : public Parser
     d_lastNamedTerm = std::make_pair(e, name);
   }
 
-  void clearLastNamedTerm() {
+  void clearLastNamedTerm()
+  {
     d_lastNamedTerm = std::make_pair(api::Term(), "");
   }
 
@@ -346,31 +363,6 @@ class Smt2 : public Parser
   api::Term mkAbstractValue(const std::string& name);
 
   /**
-   * Adds a constructor to sygus datatype dt whose sygus operator is term.
-   *
-   * ntsToUnres contains a mapping from non-terminal symbols to the unresolved
-   * types they correspond to. This map indicates how the argument term should
-   * be interpreted (instances of symbols from the domain of ntsToUnres
-   * correspond to constructor arguments).
-   *
-   * The sygus operator that is actually added to dt corresponds to replacing
-   * each occurrence of non-terminal symbols from the domain of ntsToUnres
-   * with bound variables via purifySygusGTerm, and binding these variables
-   * via a lambda.
-   */
-  void addSygusConstructorTerm(
-      api::DatatypeDecl& dt,
-      api::Term term,
-      std::map<api::Term, api::Sort>& ntsToUnres) const;
-  /**
-   * This adds constructors to dt for sygus variables in sygusVars whose
-   * type is argument type. This method should be called when the sygus grammar
-   * term (Variable type) is encountered.
-   */
-  void addSygusConstructorVariables(api::DatatypeDecl& dt,
-                                    const std::vector<api::Term>& sygusVars,
-                                    api::Sort type) const;
-  /**
    * Smt2 parser provides its own checkDeclaration, which does the
    * same as the base, but with some more helpful errors.
    */
@@ -475,22 +467,6 @@ class Smt2 : public Parser
   //------------------------- end processing parse operators
  private:
 
-  /** Purify sygus grammar term
-   *
-   * This returns a term where all occurrences of non-terminal symbols (those
-   * in the domain of ntsToUnres) are replaced by fresh variables. For each
-   * variable replaced in this way, we add the fresh variable it is replaced
-   * with to args, and the unresolved type corresponding to the non-terminal
-   * symbol to cargs (constructor args). In other words, args contains the
-   * free variables in the term returned by this method (which should be bound
-   * by a lambda), and cargs contains the types of the arguments of the
-   * sygus constructor.
-   */
-  api::Term purifySygusGTerm(api::Term term,
-                             std::map<api::Term, api::Sort>& ntsToUnres,
-                             std::vector<api::Term>& args,
-                             std::vector<api::Sort>& cargs) const;
-
   void addArithmeticOperators();
 
   void addTranscendentalOperators();
@@ -519,7 +495,7 @@ class Smt2 : public Parser
   api::Term mkAnd(const std::vector<api::Term>& es);
 }; /* class Smt2 */
 
-}/* CVC4::parser namespace */
-}/* CVC4 namespace */
+}  // namespace parser
+}  // namespace CVC4
 
 #endif /* CVC4__PARSER__SMT2_H */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index d6b304a78..45cc2426c 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -2071,33 +2071,32 @@ static void toStream(std::ostream& out, const SynthFunCommand* c)
 {
   out << '(' << c->getCommandName() << ' ' << CVC4::quoteSymbol(c->getSymbol())
       << ' ';
-  Type type = c->getFunction().getType();
-  const std::vector<Expr>& vars = c->getVars();
-  Assert(!type.isFunction() || !vars.empty());
+  const std::vector<api::Term>& vars = c->getVars();
   out << '(';
-  if (type.isFunction())
+  if (!vars.empty())
   {
     // print variable list
-    std::vector<Expr>::const_iterator i = vars.begin(), i_end = vars.end();
-    Assert(i != i_end);
-    out << '(' << *i << ' ' << i->getType() << ')';
+    std::vector<api::Term>::const_iterator i = vars.begin(), i_end = vars.end();
+    out << '(' << *i << ' ' << i->getSort() << ')';
     ++i;
     while (i != i_end)
     {
-      out << " (" << *i << ' ' << i->getType() << ')';
+      out << " (" << *i << ' ' << i->getSort() << ')';
       ++i;
     }
-    FunctionType ft = type;
-    type = ft.getRangeType();
   }
   out << ')';
   // if not invariant-to-synthesize, print return type
   if (!c->isInv())
   {
-    out << ' ' << type;
+    out << ' ' << c->getSort();
   }
+  out << '\n';
   // print grammar, if any
-  toStreamSygusGrammar(out, c->getSygusType());
+  if (c->getGrammar() != nullptr)
+  {
+    out << *c->getGrammar();
+  }
   out << ')';
 }
 
@@ -2152,7 +2151,10 @@ static void toStream(std::ostream& out, const GetAbductCommand* c)
   out << c->getConjecture();
 
   // print grammar, if any
-  toStreamSygusGrammar(out, c->getGrammarType());
+  if (c->getGrammar() != nullptr)
+  {
+    out << *c->getGrammar();
+  }
   out << ')';
 }
 
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 2e36190b4..97a51277b 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -90,7 +90,6 @@ ostream& operator<<(ostream& out, const CommandStatus* s)
   return out;
 }
 
-
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out, BenchmarkStatus status)
 {
@@ -137,7 +136,7 @@ std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps)
 
 Command::Command() : d_commandStatus(nullptr), d_muted(false) {}
 
-Command::Command(api::Solver* solver)
+Command::Command(const api::Solver* solver)
     : d_solver(solver), d_commandStatus(nullptr), d_muted(false)
 {
 }
@@ -652,40 +651,49 @@ std::string DeclareSygusFunctionCommand::getCommandName() const
 }
 
 /* -------------------------------------------------------------------------- */
-/* class SynthFunCommand                                                    */
+/* class SynthFunCommand                                                      */
 /* -------------------------------------------------------------------------- */
 
-SynthFunCommand::SynthFunCommand(const std::string& id,
-                                 Expr func,
-                                 Type sygusType,
+SynthFunCommand::SynthFunCommand(const api::Solver* solver,
+                                 const std::string& id,
+                                 api::Term fun,
+                                 const std::vector<api::Term>& vars,
+                                 api::Sort sort,
                                  bool isInv,
-                                 const std::vector<Expr>& vars)
+                                 api::Grammar* g)
     : DeclarationDefinitionCommand(id),
-      d_func(func),
-      d_sygusType(sygusType),
+      d_fun(fun),
+      d_vars(vars),
+      d_sort(sort),
       d_isInv(isInv),
-      d_vars(vars)
+      d_grammar(g)
 {
+  d_solver = solver;
 }
 
-SynthFunCommand::SynthFunCommand(const std::string& id,
-                                 Expr func,
-                                 Type sygusType,
-                                 bool isInv)
-    : SynthFunCommand(id, func, sygusType, isInv, {})
+api::Term SynthFunCommand::getFunction() const { return d_fun; }
+
+const std::vector<api::Term>& SynthFunCommand::getVars() const
 {
+  return d_vars;
 }
 
-Expr SynthFunCommand::getFunction() const { return d_func; }
-const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; }
-Type SynthFunCommand::getSygusType() const { return d_sygusType; }
+api::Sort SynthFunCommand::getSort() const { return d_sort; }
 bool SynthFunCommand::isInv() const { return d_isInv; }
 
+const api::Grammar* SynthFunCommand::getGrammar() const { return d_grammar; }
+
 void SynthFunCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+    smtEngine->declareSynthFun(d_symbol,
+                               d_fun.getExpr(),
+                               d_grammar == nullptr
+                                   ? d_sort.getType()
+                                   : d_grammar->resolve().getType(),
+                               d_isInv,
+                               api::termVectorToExprs(d_vars));
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -697,15 +705,13 @@ void SynthFunCommand::invoke(SmtEngine* smtEngine)
 Command* SynthFunCommand::exportTo(ExprManager* exprManager,
                                    ExprManagerMapCollection& variableMap)
 {
-  return new SynthFunCommand(d_symbol,
-                             d_func.exportTo(exprManager, variableMap),
-                             d_sygusType.exportTo(exprManager, variableMap),
-                             d_isInv);
+  Unimplemented();
 }
 
 Command* SynthFunCommand::clone() const
 {
-  return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+  return new SynthFunCommand(
+      d_solver, d_symbol, d_fun, d_vars, d_sort, d_isInv, d_grammar);
 }
 
 std::string SynthFunCommand::getCommandName() const
@@ -1352,7 +1358,7 @@ Command* DefineNamedFunctionCommand::clone() const
 /* -------------------------------------------------------------------------- */
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
-    api::Solver* solver,
+    const api::Solver* solver,
     api::Term func,
     const std::vector<api::Term>& formals,
     api::Term formula,
@@ -1365,7 +1371,7 @@ DefineFunctionRecCommand::DefineFunctionRecCommand(
 }
 
 DefineFunctionRecCommand::DefineFunctionRecCommand(
-    api::Solver* solver,
+    const api::Solver* solver,
     const std::vector<api::Term>& funcs,
     const std::vector<std::vector<api::Term>>& formals,
     const std::vector<api::Term>& formulas,
@@ -2094,40 +2100,49 @@ std::string GetSynthSolutionCommand::getCommandName() const
   return "get-instantiations";
 }
 
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+/* -------------------------------------------------------------------------- */
+/* class GetInterpolCommand                                                   */
+/* -------------------------------------------------------------------------- */
+
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
                                        const std::string& name,
                                        api::Term conj)
     : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
 {
 }
-GetInterpolCommand::GetInterpolCommand(api::Solver* solver,
+GetInterpolCommand::GetInterpolCommand(const api::Solver* solver,
                                        const std::string& name,
                                        api::Term conj,
-                                       const Type& gtype)
+                                       api::Grammar* g)
     : Command(solver),
       d_name(name),
       d_conj(conj),
-      d_sygus_grammar_type(gtype),
+      d_sygus_grammar(g),
       d_resultStatus(false)
 {
 }
 
 api::Term GetInterpolCommand::getConjecture() const { return d_conj; }
-Type GetInterpolCommand::getGrammarType() const { return d_sygus_grammar_type; }
+
+const api::Grammar* GetInterpolCommand::getGrammar() const
+{
+  return d_sygus_grammar;
+}
+
 api::Term GetInterpolCommand::getResult() const { return d_result; }
 
 void GetInterpolCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    if (d_sygus_grammar_type.isNull())
+    if (!d_sygus_grammar)
     {
       d_resultStatus = d_solver->getInterpolant(d_conj, d_result);
     }
     else
     {
       d_resultStatus =
-          d_solver->getInterpolant(d_conj, d_sygus_grammar_type, d_result);
+          d_solver->getInterpolant(d_conj, *d_sygus_grammar, d_result);
     }
     d_commandStatus = CommandSuccess::instance();
   }
@@ -2167,7 +2182,8 @@ Command* GetInterpolCommand::exportTo(ExprManager* exprManager,
 
 Command* GetInterpolCommand::clone() const
 {
-  GetInterpolCommand* c = new GetInterpolCommand(d_solver, d_name, d_conj);
+  GetInterpolCommand* c =
+      new GetInterpolCommand(d_solver, d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
   c->d_resultStatus = d_resultStatus;
   return c;
@@ -2178,42 +2194,50 @@ std::string GetInterpolCommand::getCommandName() const
   return "get-interpol";
 }
 
-GetAbductCommand::GetAbductCommand() {}
-GetAbductCommand::GetAbductCommand(const std::string& name, Expr conj)
-    : d_name(name), d_conj(conj), d_resultStatus(false)
+/* -------------------------------------------------------------------------- */
+/* class GetAbductCommand                                                     */
+/* -------------------------------------------------------------------------- */
+
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+                                   const std::string& name,
+                                   api::Term conj)
+    : Command(solver), d_name(name), d_conj(conj), d_resultStatus(false)
 {
 }
-GetAbductCommand::GetAbductCommand(const std::string& name,
-                                   Expr conj,
-                                   const Type& gtype)
-    : d_name(name),
+GetAbductCommand::GetAbductCommand(const api::Solver* solver,
+                                   const std::string& name,
+                                   api::Term conj,
+                                   api::Grammar* g)
+    : Command(solver),
+      d_name(name),
       d_conj(conj),
-      d_sygus_grammar_type(gtype),
+      d_sygus_grammar(g),
       d_resultStatus(false)
 {
 }
 
-Expr GetAbductCommand::getConjecture() const { return d_conj; }
-Type GetAbductCommand::getGrammarType() const { return d_sygus_grammar_type; }
+api::Term GetAbductCommand::getConjecture() const { return d_conj; }
+
+const api::Grammar* GetAbductCommand::getGrammar() const
+{
+  return d_sygus_grammar;
+}
+
 std::string GetAbductCommand::getAbductName() const { return d_name; }
-Expr GetAbductCommand::getResult() const { return d_result; }
+api::Term GetAbductCommand::getResult() const { return d_result; }
 
 void GetAbductCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    Node conjNode = Node::fromExpr(d_conj);
-    Node resn;
-    if (d_sygus_grammar_type.isNull())
+    if (!d_sygus_grammar)
     {
-      d_resultStatus = smtEngine->getAbduct(conjNode, resn);
+      d_resultStatus = d_solver->getAbduct(d_conj, d_result);
     }
     else
     {
-      TypeNode gtype = TypeNode::fromType(d_sygus_grammar_type);
-      d_resultStatus = smtEngine->getAbduct(conjNode, gtype, resn);
+      d_resultStatus = d_solver->getAbduct(d_conj, *d_sygus_grammar, d_result);
     }
-    d_result = resn.toExpr();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (exception& e)
@@ -2246,19 +2270,13 @@ void GetAbductCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* GetAbductCommand::exportTo(ExprManager* exprManager,
                                     ExprManagerMapCollection& variableMap)
 {
-  GetAbductCommand* c =
-      new GetAbductCommand(d_name, d_conj.exportTo(exprManager, variableMap));
-  c->d_sygus_grammar_type =
-      d_sygus_grammar_type.exportTo(exprManager, variableMap);
-  c->d_result = d_result.exportTo(exprManager, variableMap);
-  c->d_resultStatus = d_resultStatus;
-  return c;
+  Unimplemented();
 }
 
 Command* GetAbductCommand::clone() const
 {
-  GetAbductCommand* c = new GetAbductCommand(d_name, d_conj);
-  c->d_sygus_grammar_type = d_sygus_grammar_type;
+  GetAbductCommand* c =
+      new GetAbductCommand(d_solver, d_name, d_conj, d_sygus_grammar);
   c->d_result = d_result;
   c->d_resultStatus = d_resultStatus;
   return c;
diff --git a/src/smt/command.h b/src/smt/command.h
index 552847fee..1674e0a62 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -121,6 +121,7 @@ class CVC4_PUBLIC CommandStatus
  protected:
   // shouldn't construct a CommandStatus (use a derived class)
   CommandStatus() {}
+
  public:
   virtual ~CommandStatus() {}
   void toStream(std::ostream& out,
@@ -196,7 +197,7 @@ class CVC4_PUBLIC Command
   typedef CommandPrintSuccess printsuccess;
 
   Command();
-  Command(api::Solver* solver);
+  Command(const api::Solver* solver);
   Command(const Command& cmd);
 
   virtual ~Command();
@@ -273,7 +274,7 @@ class CVC4_PUBLIC Command
   }; /* class Command::ExportTransformer */
 
   /** The solver instance that this command is associated with. */
-  api::Solver* d_solver;
+  const api::Solver* d_solver;
 
   /**
    * This field contains a command status if the command has been
@@ -290,7 +291,7 @@ class CVC4_PUBLIC Command
    * successful execution.
    */
   bool d_muted;
-};   /* class Command */
+}; /* class Command */
 
 /**
  * EmptyCommands are the residue of a command after the parser handles
@@ -507,12 +508,12 @@ class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand
 class CVC4_PUBLIC DefineFunctionRecCommand : public Command
 {
  public:
-  DefineFunctionRecCommand(api::Solver* solver,
+  DefineFunctionRecCommand(const api::Solver* solver,
                            api::Term func,
                            const std::vector<api::Term>& formals,
                            api::Term formula,
                            bool global);
-  DefineFunctionRecCommand(api::Solver* solver,
+  DefineFunctionRecCommand(const api::Solver* solver,
                            const std::vector<api::Term>& funcs,
                            const std::vector<std::vector<api::Term> >& formals,
                            const std::vector<api::Term>& formula,
@@ -715,20 +716,23 @@ class CVC4_PUBLIC DeclareSygusFunctionCommand
 class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
 {
  public:
-  SynthFunCommand(const std::string& id,
-                  Expr func,
-                  Type sygusType,
+  SynthFunCommand(const api::Solver* solver,
+                  const std::string& id,
+                  api::Term fun,
+                  const std::vector<api::Term>& vars,
+                  api::Sort sort,
                   bool isInv,
-                  const std::vector<Expr>& vars);
-  SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv);
+                  api::Grammar* g);
   /** returns the function-to-synthesize */
-  Expr getFunction() const;
+  api::Term getFunction() const;
   /** returns the input variables of the function-to-synthesize */
-  const std::vector<Expr>& getVars() const;
-  /** returns the sygus type of the function-to-synthesize */
-  Type getSygusType() const;
+  const std::vector<api::Term>& getVars() const;
+  /** returns the sygus sort of the function-to-synthesize */
+  api::Sort getSort() const;
   /** returns whether the function-to-synthesize should be an invariant */
   bool isInv() const;
+  /** Get the sygus grammar given for the synth fun command */
+  const api::Grammar* getGrammar() const;
 
   /** invokes this command
    *
@@ -746,17 +750,15 @@ class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
 
  protected:
   /** the function-to-synthesize */
-  Expr d_func;
-  /** sygus type of the function-to-synthesize
-   *
-   * If this type is a "sygus datatype" then it encodes a grammar for the
-   * possible varlues of the function-to-sytnhesize
-   */
-  Type d_sygusType;
+  api::Term d_fun;
+  /** the input variables of the function-to-synthesize */
+  std::vector<api::Term> d_vars;
+  /** sort of the function-to-synthesize */
+  api::Sort d_sort;
   /** whether the function-to-synthesize should be an invariant */
   bool d_isInv;
-  /** the input variables of the function-to-synthesize */
-  std::vector<Expr> d_vars;
+  /** optional grammar for the possible values of the function-to-sytnhesize */
+  api::Grammar* d_grammar;
 };
 
 /** Declares a sygus constraint */
@@ -1039,7 +1041,7 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
   SmtEngine* d_smtEngine;
 }; /* class GetSynthSolutionCommand */
 
-/** The command (get-interpol s B)
+/** The command (get-interpol s B (G)?)
  *
  * This command asks for an interpolant from the current set of assertions and
  * conjecture (goal) B.
@@ -1051,19 +1053,19 @@ class CVC4_PUBLIC GetSynthSolutionCommand : public Command
 class CVC4_PUBLIC GetInterpolCommand : public Command
 {
  public:
-  GetInterpolCommand(api::Solver* solver,
+  GetInterpolCommand(const api::Solver* solver,
                      const std::string& name,
                      api::Term conj);
-  /** The argument gtype is the grammar of the interpolation query */
-  GetInterpolCommand(api::Solver* solver,
+  /** The argument g is the grammar of the interpolation query */
+  GetInterpolCommand(const api::Solver* solver,
                      const std::string& name,
                      api::Term conj,
-                     const Type& gtype);
+                     api::Grammar* g);
 
   /** Get the conjecture of the interpolation query */
   api::Term getConjecture() const;
-  /** Get the grammar sygus datatype type given for the interpolation query */
-  Type getGrammarType() const;
+  /** Get the sygus grammar given for the interpolation query */
+  const api::Grammar* getGrammar() const;
   /** Get the result of the query, which is the solution to the interpolation
    * query. */
   api::Term getResult() const;
@@ -1080,11 +1082,8 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
   std::string d_name;
   /** The conjecture of the interpolation query */
   api::Term d_conj;
-  /**
-   * The (optional) grammar of the interpolation query, expressed as a sygus
-   * datatype type.
-   */
-  Type d_sygus_grammar_type;
+  /** The (optional) grammar of the interpolation query */
+  api::Grammar* d_sygus_grammar;
   /** the return status of the command */
   bool d_resultStatus;
   /** the return expression of the command */
@@ -1100,25 +1099,29 @@ class CVC4_PUBLIC GetInterpolCommand : public Command
  * find a predicate P, then the output response of this command is:
  *   (define-fun s () Bool P)
  *
- * A grammar type G can be optionally provided to indicate the syntactic
- * restrictions on the possible solutions returned.
+ * A grammar G can be optionally provided to indicate the syntactic restrictions
+ * on the possible solutions returned.
  */
 class CVC4_PUBLIC GetAbductCommand : public Command
 {
  public:
-  GetAbductCommand();
-  GetAbductCommand(const std::string& name, Expr conj);
-  GetAbductCommand(const std::string& name, Expr conj, const Type& gtype);
+  GetAbductCommand(const api::Solver* solver,
+                   const std::string& name,
+                   api::Term conj);
+  GetAbductCommand(const api::Solver* solver,
+                   const std::string& name,
+                   api::Term conj,
+                   api::Grammar* g);
 
   /** Get the conjecture of the abduction query */
-  Expr getConjecture() const;
-  /** Get the grammar type given for the abduction query */
-  Type getGrammarType() const;
+  api::Term getConjecture() const;
+  /** Get the grammar given for the abduction query */
+  const api::Grammar* getGrammar() const;
   /** Get the name of the abduction predicate for the abduction query */
   std::string getAbductName() const;
   /** Get the result of the query, which is the solution to the abduction query.
    */
-  Expr getResult() const;
+  api::Term getResult() const;
 
   void invoke(SmtEngine* smtEngine) override;
   void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
@@ -1131,16 +1134,13 @@ class CVC4_PUBLIC GetAbductCommand : public Command
   /** The name of the abduction predicate */
   std::string d_name;
   /** The conjecture of the abduction query */
-  Expr d_conj;
-  /**
-   * The (optional) grammar of the abduction query, expressed as a sygus
-   * datatype type.
-   */
-  Type d_sygus_grammar_type;
+  api::Term d_conj;
+  /** The (optional) grammar of the abduction query */
+  api::Grammar* d_sygus_grammar;
   /** the return status of the command */
   bool d_resultStatus;
   /** the return expression of the command */
-  Expr d_result;
+  api::Term d_result;
 }; /* class GetAbductCommand */
 
 class CVC4_PUBLIC GetQuantifierEliminationCommand : public Command
@@ -1177,6 +1177,7 @@ class CVC4_PUBLIC GetUnsatAssumptionsCommand : public Command
                     ExprManagerMapCollection& variableMap) override;
   Command* clone() const override;
   std::string getCommandName() const override;
+
  protected:
   std::vector<Expr> d_result;
 }; /* class GetUnsatAssumptionsCommand */
@@ -1454,6 +1455,6 @@ class CVC4_PUBLIC DeclarationSequence : public CommandSequence
 {
 };
 
-} /* CVC4 namespace */
+}  // namespace CVC4
 
 #endif /* CVC4__COMMAND_H */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6d1e7ffbc..91ff522b5 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1604,7 +1604,9 @@ void SmtEngine::declareSynthFun(const std::string& id,
     setUserAttribute("sygus-synth-grammar", func, attr_value, "");
   }
   Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
-  Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
+  // dumping SynthFunCommand from smt-engine is currently broken (please take at
+  // CVC4/cvc4-projects#211)
+  // Dump("raw-benchmark") << SynthFunCommand(id, func, sygusType, isInv, vars);
   // sygus conjecture is now stale
   setSygusConjectureStale();
 }