Add some missing cases in evaluator (#3133)

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 818f40e8c183e91e5908091c915f5394f67833bb..ffb5b9fd45d6f486f4dec67873b5bf67727c2309 100644 (file)
--- 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>());