carefully printing trusted assertions in proofs (#2505)

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index cc5332cfde6a527eb421ae884d068bcb49cbf3d0..e7b00068af7fd154e6947630974d5a535b9aff41 100644 (file)
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -808,8 +808,7 @@ void LFSCProof::printPreprocessedAssertions(const NodeSet& assertions,
 
         ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm(inputAssertion, os, globalLetMap);
         os << " ";
-        ProofManager::currentPM()->getTheoryProofEngine()->printTheoryTerm((*it).toExpr(), os, globalLetMap);
-
+        ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap);
         os << "))";
         os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
         paren << "))";
@@ -832,9 +831,7 @@ 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 << ")";
+      ProofManager::currentPM()->printTrustedTerm(*it, os, globalLetMap);
       os << ") ";
 
       os << "(\\ "<< ProofManager::getPreprocessedAssertionName(*it, "") << "\n";
@@ -1063,5 +1060,13 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
 void ProofManager::ensureLiteral(Node node) {
   d_cnfProof->ensureLiteral(node);
 }
-
+void ProofManager::printTrustedTerm(Node term,
+                                    std::ostream& os,
+                                    ProofLetMap& globalLetMap)
+{
+  TheoryProofEngine* tpe = ProofManager::currentPM()->getTheoryProofEngine();
+  if (tpe->printsAsBool(term)) os << "(p_app ";
+  tpe->printTheoryTerm(term.toExpr(), os, globalLetMap);
+  if (tpe->printsAsBool(term)) os << ")";
+}
 } /* CVC4  namespace */

diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 89aa66c2d2eea3b3d429954fb78a726c712532f1..0342288fe92df592a02019f3a05ebdf39a26b31f 100644 (file)
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -239,6 +239,12 @@ public:
   // for SMT variable names that have spaces and other things
   static std::string sanitize(TNode var);
 
+  // wrap term with (p_app ... ) if the term is printed as a boolean, and print
+  // used for "trust" assertions
+  static void printTrustedTerm(Node term,
+                               std::ostream& os,
+                               ProofLetMap& globalLetMap);
+
   /** Add proof assertion - unlike addCoreAssertion this is post definition expansion **/
   void addAssertion(Expr formula);