summaryrefslogtreecommitdiff
path: root/src/proof/proof_manager.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r--src/proof/proof_manager.cpp369
1 files changed, 223 insertions, 146 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 005a23378..f68d5937c 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -561,184 +561,243 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
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();
@@ -1074,14 +1133,32 @@ void ProofManager::printTrustedTerm(Node term,
}
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback