diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:33:41 -0700 |
commit | 89ba584531115b7f6d47088d7614368ea05ab9d8 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/theory/uf/equality_engine.h | |
parent | 324ca0376c960c75f621f0102eeaa1186589dda7 (diff) |
Merging proof branch
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f30f1e8a0..843e7ce7f 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -902,11 +902,17 @@ 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 ) const; + void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const; };/* class EqProof */ } // Namespace eq |