diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-04-25 15:12:51 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-04-25 15:12:51 -0700 |
commit | 1ae10032fb99ca1d8f73c5f51dce3cfc976b3dfb (patch) | |
tree | 9006c24edf5605145167cea0ce1d5df829bcac57 /src/proof/theory_proof.h | |
parent | 8cc4bc292c6ac60edfa356355ad235e51ad15310 (diff) |
Refactor array-proofs and uf-proofs (#1655)
This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
Diffstat (limited to 'src/proof/theory_proof.h')
-rw-r--r-- | src/proof/theory_proof.h | 60 |
1 files changed, 56 insertions, 4 deletions
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h index 4e599f570..efe05bce8 100644 --- a/src/proof/theory_proof.h +++ b/src/proof/theory_proof.h @@ -26,10 +26,10 @@ #include "expr/expr.h" #include "proof/clause_id.h" +#include "proof/proof_utils.h" #include "prop/sat_solver_types.h" +#include "theory/uf/equality_engine.h" #include "util/proof.h" -#include "proof/proof_utils.h" - namespace CVC4 { namespace theory { @@ -207,7 +207,9 @@ protected: // Pointer to the theory for this proof theory::Theory* d_theory; TheoryProofEngine* d_proofEngine; -public: + virtual theory::TheoryId getTheoryId() = 0; + + public: TheoryProof(theory::Theory* th, TheoryProofEngine* proofEngine) : d_theory(th) , d_proofEngine(proofEngine) @@ -238,6 +240,54 @@ public: void printSort(Type type, std::ostream& os) { d_proofEngine->printSort(type, os); } + + // congrence matching term helper + inline bool match(TNode n1, TNode n2); + + /** + * Helper function for ProofUF::toStreamRecLFSC and + * ProofArray::toStreamRecLFSC + * Inputs: + * - pf: equality engine proof + * - map: A map for the let-expressions in the proof + * - subTrans: main transitivity proof part + * - pPrettyPrinter: optional pretty printer for sub-proofs + * returns: + * - the index of the contradicting node in pf. + * */ + int assertAndPrint( + const theory::eq::EqProof& pf, + const ProofLetMap& map, + std::shared_ptr<theory::eq::EqProof> subTrans, + theory::eq::EqProof::PrettyPrinter* pPrettyPrinter = nullptr); + + /** + * Helper function for ProofUF::toStreamRecLFSC and + * ProofArray::toStreamRecLFSC + * Inputs: + * - evenLengthSequence: true iff the length of the sequence + * of the identical equalities is even. + * - sequenceOver: have we reached the last equality of this sequence? + * - pf: equality engine proof + * - map: A map for the let-expressions in the proof + * - subproofStr: current stringstream content + * - outStream: output stream to which the proof is printed + * - n: transitivity sub-proof + * - nodeAfterEqualitySequence: The node after the identical sequence. + * Returns: + * A pair of nodes, that are the updated nodes n and nodeAfterEqualitySequence + * + */ + std::pair<Node, Node> identicalEqualitiesPrinterHelper( + bool evenLengthSequence, + bool sequenceOver, + const theory::eq::EqProof& pf, + const ProofLetMap& map, + const std::string subproofStr, + std::stringstream* outStream, + Node n, + Node nodeAfterEqualitySequence); + /** * Print the proof representation of the given type that belongs to THIS theory. * @@ -313,7 +363,9 @@ public: class BooleanProof : public TheoryProof { protected: ExprSet d_declarations; // all the boolean variables -public: + theory::TheoryId getTheoryId(); + + public: BooleanProof(TheoryProofEngine* proofEngine); void registerTerm(Expr term) override; |