Support sygus version 2 format (#3066)

1 files changed, 46 insertions, 3 deletions

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 2ac796166..3afbcd61a 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -233,8 +233,10 @@ class Smt2 : public Parser
   {
     return language::isInputLang_smt2_6(getLanguage(), exact);
   }
-
-  bool sygus() const { return getLanguage() == language::input::LANG_SYGUS; }
+  /** Are we using a sygus language? */
+  bool sygus() const;
+  /** Are we using the sygus version 1.0 format? */
+  bool sygus_v1() const;
 
   /**
    * Returns true if the language that we are parsing (SMT-LIB version >=2.5
@@ -332,6 +334,30 @@ class Smt2 : public Parser
                         std::vector<std::string>& unresolved_gterm_sym,
                         std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin );
 
+  /**
+   * Adds a constructor to sygus datatype dt whose sygus operator is term.
+   *
+   * ntsToUnres contains a mapping from non-terminal symbols to the unresolved
+   * types they correspond to. This map indicates how the argument term should
+   * be interpreted (instances of symbols from the domain of ntsToUnres
+   * correspond to constructor arguments).
+   *
+   * The sygus operator that is actually added to dt corresponds to replacing
+   * each occurrence of non-terminal symbols from the domain of ntsToUnres
+   * with bound variables via purifySygusGTerm, and binding these variables
+   * via a lambda.
+   */
+  void addSygusConstructorTerm(Datatype& dt,
+                               Expr term,
+                               std::map<Expr, Type>& ntsToUnres) const;
+  /**
+   * This adds constructors to dt for sygus variables in sygusVars whose
+   * type is argument type. This method should be called when the sygus grammar
+   * term (Variable type) is encountered.
+   */
+  void addSygusConstructorVariables(Datatype& dt,
+                                    std::vector<Expr>& sygusVars,
+                                    Type type) const;
 
   /**
    * Smt2 parser provides its own checkDeclaration, which does the
@@ -351,7 +377,8 @@ class Smt2 : public Parser
       return;
     }else{
       //it is allowable in sygus
-      if( sygus() && name[0]=='-' ){
+      if (sygus_v1() && name[0] == '-')
+      {
         //do not check anything
         return;
       }
@@ -449,6 +476,22 @@ private:
                              const std::vector<Type>& ltypes,
                              std::vector<Expr>& lvars);
 
+  /** Purify sygus grammar term
+   *
+   * This returns a term where all occurrences of non-terminal symbols (those
+   * in the domain of ntsToUnres) are replaced by fresh variables. For each
+   * variable replaced in this way, we add the fresh variable it is replaced
+   * with to args, and the unresolved type corresponding to the non-terminal
+   * symbol to cargs (constructor args). In other words, args contains the
+   * free variables in the term returned by this method (which should be bound
+   * by a lambda), and cargs contains the types of the arguments of the
+   * sygus constructor.
+   */
+  Expr purifySygusGTerm(Expr term,
+                        std::map<Expr, Type>& ntsToUnres,
+                        std::vector<Expr>& args,
+                        std::vector<Type>& cargs) const;
+
   void addArithmeticOperators();
 
   void addTranscendentalOperators();