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/cnf_proof.cpp | |
| parent | ab68adfc44049598ee79a3c8b4379694d786d9aa (diff) | |
better proof support for bools and formulas
Diffstat (limited to 'src/proof/cnf_proof.cpp')
| -rw-r--r-- | src/proof/cnf_proof.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp index 69b613f28..d1a228ecb 100644 --- a/src/proof/cnf_proof.cpp +++ b/src/proof/cnf_proof.cpp @@ -350,8 +350,9 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms, prop::SatVariable var = getLiteral(atom).getSatVariable(); //FIXME hideous LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine(); - // pe->printLetTerm(atom.toExpr(), os); + if (pe->printsAsBool(atom.toExpr())) os << "(p_app "; pe->printBoundTerm(atom.toExpr(), os, letMap); + if (pe->printsAsBool(atom.toExpr())) os << ")"; os << " (\\ " << ProofManager::getVarName(var, d_name); os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n"; |