diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 94 | ||||
-rw-r--r-- | src/proof/lrat/lrat_proof.h | 13 |
2 files changed, 107 insertions, 0 deletions
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp index 01dfd145f..3b4bac3f0 100644 --- a/src/proof/lrat/lrat_proof.cpp +++ b/src/proof/lrat/lrat_proof.cpp @@ -75,6 +75,69 @@ std::ostream& operator<<(std::ostream& o, const LratUPTrace& trace) return o; } +/** + * Print a list of clause indices to go to while doing UP. + * + * i.e. a value of type Trace + * + * @param o where to print to + * @param trace the trace (list of clauses) to print + */ +void printTrace(std::ostream& o, const LratUPTrace& trace) +{ + for (ClauseIdx idx : trace) + { + o << "(Tracec " << idx << " "; + } + o << "Tracen"; + std::fill_n(std::ostream_iterator<char>(o), trace.size(), ')'); +} + +/** + * Print the RAT hints for a clause addition. + * + * i.e. prints an LFSC value of type RATHints + * + * @param o where to print to + * @param hints the RAT hints to print + */ +void printHints(std::ostream& o, + const std::vector<std::pair<ClauseIdx, LratUPTrace>>& hints) +{ + for (auto& hint : hints) + { + o << "\n (RATHintsc " << hint.first << " "; + printTrace(o, hint.second); + o << " "; + } + o << "RATHintsn"; + std::fill_n(std::ostream_iterator<char>(o), hints.size(), ')'); +} + +/** + * Print an index list + * + * i.e. prints an LFSC value of type CIList + * + * @param o where to print to + * @param indices the list of indices to print + */ +void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices) +{ + // Verify that the indices are sorted! + for (size_t i = 0, n = indices.size() - 1; i < n; ++i) + { + Assert(indices[i] < indices[i + 1]); + } + + for (ClauseIdx idx : indices) + { + o << "(CIListc " << idx << " "; + } + o << "CIListn"; + std::fill_n(std::ostream_iterator<char>(o), indices.size(), ')'); +} + } // namespace // Prints the LRAT addition line in textual format @@ -248,6 +311,17 @@ LratProof::LratProof(std::istream& textualProof) } } +void LratProof::outputAsLfsc(std::ostream& o) const +{ + std::ostringstream closeParen; + for (const auto& i : d_instructions) + { + i->outputAsLfsc(o, closeParen); + } + o << "LRATProofn"; + o << closeParen.str(); +} + void LratAddition::outputAsText(std::ostream& o) const { o << d_idxOfClause << " "; @@ -261,6 +335,18 @@ void LratAddition::outputAsText(std::ostream& o) const o << "0\n"; } +void LratAddition::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const +{ + o << "\n (LRATProofa " << d_idxOfClause << " "; + closeParen << ")"; + LFSCProofPrinter::printSatClause(d_clause, o, "bb"); + o << " "; + printTrace(o, d_atTrace); + o << " "; + printHints(o, d_resolvants); + o << " "; +} + void LratDeletion::outputAsText(std::ostream& o) const { o << d_idxOfClause << " d "; @@ -271,6 +357,14 @@ void LratDeletion::outputAsText(std::ostream& o) const o << "0\n"; } +void LratDeletion::outputAsLfsc(std::ostream& o, std::ostream& closeParen) const +{ + o << "\n (LRATProofd "; + closeParen << ")"; + printIndices(o, d_clauses); + o << " "; +} + std::ostream& operator<<(std::ostream& o, const LratProof& p) { for (const auto& instr : p.getInstructions()) diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h index d976c1279..fb05bd71b 100644 --- a/src/proof/lrat/lrat_proof.h +++ b/src/proof/lrat/lrat_proof.h @@ -52,6 +52,15 @@ class LratInstruction * @param out the stream to write to */ virtual void outputAsText(std::ostream& out) const = 0; + /** + * Write this LRAT instruction as an LFSC value + * + * @param out the stream to write to + * @param closeParen the stream to write any closing parentheses to + * + */ + virtual void outputAsLfsc(std::ostream& o, + std::ostream& closeParen) const = 0; virtual ~LratInstruction() = default; }; @@ -67,6 +76,7 @@ class LratDeletion : public LratInstruction LratDeletion() = default; void outputAsText(std::ostream& out) const override; + void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override; private: // This idx doesn't really matter, but it's in the format anyway, so we parse @@ -97,6 +107,7 @@ class LratAddition : public LratInstruction } void outputAsText(std::ostream& out) const override; + void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override; private: // The idx for the new clause @@ -153,6 +164,8 @@ class LratProof return d_instructions; } + void outputAsLfsc(std::ostream& o) const; + private: // The instructions in the proof. Each is a deletion or addition. std::vector<std::unique_ptr<LratInstruction>> d_instructions; |