From c652449ac9f4a54fc8f37796f0bff3960434cf40 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Fri, 11 Jan 2019 16:04:56 -0800 Subject: LratInstruction inheritance (#2784) While implementing and testing LRAT proof output as LFSC, I discovered that my implementation of LratInstruction as a tagged union was subtly broken for reasons related to move/copy assignment/constructors. While I could have figured out how to fix it, I decided to stop fighting the system and use inheritance. This PR will be followed by one using the inheritance-based LratInstruction to implement output to LFSC. --- src/proof/lrat/lrat_proof.cpp | 149 ++++++++++++------------------------------ src/proof/lrat/lrat_proof.h | 73 +++++++++++---------- 2 files changed, 83 insertions(+), 139 deletions(-) (limited to 'src/proof') diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index 6c2c5e2e8..01dfd145f 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -20,10 +20,13 @@ #include #include #include +#include +#include #include #include "base/cvc4_assert.h" #include "base/output.h" +#include "proof/lfsc_proof_printer.h" #if CVC4_USE_DRAT2ER #include "drat2er_options.h" @@ -72,107 +75,9 @@ std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace) return o; } -// Prints the LRAT addition line in textual format -std::ostream& operator<<(std::ostream& o, const LratAdditionData& add) -{ - o << add.d_idxOfClause << " "; - textOut(o, add.d_clause) << " "; - o << add.d_atTrace; // Inludes a space at the end. - for (const auto& rat : add.d_resolvants) - { - o << "-" << rat.first << " "; - o << rat.second; // Includes a space at the end. - } - o << "0\n"; - return o; -} +} // namespace // Prints the LRAT addition line in textual format -std::ostream& operator<<(std::ostream& o, const LratDeletionData& del) -{ - o << del.d_idxOfClause << " d "; - for (const auto& idx : del.d_clauses) - { - o << idx << " "; - } - return o << "0\n"; -} - -// Prints the LRAT line in textual format -std::ostream& operator<<(std::ostream& o, const LratInstruction& i) -{ - switch (i.d_kind) - { - case LRAT_ADDITION: return o << i.d_data.d_addition; - case LRAT_DELETION: return o << i.d_data.d_deletion; - default: return o; - } -} - -} - -LratInstruction::LratInstruction(LratInstruction&& instr) : d_kind(instr.d_kind) -{ - switch (d_kind) - { - case LRAT_ADDITION: - { - d_data.d_addition = instr.d_data.d_addition; - break; - } - case LRAT_DELETION: - { - d_data.d_deletion = instr.d_data.d_deletion; - break; - } - } -} - -LratInstruction::LratInstruction(LratInstruction& instr) : d_kind(instr.d_kind) -{ - switch (d_kind) - { - case LRAT_ADDITION: - { - d_data.d_addition = instr.d_data.d_addition; - break; - } - case LRAT_DELETION: - { - d_data.d_deletion = instr.d_data.d_deletion; - break; - } - } -} - -LratInstruction::LratInstruction(LratAdditionData&& addition) - : d_kind(LRAT_ADDITION) -{ - d_data.d_addition = std::move(addition); -} - -LratInstruction::LratInstruction(LratDeletionData&& deletion) - : d_kind(LRAT_DELETION) -{ - d_data.d_deletion = std::move(deletion); -} - -LratInstruction::~LratInstruction() -{ - switch (d_kind) - { - case LRAT_ADDITION: - { - d_data.d_addition.~LratAdditionData(); - break; - } - case LRAT_DELETION: - { - d_data.d_deletion.~LratDeletionData(); - break; - } - } -} LratProof LratProof::fromDratProof( const std::unordered_map& usedClauses, @@ -284,8 +189,9 @@ LratProof::LratProof(std::istream& textualProof) clauses.push_back(di); } std::sort(clauses.begin(), clauses.end()); - d_instructions.emplace_back( - LratDeletionData(clauseIdx, std::move(clauses))); + std::unique_ptr instr( + new LratDeletion(clauseIdx, std::move(clauses))); + d_instructions.push_back(std::move(instr)); } else { @@ -332,23 +238,54 @@ LratProof::LratProof(std::istream& textualProof) // Pairs compare based on the first element, so this sorts by the // resolution target index std::sort(resolvants.begin(), resolvants.end()); - d_instructions.emplace_back(LratAdditionData(clauseIdx, - std::move(clause), - std::move(atTrace), - std::move(resolvants))); + std::unique_ptr instr( + new LratAddition(clauseIdx, + std::move(clause), + std::move(atTrace), + std::move(resolvants))); + d_instructions.push_back(std::move(instr)); } } } +void LratAddition::outputAsText(std::ostream& o) const +{ + o << d_idxOfClause << " "; + textOut(o, d_clause) << " "; + o << d_atTrace; // Inludes a space at the end. + for (const auto& rat : d_resolvants) + { + o << "-" << rat.first << " "; + o << rat.second; // Includes a space at the end. + } + o << "0\n"; +} + +void LratDeletion::outputAsText(std::ostream& o) const +{ + o << d_idxOfClause << " d "; + for (const auto& idx : d_clauses) + { + o << idx << " "; + } + o << "0\n"; +} + std::ostream& operator<<(std::ostream& o, const LratProof& p) { for (const auto& instr : p.getInstructions()) { - o << instr; + o << *instr; } return o; } +std::ostream& operator<<(std::ostream& o, const LratInstruction& i) +{ + i.outputAsText(o); + return o; +} + } // namespace lrat } // namespace proof } // namespace CVC4 diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h index 384fbbdf4..d976c1279 100644 --- a/src/proof/lrat/lrat_proof.h +++ b/src/proof/lrat/lrat_proof.h @@ -26,6 +26,7 @@ #ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H #define __CVC4__PROOF__LRAT__LRAT_PROOF_H +#include #include #include #include @@ -41,22 +42,33 @@ namespace lrat { // Refers to clause position within an LRAT proof using ClauseIdx = size_t; -enum LratInstructionKind +// This is conceptually an Either +class LratInstruction { - LRAT_DELETION, - LRAT_ADDITION, + public: + /** + * Write this LRAT instruction in textual format + * + * @param out the stream to write to + */ + virtual void outputAsText(std::ostream& out) const = 0; + virtual ~LratInstruction() = default; }; -struct LratDeletionData +class LratDeletion : public LratInstruction { - LratDeletionData(ClauseIdx idxOfClause, std::vector&& clauses) + public: + LratDeletion(ClauseIdx idxOfClause, std::vector&& clauses) : d_idxOfClause(idxOfClause), d_clauses(clauses) { // Nothing left to do } - ~LratDeletionData() = default; + LratDeletion() = default; + void outputAsText(std::ostream& out) const override; + + private: // This idx doesn't really matter, but it's in the format anyway, so we parse // it. ClauseIdx d_idxOfClause; @@ -69,12 +81,13 @@ struct LratDeletionData // propegation using LratUPTrace = std::vector; -struct LratAdditionData +class LratAddition : public LratInstruction { - LratAdditionData(ClauseIdx idxOfClause, - prop::SatClause&& clause, - LratUPTrace&& atTrace, - std::vector> resolvants) + public: + LratAddition(ClauseIdx idxOfClause, + prop::SatClause&& clause, + LratUPTrace&& atTrace, + std::vector> resolvants) : d_idxOfClause(idxOfClause), d_clause(clause), d_atTrace(atTrace), @@ -83,8 +96,9 @@ struct LratAdditionData // Nothing left to do } - ~LratAdditionData() = default; + void outputAsText(std::ostream& out) const override; + private: // The idx for the new clause ClauseIdx d_idxOfClause; // The new clause @@ -98,25 +112,6 @@ struct LratAdditionData std::vector> d_resolvants; }; -// This is conceptually an Either -struct LratInstruction -{ - LratInstructionKind d_kind; - union LratInstructionData - { - LratAdditionData d_addition; - LratDeletionData d_deletion; - ~LratInstructionData(){/* Empty destructor */}; - LratInstructionData(){/* Empty constructor */}; - } d_data; - - LratInstruction(LratInstruction&& instr); - LratInstruction(LratInstruction& instr); - LratInstruction(LratAdditionData&& addition); - LratInstruction(LratDeletionData&& deletion); - ~LratInstruction(); -}; - class LratProof { public: @@ -142,18 +137,30 @@ class LratProof */ LratProof(std::istream& textualProof); - const std::vector& getInstructions() const + /** + * Construct a LRAT proof from an explicit instruction list + * + * @param instructions + */ + LratProof(std::vector>&& instructions) + : d_instructions(std::move(instructions)) + { + // Nothing else + } + + const std::vector>& getInstructions() const { return d_instructions; } private: // The instructions in the proof. Each is a deletion or addition. - std::vector d_instructions; + std::vector> d_instructions; }; // Prints the LRAT proof in textual format std::ostream& operator<<(std::ostream& o, const LratProof& p); +std::ostream& operator<<(std::ostream& o, const LratInstruction& i); } // namespace lrat } // namespace proof -- cgit v1.2.3