diff options
| author | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
|---|---|---|
| committer | Guy <katz911@gmail.com> | 2016-06-01 17:41:17 -0700 |
| commit | de0dd1dc966b05467f1a5443ff33094262f5076a (patch) | |
| tree | 46a8539229fc31226b416755e6a88c18476ecffc /src/theory/uf/equality_engine.h | |
| parent | 89ba584531115b7f6d47088d7614368ea05ab9d8 (diff) | |
Revert "Merging proof branch"
This reverts commit 89ba584531115b7f6d47088d7614368ea05ab9d8.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
| -rw-r--r-- | src/theory/uf/equality_engine.h | 8 |
1 files changed, 1 insertions, 7 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 843e7ce7f..f30f1e8a0 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -902,17 +902,11 @@ public: class EqProof { public: - class PrettyPrinter { - public: - virtual ~PrettyPrinter() {} - virtual std::string printTag(unsigned tag) = 0; - }; - EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){} unsigned d_id; Node d_node; std::vector< EqProof * > d_children; - void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; + void debug_print( const char * c, unsigned tb = 0 ) const; };/* class EqProof */ } // Namespace eq |