Flatten sygus grammars during parsing. Remove duplicate operators from grammars.

2 files changed, 10 insertions, 1 deletions

diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp
index 7eb93b8ff..91387bc41 100644
--- a/src/expr/expr_manager_template.cpp
+++ b/src/expr/expr_manager_template.cpp
@@ -519,6 +519,12 @@ Expr ExprManager::operatorOf(Kind k) {
   return d_nodeManager->operatorOf(k).toExpr();
 }
 
+Kind ExprManager::operatorToKind(Expr e) {
+  NodeManagerScope nms(d_nodeManager);
+
+  return d_nodeManager->operatorToKind( e.getNode() );
+}
+
 /** Make a function type from domain to range. */
 FunctionType ExprManager::mkFunctionType(Type domain, Type range) {
   NodeManagerScope nms(d_nodeManager);
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 8acb7489f..d7c89ecdc 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -319,7 +319,10 @@ public:
    * e.getConst<CVC4::Kind>() will yield k.
    */
   Expr operatorOf(Kind k);
-
+  
+  /** Get a Kind from an operator expression */
+  Kind operatorToKind(Expr e);
+  
   /** Make a function type from domain to range. */
   FunctionType mkFunctionType(Type domain, Type range);