diff options
Diffstat (limited to 'src/proof/proof_manager.cpp')
-rw-r--r-- | src/proof/proof_manager.cpp | 135 |
1 files changed, 123 insertions, 12 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index e987f1c6f..1c9bb0ff0 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -211,6 +211,10 @@ std::string ProofManager::getLitName(prop::SatLiteral lit, std::string ProofManager::getPreprocessedAssertionName(Node node, const std::string& prefix) { + if (currentPM()->d_assertionFilters.find(node) != currentPM()->d_assertionFilters.end()) { + return currentPM()->d_assertionFilters[node]; + } + node = node.getKind() == kind::BITVECTOR_EAGER_ATOM ? node[0] : node; return append(prefix+".PA", node.getId()); } @@ -218,6 +222,9 @@ std::string ProofManager::getAssertionName(Node node, const std::string& prefix) { return append(prefix+".A", node.getId()); } +std::string ProofManager::getInputFormulaName(const Expr& expr) { + return currentPM()->d_inputFormulaToName[expr]; +} std::string ProofManager::getAtomName(TNode atom, const std::string& prefix) { @@ -252,7 +259,7 @@ std::string ProofManager::sanitize(TNode node) { return name; } -void ProofManager::traceDeps(TNode n) { +void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) { Debug("cores") << "trace deps " << n << std::endl; if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) || (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) { @@ -261,7 +268,7 @@ void ProofManager::traceDeps(TNode n) { if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) { // originating formula was in core set Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl; - d_outputCoreFormulas.insert(n.toExpr()); + coreAssertions->insert(n.toExpr()); } else { Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl; if(d_deps.find(n) == d_deps.end()) { @@ -272,7 +279,7 @@ void ProofManager::traceDeps(TNode n) { for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) { Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl; if( !(*i).isNull() ){ - traceDeps(*i); + traceDeps(*i, coreAssertions); } } } @@ -296,7 +303,7 @@ void ProofManager::traceUnsatCore() { rule == RULE_GIVEN) { // trace dependences back to actual assertions // (this adds them to the unsat core) - traceDeps(node); + traceDeps(node, &d_outputCoreFormulas); } } } @@ -444,6 +451,9 @@ Node ProofManager::getWeakestImplicantInUnsatCore(Node lemma) { void ProofManager::addAssertion(Expr formula) { Debug("proof:pm") << "assert: " << formula << std::endl; d_inputFormulas.insert(formula); + std::ostringstream name; + name << "A" << d_inputFormulaToName.size(); + d_inputFormulaToName[formula] = name.str(); } void ProofManager::addCoreAssertion(Expr formula) { @@ -468,6 +478,10 @@ void ProofManager::addUnsatCore(Expr formula) { d_outputCoreFormulas.insert(formula); } +void ProofManager::addAssertionFilter(const Node& node, const std::string& rewritten) { + d_assertionFilters[node] = rewritten; +} + void ProofManager::setLogic(const LogicInfo& logic) { d_logic = logic; } @@ -682,21 +696,118 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions starting" << std::endl; - for (; it != end; ++it) { - os << "(th_let_pf _ "; + if (options::fewerPreprocessingHoles()) { + // Check for assertions that did not get rewritten, and update the printing filter. + checkUnrewrittenAssertion(assertions); + + // For the remaining assertions, bind them to input assertions. + for (; it != end; ++it) { + // Rewrite preprocessing step if it cannot be eliminated + if (!ProofManager::currentPM()->have_input_assertion((*it).toExpr())) { + os << "(th_let_pf _ (trust_f (iff "; + + Expr inputAssertion; + + if (((*it).isConst() && *it == NodeManager::currentNM()->mkConst<bool>(true)) || + ((*it).getKind() == kind::NOT && (*it)[0] == NodeManager::currentNM()->mkConst<bool>(false))) { + inputAssertion = NodeManager::currentNM()->mkConst<bool>(true).toExpr(); + } else { + // Figure out which input assertion led to this assertion + ExprSet inputAssertions; + ProofManager::currentPM()->traceDeps(*it, &inputAssertions); + + Debug("pf::pm") << "Original assertions for " << *it << " are: " << std::endl; + + ProofManager::assertions_iterator assertionIt; + for (assertionIt = inputAssertions.begin(); assertionIt != inputAssertions.end(); ++assertionIt) { + Debug("pf::pm") << "\t" << *assertionIt << std::endl; + } + + if (inputAssertions.size() == 0) { + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl; + // For now just use the first assertion... + inputAssertion = *(ProofManager::currentPM()->begin_assertions()); + } else { + if (inputAssertions.size() != 1) { + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Attention: more than one original assertion was found. Picking just one." << std::endl; + } + inputAssertion = *inputAssertions.begin(); + } + } + + if (!ProofManager::currentPM()->have_input_assertion(inputAssertion)) { + // The thing returned by traceDeps does not appear in the input assertions... + Debug("pf::pm") << "LFSCProof::printPreprocessedAssertions: Count NOT find the assertion that caused this PA. Picking an arbitrary one..." << std::endl; + // For now just use the first assertion... + inputAssertion = *(ProofManager::currentPM()->begin_assertions()); + } + + Debug("pf::pm") << "Original assertion for " << *it + << " is: " + << inputAssertion + << ", AKA " + << ProofManager::currentPM()->getInputFormulaName(inputAssertion) + << std::endl; + + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap); + os << " "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + + os << "))"; + os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; + paren << "))"; - //TODO - os << "(trust_f "; - ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); - os << ") "; + std::ostringstream rewritten; - os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; - paren << "))"; + rewritten << "(or_elim_1 _ _ "; + rewritten << "(not_not_intro _ "; + rewritten << ProofManager::currentPM()->getInputFormulaName(inputAssertion); + rewritten << ") (iff_elim_1 _ _ "; + rewritten << ProofManager::getPreprocessedAssertionName(*it, ""); + rewritten << "))"; + + ProofManager::currentPM()->addAssertionFilter(*it, rewritten.str()); + } + } + } else { + for (; it != end; ++it) { + os << "(th_let_pf _ "; + + //TODO + os << "(trust_f "; + ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + os << ") "; + + os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; + paren << "))"; + } } os << "\n"; } +void LFSCProof::checkUnrewrittenAssertion(const NodeSet& rewrites) { + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion starting" << std::endl; + + NodeSet::const_iterator rewrite; + for (rewrite = rewrites.begin(); rewrite != rewrites.end(); ++rewrite) { + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: handling " << *rewrite << std::endl; + if (ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())) { + Assert(ProofManager::currentPM()->have_input_assertion((*rewrite).toExpr())); + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion was NOT rewritten!" << std::endl + << "\tAdding filter: " + << ProofManager::getPreprocessedAssertionName(*rewrite, "") + << " --> " + << ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr()) + << std::endl; + ProofManager::currentPM()->addAssertionFilter(*rewrite, + ProofManager::currentPM()->getInputFormulaName((*rewrite).toExpr())); + } else { + Debug("pf::pm") << "LFSCProof::checkUnrewrittenAssertion: this assertion WAS rewritten! " << *rewrite << std::endl; + } + } +} + //---from Morgan--- bool ProofManager::hasOp(TNode n) const { |