From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 31 Jul 2019 16:01:33 +0000 (-0500)
Subject: Add some missing cases in evaluator (#3133)
X-Git-Tag: cvc5-1.0.0~4063
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd6e11c2887a71f559ab2e278ec944246c346c04;p=cvc5.git

Add some missing cases in evaluator (#3133)
---

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>());