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

1 files changed, 97 insertions, 22 deletions

diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 680e57d39..0cca16574 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -23,6 +23,15 @@
 #include "util/cvc4_assert.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/output_channel.h"
+#include "theory/valuation.h"
+#include "util/node_visitor.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/arrays/theory_arrays.h"
+#include "context/context.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -37,7 +46,8 @@ ProofManager::ProofManager(ProofFormat format):
   d_cnfProof(NULL),
   d_theoryProof(NULL),
   d_fullProof(NULL),
-  d_format(format)
+  d_format(format),
+  d_deps()
 {
 }
 
@@ -53,7 +63,7 @@ ProofManager::~ProofManager() {
     delete it->second;
   }
 
-  for(IdToClause::iterator it = d_theoryLemmas.begin();
+  for(OrderedIdToClause::iterator it = d_theoryLemmas.begin();
       it != d_theoryLemmas.end();
       ++it) {
     delete it->second;
@@ -91,11 +101,10 @@ CnfProof* ProofManager::getCnfProof() {
 }
 
 TheoryProof* ProofManager::getTheoryProof() {
-  Assert (currentPM()->d_theoryProof);
+  //Assert (currentPM()->d_theoryProof);
   return currentPM()->d_theoryProof;
 }
 
-
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
@@ -114,35 +123,101 @@ void ProofManager::initTheoryProof() {
   currentPM()->d_theoryProof = new LFSCTheoryProof();
 }
 
-
-std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); }
-std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); }
+std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); }
 std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); }
-std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); }
-std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); }
-std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); }
+std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); }
+std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); }
+
+std::string ProofManager::getAtomName(TNode atom) {
+  prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
+  Assert(!lit.isNegated());
+  return getAtomName(lit.getSatVariable());
+}
+std::string ProofManager::getLitName(TNode lit) {
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+}
+
+void ProofManager::traceDeps(TNode n) {
+  Debug("cores") << "trace deps " << n << std::endl;
+  if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+    // originating formula was in core set
+    Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
+    d_outputCoreFormulas.insert(n.toExpr());
+  } else {
+    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
+    if(d_deps.find(n) == d_deps.end()) {
+      InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+    }
+    Assert(d_deps.find(n) != d_deps.end());
+    std::vector<Node> deps = (*d_deps.find(n)).second;
+    for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
+      Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
+      traceDeps(*i);
+    }
+  }
+}
 
 void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
-  for (unsigned i = 0; i < clause->size(); ++i) {
+  /*for (unsigned i = 0; i < clause->size(); ++i) {
     prop::SatLiteral lit = clause->operator[](i);
     d_propVars.insert(lit.getSatVariable());
-  }
+  }*/
   if (kind == INPUT) {
     d_inputClauses.insert(std::make_pair(id, clause));
-    return;
+    Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
+    Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl;
+    if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
+      Debug("cores") << " + constant unit (true or false)" << std::endl;
+    } else if(options::unsatCores()) {
+      Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
+      Debug("cores") << "core input assertion from CnfStream is " << e << std::endl;
+      Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl;
+      // Invalid proof rules are currently used for parts of CVC4 that don't
+      // support proofs (these are e.g. unproven theory lemmas) or don't need
+      // proofs (e.g. split lemmas).  We can ignore these safely when
+      // constructing unsat cores.
+      if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) {
+        // trace dependences back to actual assertions
+        traceDeps(Node::fromExpr(e));
+      }
+    }
+  } else {
+    Assert(kind == THEORY_LEMMA);
+    d_theoryLemmas.insert(std::make_pair(id, clause));
   }
-  Assert (kind == THEORY_LEMMA);
-  d_theoryLemmas.insert(std::make_pair(id, clause));
 }
 
-void ProofManager::addAssertion(Expr formula) {
+void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
+  Debug("cores") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
+  d_deps[Node::fromExpr(formula)]; // empty vector of deps
+  if(inUnsatCore || options::dumpUnsatCores()) {
+    Debug("cores") << "adding to input core forms: " << formula << std::endl;
+    d_inputCoreFormulas.insert(formula);
+  }
 }
 
-void ProofManager::setLogic(const std::string& logic_string) {
-  d_logic = logic_string;
+void ProofManager::addDependence(TNode n, TNode dep) {
+  if(dep != n) {
+    Debug("cores") << "dep: " << n << " : " << dep << std::endl;
+    if(d_deps.find(dep) == d_deps.end()) {
+      Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
+    }
+    //Assert(d_deps.find(dep) != d_deps.end());
+    d_deps[n].push_back(dep);
+  }
+}
+
+void ProofManager::setLogic(const LogicInfo& logic) {
+  d_logic = logic;
 }
 
+void ProofManager::printProof(std::ostream& os, TNode n) {
+  // no proofs here yet
+}
 
 LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
@@ -157,17 +232,18 @@ void LFSCProof::toStream(std::ostream& out) {
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check\n";
+  out << " ;; Declarations\n";
   if (d_theoryProof == NULL) {
     d_theoryProof = new LFSCTheoryProof();
   }
-  for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
+  /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
       i != d_cnfProof->end_atom_mapping();
       ++i) {
     d_theoryProof->addDeclaration(*i);
-  }
+  }*/
   d_theoryProof->printAssertions(out, paren);
+  out << " ;; Proof of empty clause follows\n";
   out << "(: (holds cln)\n";
-  d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
   d_satProof->printResolutions(out, paren);
   paren <<")))\n;;";
@@ -175,5 +251,4 @@ void LFSCProof::toStream(std::ostream& out) {
   out << "\n";
 }
 
-
 } /* CVC4  namespace */