fixed uf proof bug: now storing deleted theory lemmas

diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index e8c63bb7424e72d378016d741724329bbe70423f..e1534a635b4d16d5822deed773c9e640127b1ec5 100644 (file)
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -621,32 +621,20 @@ void SatProof::markDeleted(CRef clause) {
   if (d_clauseId.find(clause) != d_clauseId.end()) {
     ClauseId id = getClauseId(clause);
     Assert (d_deleted.find(id) == d_deleted.end()); 
-    d_deleted.insert(id); 
+    d_deleted.insert(id);
+    if (isLemmaClause(id)) {
+      const Clause& minisat_cl = getClause(clause);
+      SatClause* sat_cl = new SatClause(); 
+      MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);  
+      d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); 
+    }
   }
 }
 
 void SatProof::constructProof() {
-  // if (isLemmaClause(d_conflictId)) {
-  //   addClauseToCnfProof(d_emptyClauseId, THEORY_LEMMA);
-  // }
-  // if (isInputClause(d_emptyClauseId)) {
-  //   addClauseToCnfProof(d_emptyClauseId, INPUT); 
-  // }
   collectClauses(d_emptyClauseId); 
 }
 
-// std::string SatProof::varName(::Minisat::Lit lit) {
-//   ostringstream os;
-//   if (sign(lit)) {
-//     os << "(neg "<< ProofManager::getVarPrefix() <<var(lit) << ")" ; 
-//   }
-//   else {
-//     os << "(pos "<< ProofManager::getVarPrefix() <<var(lit) << ")"; 
-//   }
-//   return os.str(); 
-// }
-
-
 std::string SatProof::clauseName(ClauseId id) {
   ostringstream os;
   if (isInputClause(id)) {
@@ -671,6 +659,14 @@ void SatProof::addClauseToCnfProof(ClauseId id, ClauseKind kind) {
     getCnfProof()->addClause(id, clause, kind); 
     return; 
   }
+  
+  if (isDeleted(id)) {
+    Assert (kind == THEORY_LEMMA);
+    SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
+    getCnfProof()->addClause(id, clause, kind);  
+    return; 
+  }
+  
   CRef ref = getClauseRef(id);
   const Clause& minisat_cl = getClause(ref);
   SatClause* clause = new SatClause();
@@ -748,54 +744,6 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   paren << "))";                            // closing parethesis for lemma binding and satlem
 }
 
-
-// void LFSCSatProof::printInputClause(ClauseId id) {
-//   if (isUnit(id)) {
-//     ::Minisat::Lit lit = getUnit(id); 
-//     d_clauseSS << "(% " << clauseName(id) << " (holds (clc ";
-//     d_clauseSS << varName(lit) << "cln ))";
-//     d_paren << ")";
-//     return; 
-//   }
-  
-//   ostringstream os;
-//   CRef ref = getClauseRef(id);
-//   Assert (ref != CRef_Undef);
-//   Clause& c = getClause(ref);
-
-//   d_clauseSS << "(% " << clauseName(id) << " (holds ";
-//   os << ")"; // closing paren for holds
-//   d_paren << ")"; // closing paren for (%
-
-//   for(int i = 0; i < c.size(); i++) {
-//     d_clauseSS << " (clc " << varName(c[i]) <<" ";
-//     os <<")";
-//     d_seenVars.insert(var(c[i])); 
-//   }
-//   d_clauseSS << "cln";
-//   d_clauseSS << os.str() << "\n";  
-// } 
-
-
-// void LFSCSatProof::printInputClauses() {
-//   for (IdHashSet::iterator it = d_seenInput.begin(); it!= d_seenInput.end(); ++it) {
-//     printInputClause(*it);
-//   }
-// }
-
-
-// void LFSCSatProof::flush(std::ostream& out) {
-//   out << "(check \n";
-//   d_paren <<")"; 
-//   out << d_varSS.str();
-//   out << d_clauseSS.str();
-//   out << "(: (holds cln) \n"; 
-//   out << d_learntSS.str(); 
-//   d_paren << "))";
-//   out << d_paren.str();
-//   out << "\n";
-// }
-
 void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
   for(IdSet::iterator it = d_seenLearnt.begin(); it!= d_seenLearnt.end(); ++it) {
     if(*it != d_emptyClauseId) {
@@ -805,13 +753,6 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
   printResolution(d_emptyClauseId, out, paren);
 }
 
-// void LFSCSatProof::printVariables(std::ostream& out, std::ostream& paren) {
-//   for (VarSet::iterator it = d_seenVars.begin(); it != d_seenVars.end(); ++it) {
-//     out << "(% " << ProofManager::getVarPrefix() << *it <<" var \n";
-//     paren << ")"; 
-//   }
-// }
-
 
 } /* CVC4 namespace */
 

diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 5a1fa468064d2bb1c4b0a1aea7c1096ab4bb4764..c4936fd88fb4a4ada57457ee8ce51cbedf55f25f 100644 (file)
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -81,14 +81,14 @@ public:
   LitSet*   getRedundant() { return d_redundantLits; }
 };/* class ResChain */
 
