Sygus Lambda Grammars (#1390)

1 files changed, 13 insertions, 0 deletions

diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 9614c5524..84c049ce9 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -319,6 +319,19 @@ private:
                                    std::map< CVC4::Type, CVC4::Type >& sygus_to_builtin,
                                    std::map< CVC4::Type, CVC4::Expr >& sygus_to_builtin_expr );
 
+  /** make sygus bound var list
+   *
+   * This is used for converting non-builtin sygus operators to lambda
+   * expressions. It takes as input a datatype and constructor index (for
+   * naming) and a vector of type ltypes.
+   * It appends a bound variable to lvars for each type in ltypes, and returns
+   * a bound variable list whose children are lvars.
+   */
+  Expr makeSygusBoundVarList(Datatype& dt,
+                             unsigned i,
+                             const std::vector<Type>& ltypes,
+                             std::vector<Expr>& lvars);
+
   void addArithmeticOperators();
 
   void addBitvectorOperators();