Support uninterpreted constants in the evaluator (#4777)

2 files changed, 31 insertions, 3 deletions

diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp
index 7a4940328..a7228658d 100644
--- a/src/theory/evaluator.cpp
+++ b/src/theory/evaluator.cpp
@@ -43,6 +43,10 @@ EvalResult::EvalResult(const EvalResult& other)
       new (&d_str) String;
       d_str = other.d_str;
       break;
+    case UCONST:
+      new (&d_uc)
+          UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+      break;
     case INVALID: break;
   }
 }
@@ -67,6 +71,10 @@ EvalResult& EvalResult::operator=(const EvalResult& other)
         new (&d_str) String;
         d_str = other.d_str;
         break;
+      case UCONST:
+        new (&d_uc)
+            UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex());
+        break;
       case INVALID: break;
     }
   }
@@ -91,9 +99,13 @@ EvalResult::~EvalResult()
     {
       d_str.~String();
       break;
-
-      default: break;
     }
+    case UCONST:
+    {
+      d_uc.~UninterpretedConstant();
+      break;
+    }
+    default: break;
   }
 }
 
@@ -106,6 +118,7 @@ Node EvalResult::toNode() const
     case EvalResult::BITVECTOR: return nm->mkConst(d_bv);
     case EvalResult::RATIONAL: return nm->mkConst(d_rat);
     case EvalResult::STRING: return nm->mkConst(d_str);
+    case EvalResult::UCONST: return nm->mkConst(d_uc);
     default:
     {
       Trace("evaluator") << "Missing conversion from " << d_tag << " to node"
@@ -389,7 +402,13 @@ EvalResult Evaluator::evalInternal(
           results[currNode] = EvalResult(r);
           break;
         }
-
+        case kind::UNINTERPRETED_CONSTANT:
+        {
+          const UninterpretedConstant& uc =
+              currNodeVal.getConst<UninterpretedConstant>();
+          results[currNode] = EvalResult(uc);
+          break;
+        }
         case kind::PLUS:
         {
           Rational res = results[currNode[0]].d_rat;
@@ -824,6 +843,11 @@ EvalResult Evaluator::evalInternal(
               results[currNode] = EvalResult(lhs.d_str == rhs.d_str);
               break;
             }
+            case EvalResult::UCONST:
+            {
+              results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc);
+              break;
+            }
 
             default:
             {
diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h
index e986edf1f..059d21e56 100644
--- a/src/theory/evaluator.h
+++ b/src/theory/evaluator.h
@@ -25,6 +25,7 @@
 
 #include "base/output.h"
 #include "expr/node.h"
+#include "expr/uninterpreted_constant.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
 #include "util/string.h"
@@ -45,6 +46,7 @@ struct EvalResult
     BITVECTOR,
     RATIONAL,
     STRING,
+    UCONST,
     INVALID
   } d_tag;
 
@@ -55,6 +57,7 @@ struct EvalResult
     BitVector d_bv;
     Rational d_rat;
     String d_str;
+    UninterpretedConstant d_uc;
   };
 
   EvalResult(const EvalResult& other);
@@ -63,6 +66,7 @@ struct EvalResult
   EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {}
   EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {}
   EvalResult(const String& str) : d_tag(STRING), d_str(str) {}
+  EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {}
 
   EvalResult& operator=(const EvalResult& other);