Introducing internal commands for SyGuS commands (#2627)

4 files changed, 851 insertions, 30 deletions

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 3d838d21c..51cb6663f 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -562,17 +562,299 @@ Command* QueryCommand::clone() const
 std::string QueryCommand::getCommandName() const { return "query"; }
 
 /* -------------------------------------------------------------------------- */
+/* class DeclareSygusVarCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusVarCommand::DeclareSygusVarCommand(const std::string& id,
+                                               Expr var,
+                                               Type t)
+    : DeclarationDefinitionCommand(id), d_var(var), d_type(t)
+{
+}
+
+Expr DeclareSygusVarCommand::getVar() const { return d_var; }
+Type DeclareSygusVarCommand::getType() const { return d_type; }
+
+void DeclareSygusVarCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->declareSygusVar(d_symbol, d_var, d_type);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* DeclareSygusVarCommand::exportTo(ExprManager* exprManager,
+                                          ExprManagerMapCollection& variableMap)
+{
+  return new DeclareSygusVarCommand(d_symbol,
+                                    d_var.exportTo(exprManager, variableMap),
+                                    d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusVarCommand::clone() const
+{
+  return new DeclareSygusVarCommand(d_symbol, d_var, d_type);
+}
+
+std::string DeclareSygusVarCommand::getCommandName() const
+{
+  return "declare-var";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusPrimedVarCommand */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusPrimedVarCommand::DeclareSygusPrimedVarCommand(
+    const std::string& id, Type t)
+    : DeclarationDefinitionCommand(id), d_type(t)
+{
+}
+
+Type DeclareSygusPrimedVarCommand::getType() const { return d_type; }
+
+void DeclareSygusPrimedVarCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->declareSygusPrimedVar(d_symbol, d_type);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* DeclareSygusPrimedVarCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  return new DeclareSygusPrimedVarCommand(
+      d_symbol, d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusPrimedVarCommand::clone() const
+{
+  return new DeclareSygusPrimedVarCommand(d_symbol, d_type);
+}
+
+std::string DeclareSygusPrimedVarCommand::getCommandName() const
+{
+  return "declare-primed-var";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class DeclareSygusFunctionCommand                                          */
+/* -------------------------------------------------------------------------- */
+
+DeclareSygusFunctionCommand::DeclareSygusFunctionCommand(const std::string& id,
+                                                         Expr func,
+                                                         Type t)
+    : DeclarationDefinitionCommand(id), d_func(func), d_type(t)
+{
+}
+
+Expr DeclareSygusFunctionCommand::getFunction() const { return d_func; }
+Type DeclareSygusFunctionCommand::getType() const { return d_type; }
+
+void DeclareSygusFunctionCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->declareSygusFunctionVar(d_symbol, d_func, d_type);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* DeclareSygusFunctionCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  return new DeclareSygusFunctionCommand(
+      d_symbol,
+      d_func.exportTo(exprManager, variableMap),
+      d_type.exportTo(exprManager, variableMap));
+}
+
+Command* DeclareSygusFunctionCommand::clone() const
+{
+  return new DeclareSygusFunctionCommand(d_symbol, d_func, d_type);
+}
+
+std::string DeclareSygusFunctionCommand::getCommandName() const
+{
+  return "declare-fun";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SynthFunCommand                                                    */
+/* -------------------------------------------------------------------------- */
+
+SynthFunCommand::SynthFunCommand(const std::string& id,
+                                 Expr func,
+                                 Type sygusType,
+                                 bool isInv,
+                                 const std::vector<Expr>& vars)
+    : DeclarationDefinitionCommand(id),
+      d_func(func),
+      d_sygusType(sygusType),
+      d_isInv(isInv),
+      d_vars(vars)
+{
+}
+
+SynthFunCommand::SynthFunCommand(const std::string& id,
+                                 Expr func,
+                                 Type sygusType,
+                                 bool isInv)
+    : SynthFunCommand(id, func, sygusType, isInv, {})
+{
+}
+
+Expr SynthFunCommand::getFunction() const { return d_func; }
+const std::vector<Expr>& SynthFunCommand::getVars() const { return d_vars; }
+Type SynthFunCommand::getSygusType() const { return d_sygusType; }
+bool SynthFunCommand::isInv() const { return d_isInv; }
+
+void SynthFunCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->declareSynthFun(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* SynthFunCommand::exportTo(ExprManager* exprManager,
+                                   ExprManagerMapCollection& variableMap)
+{
+  return new SynthFunCommand(d_symbol,
+                             d_func.exportTo(exprManager, variableMap),
+                             d_sygusType.exportTo(exprManager, variableMap),
+                             d_isInv);
+}
+
+Command* SynthFunCommand::clone() const
+{
+  return new SynthFunCommand(d_symbol, d_func, d_sygusType, d_isInv, d_vars);
+}
+
+std::string SynthFunCommand::getCommandName() const
+{
+  return d_isInv ? "synth-inv" : "synth-fun";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SygusConstraintCommand */
+/* -------------------------------------------------------------------------- */
+
+SygusConstraintCommand::SygusConstraintCommand(const Expr& e) : d_expr(e) {}
+
+void SygusConstraintCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->assertSygusConstraint(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Expr SygusConstraintCommand::getExpr() const { return d_expr; }
+
+Command* SygusConstraintCommand::exportTo(ExprManager* exprManager,
+                                          ExprManagerMapCollection& variableMap)
+{
+  return new SygusConstraintCommand(d_expr.exportTo(exprManager, variableMap));
+}
+
+Command* SygusConstraintCommand::clone() const
+{
+  return new SygusConstraintCommand(d_expr);
+}
+
+std::string SygusConstraintCommand::getCommandName() const
+{
+  return "constraint";
+}
+
+/* -------------------------------------------------------------------------- */
+/* class SygusInvConstraintCommand */
+/* -------------------------------------------------------------------------- */
+
+SygusInvConstraintCommand::SygusInvConstraintCommand(
+    const std::vector<Expr>& predicates)
+    : d_predicates(predicates)
+{
+}
+
+SygusInvConstraintCommand::SygusInvConstraintCommand(const Expr& inv,
+                                                     const Expr& pre,
+                                                     const Expr& trans,
+                                                     const Expr& post)
+    : SygusInvConstraintCommand(std::vector<Expr>{inv, pre, trans, post})
+{
+}
+
+void SygusInvConstraintCommand::invoke(SmtEngine* smtEngine)
+{
+  try
+  {
+    smtEngine->assertSygusInvConstraint(
+        d_predicates[0], d_predicates[1], d_predicates[2], d_predicates[3]);
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+const std::vector<Expr>& SygusInvConstraintCommand::getPredicates() const
+{
+  return d_predicates;
+}
+
+Command* SygusInvConstraintCommand::exportTo(
+    ExprManager* exprManager, ExprManagerMapCollection& variableMap)
+{
+  return new SygusInvConstraintCommand(d_predicates);
+}
+
+Command* SygusInvConstraintCommand::clone() const
+{
+  return new SygusInvConstraintCommand(d_predicates);
+}
+
+std::string SygusInvConstraintCommand::getCommandName() const
+{
+  return "inv-constraint";
+}
+
+/* -------------------------------------------------------------------------- */
 /* class CheckSynthCommand                                                    */
 /* -------------------------------------------------------------------------- */
 
-CheckSynthCommand::CheckSynthCommand() : d_expr() {}
-CheckSynthCommand::CheckSynthCommand(const Expr& expr) : d_expr(expr) {}
-Expr CheckSynthCommand::getExpr() const { return d_expr; }
 void CheckSynthCommand::invoke(SmtEngine* smtEngine)
 {
   try
   {
-    d_result = smtEngine->checkSynth(d_expr);
+    d_result = smtEngine->checkSynth();
     d_commandStatus = CommandSuccess::instance();
     smt::SmtScope scope(smtEngine);
     d_solution.clear();
@@ -624,18 +906,10 @@ void CheckSynthCommand::printResult(std::ostream& out, uint32_t verbosity) const
 Command* CheckSynthCommand::exportTo(ExprManager* exprManager,
                                      ExprManagerMapCollection& variableMap)
 {
-  CheckSynthCommand* c =
-      new CheckSynthCommand(d_expr.exportTo(exprManager, variableMap));
-  c->d_result = d_result;
-  return c;
+  return new CheckSynthCommand();
 }
 
-Command* CheckSynthCommand::clone() const
-{
-  CheckSynthCommand* c = new CheckSynthCommand(d_expr);
-  c->d_result = d_result;
-  return c;
-}
+Command* CheckSynthCommand::clone() const { return new CheckSynthCommand(); }
 
 std::string CheckSynthCommand::getCommandName() const { return "check-synth"; }
 
diff --git a/src/smt/command.h b/src/smt/command.h
index be6d84305..f7824c1aa 100644
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -613,29 +613,255 @@ class CVC4_PUBLIC QueryCommand : public Command
   std::string getCommandName() const override;
 }; /* class QueryCommand */
 
-class CVC4_PUBLIC CheckSynthCommand : public Command
+/* ------------------- sygus commands  ------------------ */
+
+/** Declares a sygus universal variable */
+class CVC4_PUBLIC DeclareSygusVarCommand : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusVarCommand(const std::string& id, Expr var, Type type);
+  /** returns the declared variable */
+  Expr getVar() const;
+  /** returns the declared variable's type */
+  Type getType() const;
+  /** invokes this command
+   *
+   * The declared sygus variable is communicated to the SMT engine in case a
+   * synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the declared variable */
+  Expr d_var;
+  /** the declared variable's type */
+  Type d_type;
+};
+
+/** Declares a sygus primed variable, for invariant problems
+ *
+ * We do not actually build expressions for the declared variables because they
+ * are unnecessary for building SyGuS problems.
+ */
+class CVC4_PUBLIC DeclareSygusPrimedVarCommand
+    : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusPrimedVarCommand(const std::string& id, Type type);
+  /** returns the declared primed variable's type */
+  Type getType() const;
+
+  /** invokes this command
+   *
+   * The type of the primed variable is communicated to the SMT engine for
+   * debugging purposes when a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the type of the declared primed variable */
+  Type d_type;
+};
+
+/** Declares a sygus universal function variable */
+class CVC4_PUBLIC DeclareSygusFunctionCommand
+    : public DeclarationDefinitionCommand
+{
+ public:
+  DeclareSygusFunctionCommand(const std::string& id, Expr func, Type type);
+  /** returns the declared function variable */
+  Expr getFunction() const;
+  /** returns the declared function variable's type */
+  Type getType() const;
+  /** invokes this command
+   *
+   * The declared sygus function variable is communicated to the SMT engine in
+   * case a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the declared function variable */
+  Expr d_func;
+  /** the declared function variable's type */
+  Type d_type;
+};
+
+/** Declares a sygus function-to-synthesize
+ *
+ * This command is also used for the special case in which we are declaring an
+ * invariant-to-synthesize
+ */
+class CVC4_PUBLIC SynthFunCommand : public DeclarationDefinitionCommand
 {
  public:
-  CheckSynthCommand();
-  CheckSynthCommand(const Expr& expr);
+  SynthFunCommand(const std::string& id,
+                  Expr func,
+                  Type sygusType,
+                  bool isInv,
+                  const std::vector<Expr>& vars);
+  SynthFunCommand(const std::string& id, Expr func, Type sygusType, bool isInv);
+  /** returns the function-to-synthesize */
+  Expr 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;
+  /** returns whether the function-to-synthesize should be an invariant */
+  bool isInv() const;
+
+  /** invokes this command
+   *
+   * The declared function-to-synthesize is communicated to the SMT engine in
+   * case a synthesis conjecture is built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ 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;
+  /** 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;
+};
 
+/** Declares a sygus constraint */
+class CVC4_PUBLIC SygusConstraintCommand : public Command
+{
+ public:
+  SygusConstraintCommand(const Expr& e);
+  /** returns the declared constraint */
   Expr getExpr() const;
-  Result getResult() const;
+  /** invokes this command
+   *
+   * The declared constraint is communicated to the SMT engine in case a
+   * synthesis conjecture is built later on.
+   */
   void invoke(SmtEngine* smtEngine) override;
-  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  /** exports command to given expression manager */
   Command* exportTo(ExprManager* exprManager,
                     ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
   Command* clone() const override;
+  /** returns this command's name */
   std::string getCommandName() const override;
 
  protected:
-  /** the assertion of check-synth */
+  /** the declared constraint */
   Expr d_expr;
+};
+
+/** Declares a sygus invariant constraint
+ *
+ * Invarint constraints are declared in a somewhat implicit manner in the SyGuS
+ * language: they are declared in terms of the previously declared
+ * invariant-to-synthesize, precondition, transition relation and condition.
+ *
+ * The actual constraint must be built such that the invariant is not stronger
+ * than the precondition, not weaker than the postcondition and inductive
+ * w.r.t. the transition relation.
+ */
+class CVC4_PUBLIC SygusInvConstraintCommand : public Command
+{
+ public:
+  SygusInvConstraintCommand(const std::vector<Expr>& predicates);
+  SygusInvConstraintCommand(const Expr& inv,
+                            const Expr& pre,
+                            const Expr& trans,
+                            const Expr& post);
+  /** returns the place holder predicates */
+  const std::vector<Expr>& getPredicates() const;
+  /** invokes this command
+   *
+   * The place holders are communicated to the SMT engine and the actual
+   * invariant constraint is built, in case an actual synthesis conjecture is
+   * built later on.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
+  /** the place holder predicates with which to build the actual constraint
+   * (i.e. the invariant, precondition, transition relation and postcondition)
+   */
+  std::vector<Expr> d_predicates;
+};
+
+/** Declares a synthesis conjecture */
+class CVC4_PUBLIC CheckSynthCommand : public Command
+{
+ public:
+  CheckSynthCommand(){};
+  /** returns the result of the check-synth call */
+  Result getResult() const;
+  /** prints the result of the check-synth-call */
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+  /** invokes this command
+   *
+   * This invocation makes the SMT engine build a synthesis conjecture based on
+   * previously declared information (such as universal variables,
+   * functions-to-synthesize and so on), set up attributes to guide the solving,
+   * and then perform a satisfiability check, whose result is stored in
+   * d_result.
+   */
+  void invoke(SmtEngine* smtEngine) override;
+  /** exports command to given expression manager */
+  Command* exportTo(ExprManager* exprManager,
+                    ExprManagerMapCollection& variableMap) override;
+  /** creates a copy of this command */
+  Command* clone() const override;
+  /** returns this command's name */
+  std::string getCommandName() const override;
+
+ protected:
   /** result of the check-synth call */
   Result d_result;
   /** string stream that stores the output of the solution */
   std::stringstream d_solution;
-}; /* class CheckSynthCommand */
+};
+
+/* ------------------- sygus commands  ------------------ */
 
 // this is TRANSFORM in the CVC presentation language
 class CVC4_PUBLIC SimplifyCommand : public Command
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 196da6b9c..a2dd8276b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -497,6 +497,31 @@ class SmtEnginePrivate : public NodeManagerListener {
   /* Finishes the initialization of the private portion of SMTEngine. */
   void finishInit();
 
+  /*------------------- sygus utils ------------------*/
+  /**
+   * sygus variables declared (from "declare-var" and "declare-fun" commands)
+   *
+   * The SyGuS semantics for declared variables is that they are implicitly
+   * universally quantified in the constraints.
+   */
+  std::vector<Node> d_sygusVars;
+  /** types of sygus primed variables (for debugging) */
+  std::vector<Type> d_sygusPrimedVarTypes;
+  /** sygus constraints */
+  std::vector<Node> d_sygusConstraints;
+  /** functions-to-synthesize */
+  std::vector<Node> d_sygusFunSymbols;
+  /** maps functions-to-synthesize to their respective input variables lists */
+  std::map<Node, std::vector<Node>> d_sygusFunVars;
+  /** maps functions-to-synthesize to their respective syntactic restrictions
+   *
+   * If function has syntactic restrictions, these are encoded as a SyGuS
+   * datatype type
+   */
+  std::map<Node, TypeNode> d_sygusFunSyntax;
+
+  /*------------------- end of sygus utils ------------------*/
+
  private:
   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
 
@@ -3692,14 +3717,6 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void)
   return res;
 }
 
-Result SmtEngine::checkSynth(const Expr& e)
-{
-  SmtScope smts(this);
-  Trace("smt") << "Check synth: " << e << std::endl;
-  Trace("smt-synth") << "Check synthesis conjecture: " << e << std::endl;
-  return checkSatisfiability(e, true, false);
-}
-
 Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
 {
   Assert(ex.getExprManager() == d_exprManager);
@@ -3724,6 +3741,235 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore)
   return quickCheck().asValidityResult();
 }/* SmtEngine::assertFormula() */
 
+/*
+   --------------------------------------------------------------------------
+    Handling SyGuS commands
+   --------------------------------------------------------------------------
+*/
+
+void SmtEngine::declareSygusVar(const std::string& id, Expr var, Type type)
+{
+  d_private->d_sygusVars.push_back(Node::fromExpr(var));
+  Trace("smt") << "SmtEngine::declareSygusVar: " << var << "\n";
+}
+
+void SmtEngine::declareSygusPrimedVar(const std::string& id, Type type)
+{
+#ifdef CVC4_ASSERTIONS
+  d_private->d_sygusPrimedVarTypes.push_back(type);
+#endif
+  Trace("smt") << "SmtEngine::declareSygusPrimedVar: " << id << "\n";
+}
+
+void SmtEngine::declareSygusFunctionVar(const std::string& id,
+                                        Expr var,
+                                        Type type)
+{
+  d_private->d_sygusVars.push_back(Node::fromExpr(var));
+  Trace("smt") << "SmtEngine::declareSygusFunctionVar: " << var << "\n";
+}
+
+void SmtEngine::declareSynthFun(const std::string& id,
+                                Expr func,
+                                Type sygusType,
+                                bool isInv,
+                                const std::vector<Expr>& vars)
+{
+  Node fn = Node::fromExpr(func);
+  d_private->d_sygusFunSymbols.push_back(fn);
+  std::vector<Node> var_nodes;
+  for (const Expr& v : vars)
+  {
+    var_nodes.push_back(Node::fromExpr(v));
+  }
+  d_private->d_sygusFunVars[fn] = var_nodes;
+  // whether sygus type encodes syntax restrictions
+  if (sygusType.isDatatype()
+      && static_cast<DatatypeType>(sygusType).getDatatype().isSygus())
+  {
+    d_private->d_sygusFunSyntax[fn] = TypeNode::fromType(sygusType);
+  }
+  Trace("smt") << "SmtEngine::declareSynthFun: " << func << "\n";
+}
+
+void SmtEngine::assertSygusConstraint(Expr constraint)
+{
+  d_private->d_sygusConstraints.push_back(constraint);
+
+  Trace("smt") << "SmtEngine::assertSygusConstrant: " << constraint << "\n";
+}
+
+void SmtEngine::assertSygusInvConstraint(const Expr& inv,
+                                         const Expr& pre,
+                                         const Expr& trans,
+                                         const Expr& post)
+{
+  SmtScope smts(this);
+  // build invariant constraint
+
+  // get variables (regular and their respective primed versions)
+  std::vector<Node> terms, vars, primed_vars;
+  terms.push_back(Node::fromExpr(inv));
+  terms.push_back(Node::fromExpr(pre));
+  terms.push_back(Node::fromExpr(trans));
+  terms.push_back(Node::fromExpr(post));
+  // variables are built based on the invariant type
+  FunctionType t = static_cast<FunctionType>(inv.getType());
+  std::vector<Type> argTypes = t.getArgTypes();
+  for (const Type& ti : argTypes)
+  {
+    TypeNode tn = TypeNode::fromType(ti);
+    vars.push_back(d_nodeManager->mkBoundVar(tn));
+    d_private->d_sygusVars.push_back(vars.back());
+    std::stringstream ss;
+    ss << vars.back() << "'";
+    primed_vars.push_back(d_nodeManager->mkBoundVar(ss.str(), tn));
+    d_private->d_sygusVars.push_back(primed_vars.back());
+#ifdef CVC4_ASSERTIONS
+    bool find_new_declared_var = false;
+    for (const Type& t : d_private->d_sygusPrimedVarTypes)
+    {
+      if (t == ti)
+      {
+        d_private->d_sygusPrimedVarTypes.erase(
+            std::find(d_private->d_sygusPrimedVarTypes.begin(),
+                      d_private->d_sygusPrimedVarTypes.end(),
+                      t));
+        find_new_declared_var = true;
+        break;
+      }
+    }
+    if (!find_new_declared_var)
+    {
+      Warning()
+          << "warning: declared primed variables do not match invariant's "
+             "type\n";
+    }
+#endif
+  }
+
+  // make relevant terms; 0 -> Inv, 1 -> Pre, 2 -> Trans, 3 -> Post
+  for (unsigned i = 0; i < 4; ++i)
+  {
+    Node op = terms[i];
+    Trace("smt-debug") << "Make inv-constraint term #" << i << " : " << op
+                       << " with type " << op.getType() << "...\n";
+    std::vector<Node> children;
+    children.push_back(op);
+    // transition relation applied over both variable lists
+    if (i == 2)
+    {
+      children.insert(children.end(), vars.begin(), vars.end());
+      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
+    }
+    else
+    {
+      children.insert(children.end(), vars.begin(), vars.end());
+    }
+    terms[i] =
+        d_nodeManager->mkNode(i == 0 ? kind::APPLY_UF : kind::APPLY, children);
+    // make application of Inv on primed variables
+    if (i == 0)
+    {
+      children.clear();
+      children.push_back(op);
+      children.insert(children.end(), primed_vars.begin(), primed_vars.end());
+      terms.push_back(d_nodeManager->mkNode(kind::APPLY_UF, children));
+    }
+  }
+  // make constraints
+  std::vector<Node> conj;
+  conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[1], terms[0]));
+  Node term0_and_2 = d_nodeManager->mkNode(kind::AND, terms[0], terms[2]);
+  conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, term0_and_2, terms[4]));
+  conj.push_back(d_nodeManager->mkNode(kind::IMPLIES, terms[0], terms[3]));
+  Node constraint = d_nodeManager->mkNode(kind::AND, conj);
+
+  d_private->d_sygusConstraints.push_back(constraint);
+
+  Trace("smt") << "SmtEngine::assertSygusInvConstrant: " << constraint << "\n";
+}
+
+Result SmtEngine::checkSynth()
+{
+  SmtScope smts(this);
+  // build synthesis conjecture from asserted constraints and declared
+  // variables/functions
+  Node sygusVar =
+      d_nodeManager->mkSkolem("sygus", d_nodeManager->booleanType());
+  Node inst_attr = d_nodeManager->mkNode(kind::INST_ATTRIBUTE, sygusVar);
+  Node sygusAttr = d_nodeManager->mkNode(kind::INST_PATTERN_LIST, inst_attr);
+  std::vector<Node> bodyv;
+  Trace("smt") << "Sygus : Constructing sygus constraint...\n";
+  unsigned n_constraints = d_private->d_sygusConstraints.size();
+  Node body = n_constraints == 0
+                  ? d_nodeManager->mkConst(true)
+                  : (n_constraints == 1
+                         ? d_private->d_sygusConstraints[0]
+                         : d_nodeManager->mkNode(
+                               kind::AND, d_private->d_sygusConstraints));
+  body = body.notNode();
+  Trace("smt") << "...constructed sygus constraint " << body << std::endl;
+  if (!d_private->d_sygusVars.empty())
+  {
+    Node boundVars =
+        d_nodeManager->mkNode(kind::BOUND_VAR_LIST, d_private->d_sygusVars);
+    body = d_nodeManager->mkNode(kind::EXISTS, boundVars, body);
+    Trace("smt") << "...constructed exists " << body << std::endl;
+  }
+  if (!d_private->d_sygusFunSymbols.empty())
+  {
+    Node boundVars = d_nodeManager->mkNode(kind::BOUND_VAR_LIST,
+                                           d_private->d_sygusFunSymbols);
+    body = d_nodeManager->mkNode(kind::FORALL, boundVars, body, sygusAttr);
+  }
+  Trace("smt") << "...constructed forall " << body << std::endl;
+
+  // set attribute for synthesis conjecture
+  setUserAttribute("sygus", sygusVar.toExpr(), {}, "");
+
+  // set attributes for functions-to-synthesize
+  for (const Node& synth_fun : d_private->d_sygusFunSymbols)
+  {
+    // associate var list with function-to-synthesize
+    Assert(d_private->d_sygusFunVars.find(synth_fun)
+           != d_private->d_sygusFunVars.end());
+    const std::vector<Node>& vars = d_private->d_sygusFunVars[synth_fun];
+    Node bvl;
+    if (!vars.empty())
+    {
+      bvl = d_nodeManager->mkNode(kind::BOUND_VAR_LIST, vars);
+    }
+    std::vector<Expr> attr_val_bvl;
+    attr_val_bvl.push_back(bvl.toExpr());
+    setUserAttribute(
+        "sygus-synth-fun-var-list", synth_fun.toExpr(), attr_val_bvl, "");
+    // If the function has syntax restrition, bulid a variable "sfproxy" which
+    // carries the type, a SyGuS datatype that corresponding to the syntactic
+    // restrictions.
+    std::map<Node, TypeNode>::const_iterator it =
+        d_private->d_sygusFunSyntax.find(synth_fun);
+    if (it != d_private->d_sygusFunSyntax.end())
+    {
+      Node sym = d_nodeManager->mkBoundVar("sfproxy", it->second);
+      std::vector<Expr> attr_value;
+      attr_value.push_back(sym.toExpr());
+      setUserAttribute(
+          "sygus-synth-grammar", synth_fun.toExpr(), attr_value, "");
+    }
+  }
+
+  Trace("smt") << "Check synthesis conjecture: " << body << std::endl;
+
+  return checkSatisfiability(body.toExpr(), true, false);
+}
+
+/*
+   --------------------------------------------------------------------------
+    End of Handling SyGuS commands
+   --------------------------------------------------------------------------
+*/
+
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   return node;
 }
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 08bb773d6..5aa59fad7 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -608,11 +608,86 @@ class CVC4_PUBLIC SmtEngine {
    */
   std::vector<Expr> getUnsatAssumptions(void);
 
+  /*------------------- sygus commands  ------------------*/
+
+  /** adds a variable declaration
+   *
+   * Declared SyGuS variables may be used in SyGuS constraints, in which they
+   * are assumed to be universally quantified.
+   */
+  void declareSygusVar(const std::string& id, Expr var, Type type);
+  /** stores information for debugging sygus invariants setup
+   *
+   * Since in SyGuS the commands "declare-primed-var" are not necessary for
+   * building invariant constraints, we only use them to check that the number
+   * of variables declared corresponds to the number of arguments of the
+   * invariant-to-synthesize.
+   */
+  void declareSygusPrimedVar(const std::string& id, Type type);
+  /** adds a function variable declaration
+   *
+   * Is SyGuS semantics declared functions are treated in the same manner as
+   * declared variables, i.e. as universally quantified (function) variables
+   * which can occur in the SyGuS constraints that compose the conjecture to
+   * which a function is being synthesized.
+   */
+  void declareSygusFunctionVar(const std::string& id, Expr var, Type type);
+  /** adds a function-to-synthesize declaration
+   *
+   * The given type may not correspond to the actual function type but to a
+   * datatype encoding the syntax restrictions for the
+   * function-to-synthesize. In this case this information is stored to be used
+   * during solving.
+   *
+   * vars contains the arguments of the function-to-synthesize. These variables
+   * are also stored to be used during solving.
+   *
+   * isInv determines whether the function-to-synthesize is actually an
+   * invariant. This information is necessary if we are dumping a command
+   * corresponding to this declaration, so that it can be properly printed.
+   */
+  void declareSynthFun(const std::string& id,
+                       Expr func,
+                       Type type,
+                       bool isInv,
+                       const std::vector<Expr>& vars);
+  /** adds a regular sygus constraint */
+  void assertSygusConstraint(Expr constraint);
+  /** adds an invariant constraint
+   *
+   * Invariant constraints are not explicitly declared: they are given in terms
+   * of the invariant-to-synthesize, the pre condition, transition relation and
+   * post condition. The actual constraint is built based on the inputs of these
+   * place holder predicates :
+   *
+   * PRE(x) -> INV(x)
+   * INV() ^ TRANS(x, x') -> INV(x')
+   * INV(x) -> POST(x)
+   *
+   * The regular and primed variables are retrieved from the declaration of the
+   * invariant-to-synthesize.
+   */
+  void assertSygusInvConstraint(const Expr& inv,
+                                const Expr& pre,
+                                const Expr& trans,
+                                const Expr& post);
   /**
    * Assert a synthesis conjecture to the current context and call
    * check().  Returns sat, unsat, or unknown result.
+   *
+   * The actual synthesis conjecture is built based on the previously
+   * communicated information to this module (universal variables, defined
+   * functions, functions-to-synthesize, and which constraints compose it). The
+   * built conjecture is a higher-order formula of the form
+   *
+   * exists f1...fn . forall v1...vm . F
+   *
+   * in which f1...fn are the functions-to-synthesize, v1...vm are the declared
+   * universal variables and F is the set of declared constraints.
    */
-  Result checkSynth(const Expr& e) /* throw(Exception) */;
+  Result checkSynth() /* throw(Exception) */;
+
+  /*------------------- end of sygus commands-------------*/
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve