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.h | |
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.h')
-rw-r--r-- | src/theory/ite_utilities.h | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/src/theory/ite_utilities.h b/src/theory/ite_utilities.h index d9e6120aa..7f0986ecb 100644 --- a/src/theory/ite_utilities.h +++ b/src/theory/ite_utilities.h @@ -31,7 +31,7 @@ namespace CVC4 { namespace theory { -class ContainsTermITEVistor; +class ContainsTermITEVisitor; class IncomingArcCounter; class TermITEHeightCounter; class ITECompressor; @@ -40,7 +40,7 @@ class ITECareSimplifier; class ITEUtilities { public: - ITEUtilities(ContainsTermITEVistor* containsVisitor); + ITEUtilities(ContainsTermITEVisitor* containsVisitor); ~ITEUtilities(); Node simpITE(TNode assertion); @@ -55,7 +55,7 @@ public: void clear(); private: - ContainsTermITEVistor* d_containsVisitor; + ContainsTermITEVisitor* d_containsVisitor; ITECompressor* d_compressor; ITESimplifier* d_simplifier; ITECareSimplifier* d_careSimp; @@ -64,10 +64,10 @@ private: /** * A caching visitor that computes whether a node contains a term ite. */ -class ContainsTermITEVistor { +class ContainsTermITEVisitor { public: - ContainsTermITEVistor(); - ~ContainsTermITEVistor(); + ContainsTermITEVisitor(); + ~ContainsTermITEVisitor(); /** returns true if a node contains a term ite. */ bool containsTermITE(TNode n); @@ -140,7 +140,7 @@ private: */ class ITECompressor { public: - ITECompressor(ContainsTermITEVistor* contains); + ITECompressor(ContainsTermITEVisitor* contains); ~ITECompressor(); /* returns false if an assertion is discovered to be equal to false. */ @@ -153,7 +153,7 @@ private: Node d_true; /* Copy of true. */ Node d_false; /* Copy of false. */ - ContainsTermITEVistor* d_contains; + ContainsTermITEVisitor* d_contains; std::vector<Node>* d_assertions; IncomingArcCounter d_incoming; @@ -180,7 +180,7 @@ private: class ITESimplifier { public: - ITESimplifier(ContainsTermITEVistor* d_containsVisitor); + ITESimplifier(ContainsTermITEVisitor* d_containsVisitor); ~ITESimplifier(); Node simpITE(TNode assertion); @@ -192,7 +192,7 @@ private: Node d_true; Node d_false; - ContainsTermITEVistor* d_containsVisitor; + ContainsTermITEVisitor* d_containsVisitor; inline bool containsTermITE(TNode n) { return d_containsVisitor->containsTermITE(n); } |