diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /src/proof/theory_proof.cpp | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'src/proof/theory_proof.cpp')
-rw-r--r-- | src/proof/theory_proof.cpp | 748 |
1 files changed, 566 insertions, 182 deletions
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp index 088275b3f..d12b561a6 100644 --- a/src/proof/theory_proof.cpp +++ b/src/proof/theory_proof.cpp @@ -19,12 +19,14 @@ #include "base/cvc4_assert.h" #include "context/context.h" #include "options/bv_options.h" +#include "options/proof_options.h" #include "proof/arith_proof.h" #include "proof/array_proof.h" #include "proof/bitvector_proof.h" #include "proof/clause_id.h" #include "proof/cnf_proof.h" #include "proof/proof_manager.h" +#include "proof/proof_output_channel.h" #include "proof/proof_utils.h" #include "proof/sat_proof.h" #include "proof/uf_proof.h" @@ -45,77 +47,9 @@ namespace CVC4 { -unsigned CVC4::LetCount::counter = 0; +unsigned CVC4::ProofLetCount::counter = 0; static unsigned LET_COUNT = 1; -//for proof replay -class ProofOutputChannel : public theory::OutputChannel { -public: - Node d_conflict; - Proof* d_proof; - Node d_lemma; - - ProofOutputChannel() : d_conflict(), d_proof(NULL) {} - virtual ~ProofOutputChannel() throw() {} - - void conflict(TNode n, Proof* pf) throw() { - Trace("theory-proof-debug") << "; CONFLICT: " << n << std::endl; - Assert(d_conflict.isNull()); - Assert(!n.isNull()); - d_conflict = n; - Assert(pf != NULL); - d_proof = pf; - } - bool propagate(TNode x) throw() { - Trace("theory-proof-debug") << "got a propagation: " << x << std::endl; - return true; - } - theory::LemmaStatus lemma(TNode n, ProofRule rule, bool, bool, bool) throw() { - Trace("theory-proof-debug") << "new lemma: " << n << std::endl; - d_lemma = n; - return theory::LemmaStatus(TNode::null(), 0); - } - theory::LemmaStatus splitLemma(TNode, bool) throw() { - AlwaysAssert(false); - return theory::LemmaStatus(TNode::null(), 0); - } - void requirePhase(TNode n, bool b) throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::requirePhase called" << std::endl; - Trace("theory-proof-debug") << "requirePhase " << n << " " << b << std::endl; - } - bool flipDecision() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::flipDecision called" << std::endl; - AlwaysAssert(false); - return false; - } - void setIncomplete() throw() { - Debug("theory-proof-debug") << "ProofOutputChannel::setIncomplete called" << std::endl; - AlwaysAssert(false); - } -};/* class ProofOutputChannel */ - -//for proof replay -class MyPreRegisterVisitor { - theory::Theory* d_theory; - __gnu_cxx::hash_set<TNode, TNodeHashFunction> d_visited; -public: - typedef void return_type; - MyPreRegisterVisitor(theory::Theory* theory) - : d_theory(theory) - , d_visited() - {} - bool alreadyVisited(TNode current, TNode parent) { return d_visited.find(current) != d_visited.end(); } - void visit(TNode current, TNode parent) { - if(theory::Theory::theoryOf(current) == d_theory->getId()) { - //Trace("theory-proof-debug") << "preregister " << current << std::endl; - d_theory->preRegisterTerm(current); - d_visited.insert(current); - } - } - void start(TNode node) { } - void done(TNode node) { } -}; /* class MyPreRegisterVisitor */ - TheoryProofEngine::TheoryProofEngine() : d_registrationCache() , d_theoryProofTable() @@ -131,13 +65,12 @@ TheoryProofEngine::~TheoryProofEngine() { } } - void TheoryProofEngine::registerTheory(theory::Theory* th) { - if( th ){ + if (th) { theory::TheoryId id = th->getId(); if(d_theoryProofTable.find(id) == d_theoryProofTable.end()) { - Trace("theory-proof-debug") << "; register theory " << id << std::endl; + Trace("pf::tp") << "TheoryProofEngine::registerTheory: " << id << std::endl; if (id == theory::THEORY_UF) { d_theoryProofTable[id] = new LFSCUFProof((theory::uf::TheoryUF*)th, this); @@ -147,7 +80,6 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { if (id == theory::THEORY_BV) { BitVectorProof * bvp = new LFSCBitVectorProof((theory::bv::TheoryBV*)th, this); d_theoryProofTable[id] = bvp; - ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); return; } @@ -166,20 +98,54 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) { } } +void TheoryProofEngine::finishRegisterTheory(theory::Theory* th) { + if (th) { + theory::TheoryId id = th->getId(); + if (id == theory::THEORY_BV) { + Assert(d_theoryProofTable.find(id) != d_theoryProofTable.end()); + + BitVectorProof *bvp = (BitVectorProof *)d_theoryProofTable[id]; + ((theory::bv::TheoryBV*)th)->setProofLog( bvp ); + return; + } + } +} + TheoryProof* TheoryProofEngine::getTheoryProof(theory::TheoryId id) { + // The UF theory handles queries for the Builtin theory. + if (id == theory::THEORY_BUILTIN) { + Debug("pf::tp") << "TheoryProofEngine::getTheoryProof: BUILTIN --> UF" << std::endl; + id = theory::THEORY_UF; + } + Assert (d_theoryProofTable.find(id) != d_theoryProofTable.end()); return d_theoryProofTable[id]; } +void TheoryProofEngine::markTermForFutureRegistration(Expr term, theory::TheoryId id) { + d_exprToTheoryIds[term].insert(id); +} + +void TheoryProofEngine::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + Assert(c1.isConst()); + Assert(c2.isConst()); + + Assert(theory::Theory::theoryOf(c1) == theory::Theory::theoryOf(c2)); + getTheoryProof(theory::Theory::theoryOf(c1))->printConstantDisequalityProof(os, c1, c2); +} + void TheoryProofEngine::registerTerm(Expr term) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering term: " << term << std::endl; + if (d_registrationCache.count(term)) { return; } - Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering new term: " << term << std::endl; + + Debug("pf::tp") << "TheoryProofEngine::registerTerm: registering NEW term: " << term << std::endl; theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << "Term's theory: " << theory_id << std::endl; + Debug("pf::tp") << "Term's theory( " << term << " ) = " << theory_id << std::endl; // don't need to register boolean terms if (theory_id == theory::THEORY_BUILTIN || @@ -193,58 +159,64 @@ void TheoryProofEngine::registerTerm(Expr term) { if (!supportedTheory(theory_id)) return; + // Register the term with its owner theory getTheoryProof(theory_id)->registerTerm(term); + + // A special case: the array theory needs to know of every skolem, even if + // it belongs to another theory (e.g., a BV skolem) + if (ProofManager::getSkolemizationManager()->isSkolem(term) && theory_id != theory::THEORY_ARRAY) { + Debug("pf::tp") << "TheoryProofEngine::registerTerm: Special case: registering a non-array skolem: " << term << std::endl; + getTheoryProof(theory::THEORY_ARRAY)->registerTerm(term); + } + d_registrationCache.insert(term); } -theory::TheoryId TheoryProofEngine::getTheoryForLemma(ClauseId id) { +theory::TheoryId TheoryProofEngine::getTheoryForLemma(const prop::SatClause* clause) { ProofManager* pm = ProofManager::currentPM(); - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma( " << id << " )" - << " = " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + std::set<Node> nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + if (atom.isConst()) { + Assert (atom == utils::mkTrue()); + continue; + } - if ((pm->getLogic() == "QF_UFLIA") || (pm->getLogic() == "QF_UFLRA")) { - Debug("pf::tp") << "TheoryProofEngine::getTheoryForLemma: special hack for Arithmetic-with-holes support. " - << "Returning THEORY_ARITH" << std::endl; - return theory::THEORY_ARITH; + nodes.insert(lit.isNegated() ? node.notNode() : node); } - return pm->getCnfProof()->getOwnerTheory(id); - - // if (pm->getLogic() == "QF_UF") return theory::THEORY_UF; - // if (pm->getLogic() == "QF_BV") return theory::THEORY_BV; - // if (pm->getLogic() == "QF_AX") return theory::THEORY_ARRAY; - // if (pm->getLogic() == "ALL_SUPPORTED") return theory::THEORY_BV; - - // Debug("pf::tp") << "Unsupported logic (" << pm->getLogic() << ")" << std::endl; - - // Unreachable(); + // Ensure that the lemma is in the database. + Assert (pm->getCnfProof()->haveProofRecipe(nodes)); + return pm->getCnfProof()->getProofRecipe(nodes).getTheory(); } -void LFSCTheoryProofEngine::bind(Expr term, LetMap& map, Bindings& let_order) { - LetMap::iterator it = map.find(term); +void LFSCTheoryProofEngine::bind(Expr term, ProofLetMap& map, Bindings& let_order) { + ProofLetMap::iterator it = map.find(term); if (it != map.end()) { - LetCount& count = it->second; + ProofLetCount& count = it->second; count.increment(); return; } for (unsigned i = 0; i < term.getNumChildren(); ++i) { bind(term[i], map, let_order); } - unsigned new_id = LetCount::newId(); - map[term] = LetCount(new_id); + unsigned new_id = ProofLetCount::newId(); + map[term] = ProofLetCount(new_id); let_order.push_back(LetOrderElement(term, new_id)); } void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { - LetMap map; + ProofLetMap map; Bindings let_order; bind(term, map, let_order); std::ostringstream paren; for (unsigned i = 0; i < let_order.size(); ++i) { Expr current_expr = let_order[i].expr; unsigned let_id = let_order[i].id; - LetMap::const_iterator it = map.find(current_expr); + ProofLetMap::const_iterator it = map.find(current_expr); Assert (it != map.end()); unsigned let_count = it->second.count; Assert(let_count); @@ -253,7 +225,7 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { continue; } - os << "(@ let"<<let_id << " "; + os << "(@ let" <<let_id << " "; printTheoryTerm(current_expr, os, map); paren <<")"; } @@ -264,16 +236,13 @@ void LFSCTheoryProofEngine::printLetTerm(Expr term, std::ostream& os) { printTheoryTerm(last, os, map); } else { - os << " let"<< last_let_id; + os << " let" << last_let_id; } os << paren.str(); } - -void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCTheoryProofEngine::printTheoryTerm(Expr term, std::ostream& os, const ProofLetMap& map) { theory::TheoryId theory_id = theory::Theory::theoryOf(term); - Debug("pf::tp") << std::endl << "LFSCTheoryProofEngine::printTheoryTerm: term = " << term - << ", theory_id = " << theory_id << std::endl; // boolean terms and ITEs are special because they // are common to all theories @@ -315,6 +284,29 @@ void LFSCTheoryProofEngine::printSort(Type type, std::ostream& os) { Unreachable(); } +void LFSCTheoryProofEngine::performExtraRegistrations() { + ExprToTheoryIds::const_iterator it; + for (it = d_exprToTheoryIds.begin(); it != d_exprToTheoryIds.end(); ++it) { + if (d_registrationCache.count(it->first)) { // Only register if the term appeared + TheoryIdSet::const_iterator theoryIt; + for (theoryIt = it->second.begin(); theoryIt != it->second.end(); ++theoryIt) { + Debug("pf::tp") << "\tExtra registration of term " << it->first + << " with theory: " << *theoryIt << std::endl; + Assert(supportedTheory(*theoryIt)); + getTheoryProof(*theoryIt)->registerTerm(it->first); + } + } + } +} + +void LFSCTheoryProofEngine::treatBoolsAsFormulas(bool value) { + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); + for (; it != end; ++it) { + it->second->treatBoolsAsFormulas(value); + } +} + void LFSCTheoryProofEngine::registerTermsFromAssertions() { ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions(); ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions(); @@ -322,6 +314,8 @@ void LFSCTheoryProofEngine::registerTermsFromAssertions() { for(; it != end; ++it) { registerTerm(*it); } + + performExtraRegistrations(); } void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& paren) { @@ -333,17 +327,51 @@ void LFSCTheoryProofEngine::printAssertions(std::ostream& os, std::ostream& pare for (; it != end; ++it) { Debug("pf::tp") << "printAssertions: assertion is: " << *it << std::endl; - // FIXME: merge this with counter - os << "(% A" << counter++ << " (th_holds "; - printLetTerm(*it, os); + std::ostringstream name; + name << "A" << counter++; + os << "(% " << name.str() << " (th_holds "; + + // Assertions appear before the global let map, so we use a dummpMap to avoid letification here. + ProofLetMap dummyMap; + printBoundTerm(*it, os, dummyMap); + os << ")\n"; paren << ")"; } - //store map between assertion and counter - // ProofManager::currentPM()->setAssertion( *it ); + Debug("pf::tp") << "LFSCTheoryProofEngine::printAssertions done" << std::endl << std::endl; } +void LFSCTheoryProofEngine::printLemmaRewrites(NodePairSet& rewrites, + std::ostream& os, + std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites called" << std::endl << std::endl; + + NodePairSet::const_iterator it; + + for (it = rewrites.begin(); it != rewrites.end(); ++it) { + Debug("pf::tp") << "printLemmaRewrites: " << it->first << " --> " << it->second << std::endl; + + Node n1 = it->first; + Node n2 = it->second; + Assert(n1.toExpr() == utils::mkFalse() || + theory::Theory::theoryOf(n1) == theory::Theory::theoryOf(n2)); + + std::ostringstream rewriteRule; + rewriteRule << ".lrr" << d_assertionToRewrite.size(); + + os << "(th_let_pf _ "; + getTheoryProof(theory::Theory::theoryOf(n1))->printRewriteProof(os, n1, n2); + os << "(\\ " << rewriteRule.str() << "\n"; + + d_assertionToRewrite[it->first] = rewriteRule.str(); + Debug("pf::tp") << "d_assertionToRewrite[" << it->first << "] = " << rewriteRule.str() << std::endl; + paren << "))"; + } + + Debug("pf::tp") << "LFSCTheoryProofEngine::printLemmaRewrites done" << std::endl << std::endl; +} + void LFSCTheoryProofEngine::printSortDeclarations(std::ostream& os, std::ostream& paren) { Debug("pf::tp") << "LFSCTheoryProofEngine::printSortDeclarations called" << std::endl << std::endl; @@ -378,55 +406,150 @@ void LFSCTheoryProofEngine::printDeferredDeclarations(std::ostream& os, std::ost } } -void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, - std::ostream& os, - std::ostream& paren) { - os << " ;; Theory Lemmas \n"; - ProofManager* pm = ProofManager::currentPM(); - IdToSatClause::const_iterator it = lemmas.begin(); - IdToSatClause::const_iterator end = lemmas.end(); - - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: checking lemma owners..." << std::endl; +void LFSCTheoryProofEngine::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printAliasingDeclarations called" << std::endl; + TheoryProofTable::const_iterator it = d_theoryProofTable.begin(); + TheoryProofTable::const_iterator end = d_theoryProofTable.end(); for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: new lemma" << std::endl; - ClauseId id = it->first; - Debug("pf::tp") << "\tLemma = " << id - << ". Owner theory: " << pm->getCnfProof()->getOwnerTheory(id) << std::endl; + it->second->printAliasingDeclarations(os, paren); } - it = lemmas.begin(); +} - // BitVector theory is special case: must know all - // conflicts needed ahead of time for resolution - // proof lemmas - std::vector<Expr> bv_lemmas; - for (; it != end; ++it) { +void LFSCTheoryProofEngine::dumpTheoryLemmas(const IdToSatClause& lemmas) { + Debug("pf::dumpLemmas") << "Dumping ALL theory lemmas" << std::endl << std::endl; + + ProofManager* pm = ProofManager::currentPM(); + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; + Debug("pf::dumpLemmas") << "**** \tLemma ID = " << id << std::endl; const prop::SatClause* clause = it->second; + std::set<Node> nodes; + for(unsigned i = 0; i < clause->size(); ++i) { + prop::SatLiteral lit = (*clause)[i]; + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + if (node.isConst()) { + Assert (node.toExpr() == utils::mkTrue()); + continue; + } + nodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(nodes); + recipe.dump("pf::dumpLemmas"); + } + + Debug("pf::dumpLemmas") << "Theory lemma printing DONE" << std::endl << std::endl; +} - theory::TheoryId theory_id = getTheoryForLemma(id); - if (theory_id != theory::THEORY_BV) continue; +// TODO: this function should be moved into the BV prover. +void LFSCTheoryProofEngine::finalizeBvConflicts(const IdToSatClause& lemmas, std::ostream& os) { + // BitVector theory is special case: must know all conflicts needed + // ahead of time for resolution proof lemmas + std::vector<Expr> bv_lemmas; + + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { + const prop::SatClause* clause = it->second; std::vector<Expr> conflict; + std::set<Node> conflictNodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = ProofManager::currentPM()->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); + + // The literals (true) and (not false) are omitted from conflicts if (atom.isConst()) { Assert (atom == utils::mkTrue() || (atom == utils::mkFalse() && lit.isNegated())); continue; } + Expr expr_lit = lit.isNegated() ? atom.notExpr() : atom; conflict.push_back(expr_lit); + conflictNodes.insert(lit.isNegated() ? node.notNode() : node); + } + + LemmaProofRecipe recipe = ProofManager::currentPM()->getCnfProof()->getProofRecipe(conflictNodes); + + unsigned numberOfSteps = recipe.getNumSteps(); + + prop::SatClause currentClause = *clause; + std::vector<Expr> currentClauseExpr = conflict; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + if (currentStep->getTheory() != theory::THEORY_BV) { + continue; + } + + // If any rewrites took place, we need to update the conflict clause accordingly + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i); + std::map<Node, Node> explanationToMissingAssertion; + std::set<Node>::iterator assertionIt; + for (assertionIt = missingAssertions.begin(); + assertionIt != missingAssertions.end(); + ++assertionIt) { + Node negated = (*assertionIt).negate(); + explanationToMissingAssertion[recipe.getExplanation(negated)] = negated; + } + + currentClause = *clause; + currentClauseExpr = conflict; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + + // If this literal is the result of a rewrite, we need to translate it + if (explanationToMissingAssertion.find(previousLiteralNode) != + explanationToMissingAssertion.end()) { + previousLiteralNode = explanationToMissingAssertion[previousLiteralNode]; + } + + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If we're in the final step, the last literal is Null and should not be added. + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, currentClauseExpr)); } - bv_lemmas.push_back(utils::mkSortedExpr(kind::OR, conflict)); } - // FIXME: ugly, move into bit-vector proof by adding lemma - // queue inside each theory_proof + BitVectorProof* bv = ProofManager::getBitVectorProof(); bv->finalizeConflicts(bv_lemmas); + // bv->printResolutionProof(os, paren, letMap); +} - bv->printResolutionProof(os, paren); +void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, + std::ostream& os, + std::ostream& paren, + ProofLetMap& map) { + os << " ;; Theory Lemmas \n"; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: starting" << std::endl; + + if (Debug.isOn("pf::dumpLemmas")) { + dumpTheoryLemmas(lemmas); + } + + // finalizeBvConflicts(lemmas, os, paren, map); + ProofManager::getBitVectorProof()->printResolutionProof(os, paren, map); if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) { Assert (lemmas.size() == 1); @@ -434,61 +557,255 @@ void LFSCTheoryProofEngine::printTheoryLemmas(const IdToSatClause& lemmas, return; } - it = lemmas.begin(); - + ProofManager* pm = ProofManager::currentPM(); Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemmas..." << std::endl; - for (; it != end; ++it) { - Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing a new lemma!" << std::endl; - - // Debug("pf::tp") << "\tLemma = " << it->first << ", " << *(it->second) << std::endl; + for (IdToSatClause::const_iterator it = lemmas.begin(); it != lemmas.end(); ++it) { ClauseId id = it->first; - Debug("pf::tp") << "Owner theory:" << pm->getCnfProof()->getOwnerTheory(id) << std::endl; const prop::SatClause* clause = it->second; - // printing clause as it appears in resolution proof - os << "(satlem _ _ "; - std::ostringstream clause_paren; - Debug("pf::tp") << "CnfProof printing clause..." << std::endl; - pm->getCnfProof()->printClause(*clause, os, clause_paren); - Debug("pf::tp") << "CnfProof printing clause - Done!" << std::endl; + Debug("pf::tp") << "LFSCTheoryProofEngine::printTheoryLemmas: printing lemma. ID = " + << id << std::endl; std::vector<Expr> clause_expr; + std::set<Node> clause_expr_nodes; for(unsigned i = 0; i < clause->size(); ++i) { prop::SatLiteral lit = (*clause)[i]; - Expr atom = pm->getCnfProof()->getAtom(lit.getSatVariable()).toExpr(); + Node node = pm->getCnfProof()->getAtom(lit.getSatVariable()); + Expr atom = node.toExpr(); if (atom.isConst()) { Assert (atom == utils::mkTrue()); continue; } Expr expr_lit = lit.isNegated() ? atom.notExpr(): atom; clause_expr.push_back(expr_lit); + clause_expr_nodes.insert(lit.isNegated() ? node.notNode() : node); } - Debug("pf::tp") << "Expression printing done!" << std::endl; - - // query appropriate theory for proof of clause - theory::TheoryId theory_id = getTheoryForLemma(id); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; - Debug("theory-proof-debug") << ";; Get theory lemma from " << theory_id << "..." << std::endl; - getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren); - Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; - // os << " (clausify_false trust)"; - os << clause_paren.str(); - os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; - paren << "))"; + LemmaProofRecipe recipe = pm->getCnfProof()->getProofRecipe(clause_expr_nodes); + + if (recipe.simpleLemma()) { + // In a simple lemma, there will be no propositional resolution in the end + + Debug("pf::tp") << "Simple lemma" << std::endl; + // Printing the clause as it appears in resolution proof + os << "(satlem _ _ "; + std::ostringstream clause_paren; + pm->getCnfProof()->printClause(*clause, os, clause_paren); + + // Find and handle missing assertions, due to rewrites + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(0); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this simple lemma!" << std::endl; + } + + std::set<Node>::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < clause_expr.size(); ++k) { + if (clause_expr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + AlwaysAssert(found); + Debug("pf::tp") << "Replacing theory assertion " + << clause_expr[k] + << " with " + << *missingAssertion + << std::endl; + + clause_expr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + // Query the appropriate theory for a proof of this clause + theory::TheoryId theory_id = getTheoryForLemma(clause); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + getTheoryProof(theory_id)->printTheoryLemmaProof(clause_expr, os, paren, map); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) <<"\n"; + paren << "))"; + } else { // This is a composite lemma + + unsigned numberOfSteps = recipe.getNumSteps(); + prop::SatClause currentClause = *clause; + std::vector<Expr> currentClauseExpr = clause_expr; + + for (unsigned i = 0; i < numberOfSteps; ++i) { + const LemmaProofRecipe::ProofStep* currentStep = recipe.getStep(i); + + currentClause = *clause; + currentClauseExpr = clause_expr; + + for (unsigned j = 0; j < i; ++j) { + // Literals already used in previous steps need to be negated + Node previousLiteralNode = recipe.getStep(j)->getLiteral(); + Node previousLiteralNodeNegated = previousLiteralNode.negate(); + prop::SatLiteral previousLiteralNegated = + ProofManager::currentPM()->getCnfProof()->getLiteral(previousLiteralNodeNegated); + currentClause.push_back(previousLiteralNegated); + currentClauseExpr.push_back(previousLiteralNodeNegated.toExpr()); + } + + // If the current literal is NULL, can ignore (final step) + // Otherwise, the current literal does NOT need to be negated + Node currentLiteralNode = currentStep->getLiteral(); + if (currentLiteralNode != Node()) { + prop::SatLiteral currentLiteral = + ProofManager::currentPM()->getCnfProof()->getLiteral(currentLiteralNode); + + currentClause.push_back(currentLiteral); + currentClauseExpr.push_back(currentLiteralNode.toExpr()); + } + + os << "(satlem _ _ "; + std::ostringstream clause_paren; + + pm->getCnfProof()->printClause(currentClause, os, clause_paren); + + // query appropriate theory for proof of clause + theory::TheoryId theory_id = currentStep->getTheory(); + Debug("pf::tp") << "Get theory lemma from " << theory_id << "..." << std::endl; + + std::set<Node> missingAssertions = recipe.getMissingAssertionsForStep(i); + if (!missingAssertions.empty()) { + Debug("pf::tp") << "Have missing assertions for this step!" << std::endl; + } + + // Turn rewrite filter ON + std::set<Node>::const_iterator missingAssertion; + for (missingAssertion = missingAssertions.begin(); + missingAssertion != missingAssertions.end(); + ++missingAssertion) { + + Debug("pf::tp") << "Working on missing assertion: " << *missingAssertion << std::endl; + + Assert(recipe.wasRewritten(missingAssertion->negate())); + Node explanation = recipe.getExplanation(missingAssertion->negate()).negate(); + + Debug("pf::tp") << "Found explanation: " << explanation << std::endl; + + // We have a missing assertion. + // rewriteIt->first is the assertion after the rewrite (the explanation), + // rewriteIt->second is the original assertion that needs to be fed into the theory. + + bool found = false; + unsigned k; + for (k = 0; k < currentClauseExpr.size(); ++k) { + if (currentClauseExpr[k] == explanation.toExpr()) { + found = true; + break; + } + } + + AlwaysAssert(found); + + Debug("pf::tp") << "Replacing theory assertion " + << currentClauseExpr[k] + << " with " + << *missingAssertion + << std::endl; + + currentClauseExpr[k] = missingAssertion->toExpr(); + + std::ostringstream rewritten; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << pm->getLitName(explanation); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << d_assertionToRewrite[missingAssertion->negate()]; + rewritten << "))"; + + Debug("pf::tp") << "Setting a rewrite filter for this proof: " << std::endl + << pm->getLitName(*missingAssertion) << " --> " << rewritten.str() + << std::endl << std::endl; + + pm->addRewriteFilter(pm->getLitName(*missingAssertion), rewritten.str()); + } + + getTheoryProof(theory_id)->printTheoryLemmaProof(currentClauseExpr, os, paren, map); + + // Turn rewrite filter OFF + pm->clearRewriteFilters(); + + Debug("pf::tp") << "Get theory lemma from " << theory_id << "... DONE!" << std::endl; + os << clause_paren.str(); + os << "( \\ " << pm->getLemmaClauseName(id) << "s" << i <<"\n"; + paren << "))"; + } + + Assert(numberOfSteps >= 2); + + os << "(satlem_simplify _ _ _ "; + for (unsigned i = 0; i < numberOfSteps - 1; ++i) { + // Resolve step i with step i + 1 + if (recipe.getStep(i)->getLiteral().getKind() == kind::NOT) { + os << "(Q _ _ "; + } else { + os << "(R _ _ "; + } + + os << pm->getLemmaClauseName(id) << "s" << i; + os << " "; + } + + os << pm->getLemmaClauseName(id) << "s" << numberOfSteps - 1 << " "; + + prop::SatLiteral v; + for (int i = numberOfSteps - 2; i >= 0; --i) { + v = ProofManager::currentPM()->getCnfProof()->getLiteral(recipe.getStep(i)->getLiteral()); + os << ProofManager::getVarName(v.getSatVariable(), "") << ") "; + } + + os << "( \\ " << pm->getLemmaClauseName(id) << "\n"; + paren << "))"; + } } } -void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const LetMap& map) { - // Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; +void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const ProofLetMap& map) { + Debug("pf::tp") << "LFSCTheoryProofEngine::printBoundTerm( " << term << " ) " << std::endl; - LetMap::const_iterator it = map.find(term); + ProofLetMap::const_iterator it = map.find(term); if (it != map.end()) { unsigned id = it->second.id; unsigned count = it->second.count; + if (count > LET_COUNT) { - os <<"let"<<id; + os << "let" << id; return; } } @@ -496,7 +813,7 @@ void LFSCTheoryProofEngine::printBoundTerm(Expr term, std::ostream& os, const Le printTheoryTerm(term, os, map); } -void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const ProofLetMap& map) { if (term.isVariable()) { os << ProofManager::sanitize(term); return; @@ -596,20 +913,25 @@ void LFSCTheoryProofEngine::printCoreTerm(Expr term, std::ostream& os, const Let } -void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { - //default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory - Assert( d_theory!=NULL ); +void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, + std::ostream& os, + std::ostream& paren, + const ProofLetMap& map) { + // Default method for replaying proofs: assert (negated) literals back to a fresh copy of the theory + Assert(d_theory!=NULL); + context::UserContext fakeContext; ProofOutputChannel oc; theory::Valuation v(NULL); //make new copy of theory theory::Theory* th; - Trace("theory-proof-debug") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; - if(d_theory->getId()==theory::THEORY_UF) { + Trace("pf::tp") << ";; Print theory lemma proof, theory id = " << d_theory->getId() << std::endl; + + if (d_theory->getId()==theory::THEORY_UF) { th = new theory::uf::TheoryUF(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); - } else if(d_theory->getId()==theory::THEORY_ARRAY) { + } else if (d_theory->getId()==theory::THEORY_ARRAY) { th = new theory::arrays::TheoryArrays(&fakeContext, &fakeContext, oc, v, ProofManager::currentPM()->getLogicInfo(), "replay::"); @@ -626,11 +948,15 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - th->ProduceProofs() DONE" << std::endl; MyPreRegisterVisitor preRegVisitor(th); - for( unsigned i=0; i<lemma.size(); i++ ){ - Node lit = Node::fromExpr( lemma[i] ).negate(); - Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; - NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit); - th->assertFact(lit, false); + for (unsigned i=0; i<lemma.size(); i++) { + Node strippedLit = (lemma[i].getKind() == kind::NOT) ? lemma[i][0] : lemma[i]; + if (strippedLit.getKind() == kind::EQUAL || + d_theory->getId() == theory::Theory::theoryOf(strippedLit)) { + Node lit = Node::fromExpr( lemma[i] ).negate(); + Trace("pf::tp") << "; preregistering and asserting " << lit << std::endl; + NodeVisitor<MyPreRegisterVisitor>::run(preRegVisitor, lit); + th->assertFact(lit, false); + } } Debug("pf::tp") << "TheoryProof::printTheoryLemmaProof - calling th->check()" << std::endl; @@ -679,7 +1005,7 @@ void TheoryProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& th->check(theory::Theory::EFFORT_FULL); } Debug("pf::tp") << "Calling oc.d_proof->toStream(os)" << std::endl; - oc.d_proof->toStream(os); + oc.d_proof->toStream(os, map); Debug("pf::tp") << "Calling oc.d_proof->toStream(os) -- DONE!" << std::endl; Debug("pf::tp") << "About to delete the theory solver used for proving the lemma... " << std::endl; @@ -711,10 +1037,13 @@ void BooleanProof::registerTerm(Expr term) { } } -void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& map) { +void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap& map) { Assert (term.getType().isBoolean()); if (term.isVariable()) { - os << "(p_app " << ProofManager::sanitize(term) <<")"; + if (d_treatBoolsAsFormulas) + os << "(p_app " << ProofManager::sanitize(term) <<")"; + else + os << ProofManager::sanitize(term); return; } @@ -722,6 +1051,32 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& switch(k) { case kind::OR: case kind::AND: + if (options::lfscLetification() && term.getNumChildren() > 2) { + // If letification is on, the entire term is probably a let expression. + // However, we need to transform it from (and a b c) into (and a (and b c)) form first. + Node currentExpression = term[term.getNumChildren() - 1]; + for (int i = term.getNumChildren() - 2; i >= 0; --i) { + NodeBuilder<> builder(k); + builder << term[i]; + builder << currentExpression.toExpr(); + currentExpression = builder; + } + + // The let map should already have the current expression. + ProofLetMap::const_iterator it = map.find(term); + if (it != map.end()) { + unsigned id = it->second.id; + unsigned count = it->second.count; + + if (count > LET_COUNT) { + os << "let" << id; + break; + } + } + } + + // If letification is off or there were 2 children, same treatment as the other cases. + // (No break is intentional). case kind::XOR: case kind::IFF: case kind::IMPLIES: @@ -753,7 +1108,10 @@ void LFSCBooleanProof::printOwnedTerm(Expr term, std::ostream& os, const LetMap& return; case kind::CONST_BOOLEAN: - os << (term.getConst<bool>() ? "true" : "false"); + if (d_treatBoolsAsFormulas) + os << (term.getConst<bool>() ? "true" : "false"); + else + os << (term.getConst<bool>() ? "t_true" : "t_false"); return; default: @@ -786,10 +1144,36 @@ void LFSCBooleanProof::printDeferredDeclarations(std::ostream& os, std::ostream& // Nothing to do here at this point. } +void LFSCBooleanProof::printAliasingDeclarations(std::ostream& os, std::ostream& paren) { + // Nothing to do here at this point. +} + void LFSCBooleanProof::printTheoryLemmaProof(std::vector<Expr>& lemma, std::ostream& os, std::ostream& paren) { Unreachable("No boolean lemmas yet!"); } +void TheoryProof::printConstantDisequalityProof(std::ostream& os, Expr c1, Expr c2) { + // By default, we just print a trust statement. Specific theories can implement + // better proofs. + ProofLetMap emptyMap; + + os << "(trust_f (not (= _ "; + d_proofEngine->printBoundTerm(c1, os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(c2, os, emptyMap); + os << ")))"; +} + +void TheoryProof::printRewriteProof(std::ostream& os, const Node &n1, const Node &n2) { + // This is the default for a rewrite proof: just a trust statement. + ProofLetMap emptyMap; + os << "(trust_f (iff "; + d_proofEngine->printBoundTerm(n1.toExpr(), os, emptyMap); + os << " "; + d_proofEngine->printBoundTerm(n2.toExpr(), os, emptyMap); + os << "))"; +} + } /* namespace CVC4 */ |