Update sygus v1 parser to use ParseOp utility (#3756)

1 files changed, 8 insertions, 5 deletions

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 642b81fb0..b0ef2328f 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -29,6 +29,7 @@
 #include "expr/kind.h"
 #include "expr/symbol_table.h"
 #include "parser/input.h"
+#include "parser/parse_op.h"
 #include "parser/parser_exception.h"
 #include "util/unsafe_interrupt_exception.h"
 
@@ -58,7 +59,8 @@ public:
     gterm_ignore,
   };
   Type d_type;
-  Expr d_expr;
+  /** The parsed operator */
+  ParseOp d_op;
   std::vector< Expr > d_let_vars;
   unsigned d_gterm_type;
   std::string d_name;
@@ -367,11 +369,12 @@ public:
   virtual Expr getExpressionForNameAndType(const std::string& name, Type t);
   
   /**
-   * Returns the kind that should be used for applications of expression fun, where
-   * fun has "function-like" type, i.e. where checkFunctionLike(fun) returns true. 
-   * Returns a parse error if fun does not have function-like type.
+   * Returns the kind that should be used for applications of expression fun.
+   * This is a generalization of ExprManager::operatorToKind that also
+   * handles variables whose types are "function-like", i.e. where
+   * checkFunctionLike(fun) returns true.
    * 
-   * For example, this function returns
+   * For examples of the latter, this function returns
    *   APPLY_UF if fun has function type, 
    *   APPLY_CONSTRUCTOR if fun has constructor type.
    */