[SMT2 Parser] Move code of `sygusCommand` (#3335)

This commit moves the code in `sygusCommand` in the SMT2 parser to the
`Smt2` class. The original code was pushing and popping the current
scope inline. This commit adds a class `SynthFunFactory` that takes care
of that upon creation and destruction.

3 files changed, 212 insertions, 143 deletions

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index e838398ba..c63bc4a95 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -208,13 +208,12 @@ parseCommand returns [CVC4::Command* cmd_return = NULL]
  */
 parseSygus returns [CVC4::Command* cmd_return = NULL]
 @declarations {
-  std::unique_ptr<CVC4::Command> cmd;
   std::string name;
 }
 @after {
   cmd_return = cmd.release();
 }
-  : LPAREN_TOK sygusCommand[&cmd] RPAREN_TOK
+  : LPAREN_TOK cmd=sygusCommand RPAREN_TOK
   | EOF
   ;
 
@@ -551,19 +550,16 @@ command [std::unique_ptr<CVC4::Command>* cmd]
     }
   ;
 
-sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
+sygusCommand returns [std::unique_ptr<CVC4::Command> cmd]
 @declarations {
-  std::string name, fun;
-  std::vector<std::string> names;
   Expr expr, expr2;
   Type t, range;
-  std::vector<Expr> terms;
-  std::vector<Expr> sygus_vars;
+  std::vector<std::string> names;
   std::vector<std::pair<std::string, Type> > sortedVarNames;
-  Type sygus_ret;
-  Expr synth_fun;
-  Type sygus_type;
+  std::unique_ptr<Smt2::SynthFunFactory> synthFunFactory;
+  std::string name, fun;
   bool isInv;
+  Type grammar;
 }
   : /* declare-var */
     DECLARE_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -572,7 +568,7 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
     sortSymbol[t,CHECK_DECLARED]
     {
       Expr var = PARSER_STATE->mkBoundVar(name, t);
-      cmd->reset(new DeclareSygusVarCommand(name, var, t));
+      cmd.reset(new DeclareSygusVarCommand(name, var, t));
     }
   | /* declare-primed-var */
     DECLARE_PRIMED_VAR_TOK { PARSER_STATE->checkThatLogicIsSet(); }
@@ -582,106 +578,50 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
     {
       // spurious command, we do not need to create a variable. We only keep
       // track of the command for sanity checking / dumping
-      cmd->reset(new DeclareSygusPrimedVarCommand(name, t));
+      cmd.reset(new DeclareSygusPrimedVarCommand(name, t));
     }
 
   | /* synth-fun */
     ( SYNTH_FUN_V1_TOK { isInv = false; }
       | SYNTH_INV_V1_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
     )
-    { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     ( sortSymbol[range,CHECK_DECLARED] )?
     {
-      if (range.isNull())
-      {
-        PARSER_STATE->parseError("Must supply return type for synth-fun.");
-      }
-      if (range.isFunction())
-      {
-        PARSER_STATE->parseError(
-            "Cannot use synth-fun with function return type.");
-      }
-      std::vector<Type> var_sorts;
-      for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
-      {
-        var_sorts.push_back(p.second);
-      }
-      Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
-      Type synth_fun_type = var_sorts.size() > 0
-                                ? EXPR_MANAGER->mkFunctionType(var_sorts, range)
-                                : range;
-      // we do not allow overloading for synth fun
-      synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
-      // set the sygus type to be range by default, which is overwritten below
-      // if a grammar is provided
-      sygus_type = range;
-      // create new scope for parsing the grammar, if any
-      PARSER_STATE->pushScope(true);
-      sygus_vars = PARSER_STATE->mkBoundVars(sortedVarNames);
+      synthFunFactory.reset(new Smt2::SynthFunFactory(
+          PARSER_STATE, fun, isInv, range, sortedVarNames));
     }
     (
       // optionally, read the sygus grammar
       //
-      // the sygus type specifies the required grammar for synth_fun, expressed
-      // as a type
-      sygusGrammarV1[sygus_type, sygus_vars, fun]
+      // `grammar` specifies the required grammar for the function to
+      // synthesize, expressed as a type
+      sygusGrammarV1[grammar, synthFunFactory->getSygusVars(), fun]
     )?
     {
-      PARSER_STATE->popScope();
-      Debug("parser-sygus") << "...read synth fun " << fun << std::endl;
-      cmd->reset(
-          new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars));
+      cmd = synthFunFactory->mkCommand(grammar);
     }
   | /* synth-fun */
     ( SYNTH_FUN_TOK { isInv = false; }
       | SYNTH_INV_TOK { isInv = true; range = EXPR_MANAGER->booleanType(); }
     )
