diff options
author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2020-07-15 21:40:01 -0300 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-15 21:40:01 -0300 |
commit | 699af1774b7ddae0b1a8337cb4cd02532a6ad8b0 (patch) | |
tree | 34eb776155ece4e534aa8279857185bb0a4f80c7 /src/theory/uf/equality_engine.h | |
parent | 3b87ce3ab67fd463a733ad11402e32f94eb1017e (diff) |
(proof-new) Adding API for converting EqProof into ProofNode (#4747)
Also puts EqProof into its own module. Next will come the implementation of the API.
Diffstat (limited to 'src/theory/uf/equality_engine.h')
-rw-r--r-- | src/theory/uf/equality_engine.h | 35 |
1 files changed, 4 insertions, 31 deletions
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index cf6eabfb7..6b1f3b6aa 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -32,6 +32,7 @@ #include "expr/node.h" #include "theory/rewriter.h" #include "theory/theory.h" +#include "theory/uf/eq_proof.h" #include "theory/uf/equality_engine_types.h" #include "util/statistics_registry.h" @@ -757,9 +758,9 @@ public: } /** - * Add a kind to treat as function applications. - * When extOperator is true, this equality engine will treat the operators of this kind - * as "external" e.g. not internal nodes (see d_isInternal). This means that we will + * Add a kind to treat as function applications. + * When extOperator is true, this equality engine will treat the operators of this kind + * as "external" e.g. not internal nodes (see d_isInternal). This means that we will * consider equivalence classes containing the operators of such terms, and "hasTerm" will * return true. */ @@ -951,34 +952,6 @@ public: bool isFinished() const; };/* class EqClassIterator */ -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<std::shared_ptr<EqProof>> d_children; - /** - * Debug print this proof on debug trace c with tabulation tb and pretty - * printer prettyPrinter. - */ - void debug_print(const char* c, unsigned tb = 0, - PrettyPrinter* prettyPrinter = nullptr) const; - /** - * Debug print this proof on output stream os with tabulation tb and pretty - * printer prettyPrinter. - */ - void debug_print(std::ostream& os, - unsigned tb = 0, - PrettyPrinter* prettyPrinter = nullptr) const; -};/* class EqProof */ - } // Namespace eq } // Namespace theory } // Namespace CVC4 |