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

3 files changed, 135 insertions, 114 deletions

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();
 }