-    { PARSER_STATE->checkThatLogicIsSet(); }
     symbol[fun,CHECK_UNDECLARED,SYM_VARIABLE]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
     ( sortSymbol[range,CHECK_DECLARED] )?
     {
-      if (range.isNull())
-      {
-        PARSER_STATE->parseError("Must supply return type for synth-fun.");
-      }
-      if (range.isFunction())
-      {
-        PARSER_STATE->parseError(
-            "Cannot use synth-fun with function return type.");
-      }
-      std::vector<Type> var_sorts;
-      for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
-      {
-        var_sorts.push_back(p.second);
-      }
-      Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
-      Type synth_fun_type = var_sorts.size() > 0
-                                ? EXPR_MANAGER->mkFunctionType(var_sorts, range)
-                                : range;
-      // we do not allow overloading for synth fun
-      synth_fun = PARSER_STATE->mkBoundVar(fun, synth_fun_type);
-      // set the sygus type to be range by default, which is overwritten below
-      // if a grammar is provided
-      sygus_type = range;
-      // create new scope for parsing the grammar, if any
-      PARSER_STATE->pushScope(true);
-      sygus_vars = PARSER_STATE->mkBoundVars(sortedVarNames);
+      synthFunFactory.reset(new Smt2::SynthFunFactory(
+          PARSER_STATE, fun, isInv, range, sortedVarNames));
     }
     (
       // optionally, read the sygus grammar
       //
-      // the sygus type specifies the required grammar for synth_fun, expressed
-      // as a type
-      sygusGrammar[sygus_type, sygus_vars, fun]
+      // `grammar` specifies the required grammar for the function to
+      // synthesize, expressed as a type
+      sygusGrammar[grammar, synthFunFactory->getSygusVars(), fun]
     )?
     {
-      PARSER_STATE->popScope();
-      Debug("parser-sygus") << "...read synth fun " << fun << std::endl;
-      cmd->reset(
-          new SynthFunCommand(fun, synth_fun, sygus_type, isInv, sygus_vars));
+      cmd = synthFunFactory->mkCommand(grammar);
     }
   | /* constraint */
     CONSTRAINT_TOK {
@@ -691,39 +631,21 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
     }
     term[expr, expr2]
     { Debug("parser-sygus") << "...read constraint " << expr << std::endl;
-      cmd->reset(new SygusConstraintCommand(expr));
-    }
-  | INV_CONSTRAINT_TOK {
-      PARSER_STATE->checkThatLogicIsSet();
-      Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
-      Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
+      cmd.reset(new SygusConstraintCommand(expr));
     }
