diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-06-03 20:52:49 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-03 18:52:49 -0500 |
| commit | 418b0281e62a6b657da32f6504965269ad90c18b (patch) | |
| tree | 246d51e833789cf5620cdcb46d22bf57ff1b1000 /src/expr/node_manager.cpp | |
| parent | b19d246d75be92a0189b9aaacc71426395b8c098 (diff) | |
(proof-new) Adding rules and proof checker for EUF (#4559)
Diffstat (limited to 'src/expr/node_manager.cpp')
| -rw-r--r-- | src/expr/node_manager.cpp | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index 7bc98f65d..427afd5af 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -865,4 +865,26 @@ void NodeManager::debugHook(int debugFlag){ // For debugging purposes only, DO NOT CHECK IN ANY CODE! } +Kind NodeManager::getKindForFunction(TNode fun) +{ + TypeNode tn = fun.getType(); + if (tn.isFunction()) + { + return kind::APPLY_UF; + } + else if (tn.isConstructor()) + { + return kind::APPLY_CONSTRUCTOR; + } + else if (tn.isSelector()) + { + return kind::APPLY_SELECTOR; + } + else if (tn.isTester()) + { + return kind::APPLY_TESTER; + } + return kind::UNDEFINED_KIND; +} + }/* CVC4 namespace */ |