From 0f47a28a18bb9a599514e199d355b8e793cf06de Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 8 Mar 2014 14:42:35 -0500 Subject: [PATCH] Fixing name changes that cam in from the merge. --- src/theory/arith/arith_ite_utils.cpp | 2 +- src/theory/arith/arith_ite_utils.h | 6 +++--- src/theory/theory_engine.cpp | 2 +- 3 files changed, 5 insertions(+), 5 deletions(-) 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 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& 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){ -- 2.30.2