prop/sat_solver_factory.cpp
prop/sat_solver_factory.h
prop/bv_sat_solver_notify.h
+ prop/sat_solver_types.cpp
prop/sat_solver_types.h
prop/theory_proxy.cpp
prop/theory_proxy.h
#include <algorithm>
#include <iostream>
#include <iterator>
-#include <unordered_set>
+#include <map>
#include "options/bv_options.h"
#include "proof/clausal_bitvector_proof.h"
#include "proof/er/er_proof.h"
#include "proof/lfsc_proof_printer.h"
#include "proof/lrat/lrat_proof.h"
+#include "prop/sat_solver_types.h"
+#include "smt/smt_statistics_registry.h"
#include "theory/bv/theory_bv.h"
#if CVC4_USE_DRAT2ER
d_clauses(),
d_originalClauseIndices(),
d_binaryDratProof(),
- d_coreClauseIndices()
+ d_coreClauseIndices(),
+ d_dratTranslationStatistics(),
+ d_dratOptimizationStatistics()
{
}
void ClausalBitVectorProof::registerUsedClause(ClauseId id,
prop::SatClause& clause)
{
- d_clauses.emplace(id, clause);
+ prop::SatClause& emplaced_clause =
+ d_clauses.emplace(id, clause).first->second;
+ canonicalizeClause(emplaced_clause);
d_originalClauseIndices.push_back(id);
};
}
}
+struct SatClausePointerComparator
+{
+ inline bool operator()(const prop::SatClause* const& l,
+ const prop::SatClause* const& r) const
+ {
+ prop::SatClauseLessThan cmp;
+ return cmp(*l, *r);
+ }
+};
+
void ClausalBitVectorProof::optimizeDratProof()
{
+ TimerStat::CodeTimer optimizeDratProofTimer{
+ d_dratOptimizationStatistics.d_totalTime};
if (options::bvOptimizeSatProof()
== theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_PROOF
|| options::bvOptimizeSatProof()
std::string optDratFilename("cvc4-optimized-drat-XXXXXX");
std::string optFormulaFilename("cvc4-optimized-formula-XXXXXX");
- std::fstream formStream = openTmpFile(&formulaFilename);
- printDimacs(formStream, d_clauses, d_originalClauseIndices);
- formStream.close();
+ {
+ std::fstream formStream = openTmpFile(&formulaFilename);
+ const int64_t startPos = static_cast<int64_t>(formStream.tellp());
+ printDimacs(formStream, d_clauses, d_originalClauseIndices);
+ d_dratOptimizationStatistics.d_initialFormulaSize.setData(
+ static_cast<int64_t>(formStream.tellp()) - startPos);
+ formStream.close();
+ }
- std::fstream dratStream = openTmpFile(&dratFilename);
- dratStream << d_binaryDratProof.str();
- dratStream.close();
+ {
+ std::fstream dratStream = openTmpFile(&dratFilename);
+ const int64_t startPos = static_cast<int64_t>(dratStream.tellp());
+ dratStream << d_binaryDratProof.str();
+ d_dratOptimizationStatistics.d_initialDratSize.setData(
+ static_cast<int64_t>(dratStream.tellp()) - startPos);
+ dratStream.close();
+ }
std::fstream optDratStream = openTmpFile(&optDratFilename);
std::fstream optFormulaStream = openTmpFile(&optFormulaFilename);
#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);
+ {
+ TimerStat::CodeTimer runDratTimeOptimizationTimer{
+ d_dratOptimizationStatistics.d_toolTime};
+ 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::copy(std::istreambuf_iterator<char>(optDratStream),
- std::istreambuf_iterator<char>(),
- std::ostreambuf_iterator<char>(d_binaryDratProof));
+ {
+ d_binaryDratProof.str("");
+ Assert(d_binaryDratProof.str().size() == 0);
+
+ const int64_t startPos = static_cast<int64_t>(d_binaryDratProof.tellp());
+ std::ifstream lratStream(optDratFilename);
+ std::copy(std::istreambuf_iterator<char>(lratStream),
+ std::istreambuf_iterator<char>(),
+ std::ostreambuf_iterator<char>(d_binaryDratProof));
+ d_dratOptimizationStatistics.d_optimizedDratSize.setData(
+ static_cast<int64_t>(d_binaryDratProof.tellp()) - startPos);
+ }
if (options::bvOptimizeSatProof()
== theory::bv::BvOptimizeSatProof::BITVECTOR_OPTIMIZE_SAT_PROOF_FORMULA)
{
+ std::ifstream optFormulaStream{optFormulaFilename};
+ const int64_t startPos = static_cast<int64_t>(optFormulaStream.tellg());
std::vector<prop::SatClause> core = parseDimacs(optFormulaStream);
+ d_dratOptimizationStatistics.d_optimizedFormulaSize.setData(
+ static_cast<int64_t>(optFormulaStream.tellg()) - startPos);
+ optFormulaStream.close();
+
+ CodeTimer clauseMatchingTimer{
+ d_dratOptimizationStatistics.d_clauseMatchingTime};
// 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>
+ //
+ // TODO (aozdemir) It may be better to use a hash map instead of a tree
+ // map here.
+ std::map<const prop::SatClause*, ClauseId, SatClausePointerComparator>
cannonicalClausesToIndices;
for (const auto& kv : d_clauses)
{
- cannonicalClausesToIndices.emplace(
- std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>{
- kv.second.begin(), kv.second.end()},
- kv.first);
+ cannonicalClausesToIndices[&kv.second] = kv.first;
}
d_coreClauseIndices.clear();
- std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
- coreClauseCanonical;
- for (const prop::SatClause& coreClause : core)
+
+ for (prop::SatClause& coreClause : core)
{
- coreClauseCanonical.insert(coreClause.begin(), coreClause.end());
+ canonicalizeClause(coreClause);
d_coreClauseIndices.push_back(
- cannonicalClausesToIndices.at(coreClauseCanonical));
- coreClauseCanonical.clear();
+ cannonicalClausesToIndices.at(&coreClause));
}
Debug("bv::clausal") << "Optimizing the DRAT proof and the formula"
<< std::endl;
}
}
+void ClausalBitVectorProof::canonicalizeClause(prop::SatClause& clause)
+{
+ std::sort(clause.begin(), clause.end());
+ clause.erase(std::unique(clause.begin(), clause.end()), clause.end());
+}
+
+ClausalBitVectorProof::DratTranslationStatistics::DratTranslationStatistics()
+ : d_totalTime("proof::bv::dratTranslation::totalTime"),
+ d_toolTime("proof::bv::dratTranslation::toolTime")
+{
+ smtStatisticsRegistry()->registerStat(&d_totalTime);
+ smtStatisticsRegistry()->registerStat(&d_toolTime);
+}
+
+ClausalBitVectorProof::DratTranslationStatistics::~DratTranslationStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_totalTime);
+ smtStatisticsRegistry()->unregisterStat(&d_toolTime);
+}
+
+ClausalBitVectorProof::DratOptimizationStatistics::DratOptimizationStatistics()
+ : d_totalTime("proof::bv::dratOptimization::totalTime"),
+ d_toolTime("proof::bv::dratOptimization::toolTime"),
+ d_clauseMatchingTime("proof::bv::dratOptimization::clauseMatchingTime"),
+ d_initialDratSize("proof::bv::dratOptimization::initialDratSize", 0),
+ d_optimizedDratSize("proof::bv::dratOptimization::optimizedDratSize", 0),
+ d_initialFormulaSize("proof::bv::dratOptimization::initialFormulaSize",
+ 0),
+ d_optimizedFormulaSize(
+ "proof::bv::dratOptimization::optimizedFormulaSize", 0)
+{
+ smtStatisticsRegistry()->registerStat(&d_totalTime);
+ smtStatisticsRegistry()->registerStat(&d_toolTime);
+ smtStatisticsRegistry()->registerStat(&d_clauseMatchingTime);
+ smtStatisticsRegistry()->registerStat(&d_initialDratSize);
+ smtStatisticsRegistry()->registerStat(&d_optimizedDratSize);
+ smtStatisticsRegistry()->registerStat(&d_initialFormulaSize);
+ smtStatisticsRegistry()->registerStat(&d_optimizedFormulaSize);
+}
+
+ClausalBitVectorProof::DratOptimizationStatistics::~DratOptimizationStatistics()
+{
+ smtStatisticsRegistry()->unregisterStat(&d_totalTime);
+ smtStatisticsRegistry()->unregisterStat(&d_toolTime);
+ smtStatisticsRegistry()->unregisterStat(&d_clauseMatchingTime);
+ smtStatisticsRegistry()->unregisterStat(&d_initialDratSize);
+ smtStatisticsRegistry()->unregisterStat(&d_optimizedDratSize);
+ smtStatisticsRegistry()->unregisterStat(&d_initialFormulaSize);
+ smtStatisticsRegistry()->unregisterStat(&d_optimizedFormulaSize);
+}
+
void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
std::ostream& os,
std::ostream& paren,
os << "\n;; DRAT Proof Value\n";
os << "(@ dratProof ";
paren << ")";
- drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+ d_dratTranslationStatistics.d_totalTime.start();
+ drat::DratProof pf = drat::DratProof::fromBinary(d_binaryDratProof.str());
+ d_dratTranslationStatistics.d_totalTime.stop();
+ pf.outputAsLfsc(os, 2);
os << "\n";
os << "\n;; Verification of DRAT Proof\n";
os << "\n;; DRAT Proof Value\n";
os << "(@ lratProof ";
paren << ")";
- lrat::LratProof pf = lrat::LratProof::fromDratProof(
- d_clauses, d_coreClauseIndices, d_binaryDratProof.str());
+ d_dratTranslationStatistics.d_totalTime.start();
+ lrat::LratProof pf =
+ lrat::LratProof::fromDratProof(d_clauses,
+ d_coreClauseIndices,
+ d_binaryDratProof.str(),
+ d_dratTranslationStatistics.d_toolTime);
+ d_dratTranslationStatistics.d_totalTime.stop();
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_clauses, d_coreClauseIndices, d_binaryDratProof.str());
+ d_dratTranslationStatistics.d_totalTime.start();
+ er::ErProof pf =
+ er::ErProof::fromBinaryDratProof(d_clauses,
+ d_coreClauseIndices,
+ d_binaryDratProof.str(),
+ d_dratTranslationStatistics.d_toolTime);
+ d_dratTranslationStatistics.d_totalTime.stop();
pf.outputAsLfsc(os);
}
#include "prop/cnf_stream.h"
#include "prop/sat_solver_types.h"
#include "theory/bv/theory_bv.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
std::ostringstream d_binaryDratProof{};
std::vector<ClauseId> d_coreClauseIndices{};
+ struct DratTranslationStatistics
+ {
+ DratTranslationStatistics();
+ ~DratTranslationStatistics();
+
+ // Total time spent doing translation (optimized binary DRAT -> in memory
+ // target format including IO, postprocessing, etc.)
+ TimerStat d_totalTime;
+ // Time that the external tool actually spent
+ TimerStat d_toolTime;
+ };
+
+ DratTranslationStatistics d_dratTranslationStatistics;
+
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();
+
+ // Given reference to a SAT clause encoded as a vector of literals, puts the
+ // literals into a canonical order
+ static void canonicalizeClause(prop::SatClause& clause);
+
+ struct DratOptimizationStatistics
+ {
+ DratOptimizationStatistics();
+ ~DratOptimizationStatistics();
+
+ // Total time spent using drat-trim to optimize the DRAT proof/formula
+ // (including IO, etc.)
+ TimerStat d_totalTime;
+ // Time that drat-trim actually spent optimizing the DRAT proof/formula
+ TimerStat d_toolTime;
+ // Time that was spent matching clauses in drat-trim's output to clauses in
+ // its input
+ TimerStat d_clauseMatchingTime;
+ // Bytes in binary DRAT proof before optimization
+ IntStat d_initialDratSize;
+ // Bytes in binary DRAT proof after optimization
+ IntStat d_optimizedDratSize;
+ // Bytes in textual DIMACS bitblasted formula before optimization
+ IntStat d_initialFormulaSize;
+ // Bytes in textual DIMACS bitblasted formula after optimization
+ IntStat d_optimizedFormulaSize;
+ };
+
+ DratOptimizationStatistics d_dratOptimizationStatistics;
};
/**
ErProof ErProof::fromBinaryDratProof(
const std::unordered_map<ClauseId, prop::SatClause>& clauses,
const std::vector<ClauseId>& usedIds,
- const std::string& dratBinary)
+ const std::string& dratBinary,
+ TimerStat& toolTimer)
{
std::string formulaFilename("cvc4-dimacs-XXXXXX");
std::string dratFilename("cvc4-drat-XXXXXX");
std::fstream tracecheckStream = openTmpFile(&tracecheckFilename);
// Invoke drat2er
+ {
+ CodeTimer blockTimer{toolTimer};
#if CVC4_USE_DRAT2ER
- drat2er::TransformDRATToExtendedResolution(formulaFilename,
- dratFilename,
- tracecheckFilename,
- false,
- drat2er::options::QUIET,
- false);
+ drat2er::TransformDRATToExtendedResolution(formulaFilename,
+ dratFilename,
+ tracecheckFilename,
+ false,
+ drat2er::options::QUIET,
+ false);
#else
- Unimplemented(
- "ER proof production requires drat2er.\n"
- "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+ Unimplemented(
+ "ER proof production requires drat2er.\n"
+ "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
#endif
+ }
// Parse the resulting TRACECHECK proof into an ER proof.
TraceCheckProof pf = TraceCheckProof::fromText(tracecheckStream);
#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace proof {
* @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
+ *
+ * @return the Er proof and a timer of the execution of drat2er
*/
static ErProof fromBinaryDratProof(
const std::unordered_map<ClauseId, prop::SatClause>& clauses,
const std::vector<ClauseId>& usedIds,
- const std::string& dratBinary);
+ const std::string& dratBinary,
+ TimerStat& toolTimer
+ );
/**
* Construct an ER proof from a TRACECHECK ER proof
LratProof LratProof::fromDratProof(
const std::unordered_map<ClauseId, prop::SatClause>& clauses,
const std::vector<ClauseId> usedIds,
- const std::string& dratBinary)
+ const std::string& dratBinary,
+ TimerStat& toolTimer)
{
std::ostringstream cmd;
std::string formulaFilename("cvc4-dimacs-XXXXXX");
std::fstream lratStream = openTmpFile(&lratFilename);
+ {
+ CodeTimer blockTimer{toolTimer};
#if CVC4_USE_DRAT2ER
- drat2er::drat_trim::CheckAndConvertToLRAT(
- formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
+ drat2er::drat_trim::CheckAndConvertToLRAT(
+ formulaFilename, dratFilename, lratFilename, drat2er::options::QUIET);
#else
- Unimplemented(
- "LRAT proof production requires drat2er.\n"
- "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+ Unimplemented(
+ "LRAT proof production requires drat2er.\n"
+ "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
#endif
+ }
LratProof lrat(lratStream);
remove(formulaFilename.c_str());
#include <iosfwd>
#include <string>
#include <unordered_map>
+#include <utility>
#include <vector>
#include "proof/clause_id.h"
// Included because we need operator<< for the SAT types
#include "prop/sat_solver.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace proof {
* @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.
+ *
+ * @return an LRAT proof an a timer for how long it took to run drat-trim
*/
static LratProof fromDratProof(
const std::unordered_map<ClauseId, prop::SatClause>& clauses,
const std::vector<ClauseId> usedIds,
- const std::string& dratBinary);
+ const std::string& dratBinary,
+ TimerStat& toolTimer);
/**
* @brief Construct an LRAT proof from its textual representation
*
void LFSCProof::toStream(std::ostream& out) const
{
TimerStat::CodeTimer proofProductionTimer(
- *ProofManager::currentPM()->getProofProductionTime());
+ ProofManager::currentPM()->getStats().d_proofProductionTime);
- Assert(!d_satProof->proofConstructed());
- d_satProof->constructProof();
-
- // collecting leaf clauses in resolution proof
IdToSatClause used_lemmas;
IdToSatClause used_inputs;
- d_satProof->collectClausesUsed(used_inputs,
- used_lemmas);
+ std::set<Node> atoms;
+ NodePairSet rewrites;
+ NodeSet used_assertions;
- IdToSatClause::iterator it2;
- Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
- for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2) {
- Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
- }
- Debug("pf::pm") << std::endl;
-
- // Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
- // for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
- // Debug("pf::pm") << "\t lemma = " << *(it2->second) << std::endl;
- // }
- // Debug("pf::pm") << std::endl;
- Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
- for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2) {
-
- std::vector<Expr> clause_expr;
- for(unsigned i = 0; i < it2->second->size(); ++i) {
- prop::SatLiteral lit = (*(it2->second))[i];
- Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
- if (atom.isConst()) {
- Assert (atom == utils::mkTrue());
- continue;
- }
- Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom;
- clause_expr.push_back(expr_lit);
- }
+ {
+ CodeTimer skeletonProofTimer{
+ ProofManager::currentPM()->getStats().d_skeletonProofTraceTime};
+ Assert(!d_satProof->proofConstructed());
+ d_satProof->constructProof();
- Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second) << std::endl;
- Debug("pf::pm") << "\t";
- for (unsigned i = 0; i < clause_expr.size(); ++i) {
- Debug("pf::pm") << clause_expr[i] << " ";
+ // collecting leaf clauses in resolution proof
+ d_satProof->collectClausesUsed(used_inputs, used_lemmas);
+
+ IdToSatClause::iterator it2;
+ Debug("pf::pm") << std::endl << "Used inputs: " << std::endl;
+ for (it2 = used_inputs.begin(); it2 != used_inputs.end(); ++it2)
+ {
+ Debug("pf::pm") << "\t input = " << *(it2->second) << std::endl;
}
Debug("pf::pm") << std::endl;
- }
- Debug("pf::pm") << std::endl;
- // collecting assertions that lead to the clauses being asserted
- NodeSet used_assertions;
- d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
-
- NodeSet::iterator it3;
- Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
- for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
- Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
+ Debug("pf::pm") << std::endl << "Used lemmas: " << std::endl;
+ for (it2 = used_lemmas.begin(); it2 != used_lemmas.end(); ++it2)
+ {
+ std::vector<Expr> clause_expr;
+ for (unsigned i = 0; i < it2->second->size(); ++i)
+ {
+ prop::SatLiteral lit = (*(it2->second))[i];
+ Expr atom = d_cnfProof->getAtom(lit.getSatVariable()).toExpr();
+ if (atom.isConst())
+ {
+ Assert(atom == utils::mkTrue());
+ continue;
+ }
+ Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom;
+ clause_expr.push_back(expr_lit);
+ }
- std::set<Node> atoms;
+ Debug("pf::pm") << "\t lemma " << it2->first << " = " << *(it2->second)
+ << std::endl;
+ Debug("pf::pm") << "\t";
+ for (unsigned i = 0; i < clause_expr.size(); ++i)
+ {
+ Debug("pf::pm") << clause_expr[i] << " ";
+ }
+ Debug("pf::pm") << std::endl;
+ }
+ Debug("pf::pm") << std::endl;
- NodePairSet rewrites;
- // collects the atoms in the clauses
- d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
-
- if (!rewrites.empty()) {
- Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
- NodePairSet::const_iterator rewriteIt;
- for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end(); ++rewriteIt) {
- Debug("pf::pm") << "\t" << rewriteIt->first << " --> " << rewriteIt->second << std::endl;
+ // collecting assertions that lead to the clauses being asserted
+ d_cnfProof->collectAssertionsForClauses(used_inputs, used_assertions);
+
+ NodeSet::iterator it3;
+ Debug("pf::pm") << std::endl << "Used assertions: " << std::endl;
+ for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3)
+ Debug("pf::pm") << "\t assertion = " << *it3 << std::endl;
+
+ // collects the atoms in the clauses
+ d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites);
+
+ if (!rewrites.empty())
+ {
+ Debug("pf::pm") << std::endl << "Rewrites used in lemmas: " << std::endl;
+ NodePairSet::const_iterator rewriteIt;
+ for (rewriteIt = rewrites.begin(); rewriteIt != rewrites.end();
+ ++rewriteIt)
+ {
+ Debug("pf::pm") << "\t" << rewriteIt->first << " --> "
+ << rewriteIt->second << std::endl;
+ }
+ Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
+ }
+ else
+ {
+ Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
}
- Debug("pf::pm") << std::endl << "Rewrite printing done" << std::endl;
- } else {
- Debug("pf::pm") << "No rewrites in lemmas found" << std::endl;
- }
- // The derived/unrewritten atoms may not have CNF literals required later on.
- // If they don't, add them.
- std::set<Node>::const_iterator it;
- for (it = atoms.begin(); it != atoms.end(); ++it) {
- Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
- if (!d_cnfProof->hasLiteral(*it)) {
- // For arithmetic: these literals are not normalized, causing an error in Arith.
- if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH) {
- d_cnfProof->ensureLiteral(*it, true); // This disables preregistration with the theory solver.
- } else {
- d_cnfProof->ensureLiteral(*it); // Normal method, with theory solver preregisteration.
+ // The derived/unrewritten atoms may not have CNF literals required later
+ // on. If they don't, add them.
+ std::set<Node>::const_iterator it;
+ for (it = atoms.begin(); it != atoms.end(); ++it)
+ {
+ Debug("pf::pm") << "Ensure literal for atom: " << *it << std::endl;
+ if (!d_cnfProof->hasLiteral(*it))
+ {
+ // For arithmetic: these literals are not normalized, causing an error
+ // in Arith.
+ if (theory::Theory::theoryOf(*it) == theory::THEORY_ARITH)
+ {
+ d_cnfProof->ensureLiteral(
+ *it,
+ true); // This disables preregistration with the theory solver.
+ }
+ else
+ {
+ d_cnfProof->ensureLiteral(
+ *it); // Normal method, with theory solver preregisteration.
+ }
}
}
- }
- d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
- d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
+ d_cnfProof->collectAtomsForClauses(used_inputs, atoms);
+ d_cnfProof->collectAtomsForClauses(used_lemmas, atoms);
- // collects the atoms in the assertions
- for (NodeSet::const_iterator it = used_assertions.begin();
- it != used_assertions.end(); ++it) {
- utils::collectAtoms(*it, atoms);
- // utils::collectAtoms(*it, newAtoms);
- }
+ // collects the atoms in the assertions
+ for (NodeSet::const_iterator it = used_assertions.begin();
+ it != used_assertions.end();
+ ++it)
+ {
+ utils::collectAtoms(*it, atoms);
+ }
- std::set<Node>::iterator atomIt;
- Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: "
- << std::endl << std::endl;
- for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt) {
- Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
+ std::set<Node>::iterator atomIt;
+ Debug("pf::pm") << std::endl
+ << "Dumping atoms from lemmas, inputs and assertions: "
+ << std::endl
+ << std::endl;
+ for (atomIt = atoms.begin(); atomIt != atoms.end(); ++atomIt)
+ {
+ Debug("pf::pm") << "\tAtom: " << *atomIt << std::endl;
+ }
}
+
smt::SmtScope scope(d_smtEngine);
+ ProofLetMap globalLetMap;
std::ostringstream paren;
- out << "(check\n";
- paren << ")";
- out << " ;; Declarations\n";
-
- // declare the theory atoms
- Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
- for(it = atoms.begin(); it != atoms.end(); ++it) {
- Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
- d_theoryProof->registerTerm((*it).toExpr());
- }
-
- Debug("pf::pm") << std::endl << "Term registration done!" << std::endl << std::endl;
-
- Debug("pf::pm") << std::endl << "LFSCProof::toStream: starting to print assertions" << std::endl;
-
- // print out all the original assertions
- d_theoryProof->registerTermsFromAssertions();
- d_theoryProof->printSortDeclarations(out, paren);
- d_theoryProof->printTermDeclarations(out, paren);
- d_theoryProof->printAssertions(out, paren);
-
- Debug("pf::pm") << std::endl << "LFSCProof::toStream: print assertions DONE" << std::endl;
+ {
+ CodeTimer declTimer{
+ ProofManager::currentPM()->getStats().d_proofDeclarationsTime};
+ out << "(check\n";
+ paren << ")";
+ out << " ;; Declarations\n";
+
+ // declare the theory atoms
+ Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl;
+ for (std::set<Node>::const_iterator it = atoms.begin(); it != atoms.end(); ++it)
+ {
+ Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl;
+ d_theoryProof->registerTerm((*it).toExpr());
+ }
- out << "(: (holds cln)\n\n";
- paren << ")";
+ Debug("pf::pm") << std::endl
+ << "Term registration done!" << std::endl
+ << std::endl;
- // Have the theory proofs print deferred declarations, e.g. for skolem variables.
- out << " ;; Printing deferred declarations \n\n";
- d_theoryProof->printDeferredDeclarations(out, paren);
+ Debug("pf::pm") << std::endl
+ << "LFSCProof::toStream: starting to print assertions"
+ << std::endl;
- out << "\n ;; Printing the global let map";
- d_theoryProof->finalizeBvConflicts(used_lemmas, out);
- ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
- ProofLetMap globalLetMap;
- if (options::lfscLetification()) {
- ProofManager::currentPM()->printGlobalLetMap(atoms, globalLetMap, out, paren);
- }
+ // print out all the original assertions
+ d_theoryProof->registerTermsFromAssertions();
+ d_theoryProof->printSortDeclarations(out, paren);
+ d_theoryProof->printTermDeclarations(out, paren);
+ d_theoryProof->printAssertions(out, paren);
- out << " ;; Printing aliasing declarations \n\n";
- d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
+ Debug("pf::pm") << std::endl
+ << "LFSCProof::toStream: print assertions DONE"
+ << std::endl;
- out << " ;; Rewrites for Lemmas \n";
- d_theoryProof->printLemmaRewrites(rewrites, out, paren);
+ out << "(: (holds cln)\n\n";
+ paren << ")";
- // print trust that input assertions are their preprocessed form
- printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
+ // Have the theory proofs print deferred declarations, e.g. for skolem
+ // variables.
+ out << " ;; Printing deferred declarations \n\n";
+ d_theoryProof->printDeferredDeclarations(out, paren);
+
+ out << "\n ;; Printing the global let map";
+ d_theoryProof->finalizeBvConflicts(used_lemmas, out);
+ ProofManager::getBitVectorProof()->calculateAtomsInBitblastingProof();
+ if (options::lfscLetification())
+ {
+ ProofManager::currentPM()->printGlobalLetMap(
+ atoms, globalLetMap, out, paren);
+ }
- // print mapping between theory atoms and internal SAT variables
- out << ";; Printing mapping from preprocessed assertions into atoms \n";
- d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
+ out << " ;; Printing aliasing declarations \n\n";
+ d_theoryProof->printAliasingDeclarations(out, paren, globalLetMap);
- Debug("pf::pm") << std::endl << "Printing cnf proof for clauses" << std::endl;
+ out << " ;; Rewrites for Lemmas \n";
+ d_theoryProof->printLemmaRewrites(rewrites, out, paren);
- IdToSatClause::const_iterator cl_it = used_inputs.begin();
- // print CNF conversion proof for each clause
- for (; cl_it != used_inputs.end(); ++cl_it) {
- d_cnfProof->printCnfProofForClause(cl_it->first, cl_it->second, out, paren);
+ // print trust that input assertions are their preprocessed form
+ printPreprocessedAssertions(used_assertions, out, paren, globalLetMap);
}
- Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl;
+ {
+ CodeTimer cnfProofTimer{
+ ProofManager::currentPM()->getStats().d_cnfProofTime};
+ // print mapping between theory atoms and internal SAT variables
+ out << ";; Printing mapping from preprocessed assertions into atoms \n";
+ d_cnfProof->printAtomMapping(atoms, out, paren, globalLetMap);
+
+ Debug("pf::pm") << std::endl
+ << "Printing cnf proof for clauses" << std::endl;
+
+ IdToSatClause::const_iterator cl_it = used_inputs.begin();
+ // print CNF conversion proof for each clause
+ for (; cl_it != used_inputs.end(); ++cl_it)
+ {
+ d_cnfProof->printCnfProofForClause(
+ cl_it->first, cl_it->second, out, paren);
+ }
+ }
- Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
- d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
- Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl;
+ {
+ CodeTimer theoryLemmaTimer{
+ ProofManager::currentPM()->getStats().d_theoryLemmaTime};
+ Debug("pf::pm") << std::endl
+ << "Printing cnf proof for clauses DONE" << std::endl;
+
+ Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl;
+ d_theoryProof->printTheoryLemmas(used_lemmas, out, paren, globalLetMap);
+ Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!"
+ << std::endl;
+ }
- out << ";; Printing final unsat proof \n";
- if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
- ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
- } else {
- // print actual resolution proof
- proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
- proof::LFSCProofPrinter::printResolutionEmptyClause(d_satProof, out, paren);
+ {
+ CodeTimer finalProofTimer{
+ ProofManager::currentPM()->getStats().d_finalProofTime};
+ out << ";; Printing final unsat proof \n";
+ if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
+ && ProofManager::getBitVectorProof())
+ {
+ ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
+ }
+ else
+ {
+ // print actual resolution proof
+ proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
+ proof::LFSCProofPrinter::printResolutionEmptyClause(
+ d_satProof, out, paren);
+ }
}
out << paren.str();
}
ProofManager::ProofManagerStatistics::ProofManagerStatistics()
- : d_proofProductionTime("proof::ProofManager::proofProductionTime")
+ : d_proofProductionTime("proof::ProofManager::proofProductionTime"),
+ d_theoryLemmaTime(
+ "proof::ProofManager::proofProduction::theoryLemmaTime"),
+ d_skeletonProofTraceTime(
+ "proof::ProofManager::proofProduction::skeletonProofTraceTime"),
+ d_proofDeclarationsTime(
+ "proof::ProofManager::proofProduction::proofDeclarationsTime"),
+ d_cnfProofTime("proof::ProofManager::proofProduction::cnfProofTime"),
+ d_finalProofTime("proof::ProofManager::proofProduction::finalProofTime")
{
smtStatisticsRegistry()->registerStat(&d_proofProductionTime);
+ smtStatisticsRegistry()->registerStat(&d_theoryLemmaTime);
+ smtStatisticsRegistry()->registerStat(&d_skeletonProofTraceTime);
+ smtStatisticsRegistry()->registerStat(&d_proofDeclarationsTime);
+ smtStatisticsRegistry()->registerStat(&d_cnfProofTime);
+ smtStatisticsRegistry()->registerStat(&d_finalProofTime);
}
ProofManager::ProofManagerStatistics::~ProofManagerStatistics()
{
smtStatisticsRegistry()->unregisterStat(&d_proofProductionTime);
+ smtStatisticsRegistry()->unregisterStat(&d_theoryLemmaTime);
+ smtStatisticsRegistry()->unregisterStat(&d_skeletonProofTraceTime);
+ smtStatisticsRegistry()->unregisterStat(&d_proofDeclarationsTime);
+ smtStatisticsRegistry()->unregisterStat(&d_cnfProofTime);
+ smtStatisticsRegistry()->unregisterStat(&d_finalProofTime);
}
} /* CVC4 namespace */
std::ostream& out,
std::ostringstream& paren);
- TimerStat* getProofProductionTime() { return &d_stats.d_proofProductionTime; }
-
- private:
- void constructSatProof();
- std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
-
struct ProofManagerStatistics
{
ProofManagerStatistics();
* information)
*/
TimerStat d_proofProductionTime;
+
+ /**
+ * Time spent printing proofs of theory lemmas
+ */
+ TimerStat d_theoryLemmaTime;
+
+ /**
+ * Time spent tracing the proof of the boolean skeleton
+ * (e.g. figuring out which assertions are needed, etc.)
+ */
+ TimerStat d_skeletonProofTraceTime;
+
+ /**
+ * Time spent processing and printing declarations in the proof
+ */
+ TimerStat d_proofDeclarationsTime;
+
+ /**
+ * Time spent printing the CNF proof
+ */
+ TimerStat d_cnfProofTime;
+
+ /**
+ * Time spent printing the final proof of UNSAT
+ */
+ TimerStat d_finalProofTime;
+
}; /* struct ProofManagerStatistics */
+ ProofManagerStatistics& getStats() { return d_stats; }
+
+ private:
+ void constructSatProof();
+ std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
+
ProofManagerStatistics d_stats;
};/* class ProofManager */
--- /dev/null
+/********************* */
+/*! \file sat_solver_types.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 Implementations of SAT solver type operations which require large
+ ** std headers.
+ **
+ **/
+
+#include "prop/sat_solver_types.h"
+
+#include <algorithm>
+
+namespace CVC4 {
+namespace prop {
+bool SatClauseLessThan::operator()(const SatClause& l, const SatClause& r) const
+{
+ return std::lexicographical_compare(l.begin(), l.end(), r.begin(), r.end());
+}
+} // namespace prop
+} // namespace CVC4
return !(*this == other);
}
+ /**
+ * Compare two literals
+ */
+ bool operator<(const SatLiteral& other) const
+ {
+ return getSatVariable() == other.getSatVariable()
+ ? isNegated() < other.isNegated()
+ : getSatVariable() < other.getSatVariable();
+ }
+
/**
* Returns a string representation of the literal.
*/
}
};
+struct SatClauseLessThan
+{
+ bool operator()(const SatClause& l, const SatClause& r) const;
+};
+
/**
* Each object in the SAT solver, such as as variables and clauses, can be assigned a life span,
* so that the SAT solver can (or should) remove them when the lifespan is over.
}
}
-
-
projects / cvc5.git / commitdiff