diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-02 19:17:53 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-06-02 19:17:53 +0200 |
commit | fb092ea99c7a670e78dfdd442a19986fdbdab93f (patch) | |
tree | ad52de511073d9fbc368d9ea1636c827c69dbb85 /src/expr/expr_manager_template.cpp | |
parent | 7222fd13c68ee1352dabbe3791fae0ee13d689d1 (diff) |
Flatten sygus grammars during parsing. Remove duplicate operators from grammars.
Diffstat (limited to 'src/expr/expr_manager_template.cpp')
-rw-r--r-- | src/expr/expr_manager_template.cpp | 6 |
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); |