-    ( symbol[name,CHECK_NONE,SYM_VARIABLE] {
-        if( !terms.empty() ){
-          if (!PARSER_STATE->isDeclared(name))
-          {
-            std::stringstream ss;
-            ss << "Function " << name << " in inv-constraint is not defined.";
-            PARSER_STATE->parseError(ss.str());
-          }
-        }
-        terms.push_back( PARSER_STATE->getVariable(name) );
-      }
-    )+ {
-      if( terms.size()!=4 ){
-        PARSER_STATE->parseError("Bad syntax for inv-constraint: expected 4 "
-                                 "arguments.");
-      }
-
-      cmd->reset(new SygusInvConstraintCommand(terms));
+  | /* inv-constraint */
+    INV_CONSTRAINT_TOK
+    ( symbol[name,CHECK_NONE,SYM_VARIABLE] { names.push_back(name); } )+
+    {
+      cmd = PARSER_STATE->invConstraint(names);
     }
   | /* check-synth */
     CHECK_SYNTH_TOK
     { PARSER_STATE->checkThatLogicIsSet(); }
     {
-      cmd->reset(new CheckSynthCommand());
+      cmd.reset(new CheckSynthCommand());
     }
-  | command[cmd]
+  | command[&cmd]
   ;
 
 /** Reads a sygus grammar
@@ -736,8 +658,8 @@ sygusCommand [std::unique_ptr<CVC4::Command>* cmd]
  * datatypes constructed by this call.
  */
 sygusGrammarV1[CVC4::Type & ret,
-             std::vector<CVC4::Expr>& sygus_vars,
-             std::string& fun]
+               const std::vector<CVC4::Expr>& sygus_vars,
+               const std::string& fun]
 @declarations
 {
   Type t;
@@ -879,7 +801,7 @@ sygusGrammarV1[CVC4::Type & ret,
 // type argument vectors to cargs[index] (where typically N=1)
 // This method may also add new elements pairwise into
 // datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
+sygusGTerm[CVC4::SygusGTerm& sgt, const std::string& fun]
 @declarations {
   std::string name, name2;
   Kind k;
@@ -1013,8 +935,8 @@ sygusGTerm[CVC4::SygusGTerm& sgt, std::string& fun]
  * datatypes constructed by this call.
  */
 sygusGrammar[CVC4::Type & ret,
-             std::vector<CVC4::Expr>& sygusVars,
-             std::string& fun]
+             const std::vector<CVC4::Expr>& sygusVars,
+             const std::string& fun]
 @declarations
 {
   // the pre-declaration
diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp
index bb0881030..ec4fd0fa3 100644
--- a/src/parser/smt2/smt2.cpp
+++ b/src/parser/smt2/smt2.cpp
@@ -627,6 +627,87 @@ void Smt2::resetAssertions() {
   }
 }
 
+Smt2::SynthFunFactory::SynthFunFactory(
+    Smt2* smt2,
+    const std::string& fun,
+    bool isInv,
+    Type range,
+    std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames)
+    : d_smt2(smt2), d_fun(fun), d_isInv(isInv)
+{
+  smt2->checkThatLogicIsSet();
+  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<Type> varSorts;
+  for (const std::pair<std::string, CVC4::Type>& p : sortedVarNames)
+  {
+    varSorts.push_back(p.second);
+  }
+  Debug("parser-sygus") << "Define synth fun : " << fun << std::endl;
+  Type synthFunType =
+      varSorts.size() > 0
+          ? d_smt2->getExprManager()->mkFunctionType(varSorts, range)
+          : range;
+
+  // we do not allow overloading for synth fun
+  d_synthFun = d_smt2->mkBoundVar(fun, synthFunType);
+  // set the sygus type to be range by default, which is overwritten below
+  // if a grammar is provided
+  d_sygusType = range;
+
+  d_smt2->pushScope(true);
+  d_sygusVars = d_smt2->mkBoundVars(sortedVarNames);
+}
+
+Smt2::SynthFunFactory::~SynthFunFactory() { d_smt2->popScope(); }
+
+std::unique_ptr<Command> Smt2::SynthFunFactory::mkCommand(Type grammar)
+{
+  Debug("parser-sygus") << "...read synth fun " << d_fun << std::endl;
+  return std::unique_ptr<Command>(
+      new SynthFunCommand(d_fun,
+                          d_synthFun,
+                          grammar.isNull() ? d_sygusType : grammar,
+                          d_isInv,
+                          d_sygusVars));
+}
+
+std::unique_ptr<Command> Smt2::invConstraint(
+    const std::vector<std::string>& names)
+{
+  checkThatLogicIsSet();
+  Debug("parser-sygus") << "Sygus : define sygus funs..." << std::endl;
+  Debug("parser-sygus") << "Sygus : read inv-constraint..." << std::endl;
+
+  if (names.size() != 4)
+  {
+    parseError(
+        "Bad syntax for inv-constraint: expected 4 "
+        "arguments.");
+  }
+
+  std::vector<Expr> terms;
+  for (const std::string& name : names)
+  {
+    if (!isDeclared(name))
+    {
+      std::stringstream ss;
+      ss << "Function " << name << " in inv-constraint is not defined.";
+      parseError(ss.str());
+    }
+
+    terms.push_back(getVariable(name));
+  }
+
+  return std::unique_ptr<Command>(new SygusInvConstraintCommand(terms));
+}
+
 Command* Smt2::setLogic(std::string name, bool fromCommand)
 {
   if (fromCommand)
@@ -868,17 +949,22 @@ void Smt2::mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& o
 
 //  This method adds N operators to ops[index], N names to cnames[index] and N type argument vectors to cargs[index] (where typically N=1)
 //  This method may also add new elements pairwise into datatypes/sorts/ops/cnames/cargs in the case of non-flat gterms.
-void Smt2::processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
-                              std::vector< CVC4::Datatype >& datatypes,
-                              std::vector< CVC4::Type>& sorts,
-                              std::vector< std::vector<CVC4::Expr> >& ops,
-                              std::vector< std::vector<std::string> >& cnames,
-                              std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                              std::vector< bool >& allow_const,
-                              std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                              std::vector<CVC4::Expr>& sygus_vars,
-                              std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
-                              CVC4::Type& ret, bool isNested ){
+void Smt2::processSygusGTerm(
+    CVC4::SygusGTerm& sgt,
+    int index,
+    std::vector<CVC4::Datatype>& datatypes,
+    std::vector<CVC4::Type>& sorts,
+    std::vector<std::vector<CVC4::Expr>>& ops,
+    std::vector<std::vector<std::string>>& cnames,
+    std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+    std::vector<bool>& allow_const,
+    std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+    const std::vector<CVC4::Expr>& sygus_vars,
+    std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
+    std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
+    CVC4::Type& ret,
+    bool isNested)
+{
   if (sgt.d_gterm_type == SygusGTerm::gterm_op)
   {
     Debug("parser-sygus") << "Add " << sgt.d_expr << " to datatype " << index
@@ -1103,10 +1189,12 @@ Type Smt2::processSygusNestedGTerm( int sub_dt_index, std::string& sub_dname, st
   return t;
 }
 
-void Smt2::setSygusStartIndex( std::string& fun, int startIndex,
-                               std::vector< CVC4::Datatype >& datatypes,
-                               std::vector< CVC4::Type>& sorts,
-                               std::vector< std::vector<CVC4::Expr> >& ops ) {
+void Smt2::setSygusStartIndex(const std::string& fun,
+                              int startIndex,
+                              std::vector<CVC4::Datatype>& datatypes,
+                              std::vector<CVC4::Type>& sorts,
+                              std::vector<std::vector<CVC4::Expr>>& ops)
+{
   if( startIndex>0 ){
     CVC4::Datatype tmp_dt = datatypes[0];
     Type tmp_sort = sorts[0];
@@ -1420,7 +1508,7 @@ Expr Smt2::purifySygusGTerm(Expr term,
 }
 
 void Smt2::addSygusConstructorVariables(Datatype& dt,
-                                        std::vector<Expr>& sygusVars,
+                                        const std::vector<Expr>& sygusVars,
                                         Type type) const
 {
   // each variable of appropriate type becomes a sygus constructor in dt.
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 178634693..5caedb934 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -198,6 +198,60 @@ 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 fun 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& fun,
+        bool isInv,
+        Type range,
+        std::vector<std::pair<std::string, CVC4::Type>>& sortedVarNames);
+    ~SynthFunFactory();
+
+    const std::vector<Expr>& 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(Type grammar);
+
+   private:
+    Smt2* d_smt2;
+    std::string d_fun;
+    Expr d_synthFun;
+    Type d_sygusType;
+    bool d_isInv;
+    std::vector<Expr> d_sygusVars;
+  };
+
+  /**
+   * Creates a command that adds an invariant constraint.
+   *
+   * @param names Name of four symbols corresponding to the
+   *              function-to-synthesize, precondition, postcondition,
+   *              transition relation.
+   * @return The command that adds an invariant constraint
+   */
+  std::unique_ptr<Command> invConstraint(const std::vector<std::string>& names);
+
+  /**
    * Sets the logic for the current benchmark. Declares any logic and
    * theory symbols.
    *
@@ -295,17 +349,21 @@ class Smt2 : public Parser
 
   void mkSygusConstantsForType( const Type& type, std::vector<CVC4::Expr>& ops );
 
-  void processSygusGTerm( CVC4::SygusGTerm& sgt, int index,
-                          std::vector< CVC4::Datatype >& datatypes,
-                          std::vector< CVC4::Type>& sorts,
-                          std::vector< std::vector<CVC4::Expr> >& ops,
-                          std::vector< std::vector<std::string> >& cnames,
-                          std::vector< std::vector< std::vector< CVC4::Type > > >& cargs,
-                          std::vector< bool >& allow_const,
-                          std::vector< std::vector< std::string > >& unresolved_gterm_sym,
-                          std::vector<CVC4::Expr>& sygus_vars,
-                          std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin, std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr,
-                          CVC4::Type& ret, bool isNested = false );
+  void processSygusGTerm(
+      CVC4::SygusGTerm& sgt,
+      int index,
+      std::vector<CVC4::Datatype>& datatypes,
+      std::vector<CVC4::Type>& sorts,
+      std::vector<std::vector<CVC4::Expr>>& ops,
+      std::vector<std::vector<std::string>>& cnames,
+      std::vector<std::vector<std::vector<CVC4::Type>>>& cargs,
+      std::vector<bool>& allow_const,
+      std::vector<std::vector<std::string>>& unresolved_gterm_sym,
+      const std::vector<CVC4::Expr>& sygus_vars,
+      std::map<CVC4::Type, CVC4::Type>& sygus_to_builtin,
+      std::map<CVC4::Type, CVC4::Expr>& sygus_to_builtin_expr,
+      CVC4::Type& ret,
+      bool isNested = false);
 
   static bool pushSygusDatatypeDef( Type t, std::string& dname,
                                     std::vector< CVC4::Datatype >& datatypes,
@@ -324,10 +382,11 @@ class Smt2 : public Parser
                                    std::vector< bool >& allow_const,
                                    std::vector< std::vector< std::string > >& unresolved_gterm_sym );
 
-  void setSygusStartIndex( std::string& fun, int startIndex,
-                           std::vector< CVC4::Datatype >& datatypes,
-                           std::vector< CVC4::Type>& sorts,
-                           std::vector< std::vector<CVC4::Expr> >& ops );
+  void setSygusStartIndex(const std::string& fun,
+                          int startIndex,
+                          std::vector<CVC4::Datatype>& datatypes,
+                          std::vector<CVC4::Type>& sorts,
+                          std::vector<std::vector<CVC4::Expr>>& ops);
 
   void mkSygusDatatype( CVC4::Datatype& dt, std::vector<CVC4::Expr>& ops,
                         std::vector<std::string>& cnames, std::vector< std::vector< CVC4::Type > >& cargs,
@@ -356,7 +415,7 @@ class Smt2 : public Parser
    * term (Variable type) is encountered.
    */
   void addSygusConstructorVariables(Datatype& dt,
-                                    std::vector<Expr>& sygusVars,
+                                    const std::vector<Expr>& sygusVars,
                                     Type type) const;
 
   /**