[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.

1 files changed, 33 insertions, 111 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