better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes

1 files changed, 13 insertions, 0 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index ddd2029fb..d8eefdcf0 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -243,6 +243,10 @@ std::string ProofManager::getLitName(TNode lit,
   return litName;
 }
 
+bool ProofManager::hasLitName(TNode lit) {
+  return currentPM()->d_cnfProof->hasLiteral(lit);
+}
+
 std::string ProofManager::sanitize(TNode node) {
   Assert (node.isVar() || node.isConst());
 
@@ -875,6 +879,11 @@ void ProofManager::addRewriteFilter(const std::string &original, const std::stri
   d_rewriteFilters[original] = substitute;
 }
 
+bool ProofManager::haveRewriteFilter(TNode lit) {
+  std::string litName = getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+  return d_rewriteFilters.find(litName) != d_rewriteFilters.end();
+}
+
 void ProofManager::clearRewriteFilters() {
   d_rewriteFilters.clear();
 }
@@ -1002,4 +1011,8 @@ void ProofManager::printGlobalLetMap(std::set<Node>& atoms,
   out << std::endl << std::endl;
 }
 
+void ProofManager::ensureLiteral(Node node) {
+  d_cnfProof->ensureLiteral(node);
+}
+
 } /* CVC4  namespace */