refactoring to datatypes theory, added working prototype for proof/explanation manager

diff --git a/src/theory/datatypes/Makefile.am b/src/theory/datatypes/Makefile.am
index 69d83faf46e6fe1d60ddfb4ce19c10db0a73e3ec..f8bfa3dc533aa19cef10edbe7a1c6a00d941acdf 100644 (file)
--- a/src/theory/datatypes/Makefile.am
+++ b/src/theory/datatypes/Makefile.am
@@ -11,6 +11,8 @@ libdatatypes_la_SOURCES = \
        datatypes_rewriter.h \
        theory_datatypes.cpp \
        union_find.h \
-       union_find.cpp
+       union_find.cpp \
+       explanation_manager.h \
+       explanation_manager.cpp
 
 EXTRA_DIST = kinds

diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp
new file mode 100644 (file)
index 0000000..424ca8f
--- /dev/null
+++ b/src/theory/datatypes/explanation_manager.cpp
@@ -0,0 +1,81 @@
+#include "theory/datatypes/explanation_manager.h"\r
+\r
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::datatypes;\r
+
+void ProofManager::setExplanation( Node n, Node jn, unsigned r ) 
+{ 
+  d_exp[n] = std::pair< Node, unsigned >( jn, r ); 
+}
+
+//std::ostream& operator<<(std::ostream& os, Reason::Rule r)
+//{
+//  switch( r ){
+//    
+//  }
+//}
+
+void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm )
+{
+  if( n.getKind()==kind::AND ){
+    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
+      process( n[i], nb, pm );
+    }
+  }else{
+    if( !pm->hasExplained( n ) ){
+      context::CDMap< Node, Reason, NodeHashFunction >::iterator it = d_drv_map.find( n );
+      Reason r;
+      Node exp;
+      if( it!=d_drv_map.end() ){
+        r = (*it).second;
+        if( r.d_e ){
+          Debug("emanager") << "Em::process: Consult externally for " << n << std::endl;
+          exp = r.d_e->explain( n, pm );
+          //trivial case, r says that n is an input
+          if( exp==n ){
+            r.d_isInput = true;
+          }
+        }else if( !r.d_isInput ){
+          exp = r.d_node;
+          pm->setExplanation( n, exp, r.d_reason );
+          if( exp.isNull() ) Debug("emanager") << "Em::process: " << n << " is an axiom, reason = " << r.d_reason << endl;
+        }
+      }
+
+      if( r.d_isInput ){
+        Debug("emanager") << "Em::process: " << n << " is an input " << endl;
+        nb << n;
+        pm->setExplanation( n, Node::null(), Reason::input );
+      }else if( !exp.isNull() ){
+        Debug("emanager") << "Em::process: " << exp << " is the explanation for " << n << " " 
+                          << ", reason = " << pm->getReason( n ) << endl;
+        if( exp.getKind()==kind::AND ){
+          for( int i=0; i<(int)exp.getNumChildren(); i++ ) {
+            process( exp[i], nb, pm );
+          }
+        }else{
+          process( exp, nb, pm );
+        }
+      }
+    }else{
+      Debug("emanager") << "Em::process: proof manager has already explained " << n << endl;
+    }
+  }
+}
+
+Node ExplanationManager::explain( Node n, ProofManager* pm )
+{
+  NodeBuilder<> nb(kind::AND);
+  if( pm ){
+    pm->clear();
+    process( n, nb, pm );
+  }else{
+    ProofManager pm;
+    process( n, nb, &pm );
+  }
+  return ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
+}

diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h
new file mode 100644 (file)
index 0000000..d16f48b
--- /dev/null
+++ b/src/theory/datatypes/explanation_manager.h
@@ -0,0 +1,220 @@
+/*********************                                                        */
+/*! \file explanation_manager.h
+ ** \verbatim
+ ** Original author: ajreynol
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Theory of datatypes.
+ **
+ ** Theory of datatypes.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H
+#define __CVC4__THEORY__DATATYPES__EXPLANATION_MANAGER_H
+
+#include "theory/theory.h"
+#include "util/congruence_closure.h"
+#include "util/datatype.h"
+#include "util/hash.h"
+#include "util/trans_closure.h"
+
+#include <ext/hash_set>
+#include <iostream>
+#include <map>
+
+namespace CVC4 {
+namespace theory {
+namespace datatypes {
+
+
+class Explainer;
+
+/** reason class */
+class Reason { 
+public:
+  enum Rule {
+    unspecified = 0,
+    contradiction = 1,
+
+    cc_coarse,
+
+    //unification rules
+    idt_unify,
+    idt_cycle,
+    idt_clash,
+    //tester rules
+    idt_taxiom,
+    idt_tcong,
+    idt_tclash,
+    idt_texhaust,
+    //other rules
+    idt_inst,
+    idt_collapse,
+    idt_collapse2,
+
+    input,
+  };
+public:
+  Reason() : d_e( NULL ), d_isInput( true ){}
+  Reason( Node n, unsigned r ) : d_node( n ), d_reason( r ), d_e( NULL ), d_isInput( false ) {}
+  Reason( Explainer* e ) : d_reason( 0 ), d_e( e ), d_isInput( false ){}
+  virtual ~Reason(){}
+  Node d_node;
+  unsigned d_reason;
+  Explainer* d_e;
+  bool d_isInput;
+};
+
+/** proof manager for theory lemmas */
+class ProofManager {
+protected:
+  enum Effort {
+    MIN_EFFORT = 0,
+    STANDARD = 50,
+    FULL_EFFORT = 100
+  };/* enum Effort */
+  /** map from nodes to a description of how they are explained */
+  std::map< Node, std::pair< Node, unsigned > > d_exp;
+  /** whether to produce proofs */
+  Effort d_effort;
+public:
+  ProofManager( Effort effort = STANDARD ) : d_effort( effort ){}
+  ~ProofManager(){}
+  void setExplanation( Node n, Node jn, unsigned r = 0 );
+  bool hasExplained( Node n ) { return d_exp.find( n )!=d_exp.end(); }
+  Effort getEffort() { return d_effort; }
+  void clear() { d_exp.clear(); }
+  /** for debugging */
+  Node getJustification( Node n ) { return d_exp[n].first; }
+  unsigned getReason( Node n ) { return d_exp[n].second; }
+};
+
+class Explainer 
+{
+public:
+  /** assert that n is true */
+  virtual void assert( Node n ) = 0;
+  /** get the explanation for n.  
+      This should call pm->setExplanation( n1, jn1, r1 ) ... pm->setExplanation( nk, jnk, rk )
+        for some set of Nodes n1...nk.
+      Satisfies post conditions:
+      - If pm->getEffort() = MAX_EFFORT, then each ( ni, jni, ri ) should be a precise
+          application or rule ri, i.e. applying proof rule ri to jni derives ni.
+      - If pm->getEffort() = STANDARD, then for each ( ni, jni, ri ), 
+          jni is the (at least informal) justification for ni.
+      - Return value should be a conjunction of nodes n'1...n'k, where each n'i occurs 
+          (as a conjunct) in jn1...jnk, but not in n1...nk.  
+          For each of these literals n'i, assert( n'i ) was called previously,
+      - either pm->setExplanation( n, ... ) is called, or n is the return value
+  */
+  virtual Node explain( Node n, ProofManager* pm ) = 0;
+};
+
+template <class OutputChannel, class CongruenceOperatorList>
+class CongruenceClosureExplainer : public Explainer
+{
+protected:
+  //pointer to the congruence closure module
+  CongruenceClosure<OutputChannel, CongruenceOperatorList>* d_cc;
+public:
+  CongruenceClosureExplainer(CongruenceClosure<OutputChannel, CongruenceOperatorList>* cc) :
+    Explainer(),
+    d_cc( cc ){
+   }
+  ~CongruenceClosureExplainer(){}
+  /** assert that n is true */
+  void assert( Node n ){
+    Assert( n.getKind() == kind::EQUAL );
+    d_cc->addEquality( n );
+  }
+  /** get the explanation for n */
+  Node explain( Node n, ProofManager* pm ){
+    Assert( n.getKind() == kind::EQUAL );
+    if( pm->getEffort()==ProofManager::FULL_EFFORT ){
+      //unsupported
+      Assert( false );
+      return Node::null();
+    }else{
+      Node exp = d_cc->explain( n[0], n[1] );
+      if( exp!=n ){
+        pm->setExplanation( n, exp, Reason::cc_coarse );
+      }
+      return exp;
+    }
+  }
+};
+
+
+class ExplanationManager : public Explainer
+{
+private:
+  /** map from nodes and the reason for them */
+  context::CDMap< Node, Reason, NodeHashFunction > d_drv_map;
+  /** has conflict */
+  context::CDO< bool > d_hasConflict;
+  /** process the reason for node n */
+  void process( Node n, NodeBuilder<>& nb, ProofManager* pm );
+public:
+  ExplanationManager(context::Context* c) : Explainer(), d_drv_map(c), d_hasConflict( c, false ){}
+  ~ExplanationManager(){}
+
+  /** assert that n is true (n is an input) */
+  void assert( Node n ) { 
+    //TODO: this can be optimized: 
+    //  if the previous explanation for n was empty (n is a tautology), 
+    //  then we should not claim it to be an input.
+    Reason r = d_drv_map[n];
+    r.d_isInput = true; 
+  }
+  /** n is explained */
+  bool hasNode( Node n ) { return d_drv_map.find( n )!=d_drv_map.end(); }
+  /** n is explained */
+  bool hasConflict() { return d_hasConflict.get() || hasNode( NodeManager::currentNM()->mkConst(false) ); }
+  /** jn is why n is true, by reason r */
+  void addNode( Node n, Node jn, unsigned r = 0 ) { 
+    if( !hasNode( n ) ){
+      Assert( n!=jn );
+      Debug("emanager") << "em::addNode: (" << jn << ", " << r << ") -> " << n << std::endl;
+      d_drv_map[n] = Reason( jn, r ); 
+    }
+  }
+  /** Explainer e can tell you why n is true in the current state.  */
+  void addNode( Node n, Explainer* e ) {
+    if( !hasNode( n ) ){
+      Debug("emanager") << "em::addNodeEx: (" << e << ") -> " << n << std::endl;
+      d_drv_map[n] = Reason( e ); 
+    }
+  }
+  /** n is true by reason (axiom) r */
+  void addNodeAxiom( Node n, unsigned r = 0 ) { addNode( n, Node::null(), r ); }
+  /** conclude a contradiction by jn and reason r */
+  void addNodeConflict( Node jn, unsigned r = 0 ){
+    addNode( NodeManager::currentNM()->mkConst(false), jn, r );
+    d_hasConflict.set( true );
+  }
+  /** get explanation for n 
+      Requires pre conditions: TBD
+      Satisfies post conditions:  TBD
+  */
+  Node explain( Node n, ProofManager* pm = NULL );
+  /** get conflict */
+  Node getConflict( ProofManager* pm = NULL ){
+    return explain( NodeManager::currentNM()->mkConst(false), pm );
+  }
+};
+
+
+}
+}
+}
+
+#endif
\ No newline at end of file

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 88667de8dc94ea8b8d7cedbfd00dca2e4677fab5..1c901f38eea3a4d28404367b4cbf1cfbdacfe1cf 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -59,8 +59,6 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua
   Theory(THEORY_DATATYPES, c, out, valuation),
   d_currAsserts(c),
   d_currEqualities(c),
-  d_drv_map(c),
-  d_axioms(c),
   d_selectors(c),
   d_reps(c),
   d_selector_eq(c),
@@ -73,10 +71,10 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua
   d_cc(c, &d_ccChannel),
   d_unionFind(c),
   d_disequalities(c),
-  d_equalities(c),
-  d_conflict(),
   d_noMerge(false),
