now proofs print mapping between atom and propositional variable as a comment in LFSC

5 files changed, 48 insertions, 11 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index d6e493c8d..5f03ef5cf 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -19,8 +19,8 @@
 using namespace CVC4::prop;
 
 namespace CVC4 {
+
 CnfProof::CnfProof(CnfStream* stream) :
   d_cnfStream(stream) {}
 
-
 } /* CVC4 namespace */
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index c265e46df..984dc76c6 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -17,7 +17,7 @@
  **/
 
 #include "cvc4_private.h"
-
+#include "util/proof.h"
 #ifndef __CVC4__CNF_PROOF_H
 #define __CVC4__CNF_PROOF_H
 
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 2c0c7d036..82478464f 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -175,7 +175,8 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_temp_clauseId(),
     d_temp_idClause(),
     d_unitConflictId(),
-    d_storedUnitConflict(false)
+    d_storedUnitConflict(false),
+    d_atomToVar()
   {
     d_proxy = new ProofProxy(this); 
   }
@@ -592,6 +593,14 @@ void SatProof::markDeleted(CRef clause) {
   }
 }
 
+/// store mapping from theory atoms to new variables
+void SatProof::storeAtom(::Minisat::Lit literal, Expr atom) {
+  (d_atomToVar.find(atom) == d_atomToVar.end());
+  d_atomToVar[atom] = literal; 
+}
+
+
+
 /// LFSCSatProof class
 
 std::string LFSCSatProof::varName(::Minisat::Lit lit) {
@@ -720,6 +729,7 @@ void LFSCSatProof::printVariables() {
 
 
 void LFSCSatProof::flush(std::ostream& out) {
+  out << d_atomsSS.str(); 
   out << "(check \n";
   d_paren <<")"; 
   out << d_varSS.str();
@@ -733,7 +743,7 @@ void LFSCSatProof::flush(std::ostream& out) {
 
 void LFSCSatProof::toStream(std::ostream& out) {
   Debug("proof:sat") << " LFSCSatProof::printProof \n";
-
+  
   // first collect lemmas to print in reverse order
   collectLemmas(d_emptyClauseId); 
   for(IdSet::iterator it = d_seenLemmas.begin(); it!= d_seenLemmas.end(); ++it) {
@@ -741,13 +751,22 @@ void LFSCSatProof::toStream(std::ostream& out) {
       printResolution(*it);
     }
   }
+  printAtoms(); 
   // last resolution to be printed is the empty clause
   printResolution(d_emptyClauseId);
-
+  
   printClauses();
   printVariables();
   flush(out);
 }
 
+void LFSCSatProof::printAtoms() {
+  d_atomsSS << "; Mapping between boolean variables and theory atoms \n"; 
+  for (AtomToVar::iterator it = d_atomToVar.begin(); it != d_atomToVar.end(); ++it) {
+    d_atomsSS << "; " << it->first << " => v" << var(it->second) << "\n"; 
+  }
+}
+
+
 } /* CVC4 namespace */
 
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index a552b66fd..fb8966400 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -26,6 +26,8 @@
 #include <ext/hash_map>
 #include <ext/hash_set>
 #include <sstream>
+#include "expr/expr.h"
+
 
 namespace Minisat {
   class Solver;
@@ -90,6 +92,8 @@ typedef std::vector   < ResChain* >               ResStack;
 typedef std::hash_set < int >                     VarSet; 
 typedef std::set < ClauseId >                     IdSet; 
 typedef std::vector < ::Minisat::Lit >              LitVector; 
+typedef __gnu_cxx::hash_map<Expr, ::Minisat::Lit, ExprHashFunction >  AtomToVar; 
+
 class SatProof; 
 
 class ProofProxy : public ProofProxyAbstract {
@@ -128,7 +132,10 @@ protected:
 
   // unit conflict
   ClauseId d_unitConflictId;
-  bool d_storedUnitConflict; 
+  bool d_storedUnitConflict;
+
+  // atom mapping
+  AtomToVar d_atomToVar;
 public:  
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
 protected:
@@ -223,12 +230,20 @@ public:
    */
   void     storeUnitResolution(::Minisat::Lit lit); 
   
-  ProofProxy* getProxy() {return d_proxy; } 
+  ProofProxy* getProxy() {return d_proxy; }
+  /** 
+   * At mapping between literal and theory-atom it represents
+   * 
+   * @param literal 
+   * @param atom 
+   */
+  void storeAtom(::Minisat::Lit literal, Expr atom);
 };/* class SatProof */
 
 class LFSCSatProof: public SatProof {
 private:
-  VarSet             d_seenVars; 
+  VarSet             d_seenVars;
+  std::ostringstream d_atomsSS;
   std::ostringstream d_varSS;
   std::ostringstream d_lemmaSS;
   std::ostringstream d_clauseSS;
@@ -246,11 +261,12 @@ private:
   void printVariables();
   void printClauses();
   void flush(std::ostream& out);
-  
+  void printAtoms(); 
 public:
   LFSCSatProof(::Minisat::Solver* solver, bool checkRes = false):
     SatProof(solver, checkRes),
     d_seenVars(),
+    d_atomsSS(), 
     d_varSS(),
     d_lemmaSS(),
     d_paren(),
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 4be58bdef..8ebb461e5 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -27,7 +27,9 @@
 #include "expr/expr.h"
 #include "prop/theory_proxy.h"
 #include "theory/bv/options.h"
-
+#include "proof/proof_manager.h"
+#include "proof/sat_proof.h"
+#include "prop/minisat/minisat.h"
 #include <queue>
 
 using namespace std;
@@ -236,7 +238,7 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 
   // Make a new literal (variables are not considered theory literals)
   SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
-
+  PROOF (ProofManager::getSatProof()->storeAtom(MinisatSatSolver::toMinisatLit(lit), node.toExpr()); ); 
   // Return the resulting literal
   return lit;
 }