From: guykatzz <katz911@gmail.com>
Date: Thu, 23 Mar 2017 21:13:46 +0000 (-0700)
Subject: support incremental unsat cores
X-Git-Tag: cvc5-1.0.0~5875
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16c0d86ae359fc16064e29ed7545db5896366c9b;p=cvc5.git

support incremental unsat cores
---

diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 926dae9fd..ebe82cd91 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -47,7 +47,7 @@ BitVectorProof::BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proo
 
 void BitVectorProof::initSatProof(CVC4::BVMinisat::Solver* solver) {
   Assert (d_resolutionProof == NULL);
-  d_resolutionProof = new LFSCBVSatProof(solver, "bb", true);
+  d_resolutionProof = new LFSCBVSatProof(solver, &d_fakeContext, "bb", true);
 }
 
 void BitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 6b952e35c..fcd1d2584 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -85,6 +85,7 @@ protected:
   std::map<Expr,std::string> d_constantLetMap;
   bool d_useConstantLetification;
 
+  context::Context d_fakeContext;
 public:
   BitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine);
 
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index d8eefdcf0..cbc7f591a 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -56,17 +56,18 @@ std::string append(const std::string& str, uint64_t num) {
   return os.str();
 }
 
-ProofManager::ProofManager(ProofFormat format):
+ProofManager::ProofManager(context::Context* context, ProofFormat format):
+  d_context(context),
   d_satProof(NULL),
   d_cnfProof(NULL),
   d_theoryProof(NULL),
   d_inputFormulas(),
-  d_inputCoreFormulas(),
-  d_outputCoreFormulas(),
+  d_inputCoreFormulas(context),
+  d_outputCoreFormulas(context),
   d_nextId(0),
   d_fullProof(NULL),
   d_format(format),
-  d_deps()
+  d_deps(context)
 {
 }
 
@@ -141,7 +142,7 @@ SkolemizationManager* ProofManager::getSkolemizationManager() {
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
-  currentPM()->d_satProof = new LFSCCoreSatProof(solver, "");
+  currentPM()->d_satProof = new LFSCCoreSatProof(solver, d_context, "");
 }
 
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream,
@@ -293,13 +294,45 @@ void ProofManager::traceDeps(TNode n, ExprSet* coreAssertions) {
   }
 }
 
