diff options
author | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-01 17:46:24 -0700 |
commit | 4dac1ec234ee0d0885f058b4b35a7eeba2ca5007 (patch) | |
tree | aae1792c05c0a67c521160226deb451ca861822c /src/proof/proof_manager.cpp | |
parent | de0dd1dc966b05467f1a5443ff33094262f5076a (diff) |
Merge from proof branch
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 91 |
1 files changed, 62 insertions, 29 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index a3689d746..5ce8b523f 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -200,7 +200,6 @@ std::string ProofManager::getLitName(prop::SatLiteral lit, return append(prefix+".l", lit.toInt()); } - std::string ProofManager::getPreprocessedAssertionName(Node node, const std::string& prefix) { node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; @@ -217,9 +216,15 @@ std::string ProofManager::getAtomName(TNode atom, Assert(!lit.isNegated()); return getAtomName(lit.getSatVariable(), prefix); } + std::string ProofManager::getLitName(TNode lit, const std::string& prefix) { - return getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit), prefix); + if (currentPM()->d_rewriteFilters.find(litName) != currentPM()->d_rewriteFilters.end()) { + return currentPM()->d_rewriteFilters[litName]; + } + + return litName; } std::string ProofManager::sanitize(TNode node) { @@ -331,6 +336,9 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, {} void LFSCProof::toStream(std::ostream& out) { + + Assert(options::bitblastMode() != theory::bv::BITBLAST_MODE_EAGER); + d_satProof->constructProof(); // collecting leaf clauses in resolution proof @@ -384,8 +392,37 @@ void LFSCProof::toStream(std::ostream& out) { for (it3 = used_assertions.begin(); it3 != used_assertions.end(); ++it3) Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; - NodeSet atoms; + std::set<Node> atoms; + 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; + } + 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. + } + } + } + d_cnfProof->collectAtomsForClauses(used_inputs, atoms); d_cnfProof->collectAtomsForClauses(used_lemmas, atoms); @@ -393,38 +430,23 @@ void LFSCProof::toStream(std::ostream& out) { for (NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { utils::collectAtoms(*it, atoms); + // utils::collectAtoms(*it, newAtoms); } - NodeSet::iterator atomIt; - Debug("pf::pm") << std::endl << "Dumping atoms from lemmas, inputs and assertions: " << std::endl << 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; - - if (Debug.isOn("proof:pm")) { - // std::cout << NodeManager::currentNM(); - Debug("proof:pm") << "LFSCProof::Used assertions: "<< std::endl; - for(NodeSet::const_iterator it = used_assertions.begin(); it != used_assertions.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - - Debug("proof:pm") << "LFSCProof::Used atoms: "<< std::endl; - for(NodeSet::const_iterator it = atoms.begin(); it != atoms.end(); ++it) { - Debug("proof:pm") << " " << *it << std::endl; - } - } } - smt::SmtScope scope(d_smtEngine); std::ostringstream paren; out << "(check\n"; out << " ;; Declarations\n"; // declare the theory atoms - NodeSet::const_iterator it = atoms.begin(); - NodeSet::const_iterator end = atoms.end(); - Debug("pf::pm") << "LFSCProof::toStream: registering terms:" << std::endl; - for(; it != end; ++it) { + for(it = atoms.begin(); it != atoms.end(); ++it) { Debug("pf::pm") << "\tTerm: " << (*it).toExpr() << std::endl; d_theoryProof->registerTerm((*it).toExpr()); } @@ -444,9 +466,15 @@ void LFSCProof::toStream(std::ostream& out) { out << "(: (holds cln)\n\n"; // Have the theory proofs print deferred declarations, e.g. for skolem variables. - out << " ;; Printing deferred declarations \n"; + out << " ;; Printing deferred declarations \n\n"; d_theoryProof->printDeferredDeclarations(out, paren); + out << " ;; Printing aliasing declarations \n\n"; + d_theoryProof->printAliasingDeclarations(out, paren); + + out << " ;; Rewrites for Lemmas \n"; + d_theoryProof->printLemmaRewrites(rewrites, out, paren); + // print trust that input assertions are their preprocessed form printPreprocessedAssertions(used_assertions, out, paren); @@ -464,10 +492,6 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << std::endl << "Printing cnf proof for clauses DONE" << std::endl; - // FIXME: for now assume all theory lemmas are in CNF form so - // distinguish between them and inputs - // print theory lemmas for resolution proof - Debug("pf::pm") << "Proof manager: printing theory lemmas" << std::endl; d_theoryProof->printTheoryLemmas(used_lemmas, out, paren); Debug("pf::pm") << "Proof manager: printing theory lemmas DONE!" << std::endl; @@ -496,6 +520,8 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, NodeSet::const_iterator it = assertions.begin(); NodeSet::const_iterator end = assertions.end(); + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl; + for (; it != end; ++it) { os << "(th_let_pf _ "; @@ -506,7 +532,6 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; paren << "))"; - } os << "\n"; @@ -568,6 +593,14 @@ void ProofManager::markPrinted(const Type& type) { d_printedTypes.insert(type); } +void ProofManager::addRewriteFilter(const std::string &original, const std::string &substitute) { + d_rewriteFilters[original] = substitute; +} + +void ProofManager::clearRewriteFilters() { + d_rewriteFilters.clear(); +} + std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k) { switch(k) { case RULE_GIVEN: |