From: Alex Ozdemir Date: Sun, 13 Jan 2019 21:21:24 +0000 (-0800) Subject: LFSC LRAT Output (#2787) X-Git-Tag: cvc5-1.0.0~4290 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=300560dda47178cae18f5f4ad2edb381eabddb30;p=cvc5.git LFSC LRAT Output (#2787) * LFSC ouput & unit test * Renamed lrat unit test file * s/DRAT/LRAT/ Thanks Andres! Co-Authored-By: alex-ozdemir * Addressed Andres' comments 1. Extracted a filter whitespace function. 2. Added @param annotations. * Addressing Yoni's comments Tweaked the test method name for LRAT output as LFSC Added assertions for verifying that clause index lists are sorted during LFSC LRAT output. --- 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(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>& hints) +{ + for (auto& hint : hints) + { + o << "\n (RATHintsc " << hint.first << " "; + printTrace(o, hint.second); + o << " "; + } + o << "RATHintsn"; + std::fill_n(std::ostream_iterator(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& 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(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> d_instructions; diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt index 8d76644dc..00c893bdb 100644 --- a/test/unit/proof/CMakeLists.txt +++ b/test/unit/proof/CMakeLists.txt @@ -2,4 +2,5 @@ # Add unit tests cvc4_add_unit_test_black(drat_proof_black proof) +cvc4_add_unit_test_black(lrat_proof_black proof) cvc4_add_unit_test_black(lfsc_proof_printer_black proof) diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h new file mode 100644 index 000000000..49d18ac53 --- /dev/null +++ b/test/unit/proof/lrat_proof_black.h @@ -0,0 +1,113 @@ +/********************* */ +/*! \file lrat_proof_black.h + ** \verbatim + ** Top contributors (to current version): + ** Alex Ozdemir + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Black box testing of the LRAT proof class + ** + ** In particular, tests LRAT LFSC output. + **/ + +#include + +#include +#include +#include +#include + +#include "proof/lrat/lrat_proof.h" +#include "prop/sat_solver_types.h" + +using namespace CVC4::proof::lrat; +using namespace CVC4::prop; + +class LfscProofBlack : public CxxTest::TestSuite +{ + public: + void setUp() override {} + void tearDown() override {} + + void testOutputAsLfsc(); +}; + +/** + * Creates a new stream with whitespace removed. + * + * @param s the source string + * + * @return a string without whitespace + */ +std::string filterWhitespace(const std::string& s) +{ + std::string out; + std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) { + return !std::isspace(c); + }); + return out; +} + +void LfscProofBlack::testOutputAsLfsc() +{ + std::vector> instructions; + + // 6 d 1 2 + std::vector clausesToDelete{1, 2}; + std::unique_ptr deletion = std::unique_ptr( + new LratDeletion(6, std::move(clausesToDelete))); + instructions.push_back(std::move(deletion)); + + // 7 1 2 0 5 2 0 + std::vector firstAddedClause{SatLiteral(1, false), + SatLiteral(2, false)}; + LratUPTrace firstTrace{5, 2}; + std::vector> firstHints; + std::unique_ptr add1 = + std::unique_ptr(new LratAddition( + 7, std::move(firstAddedClause), std::move(firstTrace), firstHints)); + instructions.push_back(std::move(add1)); + + // 8 2 0 -1 3 -5 2 0 + std::vector secondAddedClause{SatLiteral(2, false)}; + LratUPTrace secondTrace; + std::vector> secondHints; + LratUPTrace secondHints0Trace{3}; + secondHints.emplace_back(1, secondHints0Trace); + LratUPTrace secondHints1Trace{2}; + secondHints.emplace_back(5, secondHints1Trace); + std::unique_ptr add2 = std::unique_ptr( + new LratAddition(8, + std::move(secondAddedClause), + std::move(secondTrace), + secondHints)); + instructions.push_back(std::move(add2)); + + LratProof proof(std::move(instructions)); + + std::ostringstream lfsc; + proof.outputAsLfsc(lfsc); + + // 6 d 1 2 + // 7 1 2 0 5 2 0 + // 8 2 0 -1 3 -5 2 0 + std::string expectedLfsc = + "(LRATProofd (CIListc 1 (CIListc 2 CIListn)) " + "(LRATProofa 7 " + " (clc (pos bb.v1) (clc (pos bb.v2) cln))" + " (Tracec 5 (Tracec 2 Tracen))" + " RATHintsn " + "(LRATProofa 8 " + " (clc (pos bb.v2) cln)" + " Tracen " + " (RATHintsc 1 (Tracec 3 Tracen)" + " (RATHintsc 5 (Tracec 2 Tracen)" + " RATHintsn)) " + "LRATProofn)))"; + + TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(expectedLfsc)); +}