diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-13 23:31:13 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-02-13 23:31:13 -0600 |
| commit | 08289dd911aff28110baf0fd815fd912f8b76fd3 (patch) | |
| tree | 74cb9775532373b6f24e54bfaf471dc1ef0bae24 /src/parser/parser.cpp | |
| parent | d84d67018234bb6bb24dd9183a888892c3bfd4d7 (diff) | |
Update sygus v1 parser to use ParseOp utility (#3756)
Diffstat (limited to 'src/parser/parser.cpp')
| -rw-r--r-- | src/parser/parser.cpp | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 9829b70d9..af193c04b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -138,6 +138,11 @@ Expr Parser::getExpressionForNameAndType(const std::string& name, Type t) { } Kind Parser::getKindForFunction(Expr fun) { + Kind k = getExprManager()->operatorToKind(fun); + if (k != UNDEFINED_KIND) + { + return k; + } Type t = fun.getType(); if (t.isFunction()) { @@ -155,11 +160,7 @@ Kind Parser::getKindForFunction(Expr fun) { { return APPLY_TESTER; } - else - { - parseError("internal error: unhandled function application kind"); - return UNDEFINED_KIND; - } + return UNDEFINED_KIND; } Type Parser::getSort(const std::string& name) { |