From e8288f7fca8ee391fcf97b7f3867fa9581a8d094 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 11 Jun 2018 18:58:57 -0700 Subject: Evaluator: support other theories for equality --- src/theory/evaluator.cpp | 25 ++++++++++++++++++++++++- 1 file changed, 24 insertions(+), 1 deletion(-) 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; } -- cgit v1.2.3