diff options
Diffstat (limited to 'src/expr/term_context.cpp')
| -rw-r--r-- | src/expr/term_context.cpp | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/src/expr/term_context.cpp b/src/expr/term_context.cpp index d339a3d28..7f8aa9eac 100644 --- a/src/expr/term_context.cpp +++ b/src/expr/term_context.cpp @@ -15,6 +15,8 @@ #include "expr/term_context.h" +#include "theory/theory.h" + namespace cvc5 { uint32_t TermContext::computeValueOp(TNode t, uint32_t tval) const @@ -133,4 +135,13 @@ void PolarityTermContext::getFlags(uint32_t val, bool& hasPol, bool& pol) pol = val == 2; } +uint32_t TheoryLeafTermContext::initialValue() const { return 0; } + +uint32_t TheoryLeafTermContext::computeValue(TNode t, + uint32_t tval, + size_t index) const +{ + return theory::Theory::isLeafOf(t, d_theoryId) ? 1 : tval; +} + } // namespace cvc5 |