6 files changed, 121 insertions, 4 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 5cf5da1e0..fc9192dd9 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -97,7 +97,9 @@ libutil_la_SOURCES = \
 	regexp.cpp \
 	bin_heap.h \
 	didyoumean.h \
-	didyoumean.cpp
+	didyoumean.cpp \
+	unsat_core.h \
+	unsat_core.cpp
 
 libstatistics_la_SOURCES = \
 	statistics_registry.h \
@@ -156,7 +158,8 @@ EXTRA_DIST = \
 	uninterpreted_constant.i \
 	chain.i \
 	regexp.i \
-	proof.i
+	proof.i \
+	unsat_core.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 68d7d9a34..97a6338ce 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -19,6 +19,7 @@
 #include "util/ite_removal.h"
 #include "expr/command.h"
 #include "theory/ite_utilities.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -47,13 +48,23 @@ size_t RemoveITE::collectedCacheSizes() const{
   return d_containsVisitor->cache_size() + d_iteCache.size();
 }
 
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
+void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
 {
+  size_t n = output.size();
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
     // Do this in two steps to avoid Node problems(?)
     // Appears related to bug 512, splitting this into two lines
     // fixes the bug on clang on Mac OS
     Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+    // In some calling contexts, not necessary to report dependence information.
+    if(reportDeps && options::unsatCores()) {
+      // new assertions have a dependence on the node
+      PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+      while(n < output.size()) {
+        PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+        ++n;
+      }
+    }
     output[i] = itesRemoved;
   }
 }
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 83c55dab7..d71f9b13d 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -50,8 +50,11 @@ public:
    * contains a map from introduced skolem variables to the index in
    * assertions containing the new Boolean ite created in conjunction
    * with that skolem variable.
+   *
+   * With reportDeps true, report reasoning dependences to the proof
+   * manager (for unsat cores).
    */
-  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
+  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
 
   /**
    * Removes the ITE from the node by introducing skolem
diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
new file mode 100644
index 000000000..27261635d
--- /dev/null
+++ b/src/util/unsat_core.cpp
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file unsat_core.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of unsat cores
+ **
+ ** Representation of unsat cores.
+ **/
+
+#include "util/unsat_core.h"
+#include "expr/command.h"
+
+namespace CVC4 {
+
+UnsatCore::const_iterator UnsatCore::begin() const {
+  return d_core.begin();
+}
+
+UnsatCore::const_iterator UnsatCore::end() const {
+  return d_core.end();
+}
+
+void UnsatCore::toStream(std::ostream& out) const {
+  for(UnsatCore::const_iterator i = begin(); i != end(); ++i) {
+    out << AssertCommand(*i) << std::endl;
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
+  core.toStream(out);
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
new file mode 100644
index 000000000..51724b33b
--- /dev/null
+++ b/src/util/unsat_core.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file unsat_core.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__UNSAT_CORE_H
+#define __CVC4__UNSAT_CORE_H
+
+#include <iostream>
+#include <vector>
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UnsatCore {
+  std::vector<Expr> d_core;
+
+public:
+  UnsatCore() {}
+
+  template <class T>
+  UnsatCore(T begin, T end) : d_core(begin, end) {}
+
+  ~UnsatCore() {}
+
+  typedef std::vector<Expr>::const_iterator iterator;
+  typedef std::vector<Expr>::const_iterator const_iterator;
+
+  const_iterator begin() const;
+  const_iterator end() const;
+
+  void toStream(std::ostream& out) const;
+
+};/* class UnsatCore */
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UNSAT_CORE_H */
diff --git a/src/util/unsat_core.i b/src/util/unsat_core.i
new file mode 100644
index 000000000..78b1360e7
--- /dev/null
+++ b/src/util/unsat_core.i
@@ -0,0 +1,5 @@
+%{
+#include "util/unsat_core.h"
+%}
+
+%include "util/unsat_core.h"