From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 8 Nov 2021 18:57:12 +0000 (-0600)
Subject: Evaluate cast-to-real operator (#7599)
X-Git-Tag: cvc5-1.0.0~864
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=20d8fe633c1f113dceade2df232a35db03e6288c;p=cvc5.git

Evaluate cast-to-real operator (#7599)

Fixes cvc5/cvc5-projects#341.
---

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 2d6c3de55..f7c5ddf0f 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -491,6 +491,13 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(x.abs());
           break;
         }
+        case kind::CAST_TO_REAL:
+        {
+          // casting to real is a no-op
+          const Rational& x = results[currNode[0]].d_rat;
+          results[currNode] = EvalResult(x);
+          break;
+        }
         case kind::CONST_STRING:
           results[currNode] = EvalResult(currNodeVal.getConst<String>());
           break;