From 5c61887222630583b48bd26fc914d166f122c252 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Mon, 28 May 2012 16:27:50 +0000
Subject: Added some BV rewrites, fixed bugs in array theory, made ite simp
 work with BV

---
 src/theory/ite_simplifier.cpp | 19 ++++++++-----------
 1 file changed, 8 insertions(+), 11 deletions(-)

(limited to 'src/theory/ite_simplifier.cpp')

diff --git a/src/theory/ite_simplifier.cpp b/src/theory/ite_simplifier.cpp
index 50881af82..7d2b6e333 100644
--- a/src/theory/ite_simplifier.cpp
+++ b/src/theory/ite_simplifier.cpp
@@ -144,19 +144,16 @@ Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVa
 
 Node ITESimplifier::getSimpVar(TypeNode t)
 {
-  if (t.isInteger()) {
-    if (d_simpVarInt.isNull()) {
-      d_simpVarInt = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarInt;
+  std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+  it = d_simpVars.find(t);
+  if (it != d_simpVars.end()) {
+    return (*it).second;
   }
-  if (t.isReal()) {
-    if (d_simpVarReal.isNull()) {
-      d_simpVarReal = NodeManager::currentNM()->mkVar(t);
-    }
-    return d_simpVarReal;
+  else {
+    Node var = NodeManager::currentNM()->mkVar(t);
+    d_simpVars[t] = var;
+    return var;
   }
-  return Node();
 }
 
 
-- 
cgit v1.2.3