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.h | |
| parent | 7222fd13c68ee1352dabbe3791fae0ee13d689d1 (diff) | |
Flatten sygus grammars during parsing. Remove duplicate operators from grammars.
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 5 |
1 files changed, 4 insertions, 1 deletions
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); |