diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-07-31 11:01:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-07-31 11:01:33 -0500 |
| commit | cd6e11c2887a71f559ab2e278ec944246c346c04 (patch) | |
| tree | 43c5279b75a606074d0c2aa728ad5dfe9dedef51 /src/theory/evaluator.cpp | |
| parent | ed2ed9dffb709c9120890f665983abc594bdc0e5 (diff) | |
Add some missing cases in evaluator (#3133)
Diffstat (limited to 'src/theory/evaluator.cpp')
| -rw-r--r-- | src/theory/evaluator.cpp | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 818f40e8c..ffb5b9fd4 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -259,6 +259,12 @@ EvalResult Evaluator::evalInternal(TNode n, break; } + case kind::UMINUS: + { + const Rational& x = results[currNode[0]].d_rat; + results[currNode] = EvalResult(-x); + break; + } case kind::MULT: { Rational res = results[currNode[0]].d_rat; @@ -277,6 +283,27 @@ EvalResult Evaluator::evalInternal(TNode n, results[currNode] = EvalResult(x >= y); break; } + case kind::LEQ: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x <= y); + break; + } + case kind::GT: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x > y); + break; + } + case kind::LT: + { + const Rational& x = results[currNode[0]].d_rat; + const Rational& y = results[currNode[1]].d_rat; + results[currNode] = EvalResult(x < y); + break; + } case kind::CONST_STRING: results[currNode] = EvalResult(currNodeVal.getConst<String>()); |