diff options
| author | guykatzz <katz911@gmail.com> | 2017-03-09 12:13:12 -0800 |
|---|---|---|
| committer | guykatzz <katz911@gmail.com> | 2017-03-09 12:14:15 -0800 |
| commit | 2f287a59e9c775d9087cddd8c72be5169c2706e1 (patch) | |
| tree | 95a6664e3b013929d9190cff2d1889045e1a2af2 /src/proof/proof_manager.cpp | |
| parent | ab68adfc44049598ee79a3c8b4379694d786d9aa (diff) | |
better proof support for bools and formulas
Diffstat (limited to 'src/proof/proof_manager.cpp')
| -rw-r--r-- | src/proof/proof_manager.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp index 5ce615366..ddd2029fb 100644 --- a/src/proof/proof_manager.cpp +++ b/src/proof/proof_manager.cpp @@ -565,6 +565,7 @@ void LFSCProof::toStream(std::ostream& out) { Debug("pf::pm") << "\t assertion = " << *it3 << std::endl; std::set<Node> atoms; + NodePairSet rewrites; // collects the atoms in the clauses d_cnfProof->collectAtomsAndRewritesForLemmas(used_lemmas, atoms, rewrites); @@ -779,7 +780,9 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions, //TODO os << "(trust_f "; + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << "(p_app "; ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap); + if (ProofManager::currentPM()->getTheoryProofEngine()->printsAsBool(*it)) os << ")"; os << ") "; os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n"; |