diff options
Diffstat (limited to 'src/proof/lrat/lrat_proof.cpp')
-rw-r--r-- | src/proof/lrat/lrat_proof.cpp | 94 |
1 files changed, 94 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()) |