((clc l c') (cnf_has_bottom rest))))))
; Return a new cnf with one copy of this clause removed.
+; If the clause is absent, returns the original cnf.
(program cnf_remove_clause ((c clause) (cs cnf)) cnf
(match cs
- (cnfn (fail cnf))
+ (cnfn cnfn)
((cnfc c' cs')
(match (clause_eq c c')
(tt cs')
(tt tt)
(ff (match (is_at cs c)
(tt tt)
- (ff (are_all_at
+ (ff (match c
+ (cln ff)
+ ((clc a b) (are_all_at ; dedent
cs
- (collect_pseudo_resolvents cs c)))))))
+ (collect_pseudo_resolvents cs c)))))))))
; Is this proof a valid DRAT proof of bottom?
(program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool
; unit, it modifies the global assignment to satisfy the clause, and returns
; the literal that was made SAT by the new mark.
;
-; Fails if `c` is a TAUT
+; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied.
(program clause_check_unit_and_maybe_mark ((c clause)) MarkResult
(match (clause_is_sat c)
(tt MRSat)
(ff (match (clause_is_unsat c)
(tt MRUnsat)
(ff (match (is_t c)
- (tt (fail MarkResult))
+ (tt MRSat)
(ff ; Dedent
(match (clause_has_floating c)
(tt (let first (clause_first_floating c)
proof/clause_id.h
proof/cnf_proof.cpp
proof/cnf_proof.h
- proof/dimacs_printer.cpp
- proof/dimacs_printer.h
+ proof/dimacs.cpp
+ proof/dimacs.h
proof/drat/drat_proof.cpp
proof/drat/drat_proof.h
proof/er/er_proof.cpp
#include "cvc4_private.h"
#include <algorithm>
+#include <iostream>
#include <iterator>
-#include <set>
+#include <unordered_set>
#include "options/bv_options.h"
#include "proof/clausal_bitvector_proof.h"
+#include "proof/dimacs.h"
#include "proof/drat/drat_proof.h"
#include "proof/er/er_proof.h"
#include "proof/lfsc_proof_printer.h"
#include "proof/lrat/lrat_proof.h"
#include "theory/bv/theory_bv.h"
+#if CVC4_USE_DRAT2ER
+#include "drat2er_options.h"
+#include "drat_trim_interface.h"
+#endif
+
namespace CVC4 {
namespace proof {
ClausalBitVectorProof::ClausalBitVectorProof(theory::bv::TheoryBV* bv,
TheoryProofEngine* proofEngine)
- : BitVectorProof(bv, proofEngine), d_usedClauses(), d_binaryDratProof()
+ : BitVectorProof(bv, proofEngine),
+ d_clauses(),
+ d_originalClauseIndices(),
+ d_binaryDratProof(),
+ d_coreClauseIndices()
{
}
void ClausalBitVectorProof::registerUsedClause(ClauseId id,
prop::SatClause& clause)
{
- d_usedClauses.emplace_back(id, clause);
+ d_clauses.emplace(id, clause);
+ d_originalClauseIndices.push_back(id);
};
void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
{
+ optimizeDratProof();
+
// Debug dump of DRAT Proof
if (Debug.isOn("bv::clausal"))
{
std::string serializedDratProof = d_binaryDratProof.str();
+ Debug("bv::clausal") << "option: " << options::bvOptimizeSatProof()
+ << std::endl;
Debug("bv::clausal") << "binary DRAT proof byte count: "
<< serializedDratProof.size() << std::endl;
- Debug("bv::clausal") << "Parsing DRAT proof ... " << std::endl;
- drat::DratProof dratProof =
- drat::DratProof::fromBinary(serializedDratProof);
-
- Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
- dratProof.outputAsText(Debug("bv::clausal"));
+ Debug("bv::clausal") << "clause count: " << d_coreClauseIndices.size()
+ << std::endl;
}
// Empty any old record of which atoms were used
d_atomsInBitblastingProof.clear();
+ Assert(d_atomsInBitblastingProof.size() == 0);
// For each used clause, ask the CNF proof which atoms are used in it
- for (const auto& usedIndexAndClause : d_usedClauses)
+ for (const ClauseId usedIdx : d_coreClauseIndices)
{
- d_cnfProof->collectAtoms(&usedIndexAndClause.second,
- d_atomsInBitblastingProof);
+ d_cnfProof->collectAtoms(&d_clauses.at(usedIdx), d_atomsInBitblastingProof);
+ }
+}
+
+void ClausalBitVectorProof::optimizeDratProof()
+{
+ if (options::bvOptimizeSatProof()
+ == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
+ || options::bvOptimizeSatProof()
+ == theory::bv::BvOptimizeSatProof::
+ BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+ {
+ Debug("bv::clausal") << "Optimizing DRAT" << std::endl;
+ char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+ char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+ char optDratFilename[] = "/tmp/cvc4-optimized-drat-XXXXXX";
+ char optFormulaFilename[] = "/tmp/cvc4-optimized-formula-XXXXXX";
+ int r;
+ r = mkstemp(formulaFilename);
+ AlwaysAssert(r > 0);
+ close(r);
+ r = mkstemp(dratFilename);
+ AlwaysAssert(r > 0);
+ close(r);
+ r = mkstemp(optDratFilename);
+ AlwaysAssert(r > 0);
+ close(r);
+ r = mkstemp(optFormulaFilename);
+ AlwaysAssert(r > 0);
+ close(r);
+
+ std::ofstream formStream(formulaFilename);
+ printDimacs(formStream, d_clauses, d_originalClauseIndices);
+ formStream.close();
+
+ std::ofstream dratStream(dratFilename);
+ dratStream << d_binaryDratProof.str();
+ dratStream.close();
+
+#if CVC4_USE_DRAT2ER
+ int dratTrimExitCode =
+ drat2er::drat_trim::OptimizeWithDratTrim(formulaFilename,
+ dratFilename,
+ optFormulaFilename,
+ optDratFilename,
+ drat2er::options::QUIET);
+ AlwaysAssert(
+ dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
+#else
+ Unimplemented(
+ "Proof production when using CryptoMiniSat requires drat2er.\n"
+ "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+ d_binaryDratProof.str("");
+ Assert(d_binaryDratProof.str().size() == 0);
+
+ std::ifstream lratStream(optDratFilename);
+ std::copy(std::istreambuf_iterator<char>(lratStream),
+ std::istreambuf_iterator<char>(),
+ std::ostreambuf_iterator<char>(d_binaryDratProof));
+
+ if (options::bvOptimizeSatProof()
+ == theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
+ {
+ std::ifstream optFormulaStream{optFormulaFilename};
+ std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+ optFormulaStream.close();
+
+ // Now we need to compute the clause indices for the UNSAT core. This is a
+ // bit difficult because drat-trim may have reordered clauses, and/or
+ // removed duplicate literals. We use literal sets as the canonical clause
+ // form.
+ std::unordered_map<
+ std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>,
+ ClauseId,
+ prop::SatClauseSetHashFunction>
+ cannonicalClausesToIndices;
+ for (const auto& kv : d_clauses)
+ {
+ cannonicalClausesToIndices.emplace(
+ std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
+ kv.second.begin(), kv.second.end()},
+ kv.first);
+ }
+
+ d_coreClauseIndices.clear();
+ std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+ coreClauseCanonical;
+ for (const prop::SatClause& coreClause : core)
+ {
+ coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+ d_coreClauseIndices.push_back(
+ cannonicalClausesToIndices.at(coreClauseCanonical));
+ coreClauseCanonical.clear();
+ }
+ Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
+ << std::endl;
+ }
+ else
+ {
+ Debug("bv::clausal") << "Optimizing the DRAT proof but not the formula"
+ << std::endl;
+ d_coreClauseIndices = d_originalClauseIndices;
+ }
+
+ Assert(d_coreClauseIndices.size() > 0);
+ remove(formulaFilename);
+ remove(dratFilename);
+ remove(optDratFilename);
+ remove(optFormulaFilename);
+ Debug("bv::clausal") << "Optimized DRAT" << std::endl;
+ }
+ else
+ {
+ Debug("bv::clausal") << "Not optimizing the formula or the DRAT proof"
+ << std::endl;
+ d_coreClauseIndices = d_originalClauseIndices;
}
}
d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
os << "\n;; BB-CNF proofs\n";
- for (const auto& idAndClause : d_usedClauses)
+ for (const ClauseId id : d_coreClauseIndices)
{
- d_cnfProof->printCnfProofForClause(
- idAndClause.first, &idAndClause.second, os, paren);
+ d_cnfProof->printCnfProofForClause(id, &d_clauses.at(id), os, paren);
}
}
os << "\n;; Proof of input to SAT solver\n";
os << "(@ proofOfSatInput ";
paren << ")";
- std::vector<ClauseId> usedIds;
- usedIds.reserve(d_usedClauses.size());
- for (const auto& idAnd : d_usedClauses)
- {
- usedIds.push_back(idAnd.first);
- };
- LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+ LFSCProofPrinter::printSatInputProof(d_coreClauseIndices, os, "bb");
os << "\n;; DRAT Proof Value\n";
os << "(@ dratProof ";
os << "\n;; Proof of input to SAT solver\n";
os << "(@ proofOfCMap ";
paren << ")";
- std::vector<ClauseId> usedIds;
- usedIds.reserve(d_usedClauses.size());
- for (const auto& idAnd : d_usedClauses)
- {
- usedIds.push_back(idAnd.first);
- };
- LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+ LFSCProofPrinter::printCMapProof(d_coreClauseIndices, os, "bb");
os << "\n;; DRAT Proof Value\n";
os << "(@ lratProof ";
paren << ")";
- lrat::LratProof pf =
- lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+ lrat::LratProof pf = lrat::LratProof::fromDratProof(
+ d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
pf.outputAsLfsc(os);
os << "\n";
"the BV theory should only be proving bottom directly in the eager "
"bitblasting mode");
- er::ErProof pf =
- er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+ er::ErProof pf = er::ErProof::fromBinaryDratProof(
+ d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
pf.outputAsLfsc(os);
}
protected:
// A list of all clauses and their ids which are passed into the SAT solver
- std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
+ std::unordered_map<ClauseId, prop::SatClause> d_clauses{};
+ std::vector<ClauseId> d_originalClauseIndices{};
// Stores the proof recieved from the SAT solver.
- std::ostringstream d_binaryDratProof;
+ std::ostringstream d_binaryDratProof{};
+ std::vector<ClauseId> d_coreClauseIndices{};
+
+ private:
+ // Optimizes the DRAT proof stored in `d_binaryDratProof` and returns a list
+ // of clause actually needed to check that proof (a smaller UNSAT core)
+ void optimizeDratProof();
};
/**
--- /dev/null
+/********************* */
+/*! \file dimacs.cpp
+ ** \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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization for SAT problems as DIMACS
+ **/
+
+#include "proof/dimacs.h"
+
+#include "base/cvc4_assert.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::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIndices)
+{
+ size_t maxVar = 0;
+ for (const ClauseId i : usedIndices)
+ {
+ const prop::SatClause& c = clauses.at(i);
+ for (const auto& l : c)
+ {
+ if (l.getSatVariable() + 1 > maxVar)
+ {
+ maxVar = l.getSatVariable() + 1;
+ }
+ }
+ }
+ o << "p cnf " << maxVar << " " << usedIndices.size() << '\n';
+ for (const ClauseId i : usedIndices)
+ {
+ const prop::SatClause& c = clauses.at(i);
+ for (const auto& l : c)
+ {
+ if (l.isNegated())
+ {
+ o << '-';
+ }
+ o << l.getSatVariable() + 1 << " ";
+ }
+ o << "0\n";
+ }
+}
+
+std::vector<prop::SatClause> parseDimacs(std::istream& in)
+{
+ std::string tag;
+ uint64_t nVars;
+ uint64_t nClauses;
+
+ in >> tag;
+ Assert(in.good());
+ Assert(tag == "p");
+
+ in >> tag;
+ Assert(in.good());
+ Assert(tag == "cnf");
+
+ in >> nVars;
+ Assert(nVars >= 0);
+
+ in >> nClauses;
+ Assert(nClauses >= 0);
+
+ std::vector<prop::SatClause> cnf;
+ for (uint64_t i = 0; i < nClauses; ++i)
+ {
+ cnf.emplace_back();
+ int64_t lit;
+ in >> lit;
+ Assert(in.good());
+ while (lit != 0)
+ {
+ cnf.back().emplace_back(std::abs(lit) - 1, lit < 0);
+ in >> lit;
+ Assert(static_cast<uint64_t>(std::abs(lit)) <= nVars);
+ Assert(in.good());
+ }
+ }
+
+ return cnf;
+}
+
+} // namespace proof
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file dimacs.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 DIMACS SAT Problem Format
+ **
+ ** Defines serialization/deserialization for SAT problems as DIMACS
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROOF__DIMACS_H
+#define CVC4__PROOF__DIMACS_H
+
+#include <iosfwd>
+#include <memory>
+#include <unordered_map>
+
+#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::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIndices);
+
+std::vector<prop::SatClause> parseDimacs(std::istream& i);
+
+} // namespace proof
+} // namespace CVC4
+
+#endif // CVC4__PROOF__DIMACS_H
+++ /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-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 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-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 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/map_util.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
#include "proof/lfsc_proof_printer.h"
#include "proof/proof_manager.h"
return pf;
}
-ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
- const std::string& dratBinary)
+ErProof ErProof::fromBinaryDratProof(
+ const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIds,
+ const std::string& dratBinary)
{
std::ostringstream cmd;
char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
// Write the formula
std::ofstream formStream(formulaFilename);
- printDimacs(formStream, usedClauses);
+ printDimacs(formStream, clauses, usedIds);
formStream.close();
// Write the (binary) DRAT proof
// Parse the resulting TRACECHECK proof into an ER proof.
std::ifstream tracecheckStream(tracecheckFilename);
- ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+ TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
+ ErProof proof(clauses, usedIds, std::move(pf));
tracecheckStream.close();
remove(formulaFilename);
return proof;
}
-ErProof::ErProof(const ClauseUseRecord& usedClauses,
+ErProof::ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIds,
TraceCheckProof&& tracecheck)
: d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck)
{
// Step zero, save input clause Ids for future printing
- std::transform(usedClauses.begin(),
- usedClauses.end(),
- std::back_inserter(d_inputClauseIds),
- [](const std::pair<ClauseId, prop::SatClause>& pair) {
- return pair.first;
- });
+ d_inputClauseIds = usedIds;
+
+ // Make a list of (idx, clause pairs), the used ones.
+ std::vector<std::pair<ClauseId, prop::SatClause>> usedClauses;
+ std::transform(
+ usedIds.begin(),
+ usedIds.end(),
+ std::back_inserter(usedClauses),
+ [&](const ClauseId& i) { return make_pair(i, clauses.at(i)); });
// Step one, verify the formula starts the proof
if (Configuration::isAssertionBuild())
originalClause{usedClauses[i].second.begin(),
usedClauses[i].second.end()};
Assert(traceCheckClause == originalClause);
- Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
- Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
- Assert(d_tracecheck.d_lines[i].d_clause.size()
- == usedClauses[i].second.size());
- for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
- {
- Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]);
- }
}
}
#define CVC4__PROOF__ER__ER_PROOF_H
#include <memory>
+#include <unordered_map>
#include <vector>
#include "proof/clause_id.h"
namespace proof {
namespace er {
-using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
-
/**
* A definition of the form:
* newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
/**
* Construct an ER proof from a DRAT proof, using drat2er
*
- * @param usedClauses The CNF formula that we're deriving bottom from.
- * @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
+ * @param clauses A store of clauses that might be in our formula
+ * @param usedIds the ids of clauses that are actually in our formula
+ * @param dratBinary The DRAT proof from the SAT solver, as a binary stream
*/
- static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
- const std::string& dratBinary);
+ static ErProof fromBinaryDratProof(
+ const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIds,
+ const std::string& dratBinary);
/**
* Construct an ER proof from a TRACECHECK ER proof
* This basically just identifies groups of lines which correspond to
* definitions, and extracts them.
*
- * @param usedClauses The CNF formula that we're deriving bottom from.
+ * @param clauses A store of clauses that might be in our formula
+ * @param usedIds the ids of clauses that are actually in our formula
* @param tracecheck The TRACECHECK proof, as a stream.
*/
- ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+ ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId>& usedIds,
+ TraceCheckProof&& tracecheck);
/**
* Write the ER proof as an LFSC value of type (holds cln).
#include "base/cvc4_assert.h"
#include "base/output.h"
-#include "proof/dimacs_printer.h"
+#include "proof/dimacs.h"
#include "proof/lfsc_proof_printer.h"
#if CVC4_USE_DRAT2ER
*/
void printIndices(std::ostream& o, const std::vector<ClauseIdx>& indices)
{
+ Assert(indices.size() > 0);
// Verify that the indices are sorted!
for (size_t i = 0, n = indices.size() - 1; i < n; ++i)
{
// Prints the LRAT addition line in textual format
LratProof LratProof::fromDratProof(
- const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+ const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId> usedIds,
const std::string& dratBinary)
{
std::ostringstream cmd;
AlwaysAssert(r > 0);
close(r);
std::ofstream formStream(formulaFilename);
- printDimacs(formStream, usedClauses);
+ printDimacs(formStream, clauses, usedIds);
formStream.close();
std::ofstream dratStream(dratFilename);
}
clauses.push_back(di);
}
- std::sort(clauses.begin(), clauses.end());
- std::unique_ptr<LratInstruction> instr(
- new LratDeletion(clauseIdx, std::move(clauses)));
- d_instructions.push_back(std::move(instr));
+ if (clauses.size() > 0)
+ {
+ std::sort(clauses.begin(), clauses.end());
+ std::unique_ptr<LratInstruction> instr(
+ new LratDeletion(clauseIdx, std::move(clauses)));
+ d_instructions.push_back(std::move(instr));
+ }
}
else
{
/**
* @brief Construct an LRAT proof from a DRAT proof, using drat-trim
*
- * @param usedClauses The CNF formula that we're deriving bottom from.
- * It's a map because other parts of the system represent
- * it this way.
- * @param clauseOrder A record of the order in which those clauses were
- * given to the SAT solver.
+ * @param clauses A store of clauses that might be in our formula
+ * @param usedIds the ids of clauses that are actually in our formula
* @param dratBinary The DRAT proof from the SAT solver, as a binary stream.
*/
static LratProof fromDratProof(
- const std::vector<std::pair<ClauseId, prop::SatClause>>& usedClauses,
+ const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+ const std::vector<ClauseId> usedIds,
const std::string& dratBinary);
/**
* @brief Construct an LRAT proof from its textual representation
#include <cctype>
#include <iostream>
#include <iterator>
+#include <unordered_map>
#include <vector>
#include "proof/clause_id.h"
void testErTraceCheckOutputMedium();
};
+/**
+ * @brief Add a new clause to the clause store and list of used clauses
+ *
+ * @param clauses the clause store
+ * @param usedIds the used clauses
+ * @param id the id of the new clause
+ * @param clause the clause itself
+ */
+void addClause(std::unordered_map<ClauseId, SatClause>& clauses,
+ std::vector<ClauseId>& usedIds,
+ ClauseId id,
+ SatClause&& clause)
+{
+ clauses.emplace(id, std::move(clause));
+ usedIds.push_back(id);
+}
+
void ErProofBlack::testTraceCheckParse1Line()
{
std::string tracecheckText = "1 -2 3 0 4 2 0\n";
std::istringstream stream(tracecheckText);
TraceCheckProof tc = TraceCheckProof::fromText(stream);
- std::vector<std::pair<ClauseId, SatClause>> usedClauses;
- usedClauses.emplace_back(
+ std::unordered_map<ClauseId, SatClause> clauses;
+ std::vector<ClauseId> usedIds;
+ addClause(
+ clauses,
+ usedIds,
1,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
2,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
3,
std::vector<SatLiteral>{
SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
4,
std::vector<SatLiteral>{
SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- usedClauses.emplace_back(
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(clauses,
+ usedIds,
+ 5,
+ std::vector<SatLiteral>{
+ SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+ addClause(
+ clauses,
+ usedIds,
6,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
7,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
8,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(usedClauses, std::move(tc));
+ ErProof pf(clauses, usedIds, std::move(tc));
TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17);
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3);
- TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0], SatLiteral(0, false));
- TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1], SatLiteral(1, false));
- TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2], SatLiteral(2, true));
+ TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0],
+ SatLiteral(0, false));
+ TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1],
+ SatLiteral(1, false));
+ TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2],
+ SatLiteral(2, true));
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0);
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1);
- TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0], SatLiteral(1, false));
+ TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0],
+ SatLiteral(1, false));
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3);
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3);
TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15);
std::istringstream stream(tracecheckText);
TraceCheckProof tc = TraceCheckProof::fromText(stream);
- std::vector<std::pair<ClauseId, SatClause>> usedClauses;
- usedClauses.emplace_back(
+ std::unordered_map<ClauseId, SatClause> clauses;
+ std::vector<ClauseId> usedIds;
+ addClause(
+ clauses,
+ usedIds,
1,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
2,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
3,
std::vector<SatLiteral>{
SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
4,
std::vector<SatLiteral>{
SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- usedClauses.emplace_back(
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(clauses,
+ usedIds,
+ 5,
+ std::vector<SatLiteral>{
+ SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+ addClause(
+ clauses,
+ usedIds,
6,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
7,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
8,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(usedClauses, std::move(tc));
+ ErProof pf(clauses, usedIds, std::move(tc));
std::ostringstream lfsc;
pf.outputAsLfsc(lfsc);
"7 -1 2 4 0 0\n"
"8 1 -2 -4 0 0\n"
- "9 5 2 4 0 0\n" // Definition with 2 other variables
+ "9 5 2 4 0 0\n" // Definition with 2 other variables
"10 5 1 0 0\n"
"11 2 -5 -1 0 0\n"
"12 4 -5 -1 0 0\n"
- "13 6 0 0\n" // Definition with no other variables
+ "13 6 0 0\n" // Definition with no other variables
"14 6 -3 0 0\n"
- "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses
+ "15 -3 4 0 11 1 10 7 4 0\n" // Chain w/ both def. and input clauses
- "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof
+ "16 -2 -4 0 2 5 8 0\n" // The useful bit of the proof
"17 4 3 0 7 2 6 0\n"
"18 2 -3 0 7 5 1 0\n"
"19 2 0 3 17 18 0\n"
std::istringstream stream(tracecheckText);
TraceCheckProof tc = TraceCheckProof::fromText(stream);
- std::vector<std::pair<ClauseId, SatClause>> usedClauses;
- usedClauses.emplace_back(
+ std::unordered_map<ClauseId, SatClause> clauses;
+ std::vector<ClauseId> usedIds;
+ addClause(
+ clauses,
+ usedIds,
1,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
2,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
3,
std::vector<SatLiteral>{
SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
4,
std::vector<SatLiteral>{
SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
- usedClauses.emplace_back(
- 5,
- std::vector<SatLiteral>{
- SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
- usedClauses.emplace_back(
+ addClause(clauses,
+ usedIds,
+ 5,
+ std::vector<SatLiteral>{
+ SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
+ addClause(
+ clauses,
+ usedIds,
6,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
7,
std::vector<SatLiteral>{
SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
- usedClauses.emplace_back(
+ addClause(
+ clauses,
+ usedIds,
8,
std::vector<SatLiteral>{
SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
- ErProof pf(usedClauses, std::move(tc));
+ ErProof pf(clauses, usedIds, std::move(tc));
std::ostringstream lfsc;
pf.outputAsLfsc(lfsc);
projects / cvc5.git / commitdiff