Creating LRAT proofs reuqires writing SAT problems in the DIMACS format.
Before this code was in the LRAT class.
However, since creating ER proofs will also require writing DIMACS, I
decided to extract it.
At the same time I realized that my prior representation of used clauses
was unnecessarily poor. I had chosen it to align with
`CnfProof::collectAtomsForClauses`, but the format is really bad (it
requires extra allocations & manual memory management), and I discovered
that the aforementioned method is super simple, so I'm moving to a
better format.
proof/clause_id.h
proof/cnf_proof.cpp
proof/cnf_proof.h
+ proof/dimacs_printer.cpp
+ proof/dimacs_printer.h
proof/drat/drat_proof.cpp
proof/drat/drat_proof.h
proof/lemma_proof.cpp
--- /dev/null
+/********************* */
+/*! \file dimacs_printer.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization for SAT problems as DIMACS
+ **/
+
+#include "proof/dimacs_printer.h"
+
+#include <iostream>
+
+namespace CVC4 {
+namespace proof {
+
+// Prints the literal as a (+) or (-) int
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l)
+{
+ if (l.isNegated())
+ {
+ o << "-";
+ }
+ return o << l.getSatVariable() + 1;
+}
+
+// Prints the clause as a space-separated list of ints
+// Not operator<< b/c that represents negation as ~
+std::ostream& textOut(std::ostream& o, const prop::SatClause& c)
+{
+ for (const auto& l : c)
+ {
+ textOut(o, l) << " ";
+ }
+ return o << "0";
+}
+
+void printDimacs(
+ std::ostream& o,
+ const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses)
+{
+ size_t maxVar = 0;
+ for (const auto& c : usedClauses)
+ {
+ for (const auto& l : c.second)
+ {
+ if (l.getSatVariable() + 1 > maxVar)
+ {
+ maxVar = l.getSatVariable() + 1;
+ }
+ }
+ }
+ o << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
+ for (const auto& idAndClause : usedClauses)
+ {
+ for (const auto& l : idAndClause.second)
+ {
+ if (l.isNegated())
+ {
+ o << '-';
+ }
+ o << l.getSatVariable() + 1 << " ";
+ }
+ o << "0\n";
+ }
+}
+
+} // namespace proof
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file dimacs_printer.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization for SAT problems as DIMACS
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PROOF__DIMACS_PRINTER_H
+#define __CVC4__PROOF__DIMACS_PRINTER_H
+
+#include <iosfwd>
+#include <memory>
+
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+namespace proof {
+
+/**
+ * Prints the literal as a (+) or (-) int
+ * Not operator<< b/c that represents negation as ~
+ *
+ * @param o where to print
+ * @param l the literal to print
+ *
+ * @return the original stream
+ */
+std::ostream& textOut(std::ostream& o, const prop::SatLiteral& l);
+
+/**
+ * Prints the clause as a space-separated list of ints
+ * Not operator<< b/c that represents literal negation as ~
+ *
+ * @param o where to print
+ * @param c the clause to print
+ *
+ * @return the original stream
+ */
+std::ostream& textOut(std::ostream& o, const prop::SatClause& c);
+
+/**
+ * Prints a CNF formula in DIMACS format
+ *
+ * @param o where to print to
+ * @param usedClauses the CNF formula
+ */
+void printDimacs(
+ std::ostream& o,
+ const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses);
+
+} // namespace proof
+} // namespace CVC4
+
+#endif // __CVC4__PROOF__DIMACS_PRINTER_H
#include "base/cvc4_assert.h"
#include "base/output.h"
+#include "proof/dimacs_printer.h"
#include "proof/lfsc_proof_printer.h"
#if CVC4_USE_DRAT2ER
using prop::SatVariable;
namespace {
-// Prints the literal as a (+) or (-) int
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const SatLiteral& l)
-{
- if (l.isNegated())
- {
- o << "-";
- }
- return o << l.getSatVariable();
-}
-
-// Prints the clause as a space-separated list of ints
-// Not operator<< b/c that represents negation as ~
-std::ostream& textOut(std::ostream& o, const SatClause& c)
-{
- for (const auto l : c)
- {
- textOut(o, l) << " ";
- }
- return o << "0";
-}
// Prints the trace as a space-separated list of (+) ints with a space at the
// end.
// Prints the LRAT addition line in textual format
LratProof LratProof::fromDratProof(
- const std::unordered_map<ClauseId, SatClause*>& usedClauses,
- const std::vector<ClauseId>& clauseOrder,
+ const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
const std::string& dratBinary)
{
std::ostringstream cmd;
AlwaysAssert(r > 0);
close(r);
std::ofstream formStream(formulaFilename);
- size_t maxVar = 0;
- for (auto& c : usedClauses)
- {
- for (auto l : *(c.second))
- {
- if (l.getSatVariable() + 1 > maxVar)
- {
- maxVar = l.getSatVariable() + 1;
- }
- }
- }
- formStream << "p cnf " << maxVar << " " << usedClauses.size() << '\n';
- for (auto ci : clauseOrder)
- {
- auto iterator = usedClauses.find(ci);
- Assert(iterator != usedClauses.end());
- for (auto l : *(iterator->second))
- {
- if (l.isNegated())
- {
- formStream << '-';
- }
- formStream << l.getSatVariable() + 1 << " ";
- }
- formStream << "0\n";
- }
+ printDimacs(formStream, usedClauses);
formStream.close();
std::ofstream dratStream(dratFilename);
drat2er::drat_trim::CheckAndConvertToLRAT(
formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
#else
- Unimplemented("LRAT proof production requires drat2er.\n"
+ Unimplemented(
+ "LRAT proof production requires drat2er.\n"
"Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
#endif
* @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
*/
static LratProof fromDratProof(
- const std::unordered_map<ClauseId, prop::SatClause*>& usedClauses,
- const std::vector<ClauseId>& clauseOrder,
+ const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
const std::string& dratBinary);
/**
* @brief Construct an LRAT proof from its textual representation
projects / cvc5.git / commitdiff