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
}
}
+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 << " ";
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 ";
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())
* @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;
};
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
}
void outputAsText(std::ostream& out) const override;
+ void outputAsLfsc(std::ostream& o, std::ostream& closeParen) const override;
private:
// The idx for the new clause
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;
# 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)
--- /dev/null
+/********************* */
+/*! \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 <cxxtest/TestSuite.h>
+
+#include <algorithm>
+#include <cctype>
+#include <iostream>
+#include <iterator>
+
+#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<std::unique_ptr<LratInstruction>> instructions;
+
+ // 6 d 1 2
+ std::vector<ClauseIdx> clausesToDelete{1, 2};
+ std::unique_ptr<LratDeletion> deletion = std::unique_ptr<LratDeletion>(
+ new LratDeletion(6, std::move(clausesToDelete)));
+ instructions.push_back(std::move(deletion));
+
+ // 7 1 2 0 5 2 0
+ std::vector<SatLiteral> firstAddedClause{SatLiteral(1, false),
+ SatLiteral(2, false)};
+ LratUPTrace firstTrace{5, 2};
+ std::vector<std::pair<ClauseIdx, LratUPTrace>> firstHints;
+ std::unique_ptr<LratAddition> add1 =
+ std::unique_ptr<LratAddition>(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<SatLiteral> secondAddedClause{SatLiteral(2, false)};
+ LratUPTrace secondTrace;
+ std::vector<std::pair<ClauseIdx, LratUPTrace>> secondHints;
+ LratUPTrace secondHints0Trace{3};
+ secondHints.emplace_back(1, secondHints0Trace);
+ LratUPTrace secondHints1Trace{2};
+ secondHints.emplace_back(5, secondHints1Trace);
+ std::unique_ptr<LratAddition> add2 = std::unique_ptr<LratAddition>(
+ 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));
+}
projects / cvc5.git / commitdiff