[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, 75 insertions, 16 deletions

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;
 
   /**