Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)

This PR is part of migrating commands. DeclareSygusVarCommand and SynthFunCommand now call public API function instead of their corresponding SmtEngine functions. Those two commands don't fully initialize the solver anymore. Some operations in SygusInterpol::solveInterpolation, which creates an interpolation sub-solver, depend on the solver being fully initialized and were affected by this change. Those operations are now executed by the main solver instead of the sub-solver, which is not fully initialized by the time they are needed.

3 files changed, 24 insertions, 96 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 232723fc0..7c1c5dc3e 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -537,12 +537,12 @@ command [std::unique_ptr<CVC4::Command>* cmd]
 
 sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
 @declarations {
-  CVC4::api::Term expr, expr2;
+  CVC4::api::Term expr, expr2, fun;
   CVC4::api::Sort t, range;
   std::vector<std::string> names;
   std::vector<std::pair<std::string, CVC4::api::Sort> > sortedVarNames;
-  std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
-  std::string name, fun;
+  std::vector<CVC4::api::Term> sygusVars;
+  std::string name;
   bool isInv;
   CVC4::api::Grammar* grammar = nullptr;
 }
@@ -552,7 +552,8 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
     { PARSER_STATE->checkUserSymbol(name); }
     sortSymbol[t,CHECK_DECLARED]
     {
-      api::Term var = PARSER_STATE->bindBoundVar(name, t);
+      api::Term var = SOLVER->mkSygusVar(t, name);
+      PARSER_STATE->defineVar(name, var);
       cmd.reset(new DeclareSygusVarCommand(name, var, t));
     }
   | /* synth-fun */
@@ -560,22 +561,36 @@ sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
       | SYNTH_INV_TOK { isInv = true; range = SOLVER->getBooleanSort(); }
     )
     { PARSER_STATE->checkThatLogicIsSet(); }
-    symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
+    symbol[name,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     ( sortSymbol[range,CHECK_DECLARED] )?
     {
-      synthFunFactory.reset(new Smt2::SynthFunFactory(
-          PARSER_STATE, fun, isInv, range, sortedVarNames));
+      PARSER_STATE->pushScope(true);
+      sygusVars = PARSER_STATE->bindBoundVars(sortedVarNames);
     }
     (
       // optionally, read the sygus grammar
       //
       // `grammar` specifies the required grammar for the function to
       // synthesize, expressed as a type
-      sygusGrammar[grammar, synthFunFactory->getSygusVars(), fun]
+      sygusGrammar[grammar, sygusVars, name]
     )?
     {
-      cmd = synthFunFactory->mkCommand(grammar);
+      Debug("parser-sygus") << "Define synth fun : " << name << std::endl;
+
+      fun = isInv ? (grammar == nullptr
+                         ? SOLVER->synthInv(name, sygusVars)
+                         : SOLVER->synthInv(name, sygusVars, *grammar))
+                  : (grammar == nullptr
+                         ? SOLVER->synthFun(name, sygusVars, range)
+                         : SOLVER->synthFun(name, sygusVars, range, *grammar));
+
+      Debug("parser-sygus") << "...read synth fun " << name << std::endl;
+      PARSER_STATE->popScope();
+      // we do not allow overloading for synth fun
+      PARSER_STATE->defineVar(name, fun);
+      cmd = std::unique_ptr<Command>(
+          new SynthFunCommand(name, fun, sygusVars, range, isInv, grammar));
     }
   | /* constraint */
     CONSTRAINT_TOK {
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index 81a4bd4a6..629164593 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -482,50 +482,6 @@ void Smt2::resetAssertions() {
   pushScope(true);
 }
 
-Smt2::SynthFunFactory::SynthFunFactory(
-    Smt2* smt2,
-    const std::string& id,
-    bool isInv,
-    api::Sort range,
-    std::vector<std::pair<std::string, api::Sort>>& sortedVarNames)
-    : d_smt2(smt2), d_id(id), d_sort(range), d_isInv(isInv)
-{
-  if (range.isNull())
-  {
-    smt2->parseError("Must supply return type for synth-fun.");
-  }
-  if (range.isFunction())
-  {
-    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);
-  }
-
-  api::Sort funSort = varSorts.empty()
-                          ? range
-                          : d_smt2->d_solver->mkFunctionSort(varSorts, range);
-
-  // we do not allow overloading for synth fun
-  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);
-}
-
-std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(api::Grammar* grammar)
-{
-  Debug("parser-sygus") << "...read synth fun " << d_id << std::endl;
-  d_smt2->popScope();
-  return std::unique_ptr<Command>(
-      new SynthFunCommand(d_id, d_fun, d_sygusVars, d_sort, d_isInv, grammar));
-}
-
 std::unique_ptr<Command> Smt2::invConstraint(
     const std::vector<std::string>& names)
 {
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 5fcf49637..1aa0ebac7 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -195,49 +195,6 @@ class Smt2 : public Parser
   void resetAssertions();
 
   /**
-   * Class for creating instances of `SynthFunCommand`s. Creating an instance
-   * of this class pushes the scope, destroying it pops the scope.
-   */
-  class SynthFunFactory
-  {
-   public:
-    /**
-     * Creates an instance of `SynthFunFactory`.
-     *
-     * @param smt2 Pointer to the parser state
-     * @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
-     * @param sortedVarNames The parameters of the function-to-synthesize
-     */
-    SynthFunFactory(
-        Smt2* smt2,
-        const std::string& id,
-        bool isInv,
-        api::Sort range,
-        std::vector<std::pair<std::string, api::Sort>>& sortedVarNames);
-
-    const std::vector<api::Term>& getSygusVars() const { return d_sygusVars; }
-
-    /**
-     * Create an instance of `SynthFunCommand`.
-     *
-     * @param grammar Optional grammar associated with the synth-fun command
-     * @return The instance of `SynthFunCommand`
-     */
-    std::unique_ptr<Command> mkCommand(api::Grammar* grammar);
-
-   private:
-    Smt2* d_smt2;
-    std::string d_id;
-    api::Term d_fun;
-    api::Sort d_sort;
-    bool d_isInv;
-    std::vector<api::Term> d_sygusVars;
-  };
-
-  /**
    * Creates a command that adds an invariant constraint.
    *
    * @param names Name of four symbols corresponding to the