-  d_inCheck(false){
+  d_inCheck(false),
+  d_em(c),
+  d_cce(&d_cc){
 
   ////bug test for transitive closure
   //TransitiveClosure tc( c );
@@ -98,20 +96,13 @@ void TheoryDatatypes::addSharedTerm(TNode t) {
 void TheoryDatatypes::notifyEq(TNode lhs, TNode rhs) {
   Debug("datatypes") << "TheoryDatatypes::notifyEq(): "
                      << lhs << " = " << rhs << endl;
-  //if(!d_conflict.isNull()) {
-  //  return;
-  //}
-  //merge(lhs,rhs);
-  //FIXME
-  //Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, lhs, rhs);
-  //addEquality(eq);
-  //d_drv_map[eq] = d_cc.explain( lhs, rhs );
+  
 }
 
 void TheoryDatatypes::notifyCongruent(TNode lhs, TNode rhs) {
   Debug("datatypes") << "TheoryDatatypes::notifyCongruent(): "
                      << lhs << " = " << rhs << endl;
-  if(d_conflict.isNull()) {
+  if(!hasConflict()) {
     merge(lhs,rhs);
   }
   Debug("datatypes-debug") << "TheoryDatatypes::notifyCongruent(): done." << endl;
@@ -137,7 +128,8 @@ void TheoryDatatypes::check(Effort e) {
 
   while(!done()) {
     Node assertion = get();
-    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) {
+    if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles")
+        || Debug.isOn("datatypes-debug-pf") ) {
       cout << "*** TheoryDatatypes::check(): " << assertion << endl;
       d_currAsserts.push_back( assertion );
     }
@@ -145,10 +137,10 @@ void TheoryDatatypes::check(Effort e) {
     //clear from the derived map
     d_inCheck = true;
     collectTerms( assertion );
-    if( d_conflict.isNull() ){
-      if( !d_drv_map[assertion].get().isNull() ) {
+    if( !hasConflict() ){
+      if( d_em.hasNode( assertion ) ){
         Debug("datatypes") << "Assertion has already been derived" << endl;
-        d_drv_map[assertion] = Node::null();
+        d_em.assert( assertion );
       } else {
         switch(assertion.getKind()) {
         case kind::EQUAL:
@@ -156,7 +148,7 @@ void TheoryDatatypes::check(Effort e) {
           addEquality(assertion);
           break;
         case kind::APPLY_TESTER:
-          checkTester( assertion );
+          addTester( assertion );
           break;
         case kind::NOT:
           {
@@ -176,16 +168,17 @@ void TheoryDatatypes::check(Effort e) {
                               << "  find(b) == > " << debugFind(b) << endl;
                 }
                 // There are two ways to get a conflict here.
-                if(d_conflict.isNull()) {
+                if(!hasConflict()) {
                   if(find(a) == find(b)) {
                     // We get a conflict this way if we WERE previously watching
                     // a, b and were notified previously (via notifyCongruent())
                     // that they were congruent.
-                    NodeBuilder<> nb(kind::AND);
-                    nb << d_cc.explain( assertion[0][0], assertion[0][1] );
-                    nb << assertion;
-                    d_conflict = nb;
-                    Debug("datatypes") << "Disequality conflict " << d_conflict << endl;
+                    Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, assertion[0][0], assertion[0][1] );
+                    NodeBuilder<> nbc(kind::AND);
+                    nbc << ccEq << assertion;
+                    Node contra = nbc;
+                    d_em.addNode( ccEq, &d_cce );
+                    d_em.addNodeConflict( contra, Reason::contradiction );
                   } else {
                     // If we get this far, there should be nothing conflicting due
                     // to this disequality.
@@ -195,7 +188,7 @@ void TheoryDatatypes::check(Effort e) {
               }
               break;
             case kind::APPLY_TESTER:
-              checkTester( assertion );
+              addTester( assertion );
               break;
             default:
               Unhandled(assertion[0].getKind());
@@ -209,9 +202,19 @@ void TheoryDatatypes::check(Effort e) {
         }
       }
     }
+    Debug("datatypes-debug-pf") << "Done check " << assertion << " " << hasConflict() << std::endl;
     d_inCheck = false;
-    if(!d_conflict.isNull()) {
-      throwConflict();
+    if( hasConflict() ) {
+      Debug("datatypes-conflict") << "Constructing conflict..." << endl;
+      Node conflict = d_em.getConflict();
+      if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || 
+          Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){
+        cout << "Conflict constructed : " << conflict << endl;
+      }
+      //if( conflict.getKind()!=kind::AND ){
+      //  conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict);
+      //}
+      d_out->conflict( conflict, false );
       return;
     }
   }
@@ -222,20 +225,56 @@ void TheoryDatatypes::check(Effort e) {
     for( EqLists::iterator i = d_labels.begin(); i != d_labels.end(); i++ ) {
       Node sf = find( (*i).first );
       if( sf == (*i).first || sf.getKind() != APPLY_CONSTRUCTOR ) {
+        addTermToLabels( sf );
         EqList* lbl = (sf == (*i).first) ? (*i).second : (*d_labels.find( sf )).second;
-        Debug("datatypes-split") << "Check for splitting " << (*i).first << ", ";
-        Debug("datatypes-split") << "label size = " << lbl->size() << endl;
-        Node cons = getPossibleCons( (*i).first, false );
-        if( !cons.isNull() ) {
-          const Datatype::Constructor& cn = getConstructor( cons );
-          Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
-          Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
-          NodeBuilder<> nb(kind::OR);
-          nb << test << test.notNode();
-          Node lemma = nb;
-          Debug("datatypes-split") << "Lemma is " << lemma << endl;
-          d_out->lemma( lemma );
-          return;
+        Debug("datatypes-split") << "Check for splitting " << (*i).first
+                                 << ", label size = " << lbl->size() << endl;
+        if( lbl->empty() || (*lbl)[ lbl->size()-1 ].getKind() == NOT ) {
+          TypeNode typ = sf.getType();
+          const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype();
+          vector< bool > possibleCons;
+          possibleCons.resize( dt.getNumConstructors(), true );
+          for( EqList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ) {
+            TNode leqn = (*j);
+            possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
+          }
+          Node cons;
+          bool foundSel = false;
+          for( unsigned int j=0; j<possibleCons.size(); j++ ) {
+            if( !foundSel && possibleCons[j] ) {
+              cons = Node::fromExpr( dt[ j ].getConstructor() );
+              //if there is a selector, split
+              for( unsigned int k=0; k<dt[ j ].getNumArgs(); k++ ) {
+                Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[j][k].getSelector() ), sf );
+                if( d_selectors.find( s ) != d_selectors.end() ) {
+                  Debug("datatypes") << "  getPosCons: found selector " << s << endl;
+                  foundSel = true;
+                  break;
+                }
+              }
+            }
+          }
+          if( !foundSel ){
+            for( unsigned int j=0; j<(int)possibleCons.size(); j++ ) {
+              if( possibleCons[j] && !dt[ j ].isFinite() ) {
+                Debug("datatypes") << "Did not find selector for " << sf
+                                  << " and " << dt[ j ].getConstructor() << " is not finite." << endl;
+                cons = Node::null();
+                break;
+              }
+            }
+          }
+          if( !cons.isNull() ) {
+            const Datatype::Constructor& cn = getConstructor( cons );
+            Debug("datatypes-split") << "*************Split for possible constructor " << cons << endl;
+            Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), (*i).first );
+            NodeBuilder<> nb(kind::OR);
+            nb << test << test.notNode();
+            Node lemma = nb;
+            Debug("datatypes-split") << "Lemma is " << lemma << endl;
+            d_out->lemma( lemma );
+            return;
+          }
         }
       } else {
         Debug("datatypes-split") << (*i).first << " is " << sf << endl;
@@ -247,127 +286,132 @@ void TheoryDatatypes::check(Effort e) {
   }
 }
 
-void TheoryDatatypes::checkTester( Node assertion, bool doAdd ) {
+bool TheoryDatatypes::checkTester( Node assertion, Node& conflict, unsigned& r ){
   Debug("datatypes") << "Check tester " << assertion << endl;
 
+  //preprocess the tester
   Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion;
-  const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() );
+  Assert( find( tassertion[0] ) == tassertion[0] );
+
+  //if argument is a constructor, it is trivial
+  if( tassertion[0].getKind() == APPLY_CONSTRUCTOR ) {
+    size_t tIndex = Datatype::indexOf(tassertion.getOperator().toExpr());
+    size_t cIndex = Datatype::indexOf(tassertion[0].getOperator().toExpr());
+    if( (tIndex==cIndex) == (assertion.getKind() == NOT) ) {
+      conflict = assertion;
+      r = Reason::idt_tclash;
+    }
+    return false;
+  }
 
+  addTermToLabels( tassertion[0] );
+  EqLists::iterator lbl_i = d_labels.find( tassertion[0] );
+  EqList* lbl = (*lbl_i).second;
+  Assert( !lbl->empty() || lbl->begin()==lbl->end() );
+  //check if empty label (no possible constructors for term)
+  bool redundant = false;
+  for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+    Node leqn = (*i);
+    if( leqn.getKind() == kind::NOT ) {
+      if( leqn[0].getOperator() == tassertion.getOperator() ) {
+        if( assertion.getKind() == NOT ) {
+          redundant = true;
+        } else {
+          conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion );
+          r = Reason::contradiction;
+          Debug("datatypes") << "Contradictory labels " << conflict << endl;
+          return false;
+        }
+        break;
+      }
+    }else{
+      if( (leqn.getOperator() == tassertion.getOperator()) == (assertion.getKind() == NOT) ) {
+        conflict = NodeManager::currentNM()->mkNode( AND, leqn, assertion );
+        r = Reason::idt_tclash;
+        Debug("datatypes") << "Contradictory labels(2) " << conflict << endl;
+        return false;
+      }
+      redundant = true;
+      break;
+    }
+  }
+  return !redundant;
+}
+
+void TheoryDatatypes::addTester( Node assertion ){
+  Debug("datatypes") << "Add tester " << assertion << endl;
+
+  //preprocess the tester
+  Node tassertion = ( assertion.getKind() == NOT ) ? assertion[0] : assertion;
   //add the term into congruence closure consideration
   d_cc.addTerm( tassertion[0] );
 
-  Node assertionRep = assertion;
-  Node tassertionRep = tassertion;
+  Node assertionRep;
+  Node tassertionRep;
   Node tRep = tassertion[0];
-  //tRep = collapseSelector( tRep, Node::null(), true );
   tRep = find( tRep );
-  Debug("datatypes") << "tRep is " << tRep << " " << tassertion[0] << endl;
   //add label instead for the representative (if it is different)
   if( tRep != tassertion[0] ) {
     tassertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, tassertion.getOperator(), tRep );
     assertionRep = ( assertion.getKind() == NOT ) ? tassertionRep.notNode() : tassertionRep;
     //add explanation
-    if( doAdd ) {
-      Node explanation = d_cc.explain( tRep, tassertion[0] );
-      NodeBuilder<> nb(kind::AND);
-      nb << explanation << assertion;
-      explanation = nb;
-      Debug("datatypes-drv") << "Check derived tester " << assertionRep << endl;
-      Debug("datatypes-drv") << "  Justification is " << explanation << endl;
-      d_drv_map[assertionRep] = explanation;
-    }
-  }
-
-  //if tRep is a constructor, it is trivial
-  if( tRep.getKind() == APPLY_CONSTRUCTOR ) {
-    if( checkTrivialTester( tassertionRep ) == (assertionRep.getKind() == NOT) ) {
-      d_conflict = doAdd ? assertionRep : NodeManager::currentNM()->mkConst(true);
-      Debug("datatypes") << "Trivial conflict " << assertionRep << endl;
-    }
-    return;
+    Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, tRep, tassertion[0] );
+    d_em.addNode( ccEq, &d_cce );
+    NodeBuilder<> nb2(kind::AND);
+    nb2 << assertion << ccEq;
+    Node expl = nb2;
+    d_em.addNode( assertionRep, expl, Reason::idt_tcong );
+  }else{
+    tassertionRep = tassertion;
+    assertionRep = assertion;
   }
 
-  addTermToLabels( tRep );
-  EqLists::iterator lbl_i = d_labels.find(tRep);
-  //Debug("datatypes") << "Found " << (lbl_i == d_labels.end()) << endl;
-  Assert( lbl_i != d_labels.end() );
-
-  EqList* lbl = (*lbl_i).second;
-  //Debug("datatypes") << "Check lbl = " << lbl << ", size = " << lbl->size() << endl;
-
-  //check if empty label (no possible constructors for term)
-  bool add = true;
-  unsigned int notCount = 0;
-  if( !lbl->empty() ) {
-    for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-      Node leqn = (*i);
-      if( leqn.getKind() == kind::NOT ) {
-        if( leqn[0].getOperator() == tassertionRep.getOperator() ) {
-          if( assertionRep.getKind() == NOT ) {
-            add = false;
-          } else {
-            NodeBuilder<> nb(kind::AND);
-            nb << leqn;
-            if( doAdd ) nb << assertionRep;
-            d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
-            Debug("datatypes") << "Contradictory labels " << d_conflict << endl;
-            return;
-          }
-          break;
-        }
-        notCount++;
-      } else {
-        if( (leqn.getOperator() == tassertionRep.getOperator()) == (assertionRep.getKind() == NOT) ) {
-          NodeBuilder<> nb(kind::AND);
-          nb << leqn;
-          if( doAdd ) nb << assertionRep;
-          d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
-          Debug("datatypes") << "Contradictory labels(2) " << d_conflict << endl;
-          return;
-        }
-        add = false;
-        break;
-      }
-    }
-  }
-  if( add ) {
-    if( assertionRep.getKind() == NOT && notCount == dt.getNumConstructors()-1 ) {
-      NodeBuilder<> nb(kind::AND);
-      if( !lbl->empty() ) {
+  Node conflict;
+  unsigned r;
+  if( checkTester( assertionRep, conflict, r ) ){
+    EqLists::iterator lbl_i = d_labels.find( tRep );
+    EqList* lbl = (*lbl_i).second;
+    lbl->push_back( assertionRep );
+    Debug("datatypes") << "Add to labels " << lbl->size() << endl;
+    if( assertionRep.getKind()==NOT ){
+      const Datatype& dt = Datatype::datatypeOf( tassertion.getOperator().toExpr() );
+      //we can conclude the final one
+      if( lbl->size()==dt.getNumConstructors()-1 ){
+        vector< bool > possibleCons;
+        possibleCons.resize( dt.getNumConstructors(), true );
+        NodeBuilder<> nb(kind::AND);
         for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
+          possibleCons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false;
           nb << (*i);
         }
+        unsigned int testerIndex = -1;
+        for( unsigned int i=0; i<possibleCons.size(); i++ ) {
+          if( possibleCons[i] ){
+            Assert( testerIndex==-1 );
+            testerIndex = i;
+          }
+        }
+        Assert( testerIndex!=-1 );
+        assertionRep = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[testerIndex].getTester() ), tRep );
+        Node exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
+        d_em.addNode( assertionRep, exp, Reason::idt_texhaust );
+        addTester( assertionRep );    //add stronger statement
+        return;
       }
-      if( doAdd ) nb << assertionRep;
-      d_conflict = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
-      Debug("datatypes") << "Exhausted possibilities for labels " << d_conflict << endl;
-      return;
     }
-    if( doAdd ) {
-      lbl->push_back( assertionRep );
-      Debug("datatypes") << "Add to labels " << lbl->size() << endl;
-    }
-  }
-  if( doAdd ) {
-    checkInstantiate( tRep );
-    if( !d_conflict.isNull() ) {
-      return;
+    if( assertionRep.getKind()==APPLY_TESTER ){
+      //we have concluded that tRep must be a particular tester
+      //test all nodes in the equivalence class of tRep for instantiation
+      checkInstantiate( tRep );
+      if( hasConflict() ) {
+        return;
+      }
+      //test all selectors whose arguments are in the equivalence class of tRep
+      updateSelectors( tRep );
     }
-    //inspect selectors
-    updateSelectors( tRep );
+  }else if( !conflict.isNull() ){
+    d_em.addNodeConflict( conflict, r );
   }
-  return;
-}
-
-bool TheoryDatatypes::checkTrivialTester(Node assertion) {
-  AssertArgument(assertion.getKind() == APPLY_TESTER &&
-                 assertion[0].getKind() == APPLY_CONSTRUCTOR,
-                 assertion, "argument must be a tester-over-constructor");
-  TNode tester = assertion.getOperator();
-  TNode ctor = assertion[0].getOperator();
-  // if they have the same index (and the node has passed
-  // typechecking) then this is a trivial tester
-  return Datatype::indexOf(tester.toExpr()) == Datatype::indexOf(ctor.toExpr());
 }
 
 void TheoryDatatypes::checkInstantiate( Node t ) {
@@ -378,61 +422,65 @@ void TheoryDatatypes::checkInstantiate( Node t ) {
   if( t.getKind() != APPLY_CONSTRUCTOR ) {
     //for each term in equivalance class
     initializeEqClass( t );
+    TypeNode typ = t.getType();
     EqListN* eqc = (*d_equivalence_class.find( t )).second;
     for( EqListN::const_iterator iter = eqc->begin(); iter != eqc->end(); iter++ ) {
       Node te = *iter;
       Assert( find( te ) == t );
+      //if term has not yet been instantiated
       if( d_inst_map.find( te ) == d_inst_map.end() ) {
-        Node cons = getPossibleCons( te, true );
         EqLists::iterator lbl_i = d_labels.find( t );
-        //there is one remaining constructor
-        if( !cons.isNull() && lbl_i != d_labels.end() ) {
+        if( lbl_i!=d_labels.end() ) {
           EqList* lbl = (*lbl_i).second;
-          const Datatype::Constructor& cn = Datatype::datatypeOf( cons.toExpr() )[ Datatype::indexOf( cons.toExpr() ) ];
-
-          //only one constructor possible for term (label is singleton), apply instantiation rule
-          //find if selectors have been applied to t
-          vector< Node > selectorVals;
-          selectorVals.push_back( cons );
-          NodeBuilder<> justifyEq(kind::AND);
-          bool foundSel = false;
-          for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
-            Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
-            Debug("datatypes") << "Selector[" << i << "] = " << s << endl;
-            if( d_selectors.find( s ) != d_selectors.end() ) {
-              Node sf = find( s );
-              if( sf != s && sf.getKind() != SKOLEM ) {
-                justifyEq << d_cc.explain( sf, s );
+          //check there is one remaining constructor
+          const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype();
+          Node cons;
+          if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
+            size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() );
+            Node cons = Node::fromExpr( dt[ testerIndex ].getConstructor() );
+            const Datatype::Constructor& cn = Datatype::datatypeOf( cons.toExpr() )[ Datatype::indexOf( cons.toExpr() ) ];
+
+            //only one constructor possible for term (label is singleton), apply instantiation rule
+            //find if selectors have been applied to t
+            vector< Node > selectorVals;
+            selectorVals.push_back( cons );
+            bool foundSel = false;
+            for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
+              Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
+              if( d_selectors.find( s ) != d_selectors.end() ) {
+                foundSel = true;
+                s = find( s );
               }
-              foundSel = true;
-              s = sf;
+              selectorVals.push_back( s );
             }
-            selectorVals.push_back( s );
-          }
-          if( cn.isFinite() || foundSel ) {
-            d_inst_map[ te ] = true;
-            //instantiate, add equality
-            Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
-            if( find( val ) != find( te ) ) {
-              Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te );
-              Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl;
-              if( lbl->size() == 1 || (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
-                justifyEq << (*lbl)[ lbl->size()-1 ];
-              } else {
-                if( !lbl->empty() ) {
-                  for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-                    justifyEq << (*i);
+            if( cn.isFinite() || foundSel ) {
+              d_inst_map[ te ] = true;
+              //instantiate, add equality
+              Node val = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, selectorVals );
+              if( find( val ) != find( te ) ) {
+                collectTerms( val );
+                NodeBuilder<> nb(kind::AND);
+                nb << (*lbl)[ lbl->size()-1 ];
+                for( unsigned int i=0; i<cn.getNumArgs(); i++ ) {
+                  Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( cn[i].getSelector() ), te );
+                  if( selectorVals[i+1]!=s ){
+                    Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, selectorVals[i+1], s );
+                    d_em.addNode( ccEq, &d_cce );
+                    nb << ccEq;
+                  }else{
+                    //reflexive for s, if we want fined grained
                   }
                 }
+                Node jeq = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
+                Node newEq = NodeManager::currentNM()->mkNode( EQUAL, val, te );
+                Debug("datatypes") << "Instantiate Equal: " << newEq << "." << endl;
+                d_em.addNode( newEq, jeq, Reason::idt_inst );
+                addEquality( newEq );
+                return;
               }
-              Node jeq = ( justifyEq.getNumChildren() == 1 ) ? justifyEq.getChild( 0 ) : justifyEq;
-              Debug("datatypes-split") << "Instantiate " << newEq << endl;
-              preRegisterTerm( val );
-              addDerivedEquality( newEq, jeq );
-              return;
+            } else {
+              Debug("datatypes") << "infinite constructor, no selectors " << cons << endl;
             }
-          } else {
-            Debug("datatypes") << "infinite constructor, no selectors " << cons << endl;
           }
         }
       }
@@ -440,65 +488,6 @@ void TheoryDatatypes::checkInstantiate( Node t ) {
   }
 }
 
-//checkInst = true is for checkInstantiate, checkInst = false is for splitting
-Node TheoryDatatypes::getPossibleCons( Node t, bool checkInst ) {
-  Node tf = find( t );
-  EqLists::iterator lbl_i = d_labels.find( tf );
-  if( lbl_i != d_labels.end() ) {
-    EqList* lbl = (*lbl_i).second;
-    TypeNode typ = t.getType();
-
-    const Datatype& dt = ((DatatypeType)typ.toType()).getDatatype();
-
-    //if ended by one positive tester
-    if( !lbl->empty() && (*lbl)[ lbl->size()-1 ].getKind() != NOT ) {
-      if( checkInst ) {
-        size_t testerIndex = Datatype::indexOf( (*lbl)[ lbl->size()-1 ].getOperator().toExpr() );
-        return Node::fromExpr( dt[ testerIndex ].getConstructor() );
-      }
-    //if (n-1) negative testers
-    } else if( !checkInst || lbl->size() == dt.getNumConstructors()-1 ) {
-      vector< bool > possibleCons;
-      possibleCons.resize( dt.getNumConstructors(), true );
-      if( !lbl->empty() ) {
-        for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-          TNode leqn = (*i);
-          possibleCons[ Datatype::indexOf( leqn[0].getOperator().toExpr() ) ] = false;
-        }
-      }
-      Node cons = Node::null();
-      for( unsigned int i=0; i<possibleCons.size(); i++ ) {
-        if( possibleCons[i] ) {
-          cons = Node::fromExpr( dt[ i ].getConstructor() );
-          if( !checkInst ) {
-            //if there is a selector, split
-            for( unsigned int j=0; j<dt[ i ].getNumArgs(); j++ ) {
-              Node s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[i][j].getSelector() ), tf );
-              if( d_selectors.find( s ) != d_selectors.end() ) {
-                Debug("datatypes") << "  getPosCons: found selector " << s << endl;
-                return cons;
-              }
-            }
-          }
-        }
-      }
-      if( !checkInst ) {
-        for( int i=0; i<(int)possibleCons.size(); i++ ) {
-          if( possibleCons[i] && !dt[ i ].isFinite() ) {
-            Debug("datatypes") << "Did not find selector for " << tf;
-            Debug("datatypes") << " and " << dt[ i ].getConstructor() << " is not finite." << endl;
-            return Node::null();
-          }
-        }
-      } else {
-        Assert( !cons.isNull() );
-      }
-      return cons;
-    }
-  }
-  return Node::null();
-}
-
 Node TheoryDatatypes::getValue(TNode n) {
   NodeManager* nodeManager = NodeManager::currentNM();
 
@@ -522,7 +511,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
     d_merge_pending[d_merge_pending.size()-1].push_back( pair< Node, Node >( a, b ) );
     return;
   }
-  Assert(d_conflict.isNull());
+  Assert(!hasConflict());
   a = find(a);
   b = find(b);
   if( a == b) {
@@ -566,15 +555,15 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   NodeBuilder<> explanation(kind::AND);
   if( a.getKind() == kind::APPLY_CONSTRUCTOR && b.getKind() == kind::APPLY_CONSTRUCTOR 
       && a.getOperator()!=b.getOperator() ){
-    explanation << d_cc.explain( a, b );
-    d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
+    Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b );
+    d_em.addNode( ccEq, &d_cce );
+    d_em.addNodeConflict( ccEq, Reason::idt_clash );
     Debug("datatypes") << "Clash " << a << " " << b << endl;
-    Debug("datatypes") << "Conflict is " << d_conflict << endl;
     return; 
   }
   Debug("datatypes-debug") << "Done clash" << endl;
 
-  Debug("datatypes") << "Set canon: "<< a << " " << b << endl;
+  Debug("datatypes-debug-pf") << "Set canon: "<< a << " " << b << endl;
   // b becomes the canon of a
   d_unionFind.setCanon(a, b);
   d_reps[a] = false;
@@ -601,7 +590,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
      * since the representative of b does not change and we check all the things
      * in a's class when we look at the diseq list of find(a)
      */
-
     EqLists::iterator deq_ib = d_disequalities.find(b);
     if(deq_ib != d_disequalities.end()) {
       EqList* deq = (*deq_ib).second;
@@ -626,7 +614,6 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
      * the side effect that it adds them to the list of b (which
      * became the canonical representative)
      */
-
     EqList* deqa = (*deq_ia).second;
     for(EqList::const_iterator i = deqa->begin(); i != deqa->end(); i++) {
       TNode deqn = (*i);
@@ -638,15 +625,13 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
       TNode tp = find(t);
       if(sp == tp) {
         Debug("datatypes") << "Construct standard conflict " << deqn << " " << sp << endl;
-        Node explanation = d_cc.explain(deqn[0], deqn[1]);
-        d_conflict = NodeManager::currentNM()->mkNode( kind::AND, explanation, deqn.notNode() );
-        Debug("datatypes") << "Conflict is " << d_conflict << endl;
+        d_em.addNode( deqn, &d_cce );
+        d_em.addNodeConflict( NodeManager::currentNM()->mkNode( kind::AND, deqn, deqn.notNode() ), Reason::contradiction );
         return;
       }
       Assert( sp == b || tp == b, "test2");
 
       // make sure not to add duplicates
-
       if(sp == b) {
         if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
           appendToDiseqList(b, deqn);
@@ -667,13 +652,12 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl;
   if( d_hasSeenCycle.get() ){
     checkCycles();
-    if( !d_conflict.isNull() ){
+    if( hasConflict() ){
       return;
     }
   }else{
     checkCycles();
-    if( !d_conflict.isNull() ){
-      Debug("datatypes-cycles") << "Cycle is " << d_conflict << std::endl;
+    if( hasConflict() ){
       for( int i=0; i<(int)d_currEqualities.size(); i++ ) {
         Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl;
       }
@@ -683,7 +667,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   }
 #else
   checkCycles();
-  if( !d_conflict.isNull() ){
+  if( hasConflict() ){
     return;
   }
 #endif
@@ -691,7 +675,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
 
   //merge selector lists
   updateSelectors( a );
-  if( !d_conflict.isNull() ){
+  if( hasConflict() ){
     return;
   }
   Debug("datatypes-debug") << "Done collapse" << endl;
@@ -702,8 +686,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
     EqList* lbl = (*lbl_i).second;
     if( !lbl->empty() ) {
       for( EqList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
-        checkTester( *i );
-        if( !d_conflict.isNull() ) {
+        addTester( *i );
+        if( hasConflict() ) {
           return;
         }
       }
@@ -712,15 +696,16 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   Debug("datatypes-debug") << "Done merge labels" << endl;
 
   //do unification
-  Assert( d_conflict.isNull() );
   if( a.getKind() == APPLY_CONSTRUCTOR && b.getKind() == APPLY_CONSTRUCTOR &&
       a.getOperator() == b.getOperator() ) {
     Debug("datatypes") << "Unification: " << a << " and " << b << "." << endl;
     for( int i=0; i<(int)a.getNumChildren(); i++ ) {
       if( find( a[i] ) != find( b[i] ) ) {
+        Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, a, b );
         Node newEq = NodeManager::currentNM()->mkNode( EQUAL, a[i], b[i] );
-        Node jEq = d_cc.explain(a, b);
-        addDerivedEquality( newEq, jEq );
+        d_em.addNode( ccEq, &d_cce );
+        d_em.addNode( newEq, ccEq, Reason::idt_unify );
+        addEquality( newEq );
       }
     }
   }
@@ -728,8 +713,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) {
   Debug("datatypes-debug") << "merge(): Done" << endl;
 }
 
-Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
-  if( t.getKind() == APPLY_SELECTOR ) {
+Node TheoryDatatypes::collapseSelector( Node t ) {
+  if( !hasConflict() && t.getKind() == APPLY_SELECTOR ) {
     //collapse constructor
     TypeNode typ = t[0].getType();
     Node sel = t.getOperator();
@@ -750,37 +735,51 @@ Node TheoryDatatypes::collapseSelector( TNode t, bool useContext ) {
         Debug("datatypes") << selType[1].mkGroundTerm() << " of type " << selType[1] << endl;
         retNode = selType[1].mkGroundTerm();
       }
-      if( useContext ) {
-        Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
-        d_axioms[neq] = true;
-        Debug("datatypes-split") << "Collapse selector " << neq << endl;
-        addEquality( neq );
+      if( tmp!=t[0] ){
+        t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, t.getOperator(), tmp );
       }
+      Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
+      d_em.addNodeAxiom( neq, Reason::idt_collapse );
+      Debug("datatypes") << "Collapse selector " << neq << endl;
+      addEquality( neq );
     } else {
-      if( useContext ) {
-        //check labels
-        Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp );
-        checkTester( tester, false );
-        if( !d_conflict.isNull() ) {
-          Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
-          retNode = selType[1].mkGroundTerm();
-
-          Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
-          NodeBuilder<> nb(kind::AND);
-          Node trueNode = NodeManager::currentNM()->mkConst(true);
-          if( d_conflict != trueNode ) {
-            nb << d_conflict;
-          }
-          d_conflict = Node::null();
-          tmp = find( tmp );
-          if( tmp != t[0] ) {
-            nb << d_cc.explain( tmp, t[0] );
+      //see whether we can prove that the selector is applied to the wrong tester
+      Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), tmp );
+      Node conflict;
+      unsigned r;
+      checkTester( tester, conflict, r );
+      if( !conflict.isNull() ) {
+        Debug("datatypes") << "Applied selector " << t << " to provably wrong constructor." << endl;
+        // conflict = c ^ tester, conflict => false
+        // want to say c => ~tester
+        //must remove tester from conflict
+        if( conflict.getKind()==kind::AND ){
+          NodeBuilder<> jt(kind::AND);
+          for( int i=0; i<(int)conflict.getNumChildren(); i++ ){
+            if( conflict[i]!=tester ){
+              jt << conflict[i];
+            }
           }
-          Assert( nb.getNumChildren()>0 );
-          Node jEq = nb.getNumChildren() == 1 ? nb.getChild( 0 ) : nb;
-          Debug("datatypes-drv") << "Collapse selector " << neq << endl;
-          addDerivedEquality( neq, jEq );
+          conflict = ( jt.getNumChildren()==1 ) ? jt.getChild( 0 ) : jt;
+        }else if( conflict==tester ){
+          conflict = Node::null();
+        }
+        if( conflict!=tester.notNode() ){
+          d_em.addNode( tester.notNode(), conflict, r );
         }
+
+        if( tmp != t[0] ) {
+          Node teq = NodeManager::currentNM()->mkNode( EQUAL, tmp, t[0] );
+          d_em.addNode( teq, &d_cce );
+          Node exp = NodeManager::currentNM()->mkNode( AND, tester.notNode(), teq );
+          tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( cn.getTester() ), t[0] );
+          d_em.addNode( tester.notNode(), exp, Reason::idt_tcong );
+        }
+        retNode = selType[1].mkGroundTerm();
+        Node neq = NodeManager::currentNM()->mkNode( EQUAL, retNode, t );
+
+        d_em.addNode( neq, tester.notNode(), Reason::idt_collapse2 );
+        addEquality( neq );
       }
     }
     return retNode;
@@ -809,21 +808,15 @@ void TheoryDatatypes::updateSelectors( Node a ) {
           }
           a = b;
         }
-        Debug("datatypes") << "Merge selector " << s << " into " << b << endl;
-        Debug("datatypes") << "Find is " << find( s[0] ) << endl;
-        Assert( s.getKind() == APPLY_SELECTOR &&
-                find( s[0] ) == b );
+        //Debug("datatypes") << "Merge selector " << s << " into " << b
+        //Debug("datatypes") << ", find is " << find( s[0] ) << endl;
+        Assert( s.getKind() == APPLY_SELECTOR && find( s[0] ) == b );
         if( b != s[0] ) {
           Node t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), b );
-          //add to labels
-          addTermToLabels( t );
-          merge( s, t );
-          s = t;
-          d_selectors[s] = true;
-          d_cc.addTerm( s );
+          d_cc.addTerm( t );
         }
-        s = collapseSelector( s, true );
-        if( !d_conflict.isNull() ) {
+        s = collapseSelector( s );
+        if( hasConflict() ) {
           return;
         }
         if( sel_b && s.getKind() == APPLY_SELECTOR ) {
@@ -845,6 +838,13 @@ void TheoryDatatypes::addTermToLabels( Node t ) {
       if(lbl_i == d_labels.end()) {
         EqList* lbl = new(getContext()->getCMM()) EqList(true, getContext(), false,
                                                 ContextMemoryAllocator<TNode>(getContext()->getCMM()));
+        //if there is only one constructor, then it must be
+        const Datatype& dt = ((DatatypeType)(t.getType()).toType()).getDatatype();
+        if( dt.getNumConstructors()==1 ){
+          Node tester = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), t );
+          addTester( tester );
+          d_em.addNodeAxiom( tester, Reason::idt_texhaust );
+        }
         d_labels.insertDataFromContextMemory(tmp, lbl);
       }
     }
@@ -882,7 +882,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
   }
   if( n.getKind() == APPLY_SELECTOR ) {
     if( d_selectors.find( n ) == d_selectors.end() ) {
-      Debug("datatypes-split") << "  Found selector " << n << endl;
+      Debug("datatypes") << "  Found selector " << n << endl;
       d_selectors[ n ] = true;
       d_cc.addTerm( n );
       Node tmp = find( n[0] );
@@ -892,9 +892,7 @@ void TheoryDatatypes::collectTerms( Node n ) {
       if( tmp != n[0] ) {
         s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp );
       }
-      Debug("datatypes-split") << "  Before collapse: " << s << endl;
-      s = collapseSelector( s, true );
-      Debug("datatypes-split") << "  After collapse: " << s << endl;
+      s = collapseSelector( s );
       if( s.getKind() == APPLY_SELECTOR ) {
         //add selector to selector eq list
         Debug("datatypes") << "  Add selector to list " << tmp << " " << n << endl;
@@ -937,30 +935,30 @@ void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) {
   //}
 }
 
-void TheoryDatatypes::addDerivedEquality(TNode eq, TNode jeq) {
-  Debug("datatypes-drv") << "Justification for " << eq << "is: " << jeq << "." << endl;
-  d_drv_map[eq] = jeq;
-  addEquality( eq );
-}
+#define DELAY_MERGE
 
 void TheoryDatatypes::addEquality(TNode eq) {
   Assert(eq.getKind() == kind::EQUAL ||
          eq.getKind() == kind::IFF);
-  if( eq[0] != eq[1] ) {
+  if( find( eq[0] ) != find( eq[1] ) ) {
     Debug("datatypes") << "Add equality " << eq << "." << endl;
+    Debug("datatypes-debug-pf") << "Add equality " << eq << "." << endl;
 
     //setup merge pending list
+#ifdef DELAY_MERGE
     d_merge_pending.push_back( vector< pair< Node, Node > >() );
     bool prevNoMerge = d_noMerge;
     d_noMerge = true;
+#endif
 
     d_cc.addTerm(eq[0]);
     d_cc.addTerm(eq[1]);
-    d_cc.addEquality(eq);
+    d_cce.assert(eq);
     if( Debug.isOn("datatypes") || Debug.isOn("datatypes-cycles") ){
       d_currEqualities.push_back(eq);
     }
 
+#ifdef DELAY_MERGE
     //record which nodes are waiting to be merged
     d_noMerge = prevNoMerge;
     vector< pair< Node, Node > > mp;
@@ -968,17 +966,20 @@ void TheoryDatatypes::addEquality(TNode eq) {
                d_merge_pending[d_merge_pending.size()-1].begin(), 
                d_merge_pending[d_merge_pending.size()-1].end() );
     d_merge_pending.pop_back();
+#endif
 
     //merge original nodes
-    if( d_conflict.isNull() ) {
-      merge(eq[0], eq[1]);
+    if( !hasConflict() ) {
+      merge( eq[0], eq[1] );
     }
+#ifdef DELAY_MERGE
     //merge nodes waiting to be merged
     for( int i=0; i<(int)mp.size(); i++ ) {
-      if( d_conflict.isNull() ) {
+      if( !hasConflict() ) {
         merge( mp[i].first, mp[i].second );
       }
     }
+#endif
   }
 }
 
@@ -993,44 +994,16 @@ void TheoryDatatypes::addDisequality(TNode eq) {
   appendToDiseqList(find(b), eq);
 }
 
-void TheoryDatatypes::throwConflict() {
-  Debug("datatypes") << "Convert conflict : " << d_conflict << endl;
-  NodeBuilder<> nb(kind::AND);
-  convertDerived( d_conflict, nb );
-  d_conflict = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
-  if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") ) {
-    cout << "Conflict constructed : " << d_conflict << endl;
-  }
-  //if( d_conflict.getKind()!=kind::AND ){
-  //  d_conflict = NodeManager::currentNM()->mkNode(kind::AND, d_conflict, d_conflict);
-  //}
-  d_out->conflict( d_conflict, false );
-  d_conflict = Node::null();
-}
-
-void TheoryDatatypes::convertDerived(Node n, NodeBuilder<>& nb) {
-  if( n.getKind() == kind::AND ) {
-    for( int i=0; i<(int)n.getNumChildren(); i++ ) {
-      convertDerived( n[i], nb );
-    }
-  } else if( !d_drv_map[ n ].get().isNull() ) {
-    //Debug("datatypes") << "Justification for " << n << " is " << d_drv_map[ n ].get() << endl;
-    convertDerived( d_drv_map[ n ].get(), nb );
-  } else if( d_axioms.find( n ) == d_axioms.end() ) {
-    nb << n;
-  }
-}
-
 void TheoryDatatypes::checkCycles() {
   for( BoolMap::iterator i = d_reps.begin(); i != d_reps.end(); i++ ) {
     if( (*i).second ) {
       map< Node, bool > visited;
       NodeBuilder<> explanation(kind::AND);
       if( searchForCycle( (*i).first, (*i).first, visited, explanation ) ) {
-        Assert( explanation.getNumChildren()>0 );
-        d_conflict = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
+        Node cCycle = explanation.getNumChildren() == 1 ? explanation.getChild( 0 ) : explanation;
+        d_em.addNodeConflict( cCycle, Reason::idt_cycle );
         Debug("datatypes") << "Detected cycle for " << (*i).first << endl;
-        Debug("datatypes") << "Conflict is " << d_conflict << endl;
+        Debug("datatypes") << "Conflict is " << cCycle << endl;
         return;
       }
     }
@@ -1052,19 +1025,12 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on,
             Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << n[i] << "!!!!" << std::endl;
           }
           if( nn != n[i] ) {
-            Node e = d_cc.explain( nn, n[i] );
             if( !d_cycle_check.isConnectedNode( n[i], nn ) ){
               Debug("datatypes-cycles") << "Cycle equality: " << n[i] << " is not -> " << nn << "!!!!" << std::endl;
-              Debug("datatypes-cycles") << "Explanation: " << e << std::endl;
-              if( e.getKind()==kind::AND ){
-                for( int a=0; a<e.getNumChildren(); a++ ){
-                  Debug("datatypes-cycles") << e[a][0] << " " << e[a][1] << " "
-                    << d_cycle_check.isConnectedNode( e[a][1], e[a][0] ) << " "
-                    << d_cycle_check.isConnectedNode( e[a][0], e[a][1] ) << std::endl;
-                }
-              }
             }
-            explanation << e;
+            Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, nn, n[i] );
+            d_em.addNode( ccEq, &d_cce );
+            explanation << ccEq;
           }
           return true;
         }

diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 1a944a6e0df9c58c0ac3f4aa0af4d43fb0548e01..1e715b4e47a4048114543f39208b399a41321582 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -27,6 +27,7 @@
 #include "theory/datatypes/union_find.h"
 #include "util/hash.h"
 #include "util/trans_closure.h"
+#include "theory/datatypes/explanation_manager.h"
 
 #include <ext/hash_set>
 #include <iostream>
@@ -48,10 +49,6 @@ private:
   context::CDList<Node> d_currAsserts;
   context::CDList<Node> d_currEqualities;
 
-  /** map from equalties and the equalities they are derived from */
-  context::CDMap< Node, Node, NodeHashFunction > d_drv_map;
-  /** equalities that are axioms */
-  BoolMap d_axioms;
   /** list of all selectors */
   BoolMap d_selectors;
   /** list of all representatives */
@@ -74,7 +71,8 @@ private:
   /**
    * map from terms to testers asserted for that term
    * for each t, this is either a list of equations of the form
-   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers,
+   *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers
+   *   and n is less than the number of possible constructors for t,
    * or a list of equations of the form
    *   NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t )  followed by
    *   is_[constructor_(n+1)]( t ), each of which is a unique tester.
@@ -120,20 +118,19 @@ private:
    * */
   EqLists d_disequalities;
 
-  /** List of all (potential) equalities to be propagated. */
-  EqLists d_equalities;
-
-  /**
-   * stores the conflicting disequality (still need to call construct
-   * conflict to get the actual explanation)
-   */
-  Node d_conflict;
   /**
    * information for delayed merging (is this necessary?)
    */
   bool d_noMerge;
   std::vector< std::vector< std::pair< Node, Node > > > d_merge_pending;
   bool d_inCheck;
+
+  /**
+   * explanation manager
+   */
+  ExplanationManager d_em;
+  CongruenceClosureExplainer<CongruenceChannel, CONGRUENCE_OPERATORS_2 (kind::APPLY_CONSTRUCTOR, kind::APPLY_SELECTOR)> d_cce;
+
 public:
   TheoryDatatypes(context::Context* c, OutputChannel& out, Valuation valuation);
   ~TheoryDatatypes();
@@ -149,33 +146,34 @@ public:
 
 private:
   /* Helper methods */
-  void checkTester( Node assertion, bool doAdd = true );
-  bool checkTrivialTester(Node assertion);
+  bool checkTester( Node assertion, Node& conflict, unsigned& r );
+  void addTester( Node assertion );
   void checkInstantiate( Node t );
-  Node getPossibleCons( Node t, bool checkInst = false );
-  Node collapseSelector( TNode t, bool useContext = false );
+  Node collapseSelector( Node t );
   void updateSelectors( Node a );
   void addTermToLabels( Node t );
   void initializeEqClass( Node t );
   void collectTerms( Node n );
+  bool hasConflict();
 
   /* from uf_morgan */
   void merge(TNode a, TNode b);
-  inline TNode find(TNode a);
+  inline TNode find(TNode a); 
   inline TNode debugFind(TNode a) const;
   void appendToDiseqList(TNode of, TNode eq);
   void addDisequality(TNode eq);
-  void addDerivedEquality(TNode eq, TNode jeq);
   void addEquality(TNode eq);
 
-  void convertDerived(Node n, NodeBuilder<>& nb);
-  void throwConflict();
   void checkCycles();
   bool searchForCycle( Node n, Node on,
                        std::map< Node, bool >& visited,
                        NodeBuilder<>& explanation );
 };/* class TheoryDatatypes */
 
+inline bool TheoryDatatypes::hasConflict() { 
+  return d_em.hasConflict(); 
+}
+
 inline TNode TheoryDatatypes::find(TNode a) {
   return d_unionFind.find(a);
 }