Support for printing a global let map in LFSC proofs.

Added a flag to enable/disbale this feature (enabled by default).

Also, added some infrastructure for proving rewrite rules.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index abe48e3cd..b58ade35e 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -337,6 +337,28 @@ void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
   }
 }
 
+void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
+                                    std::ostream& os,
+                                    std::ostream& paren,
+                                    ProofLetMap &letMap) {
+  std::set<Node>::const_iterator it = atoms.begin();
+  std::set<Node>::const_iterator end = atoms.end();
+
+  for (;it != end; ++it) {
+    os << "(decl_atom ";
+    Node atom = *it;
+    prop::SatVariable var = getLiteral(atom).getSatVariable();
+    //FIXME hideous
+    LFSCTheoryProofEngine* pe = (LFSCTheoryProofEngine*)ProofManager::currentPM()->getTheoryProofEngine();
+    // pe->printLetTerm(atom.toExpr(), os);
+    pe->printBoundTerm(atom.toExpr(), os, letMap);
+
+    os << " (\\ " << ProofManager::getVarName(var, d_name);
+    os << " (\\ " << ProofManager::getAtomName(var, d_name) << "\n";
+    paren << ")))";
+  }
+}
+
 // maps each expr to the position it had in the clause and the polarity it had
 Node LFSCCnfProof::clauseToNode(const prop::SatClause& clause,
                                 std::map<Node, unsigned>& childIndex,