Merged bit-vector and uf proof branch.

1 files changed, 32 insertions, 20 deletions

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index e21b7ef7d..93a920f82 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -20,30 +20,34 @@
 #include "options/quantifiers_options.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
+#include "proof/proof_manager.h"
+#include "proof/theory_proof.h"
+#include "proof/uf_proof.h"
 #include "theory/theory_model.h"
 #include "theory/type_enumerator.h"
 #include "theory/uf/theory_uf_strong_solver.h"
 
 using namespace std;
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
 
 /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
 TheoryUF::TheoryUF(context::Context* c, context::UserContext* u,
                    OutputChannel& out, Valuation valuation,
-                   const LogicInfo& logicInfo, SmtGlobals* globals)
-    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals),
+                   const LogicInfo& logicInfo, SmtGlobals* globals, std::string name)
+    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, globals, name),
       d_notify(*this),
       /* The strong theory solver can be notified by EqualityEngine::init(),
        * so make sure it's initialized first. */
       d_thss(NULL),
-      d_equalityEngine(d_notify, c, "theory::uf::TheoryUF", true),
+      d_equalityEngine(d_notify, c, name + "theory::uf::TheoryUF", true),
       d_conflict(c, false),
       d_literalsToPropagate(c),
       d_literalsToPropagateIndex(c, 0),
       d_functionsTerms(c),
-      d_symb(u)
+      d_symb(u, name)
 {
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
@@ -204,27 +208,29 @@ Node TheoryUF::getNextDecisionRequest(){
   }
 }
 
-void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions) {
+void TheoryUF::explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf) {
   // Do the work
   bool polarity = literal.getKind() != kind::NOT;
   TNode atom = polarity ? literal : literal[0];
-  eq::EqProof * eqp = d_proofEnabled ? new eq::EqProof : NULL;
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
-    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, eqp);
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions, pf);
   } else {
-    d_equalityEngine.explainPredicate(atom, polarity, assumptions, eqp);
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions, pf);
   }
-  //for now, just print debug
-  //TODO : send the proof outwards : d_out->conflict( lem, eqp );
-  if( eqp ){
-    eqp->debug_print("uf-pf");
+  if( pf ){
+    Debug("uf-pf") << std::endl;
+    pf->debug_print("uf-pf");
   }
 }
 
 Node TheoryUF::explain(TNode literal) {
+  return explain(literal, NULL);
+}
+
+Node TheoryUF::explain(TNode literal, eq::EqProof* pf) {
   Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
   std::vector<TNode> assumptions;
-  explain(literal, assumptions);
+  explain(literal, assumptions, pf);
   return mkAnd(assumptions);
 }
 
@@ -508,13 +514,14 @@ void TheoryUF::computeCareGraph() {
 }/* TheoryUF::computeCareGraph() */
 
 void TheoryUF::conflict(TNode a, TNode b) {
-  //TODO: create EqProof at this level if d_proofEnabled = true
+  eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
   if (a.getKind() == kind::CONST_BOOLEAN) {
-    d_conflictNode = explain(a.iffNode(b));
+    d_conflictNode = explain(a.iffNode(b),pf);
   } else {
-    d_conflictNode = explain(a.eqNode(b));
+    d_conflictNode = explain(a.eqNode(b),pf);
   }
-  d_out->conflict(d_conflictNode);
+  ProofUF * puf = d_proofsEnabled ? new ProofUF( pf ) : NULL;
+  d_out->conflict(d_conflictNode, puf);
   d_conflict = true;
 }
 
@@ -541,3 +548,8 @@ void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
     d_thss->assertDisequal(t1, t2, reason);
   }
 }
+
+
+} /* namespace CVC4::theory::uf */
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */