Unsat core infrastruture and API (SMT-LIB compliance to come).

1 files changed, 93 insertions, 35 deletions

diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 3dfb61428..22a40ff69 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -30,6 +30,8 @@ CnfProof::CnfProof(CnfStream* stream)
   : d_cnfStream(stream)
 {}
 
+CnfProof::~CnfProof() {
+}
 
 Expr CnfProof::getAtom(prop::SatVariable var) {
   prop::SatLiteral lit (var);
@@ -38,34 +40,33 @@ Expr CnfProof::getAtom(prop::SatVariable var) {
   return atom;
 }
 
-CnfProof::~CnfProof() {
-}
-
-LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->begin_vars());
+prop::SatLiteral CnfProof::getLiteral(TNode atom) {
+  return d_cnfStream->getLiteral(atom);
 }
 
-LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->end_vars());
+Expr CnfProof::getAssertion(uint64_t id) {
+  return d_cnfStream->getAssertion(id).toExpr();
 }
 
-void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
-  ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
-  ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
-
-  for (;it != end;  ++it) {
-    os << "(decl_atom ";
-
-    if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
-      Expr atom = getAtom(*it);
-      LFSCTheoryProof::printTerm(atom, os);
-    } else {
-      // print fake atoms for all other logics
-      os << "true ";
+void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) {
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = clause->operator[](i);
+    if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) {
+      d_atomsDeclared.insert(lit.getSatVariable());
+      os << "(decl_atom ";
+      if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) {
+        Expr atom = getAtom(lit.getSatVariable());
+        LFSCTheoryProof::printTerm(atom, os);
+      } else {
+        // print fake atoms for all other logics (for now)
+        os << "true ";
+      }
+
+      os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n";
+      paren << ")))";
     }
-
-    os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
-    paren << ")))";
   }
 }
 
@@ -75,36 +76,93 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
 }
 
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
-  os << " ;; Input Clauses \n";
+  os << " ;; Clauses\n";
   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
   ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
 
   for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
+    os << "(clausify_false trust)" << clause_paren.str()
+       << " (\\ " << ProofManager::getInputClauseName(id) << "\n";
     paren << "))";
   }
 }
 
-
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";
-  ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
-  ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
+  os << " ;; Theory Lemmas\n";
+  ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas();
+  ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas();
+
+  for(size_t n = 0; it != end; ++it, ++n) {
+    if(n % 100 == 0) {
+      Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl;
+    }
 
-  for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    NodeBuilder<> c(kind::AND);
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      prop::SatVariable var = lit.getSatVariable();
+      if(lit.isNegated()) {
+        c << Node::fromExpr(getAtom(var));
+      } else {
+        c << Node::fromExpr(getAtom(var)).notNode();
+      }
+    }
+    Node cl = c;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional lemma!" << std::endl;
+        Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT);
+        TNode myk = cl[0][0][1];
+        Debug("cores") << "; so my skolemized k is " << myk << std::endl;
+        os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n";
+        paren << ")))";
+      }
+    }
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
+
+    Debug("cores") << "\n;id is " << id << std::endl;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl;
+      Assert(int32_t(proof_id & 0xffffffff) != -1);
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl;
+      Debug("cores") << "; that means the lemma was " << orig << std::endl;
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional" << std::endl;
+        os << "(clausify_false trust)\n";
+      } else if(proof_id == 0) {
+        // theory propagation caused conflict
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) {
+        os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else {
+        os << "\n;; need to generate a (lemma) proof of " << cl;
+        os << "\n;; DON'T KNOW HOW !!\n";
+        os << "(clausify_false trust)\n";
+      }
+    } else {
+      os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+      ProofManager::currentPM()->printProof(os, cl);
+    }
+    os << clause_paren.str()
+       << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n";
     paren << "))";
   }
 }
@@ -114,10 +172,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os,
     prop::SatLiteral lit = clause[i];
     prop::SatVariable var = lit.getSatVariable();
     if (lit.isNegated()) {
-      os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     } else {
-      os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     }
   }