From: Tim King <taking@cs.nyu.edu>
Date: Sat, 8 Mar 2014 19:42:35 +0000 (-0500)
Subject: Fixing name changes that cam in from the merge.
X-Git-Tag: cvc5-1.0.0~7035^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f47a28a18bb9a599514e199d355b8e793cf06de;p=cvc5.git

Fixing name changes that cam in from the merge.
---

diff --git a/src/theory/arith/arith_ite_utils.cpp b/src/theory/arith/arith_ite_utils.cpp
index 61bf5c76e..4f182fb69 100644
--- a/src/theory/arith/arith_ite_utils.cpp
+++ b/src/theory/arith/arith_ite_utils.cpp
@@ -120,7 +120,7 @@ Node ArithIteUtils::reduceVariablesInItes(Node n){
   return Node::null();
 }
 
-ArithIteUtils::ArithIteUtils(ContainsTermITEVistor& contains,
+ArithIteUtils::ArithIteUtils(ContainsTermITEVisitor& contains,
                              context::Context* uc,
                              TheoryModel* model)
   : d_contains(contains)
diff --git a/src/theory/arith/arith_ite_utils.h b/src/theory/arith/arith_ite_utils.h
index fab0f32cb..5bdcd52da 100644
--- a/src/theory/arith/arith_ite_utils.h
+++ b/src/theory/arith/arith_ite_utils.h
@@ -18,14 +18,14 @@
 
 namespace CVC4 {
 namespace theory {
-class ContainsTermITEVistor;
+class ContainsTermITEVisitor;
 class SubstitutionMap;
 class TheoryModel;
 
 namespace arith {
 
 class ArithIteUtils {
-  ContainsTermITEVistor& d_contains;
+  ContainsTermITEVisitor& d_contains;
   SubstitutionMap* d_subs;
   TheoryModel* d_model;
 
@@ -56,7 +56,7 @@ class ArithIteUtils {
   std::vector<Node> d_orBinEqs;
 
 public:
-  ArithIteUtils(ContainsTermITEVistor& contains,
+  ArithIteUtils(ContainsTermITEVisitor& contains,
                 context::Context* userContext,
                 TheoryModel* model);
   ~ArithIteUtils();
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 2a263857a..80d1152da 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1492,7 +1492,7 @@ bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
   // Do theory specific preprocessing passes
   if(d_logicInfo.isTheoryEnabled(theory::THEORY_ARITH)){
     if(!simpDidALotOfWork){
-      ContainsTermITEVistor& contains = *d_iteRemover.getContainsVisitor();
+      ContainsTermITEVisitor& contains = *d_iteRemover.getContainsVisitor();
       arith::ArithIteUtils aiteu(contains, d_userContext, getModel());
       bool anyItes = false;
       for(size_t i = 0;  i < assertions.size(); ++i){