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

1 files changed, 6 insertions, 0 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);