+void ProofManager::traceDeps(TNode n, CDExprSet* coreAssertions) {
+  Debug("cores") << "trace deps " << n << std::endl;
+  if ((n.isConst() && n == NodeManager::currentNM()->mkConst<bool>(true)) ||
+      (n.getKind() == kind::NOT && n[0] == NodeManager::currentNM()->mkConst<bool>(false))) {
+    return;
+  }
+  if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+    // originating formula was in core set
+    Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
+    coreAssertions->insert(n.toExpr());
+  } else {
+    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
+    if(d_deps.find(n) == d_deps.end()) {
+      if (options::allowEmptyDependencies()) {
+        Debug("cores") << " -- Could not track cause assertion. Failing silently." << std::endl;
+        return;
+      }
+      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;
+      if( !(*i).isNull() ){
+        traceDeps(*i, coreAssertions);
+      }
+    }
+  }
+}
+
 void ProofManager::traceUnsatCore() {
   Assert (options::unsatCores());
-  constructSatProof();
+  d_satProof->refreshProof();
   IdToSatClause used_lemmas;
   IdToSatClause used_inputs;
   d_satProof->collectClausesUsed(used_inputs,
                                  used_lemmas);
+
   IdToSatClause::const_iterator it = used_inputs.begin();
   for(; it != used_inputs.end(); ++it) {
     Node node = d_cnfProof->getAssertionForClause(it->first);
@@ -320,6 +353,17 @@ bool ProofManager::unsatCoreAvailable() const {
   return d_satProof->derivedEmptyClause();
 }
 
+std::vector<Expr> ProofManager::extractUnsatCore() {
+  std::vector<Expr> result;
+  output_core_iterator it = begin_unsat_core();
+  output_core_iterator end = end_unsat_core();
+  while ( it != end ) {
+    result.push_back(*it);
+    ++it;
+  }
+  return result;
+}
+
 void ProofManager::constructSatProof() {
   if (!d_satProof->proofConstructed()) {
     d_satProof->constructProof();
@@ -476,8 +520,9 @@ void ProofManager::addDependence(TNode n, TNode dep) {
     if( !dep.isNull() && 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);
+    std::vector<Node> deps = d_deps[n].get();
+    deps.push_back(dep);
+    d_deps[n].set(deps);
   }
 }
 
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 19215589f..31638e8ee 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -22,6 +22,8 @@
 #include <iosfwd>
 #include <map>
 #include "expr/node.h"
+#include "context/cdhashset.h"
+#include "context/cdhashmap.h"
 #include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "proof/proof_utils.h"
@@ -95,9 +97,11 @@ enum ProofFormat {
 std::string append(const std::string& str, uint64_t num);
 
 typedef __gnu_cxx::hash_map < ClauseId, prop::SatClause* > IdToSatClause;
-typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
+typedef __gnu_cxx::hash_set<Expr, ExprHashFunction> ExprSet;
+typedef context::CDHashSet<Expr, ExprHashFunction> CDExprSet;
 typedef __gnu_cxx::hash_set<Node, NodeHashFunction > NodeSet;
 typedef __gnu_cxx::hash_map<Node, std::vector<Node>, NodeHashFunction > NodeToNodes;
+typedef context::CDHashMap<Node, std::vector<Node>, NodeHashFunction > CDNodeToNodes;
 typedef std::hash_set<ClauseId> IdHashSet;
 
 enum ProofRule {
@@ -139,6 +143,8 @@ private:
 };
 
 class ProofManager {
+  context::Context* d_context;
+
   CoreSatProof*  d_satProof;
   CnfProof*      d_cnfProof;
   TheoryProofEngine* d_theoryProof;
@@ -146,8 +152,8 @@ class ProofManager {
   // information that will need to be shared across proofs
   ExprSet    d_inputFormulas;
   std::map<Expr, std::string> d_inputFormulaToName;
-  ExprSet    d_inputCoreFormulas;
-  ExprSet    d_outputCoreFormulas;
+  CDExprSet    d_inputCoreFormulas;
+  CDExprSet    d_outputCoreFormulas;
 
   SkolemizationManager d_skolemizationManager;
 
@@ -156,7 +162,7 @@ class ProofManager {
   Proof* d_fullProof;
   ProofFormat d_format; // used for now only in debug builds
 
-  NodeToNodes d_deps;
+  CDNodeToNodes d_deps;
 
   std::set<Type> d_printedTypes;
 
@@ -169,13 +175,13 @@ protected:
   LogicInfo d_logic;
 
 public:
-  ProofManager(ProofFormat format = LFSC);
+  ProofManager(context::Context* context, ProofFormat format = LFSC);
   ~ProofManager();
 
   static ProofManager* currentPM();
 
   // initialization
-  static void         initSatProof(Minisat::Solver* solver);
+  void         initSatProof(Minisat::Solver* solver);
   static void         initCnfProof(CVC4::prop::CnfStream* cnfStream,
                                    context::Context* ctx);
   static void         initTheoryProofEngine();
@@ -248,10 +254,15 @@ public:
 
   // trace dependences back to unsat core
   void traceDeps(TNode n, ExprSet* coreAssertions);
+  void traceDeps(TNode n, CDExprSet* coreAssertions);
   void traceUnsatCore();
-  assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
-  assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
+
+  typedef CDExprSet::const_iterator output_core_iterator;
+
+  output_core_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
+  output_core_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
   size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+  std::vector<Expr> extractUnsatCore();
 
   bool unsatCoreAvailable() const;
   void getLemmasInUnsatCore(theory::TheoryId theory, std::vector<Node> &lemmas);
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 52e059e95..5691d1bd2 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -28,6 +28,7 @@
 #include <sstream>
 #include <vector>
 
+#include "context/cdhashmap.h"
 #include "expr/expr.h"
 #include "proof/clause_id.h"
 #include "proof/proof_manager.h"
@@ -101,9 +102,9 @@ class TSatProof {
   typedef std::set<typename Solver::TVar> VarSet;
   typedef std::hash_map<ClauseId, typename Solver::TCRef> IdCRefMap;
   typedef std::hash_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
-  typedef std::hash_map<ClauseId, typename Solver::TLit> IdUnitMap;
-  typedef std::hash_map<int, ClauseId> UnitIdMap;
-  typedef std::hash_map<ClauseId, ResolutionChain*> IdResMap;
+  typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
+  typedef context::CDHashMap<int, ClauseId> UnitIdMap;
+  typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
   typedef std::hash_map<ClauseId, uint64_t> IdProofRuleMap;
   typedef std::vector<ResolutionChain*> ResStack;
   typedef std::set<ClauseId> IdSet;
@@ -113,7 +114,8 @@ class TSatProof {
   typedef __gnu_cxx::hash_map<ClauseId, LitVector*> IdToConflicts;
 
  public:
-  TSatProof(Solver* solver, const std::string& name, bool checkRes = false);
+  TSatProof(Solver* solver, context::Context* context,
+            const std::string& name, bool checkRes = false);
   virtual ~TSatProof();
   void setCnfProof(CnfProof* cnf_proof);
 
@@ -198,6 +200,8 @@ class TSatProof {
    */
   void constructProof(ClauseId id);
   void constructProof() { constructProof(d_emptyClauseId); }
+  void refreshProof(ClauseId id);
+  void refreshProof() { refreshProof(d_emptyClauseId); }
   bool proofConstructed() const;
   void collectClauses(ClauseId id);
   bool derivedEmptyClause() const;
@@ -298,6 +302,7 @@ class TSatProof {
 
   // Internal data.
   typename Solver::Solver* d_solver;
+  context::Context* d_context;
   CnfProof* d_cnfProof;
 
   // clauses
@@ -389,9 +394,9 @@ template <class SatSolver>
 class LFSCSatProof : public TSatProof<SatSolver> {
  private:
  public:
-  LFSCSatProof(SatSolver* solver, const std::string& name,
-               bool checkRes = false)
-      : TSatProof<SatSolver>(solver, name, checkRes) {}
+  LFSCSatProof(SatSolver* solver, context::Context* context,
+               const std::string& name, bool checkRes = false)
+    : TSatProof<SatSolver>(solver, context, name, checkRes) {}
   virtual void printResolution(ClauseId id, std::ostream& out,
                                std::ostream& paren);
   virtual void printResolutions(std::ostream& out, std::ostream& paren);
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 603559da1..bcc849906 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -196,20 +196,22 @@ void ProofProxy<Solver>::updateCRef(typename Solver::TCRef oldref,
 
 /// SatProof
 template <class Solver>
-TSatProof<Solver>::TSatProof(Solver* solver, const std::string& name,
-                             bool checkRes)
+TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
+                             const std::string& name, bool checkRes)
     : d_solver(solver),
+      d_context(context),
       d_cnfProof(NULL),
       d_idClause(),
       d_clauseId(),
-      d_idUnit(),
+      d_idUnit(context),
+      d_unitId(context),
       d_deleted(),
       d_inputClauses(),
       d_lemmaClauses(),
       d_assumptions(),
       d_assumptionConflicts(),
       d_assumptionConflictsDebug(),
-      d_resolutionChains(),
+      d_resolutionChains(d_context),
       d_resStack(),
       d_checkRes(checkRes),
       d_emptyClauseId(ClauseIdEmpty),
@@ -263,7 +265,7 @@ TSatProof<Solver>::~TSatProof() {
   ResolutionChainIterator resolution_it = d_resolutionChains.begin();
   ResolutionChainIterator resolution_it_end = d_resolutionChains.end();
   for (; resolution_it != resolution_it_end; ++resolution_it) {
-    ResChain<Solver>* current = resolution_it->second;
+    ResChain<Solver>* current = (*resolution_it).second;
     delete current;
   }
 
@@ -378,7 +380,7 @@ template <class Solver>
 ClauseId TSatProof<Solver>::getClauseIdForLiteral(
     typename Solver::TLit lit) const {
   Assert(hasClauseIdForLiteral(lit));
-  return d_unitId.find(toInt(lit))->second;
+  return (*d_unitId.find(toInt(lit))).second;
 }
 
 template <class Solver>
@@ -432,7 +434,7 @@ bool TSatProof<Solver>::isUnit(ClauseId id) const {
 template <class Solver>
 typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) const {
   Assert(isUnit(id));
-  return d_idUnit.find(id)->second;
+  return (*d_idUnit.find(id)).second;
 }
 
 template <class Solver>
@@ -443,7 +445,7 @@ bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) const {
 template <class Solver>
 ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) const {
   Assert(isUnit(lit));
-  return d_unitId.find(toInt(lit))->second;
+  return (*d_unitId.find(toInt(lit))).second;
 }
 
 template <class Solver>
@@ -455,7 +457,7 @@ template <class Solver>
 const typename TSatProof<Solver>::ResolutionChain&
 TSatProof<Solver>::getResolutionChain(ClauseId id) const {
   Assert(hasResolutionChain(id));
-  const ResolutionChain* chain = d_resolutionChains.find(id)->second;
+  const ResolutionChain* chain = (*d_resolutionChains.find(id)).second;
   return *chain;
 }
 
@@ -535,6 +537,7 @@ ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause,
   typename ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
+
     d_clauseId.insert(std::make_pair(clause, newId));
     d_idClause.insert(std::make_pair(newId, clause));
     if (kind == INPUT) {
@@ -568,8 +571,11 @@ ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
   typename UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
     ClauseId newId = ProofManager::currentPM()->nextId();
-    d_unitId.insert(std::make_pair(toInt(lit), newId));
-    d_idUnit.insert(std::make_pair(newId, lit));
+
+    if (d_unitId.find(toInt(lit)) == d_unitId.end())
+      d_unitId[toInt(lit)] = newId;
+    if (d_idUnit.find(newId) == d_idUnit.end())
+      d_idUnit[newId] = lit;
 
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
@@ -719,13 +725,12 @@ void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) {
   // could be the case that a resolution chain for this clause already
   // exists (e.g. when removing units in addClause).
   if (hasResolutionChain(id)) {
-    ResChain<Solver>* current = d_resolutionChains.find(id)->second;
+    ResChain<Solver>* current = (*d_resolutionChains.find(id)).second;
     delete current;
-    d_resolutionChains.erase(id);
   }
-  Assert(!hasResolutionChain(id));
+  if (d_resolutionChains.find(id) == d_resolutionChains.end())
+    d_resolutionChains.insert(id, res);
 
-  d_resolutionChains.insert(std::make_pair(id, res));
   if (Debug.isOn("proof:sat")) {
     printRes(id);
   }
@@ -823,6 +828,7 @@ void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) {
 template <class Solver>
 ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
   // first check if we already have a resolution for lit
+
   if (isUnit(lit)) {
     ClauseId id = getClauseIdForLiteral(lit);
     Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id));
@@ -882,10 +888,9 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
     typename Solver::TLit lit = d_idUnit[conflict_id];
     ClauseId res_id = resolveUnit(~lit);
     res->addStep(lit, res_id, !sign(lit));
-
     registerResolution(d_emptyClauseId, res);
-
     return;
+
   } else {
     Assert(!d_storedUnitConflict);
     conflict_id = registerClause(conflict_ref, LEARNT);  // FIXME
@@ -894,6 +899,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
   if (Debug.isOn("proof:sat")) {
     Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
     print(conflict_id);
+    Debug("proof:sat") << std::endl;
   }
 
   ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
@@ -907,6 +913,7 @@ void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
     res->addStep(lit, res_id, !sign(lit));
     conflict_size = conflict.size();
   }
+
   registerResolution(d_emptyClauseId, res);
 }
 
@@ -962,6 +969,30 @@ void TSatProof<Solver>::constructProof(ClauseId conflict) {
   collectClauses(conflict);
 }
 
+template <class Solver>
+void TSatProof<Solver>::refreshProof(ClauseId conflict) {
+  IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin();
+  IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end();
+
+  for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) {
+    if (d_deletedTheoryLemmas.find(seen_lemma_it->first) == d_deletedTheoryLemmas.end())
+      delete seen_lemma_it->second;
+  }
+
+  IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin();
+  IdToSatClause::const_iterator seen_input_end = d_seenInputs.end();
+
+  for (; seen_input_it != seen_input_end; ++seen_input_it) {
+    delete seen_input_it->second;
+  }
+
+  d_seenInputs.clear();
+  d_seenLemmas.clear();
+  d_seenLearnt.clear();
+
+  collectClauses(conflict);
+}
+
 template <class Solver>
 bool TSatProof<Solver>::proofConstructed() const {
   return d_satProofConstructed;
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index a238f0a6a..50a01bedb 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -45,8 +45,7 @@ class CVC4_PUBLIC UnsatCore {
 public:
   UnsatCore() : d_smt(NULL) {}
 
-  template <class T>
-  UnsatCore(SmtEngine* smt, T begin, T end) : d_smt(smt), d_core(begin, end) {
+  UnsatCore(SmtEngine* smt, std::vector<Expr> core) : d_smt(smt), d_core(core) {
     initMessage();
   }
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index d898b66a2..26af5f146 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -131,7 +131,7 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
   , propagation_budget (-1)
   , asynch_interrupt   (false)
 {
-  PROOF(ProofManager::initSatProof(this);)
+  PROOF(ProofManager::currentPM()->initSatProof(this);)
 
   // Create the constant variables
   varTrue = newVar(true, false, false);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 998967c5e..911728cb1 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1012,7 +1012,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   // being parsed from the input file. Because of this, we cannot trust
   // that options::proof() is set correctly yet.
 #ifdef CVC4_PROOF
-  d_proofManager = new ProofManager();
+  d_proofManager = new ProofManager(d_userContext);
 #endif
 
   // We have mutual dependency here, so we add the prop engine to the theory
@@ -1996,7 +1996,7 @@ void SmtEngine::setDefaults() {
     }
   }
 
-  if(options::incrementalSolving() && (options::proof() || options::unsatCores())) {
+  if(options::incrementalSolving() && options::proof()) {
     Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof or --produce-unsat-cores, try --tear-down-incremental instead)" << endl;
     setOption("incremental", SExpr("false"));
   }
@@ -5054,7 +5054,7 @@ UnsatCore SmtEngine::getUnsatCore() throw(ModalException, UnsafeInterruptExcepti
   }
 
   d_proofManager->traceUnsatCore();// just to trigger core creation
-  return UnsatCore(this, d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
+  return UnsatCore(this, d_proofManager->extractUnsatCore());
 #else /* IS_PROOFS_BUILD */
   throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
 #endif /* IS_PROOFS_BUILD */