diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 10:24:04 -0500 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-07 23:48:49 -0500 |
commit | d01269e2d5a02952fbda74dcd9629acfbf23dfd4 (patch) | |
tree | d8f2a90ddd94ade15edf84b48523e7ff76f78554 /src/theory/ite_utilities.cpp | |
parent | 01cff049fac316d84ee05f747975a26b04e9c3a2 (diff) |
Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.
Diffstat (limited to 'src/theory/ite_utilities.cpp')
-rw-r--r-- | src/theory/ite_utilities.cpp | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/theory/ite_utilities.cpp b/src/theory/ite_utilities.cpp index 1b4e096f2..a4af4f26f 100644 --- a/src/theory/ite_utilities.cpp +++ b/src/theory/ite_utilities.cpp @@ -28,6 +28,7 @@ namespace CVC4 { namespace theory { namespace ite { + inline static bool isTermITE(TNode e) { return (e.getKind() == kind::ITE && !e.getType().isBoolean()); } @@ -77,9 +78,7 @@ struct CTIVStackElement { } /* CVC4::theory::ite */ - - -ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor) +ITEUtilities::ITEUtilities(ContainsTermITEVisitor* containsVisitor) : d_containsVisitor(containsVisitor) , d_compressor(NULL) , d_simplifier(NULL) @@ -144,11 +143,11 @@ void ITEUtilities::clear(){ } /********************* */ -/* ContainsTermITEVistor +/* ContainsTermITEVisitor */ -ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {} -ContainsTermITEVistor::~ContainsTermITEVistor(){} -bool ContainsTermITEVistor::containsTermITE(TNode e){ +ContainsTermITEVisitor::ContainsTermITEVisitor(): d_cache() {} +ContainsTermITEVisitor::~ContainsTermITEVisitor(){} +bool ContainsTermITEVisitor::containsTermITE(TNode e){ /* throughout execution skip through NOT nodes. */ e = (e.getKind() == kind::NOT) ? e[0] : e; if(ite::triviallyContainsNoTermITEs(e)){ return false; } @@ -197,7 +196,7 @@ bool ContainsTermITEVistor::containsTermITE(TNode e){ } return foundTermIte; } -void ContainsTermITEVistor::garbageCollect() { +void ContainsTermITEVisitor::garbageCollect() { d_cache.clear(); } @@ -249,7 +248,7 @@ void IncomingArcCounter::clear() { /********************* */ /* ITECompressor */ -ITECompressor::ITECompressor(ContainsTermITEVistor* contains) +ITECompressor::ITECompressor(ContainsTermITEVisitor* contains) : d_contains(contains) , d_assertions(NULL) , d_incoming(true, true) @@ -547,7 +546,7 @@ uint32_t TermITEHeightCounter::termITEHeight(TNode e){ -ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains) +ITESimplifier::ITESimplifier(ContainsTermITEVisitor* contains) : d_containsVisitor(contains) , d_termITEHeight() , d_constantLeaves() @@ -1608,6 +1607,5 @@ Node ITECareSimplifier::simplifyWithCare(TNode e) return substitute(e, substTable, cache); } - } /* namespace theory */ } /* namespace CVC4 */ |