better proof support for bools and formulas

1 files changed, 14 insertions, 7 deletions

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 41262051c..d3da2bcdb 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -701,17 +701,13 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
   Assert (theory::Theory::theoryOf(term) == theory::THEORY_UF);
 
   if (term.getKind() == kind::VARIABLE ||
-      term.getKind() == kind::SKOLEM) {
+      term.getKind() == kind::SKOLEM ||
+      term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
     os << term;
     return;
   }
-  if (term.getKind() == kind::BOOLEAN_TERM_VARIABLE) {
-    os << "(p_app " << term << ")";
-    return;
-  }
 
   Assert (term.getKind() == kind::APPLY_UF);
-  d_proofEngine->treatBoolsAsFormulas(false);
 
   if(term.getType().isBoolean()) {
     os << "(p_app ";
@@ -722,13 +718,15 @@ void LFSCUFProof::printOwnedTerm(Expr term, std::ostream& os, const ProofLetMap&
   }
   os << func << " ";
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    bool convertToBool = (term[i].getType().isBoolean() && !d_proofEngine->printsAsBool(term[i]));
+    if (convertToBool) os << "(f_to_b ";
     d_proofEngine->printBoundTerm(term[i], os, map);
+    if (convertToBool) os << ")";
     os << ")";
   }
   if(term.getType().isBoolean()) {
     os << ")";
   }
-  d_proofEngine->treatBoolsAsFormulas(true);
 }
 
 void LFSCUFProof::printOwnedSort(Type type, std::ostream& os) {
@@ -803,4 +801,13 @@ void LFSCUFProof::printAliasingDeclarations(std::ostream& os, std::ostream& pare
   // Nothing to do here at this point.
 }
 
+bool LFSCUFProof::printsAsBool(const Node &n)
+{
+  Debug("gk::temp") << "\nUF printsAsBool: " << n << std::endl;
+  if (n.getKind() == kind::BOOLEAN_TERM_VARIABLE)
+    return true;
+
+  return false;
+}
+
 } /* namespace CVC4 */