diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-11 18:58:57 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-11 18:59:30 -0700 |
commit | e8288f7fca8ee391fcf97b7f3867fa9581a8d094 (patch) | |
tree | 3f30479359183f6354aecd59fafbd8b0591e09ee | |
parent | 6d3f13fe351cf22bb3fbf10b8819a473e91f4d0d (diff) |
Evaluator: support other theories for equalityeval3
-rw-r--r-- | src/theory/evaluator.cpp | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 15ad20b1e..e029dd57c 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -17,6 +17,7 @@ #include "theory/evaluator.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/theory.h" namespace CVC4 { namespace theory { @@ -181,7 +182,29 @@ Node Evaluator::eval(TNode n, Result lhs = d_results[currNode[0]]; Result rhs = d_results[currNode[1]]; - d_results[currNode] = Result(lhs.d_bv == rhs.d_bv); + switch (Theory::theoryOf(currNode[0])) + { + case THEORY_BOOL: + { + d_results[currNode] = Result(lhs.d_bool == rhs.d_bool); + break; + } + + case THEORY_BV: + { + d_results[currNode] = Result(lhs.d_bv == rhs.d_bv); + break; + } + + default: + { + Trace("evaluator") << "Theory " << Theory::theoryOf(currNode[0]) + << " not supported" << std::endl; + d_results[currNode] = Result(); + break; + } + } + break; } |