-typedef std::hash_map < ClauseId, ::Minisat::CRef > IdClauseMap;
+typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap;
 typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
 typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
 typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME 
 typedef std::hash_map < ClauseId, ResChain*>      IdResMap; 
 typedef std::hash_set < ClauseId >                IdHashSet;
 typedef std::vector   < ResChain* >               ResStack; 
-
+typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;             
 typedef std::set < ClauseId >                     IdSet; 
 typedef std::vector < ::Minisat::Lit >              LitVector; 
 typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
@@ -116,11 +116,12 @@ class SatProof {
 protected:
   ::Minisat::Solver*    d_solver;
   // clauses 
-  IdClauseMap         d_idClause;
+  IdCRefMap           d_idClause;
   ClauseIdMap         d_clauseId;
   IdUnitMap           d_idUnit;
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
+  IdToSatClause       d_deletedTheoryLemmas; 
   IdHashSet           d_inputClauses; 
   IdHashSet           d_lemmaClauses; 
   // resolutions 
@@ -136,7 +137,7 @@ protected:
   
   // temporary map for updating CRefs
   ClauseIdMap         d_temp_clauseId;
-  IdClauseMap         d_temp_idClause;
+  IdCRefMap         d_temp_idClause;
 
   // unit conflict
   ClauseId d_unitConflictId;
@@ -223,6 +224,7 @@ public:
    * @param clause 
    */
   void markDeleted(::Minisat::CRef clause);
+  bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
   /** 
    * Constructs the resolution of ~q and resolves it with the current
    * resolution thus eliminating q from the current clause

diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index ecd9f9810a7825ebb76d89026a9171df5c5a7d03..5b5a2ae1505af23ad14203f51b878dd522a7c744 100644 (file)
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -65,19 +65,17 @@ void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
     os << term; 
     return;
   }
-  std::ostringstream paren; 
+
   Assert (term.getKind() == kind::APPLY_UF);
   Expr func = term.getOperator();
-  os << "(apply _ _ " << func << " ";
+  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+    os<< "(apply _ _ ";
+  }
+  os << func << " "; 
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
     printTerm(term[i], os);
-    if (i < term.getNumChildren() - 1) {
-      os << "(apply _ _ " << func << " ";
-      paren << ")"; 
-    }
-    os << ")" ; 
+    os << ")"; 
   }
-  os << paren.str(); 
 }
 
 std::string toLFSCKind(Kind kind) {
@@ -95,7 +93,7 @@ std::string toLFSCKind(Kind kind) {
 
 void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
   // should make this more general and overall sane
-  Assert (atom.getType().isBoolean());
+  Assert (atom.getType().isBoolean() && "Only printing booleans." );
   Kind kind = atom.getKind(); 
   // this is the only predicate we have
   if (kind == kind::EQUAL) {
@@ -106,6 +104,13 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
     os <<" "; 
     printTerm(atom[1], os);
     os <<")"; 
+  } else if ( kind == kind::DISTINCT) {
+    os <<"(not (= ";
+    os << atom[0].getType() <<" "; 
+    printTerm(atom[0], os);
+    os <<" "; 
+    printTerm(atom[1], os);
+    os <<"))"; 
   } else if ( kind == kind::OR ||
               kind == kind::AND ||
               kind == kind::XOR ||
@@ -134,8 +139,15 @@ void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
       }
       os <<")"; 
     }
-  } else {
-    Assert (false); 
+  } else if (kind == kind::CONST_BOOLEAN) {
+    if (atom.getConst<bool>())
+      os << "true";
+    else
+      os << "false"; 
+  }
+  else {
+    std::cout << kind << "\n"; 
+    Assert (false && "Unsupported kind"); 
   }
 }
 

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 45127a182cc1e5d186e7575e8cf59076d6960861..16fa3ba600421988024632e805c1c93c27373e1d 100644 (file)
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -369,9 +369,8 @@ void Solver::attachClause(CRef cr) {
 
 
 void Solver::detachClause(CRef cr, bool strict) {
-    PROOF( ProofManager::getSatProof()->markDeleted(cr); ) 
-
     const Clause& c = ca[cr];
+    PROOF( ProofManager::getSatProof()->markDeleted(cr); ) 
     Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
 

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5a3334d647f7d56d981be54ec66738344bb349d7..160a16652a8d049d4cdd389f4eb4d4550da968f6 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3105,11 +3105,11 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
 
 Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
-  // PROOF (
-  ProofManager* pm = ProofManager::currentPM();
-  TheoryProof* pf = pm->getTheoryProof();
-  pf->assertFormula(ex);
-         //  ); 
+#ifdef CVC4_PROOF
+  //  if (options::proof()) { <-- SEGFAULT!!
+    ProofManager::currentPM()->getTheoryProof()->assertFormula(ex);
+  //}
+#endif  
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
@@ -3253,8 +3253,11 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
 Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
-  //PROOF (
-  ProofManager::currentPM()->getTheoryProof()->assertFormula(ex); //); 
+#ifdef CVC4_PROOF
+  // if (options::proof()) { <-- SEGFAULT!!!
+    ProofManager::currentPM()->getTheoryProof()->assertFormula(ex);
+  // }
+#endif
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();