src/theory/datatypes/theory_datatypes.cpp

   1 /*********************                                                        */
   2 /*! \file theory_datatypes.cpp
   3  ** \verbatim
   4  ** Original author: Morgan Deters
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Dejan Jovanovic
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2013  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Implementation of the theory of datatypes
  13  **
  14  ** Implementation of the theory of datatypes.
  15  **/
  16
  17
  18 #include "theory/datatypes/theory_datatypes.h"
  19 #include "theory/valuation.h"
  20 #include "expr/kind.h"
  21 #include "util/datatype.h"
  22 #include "util/cvc4_assert.h"
  23 #include "theory/datatypes/datatypes_rewriter.h"
  24 #include "theory/datatypes/theory_datatypes_type_rules.h"
  25 #include "theory/model.h"
  26 #include "smt/options.h"
  27 #include "smt/boolean_terms.h"
  28 #include "theory/quantifiers/options.h"
  29
  30 #include <map>
  31
  32 using namespace std;
  33 using namespace CVC4;
  34 using namespace CVC4::kind;
  35 using namespace CVC4::context;
  36 using namespace CVC4::theory;
  37 using namespace CVC4::theory::datatypes;
  38
  39
  40 TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
  41   Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo, qe),
  42   d_cycle_check(c),
  43   d_hasSeenCycle(c, false),
  44   d_infer(c),
  45   d_infer_exp(c),
  46   d_notify( *this ),
  47   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
  48   d_selector_apps( c ),
  49   d_labels( c ),
  50   d_conflict( c, false ),
  51   d_collectTermsCache( c ){
  52
  53   // The kinds we are treating as function application in congruence
  54   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
  55   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR);
  56   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
  57 }
  58
  59 TheoryDatatypes::~TheoryDatatypes() {
  60 }
  61
  62 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  63   d_equalityEngine.setMasterEqualityEngine(eq);
  64 }
  65
  66 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake ){
  67   std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
  68   if( !hasEqcInfo( n ) ){
  69     if( doMake ){
  70       //add to labels
  71       NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
  72                                                              ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
  73       d_labels.insertDataFromContextMemory( n, lbl );
  74       EqcInfo* ei;
  75       if( eqc_i!=d_eqc_info.end() ){
  76         ei = eqc_i->second;
  77       }else{
  78         ei = new EqcInfo( getSatContext() );
  79         d_eqc_info[n] = ei;
  80       }
  81       if( n.getKind()==APPLY_CONSTRUCTOR ){
  82         ei->d_constructor = n;
  83       }
  84       return ei;
  85     }else{
  86       return NULL;
  87     }
  88   }else{
  89     return (*eqc_i).second;
  90   }
  91 }
  92
  93 void TheoryDatatypes::check(Effort e) {
  94
  95   while(!done() && !d_conflict) {
  96     // Get all the assertions
  97     Assertion assertion = get();
  98     TNode fact = assertion.assertion;
  99     Trace("datatypes-assert") << "Assert " << fact << std::endl;
 100
 101     TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
 102
 103     // extra debug check to make sure that the rewriter did its job correctly
 104     Assert( atom.getKind() != kind::EQUAL ||
 105             ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
 106               atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
 107               atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
 108               atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
 109               atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
 110               atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
 111             "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
 112
 113     //assert the fact
 114     assertFact( fact, fact );
 115     flushPendingFacts();
 116   }
 117
 118   if( e == EFFORT_FULL ) {
 119     Debug("datatypes-split") << "Check for splits " << e << endl;
 120     bool addedFact = false;
 121     do {
 122       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 123       while( !eqcs_i.isFinished() ){
 124         Node n = (*eqcs_i);
 125         if( DatatypesRewriter::isTermDatatype( n ) ){
 126           Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
 127           EqcInfo* eqc = getOrMakeEqcInfo( n, true );
 128           //if there are more than 1 possible constructors for eqc
 129           if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) {
 130             Trace("datatypes-debug") << "No constructor..." << std::endl;
 131             const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
 132             //if only one constructor, then this term must be this constructor
 133             if( dt.getNumConstructors()==1 ){
 134               Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
 135               d_pending.push_back( t );
 136               d_pending_exp[ t ] = NodeManager::currentNM()->mkConst( true );
 137               Trace("datatypes-infer") << "DtInfer : " << t << ", trivial" << std::endl;
 138               d_infer.push_back( t );
 139             }else{
 140               std::vector< bool > pcons;
 141               getPossibleCons( eqc, n, pcons );
 142               //std::cout << "pcons " << n << " = ";
 143               //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
 144               //std::cout << std::endl;
 145               //check if we do not need to resolve the constructor type for this equivalence class.
 146               // this is if there are no selectors for this equivalence class, its possible values are infinite,
 147               //  and we are not producing a model, then do not split.
 148               int consIndex = -1;
 149               bool needSplit = true;
 150               for( unsigned int j=0; j<pcons.size(); j++ ) {
 151                 if( pcons[j] ) {
 152                   if( consIndex==-1 ){
 153                     consIndex = j;
 154                   }
 155                   if( !dt[ j ].isFinite() && !eqc->d_selectors ) {
 156                     needSplit = false;
 157                   }
 158                 }
 159               }
 160               if( !needSplit && mustSpecifyAssignment() ){
 161                 //for the sake of termination, we must choose the constructor of a ground term
 162                 //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
 163                 //** TODO: this is probably not good enough, actually need fair enumeration strategy
 164                 Node groundTerm = n.getType().mkGroundTerm();
 165                 int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
 166                 if( pcons[index] ){
 167                   consIndex = index;
 168                 }
 169                 needSplit = true;
 170               }
 171               if( needSplit && consIndex!=-1 ) {
 172                 Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
 173                 Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
 174                 test = Rewriter::rewrite( test );
 175                 NodeBuilder<> nb(kind::OR);
 176                 nb << test << test.notNode();
 177                 Node lemma = nb;
 178                 d_out->lemma( lemma );
 179                 d_out->requirePhase( test, true );
 180                 return;
 181               }else{
 182                 Trace("dt-split") << "Do not split constructor for " << n << std::endl;
 183               }
 184             }
 185           }else{
 186             Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
 187           }
 188         }
 189         ++eqcs_i;
 190       }
 191       Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
 192       addedFact = !d_pending.empty();
 193       flushPendingFacts();
 194       if( !d_conflict ){
 195         if( options::dtRewriteErrorSel() ){
 196           collapseSelectors();
 197           flushPendingFacts();
 198           if( d_conflict ){
 199             return;
 200           }
 201         }
 202       }else{
 203         return;
 204       }
 205     }while( addedFact );
 206     Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
 207     if( !d_conflict ){
 208       Trace("dt-model-test") << std::endl;
 209       printModelDebug("dt-model-test");
 210     }
 211   }
 212
 213   if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
 214     Notice() << "TheoryDatatypes::check(): done" << endl;
 215   }
 216 }
 217
 218 void TheoryDatatypes::flushPendingFacts(){
 219   doPendingMerges();
 220   if( !d_pending.empty() ){
 221     int i = 0;
 222     while( !d_conflict && i<(int)d_pending.size() ){
 223       Node fact = d_pending[i];
 224       Node exp = d_pending_exp[ fact ];
 225       //check to see if we have to communicate it to the rest of the system
 226       if( mustCommunicateFact( fact, exp ) ){
 227         Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
 228         Node lem = fact;
 229         if( exp.isNull() || exp==NodeManager::currentNM()->mkConst( true ) ){
 230           lem = fact;
 231         }else{
 232           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
 233           Node ee_exp = explain( exp );
 234           Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
 235           lem = NodeManager::currentNM()->mkNode( IMPLIES, ee_exp, fact );
 236           lem = Rewriter::rewrite( lem );
 237         }
 238         Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
 239         d_out->lemma( lem );
 240       }else{
 241         assertFact( fact, exp );
 242       }
 243       i++;
 244     }
 245     d_pending.clear();
 246     d_pending_exp.clear();
 247   }
 248 }
 249
 250 void TheoryDatatypes::doPendingMerges(){
 251   //do all pending merges
 252   int i=0;
 253   while( i<(int)d_pending_merge.size() ){
 254     Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
 255     merge( d_pending_merge[i][0], d_pending_merge[i][1] );
 256     i++;
 257   }
 258   d_pending_merge.clear();
 259 }
 260
 261 void TheoryDatatypes::assertFact( Node fact, Node exp ){
 262   Assert( d_pending_merge.empty() );
 263   bool polarity = fact.getKind() != kind::NOT;
 264   TNode atom = polarity ? fact : fact[0];
 265   if (atom.getKind() == kind::EQUAL) {
 266     d_equalityEngine.assertEquality( atom, polarity, exp );
 267   }else{
 268     d_equalityEngine.assertPredicate( atom, polarity, exp );
 269   }
 270   doPendingMerges();
 271   //add to tester if applicable
 272   if( atom.getKind()==kind::APPLY_TESTER ){
 273     Node rep = getRepresentative( atom[0] );
 274     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
 275     addTester( fact, eqc, rep );
 276   }
 277   doPendingMerges();
 278 }
 279
 280 void TheoryDatatypes::preRegisterTerm(TNode n) {
 281   Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
 282   collectTerms( n );
 283   switch (n.getKind()) {
 284   case kind::EQUAL:
 285     // Add the trigger for equality
 286     d_equalityEngine.addTriggerEquality(n);
 287     break;
 288   case kind::APPLY_TESTER:
 289     // Get triggered for both equal and dis-equal
 290     d_equalityEngine.addTriggerPredicate(n);
 291     break;
 292   default:
 293     // Maybe it's a predicate
 294     if (n.getType().isBoolean()) {
 295       // Get triggered for both equal and dis-equal
 296       d_equalityEngine.addTriggerPredicate(n);
 297     } else {
 298       // Function applications/predicates
 299       d_equalityEngine.addTerm(n);
 300     }
 301     break;
 302   }
 303   flushPendingFacts();
 304 }
 305
 306 void TheoryDatatypes::presolve() {
 307   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 308 }
 309
 310 Node TheoryDatatypes::ppRewrite(TNode in) {
 311   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
 312
 313   if(in.getKind() == kind::TUPLE_SELECT) {
 314     TypeNode t = in[0].getType();
 315     if(t.hasAttribute(expr::DatatypeTupleAttr())) {
 316       t = t.getAttribute(expr::DatatypeTupleAttr());
 317     }
 318     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
 319     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 320     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
 321   } else if(in.getKind() == kind::RECORD_SELECT) {
 322     TypeNode t = in[0].getType();
 323     if(t.hasAttribute(expr::DatatypeRecordAttr())) {
 324       t = t.getAttribute(expr::DatatypeRecordAttr());
 325     }
 326     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
 327     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 328     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
 329   }
 330
 331   TypeNode t = in.getType();
 332
 333   // we only care about tuples and records here
 334   if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
 335      in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
 336     if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
 337       Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
 338       Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
 339       if(t.isTuple()) {
 340         Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
 341         Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
 342         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
 343       } else {
 344         Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
 345         Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
 346         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
 347       }
 348     }
 349     // nothing to do
 350     return in;
 351   }
 352
 353   if(t.hasAttribute(expr::DatatypeTupleAttr())) {
 354     t = t.getAttribute(expr::DatatypeTupleAttr());
 355   } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
 356     t = t.getAttribute(expr::DatatypeRecordAttr());
 357   }
 358
 359   // if the type doesn't have an associated datatype, then make one for it
 360   TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
 361
 362   const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 363
 364   // now rewrite the expression
 365   Node n;
 366   if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
 367     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 368     b << Node::fromExpr(dt[0].getConstructor());
 369     b.append(in.begin(), in.end());
 370     n = b;
 371   } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
 372     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 373     b << Node::fromExpr(dt[0].getConstructor());
 374     size_t size, updateIndex;
 375     if(in.getKind() == kind::TUPLE_UPDATE) {
 376       size = t.getNumChildren();
 377       updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
 378     } else { // kind::RECORD_UPDATE
 379       const Record& record = t.getConst<Record>();
 380       size = record.getNumFields();
 381       updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
 382     }
 383     Debug("tuprec") << "expr is " << in << std::endl;
 384     Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
 385     Debug("tuprec") << "t is " << t << std::endl;
 386     Debug("tuprec") << "t has arity " << size << std::endl;
 387     for(size_t i = 0; i < size; ++i) {
 388       if(i == updateIndex) {
 389         b << in[1];
 390         Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
 391       } else {
 392         b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, Node::fromExpr(dt[0][i].getSelector()), in[0]);
 393         Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
 394       }
 395     }
 396     Debug("tuprec") << "builder says " << b << std::endl;
 397     n = b;
 398   }
 399
 400   Assert(!n.isNull());
 401
 402   Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
 403
 404   return n;
 405 }
 406
 407 void TheoryDatatypes::addSharedTerm(TNode t) {
 408   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
 409                      << t << " " << t.getType().isBoolean() << endl;
 410   if( t.getType().isBoolean() ){
 411     //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
 412   }else{
 413     d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
 414   }
 415   Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 416 }
 417
 418 /** propagate */
 419 void TheoryDatatypes::propagate(Effort effort){
 420
 421 }
 422
 423 /** propagate */
 424 bool TheoryDatatypes::propagate(TNode literal){
 425   Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal  << ")" << std::endl;
 426   // If already in conflict, no more propagation
 427   if (d_conflict) {
 428     Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl;
 429     return false;
 430   }
 431   Trace("dt-prop") << "dtPropagate " << literal << std::endl;
 432   // Propagate out
 433   bool ok = d_out->propagate(literal);
 434   if (!ok) {
 435     d_conflict = true;
 436   }
 437   return ok;
 438 }
 439
 440 /** explain */
 441 void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
 442   Debug("datatypes-explain") << "Explain " << literal << std::endl;
 443   bool polarity = literal.getKind() != kind::NOT;
 444   TNode atom = polarity ? literal : literal[0];
 445   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 446     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 447   } else {
 448     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 449   }
 450 }
 451
 452 Node TheoryDatatypes::explain( TNode literal ){
 453   std::vector< TNode > assumptions;
 454   explain( literal, assumptions );
 455   if( assumptions.empty() ){
 456     return NodeManager::currentNM()->mkConst( true );
 457   }else if( assumptions.size()==1 ){
 458     return assumptions[0];
 459   }else{
 460     return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
 461   }
 462 }
 463
 464 /** Conflict when merging two constants */
 465 void TheoryDatatypes::conflict(TNode a, TNode b){
 466   if (a.getKind() == kind::CONST_BOOLEAN) {
 467     d_conflictNode = explain( a.iffNode(b) );
 468   } else {
 469     d_conflictNode = explain( a.eqNode(b) );
 470   }
 471   Debug("datatypes-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
 472   d_out->conflict( d_conflictNode );
 473   d_conflict = true;
 474 }
 475
 476 /** called when a new equivalance class is created */
 477 void TheoryDatatypes::eqNotifyNewClass(TNode t){
 478   if( t.getKind()==APPLY_CONSTRUCTOR ){
 479     getOrMakeEqcInfo( t, true );
 480   }
 481 }
 482
 483 /** called when two equivalance classes will merge */
 484 void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
 485
 486 }
 487
 488 /** called when two equivalance classes have merged */
 489 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
 490   if( DatatypesRewriter::isTermDatatype( t1 ) ){
 491     d_pending_merge.push_back( t1.eqNode( t2 ) );
 492   }
 493 }
 494
 495 void TheoryDatatypes::merge( Node t1, Node t2 ){
 496   if( !d_conflict ){
 497     Node trep1 = t1;
 498     Node trep2 = t2;
 499     Debug("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
 500     EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
 501     if( eqc2 ){
 502       bool checkInst = false;
 503       if( !eqc2->d_constructor.get().isNull() ){
 504         trep2 = eqc2->d_constructor.get();
 505       }
 506       EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
 507       if( eqc1 ){
 508         if( !eqc1->d_constructor.get().isNull() ){
 509           trep1 = eqc1->d_constructor.get();
 510         }
 511         //check for clash
 512         Node cons1 = eqc1->d_constructor;
 513         Node cons2 = eqc2->d_constructor;
 514         if( !cons1.isNull() && !cons2.isNull() ){
 515           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
 516           if( cons1.getOperator()!=cons2.getOperator() ){
 517             //check for clash
 518             d_conflictNode = explain( cons1.eqNode( cons2 ) );
 519             Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
 520             d_out->conflict( d_conflictNode );
 521             d_conflict = true;
 522             return;
 523           }else{
 524             //do unification
 525             Node unifEq = cons1.eqNode( cons2 );
 526             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
 527               if( cons1[i]!=cons2[i] ){
 528                 Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
 529                 d_pending.push_back( eq );
 530                 d_pending_exp[ eq ] = unifEq;
 531                 Trace("datatypes-infer") << "DtInfer : " << eq << " by " << unifEq << std::endl;
 532                 d_infer.push_back( eq );
 533                 d_infer_exp.push_back( unifEq );
 534               }
 535             }
 536           }
 537         }
 538         if( !eqc1->d_inst && eqc2->d_inst ){
 539           eqc1->d_inst = true;
 540         }
 541         if( cons1.isNull() && !cons2.isNull() ){
 542           checkInst = true;
 543           eqc1->d_constructor.set( eqc2->d_constructor );
 544         }
 545       }else{
 546         Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
 547         //just copy the equivalence class information
 548         eqc1 = getOrMakeEqcInfo( t1, true );
 549         eqc1->d_inst.set( eqc2->d_inst );
 550         eqc1->d_constructor.set( eqc2->d_constructor );
 551       }
 552       //merge labels
 553       Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
 554       NodeListMap::iterator lbl_i = d_labels.find( t2 );
 555       if( lbl_i != d_labels.end() ){
 556         NodeList* lbl = (*lbl_i).second;
 557         for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
 558           addTester( *j, eqc1, t1 );
 559           if( d_conflict ){
 560             return;
 561           }
 562         }
 563       }
 564       //merge selectors
 565       if( !eqc1->d_selectors && eqc2->d_selectors ){
 566         eqc1->d_selectors = true;
 567         checkInst = true;
 568       }
 569       if( checkInst ){
 570         instantiate( eqc1, t1 );
 571         if( d_conflict ){
 572           return;
 573         }
 574       }
 575     }
 576     //add this to the transitive closure module
 577     Node oldRep = trep2;
 578     Node newRep = trep1;
 579     if( trep1.getKind()!=APPLY_CONSTRUCTOR && trep2.getKind()==APPLY_CONSTRUCTOR ){
 580       oldRep = trep1;
 581       newRep = trep2;
 582     }
 583     bool result = d_cycle_check.addEdgeNode( oldRep, newRep );
 584     d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
 585     Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << d_hasSeenCycle.get() << endl;
 586     if( d_hasSeenCycle.get() ){
 587       checkCycles();
 588       if( d_conflict ){
 589         return;
 590       }
 591     }
 592   }
 593 }
 594
 595 /** called when two equivalence classes are made disequal */
 596 void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 597
 598 }
 599
 600 TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) :
 601 d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){
 602
 603 }
 604
 605 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
 606   return !eqc->d_constructor.get().isNull() || !getLabel( n ).isNull();
 607 }
 608
 609 Node TheoryDatatypes::getLabel( Node n ) {
 610   NodeListMap::iterator lbl_i = d_labels.find( n );
 611   if( lbl_i != d_labels.end() ){
 612     NodeList* lbl = (*lbl_i).second;
 613     if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()==kind::APPLY_TESTER ){
 614       return (*lbl)[ (*lbl).size() - 1 ];
 615     }
 616   }
 617   return Node::null();
 618 }
 619
 620 int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
 621   if( !eqc->d_constructor.get().isNull() ){
 622     return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
 623   }else{
 624     return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
 625   }
 626 }
 627
 628 void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){
 629   const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
 630   pcons.resize( dt.getNumConstructors(), !hasLabel( eqc, n ) );
 631   if( hasLabel( eqc, n ) ){
 632     pcons[ getLabelIndex( eqc, n ) ] = true;
 633   }else{
 634     NodeListMap::iterator lbl_i = d_labels.find( n );
 635     if( lbl_i != d_labels.end() ){
 636       NodeList* lbl = (*lbl_i).second;
 637       for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 638         Assert( (*i).getKind()==NOT );
 639         pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false;
 640       }
 641     }
 642   }
 643 }
 644
 645 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
 646   if( !d_conflict ){
 647     Debug("datatypes-labels") << "Add tester " << t << " " << eqc << std::endl;
 648     bool tpolarity = t.getKind()!=NOT;
 649     Node tt = ( t.getKind() == NOT ) ? t[0] : t;
 650     int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
 651     Node j, jt;
 652     if( hasLabel( eqc, n ) ){
 653       //if we already know the constructor type, check whether it is in conflict or redundant
 654       int jtindex = getLabelIndex( eqc, n );
 655       if( (jtindex==ttindex)!=tpolarity ){
 656         d_conflict = true;
 657         if( !eqc->d_constructor.get().isNull() ){
 658           //conflict because equivalence class contains a constructor
 659           std::vector< TNode > assumptions;
 660           explain( t, assumptions );
 661           explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions );
 662           d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
 663           Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
 664           d_out->conflict( d_conflictNode );
 665           return;
 666         }else{
 667           //conflict because the existing label is contradictory
 668           j = getLabel( n );
 669           jt = j;
 670         }
 671       }else{
 672         return;
 673       }
 674     }else{
 675       //otherwise, scan list of labels
 676       NodeListMap::iterator lbl_i = d_labels.find( n );
 677       Assert( lbl_i != d_labels.end() );
 678       NodeList* lbl = (*lbl_i).second;
 679       for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 680         Assert( (*i).getKind()==NOT );
 681         j = *i;
 682         jt = j[0];
 683         int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
 684         if( jtindex==ttindex ){
 685           if( tpolarity ){  //we are in conflict
 686             d_conflict = true;
 687             break;
 688           }else{            //it is redundant
 689             return;
 690           }
 691         }
 692       }
 693       if( !d_conflict ){
 694         Debug("datatypes-labels") << "Add to labels " << t << std::endl;
 695         lbl->push_back( t );
 696         const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype();
 697         Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
 698         if( tpolarity ){
 699           instantiate( eqc, n );
 700         }else{
 701           //check if we have reached the maximum number of testers
 702           // in this case, add the positive tester
 703           if( lbl->size()==dt.getNumConstructors()-1 ){
 704             std::vector< bool > pcons;
 705             getPossibleCons( eqc, n, pcons );
 706             int testerIndex = -1;
 707             for( int i=0; i<(int)pcons.size(); i++ ) {
 708               if( pcons[i] ){
 709                 testerIndex = i;
 710                 break;
 711               }
 712             }
 713             Assert( testerIndex!=-1 );
 714             //we must explain why each term in the set of testers for this equivalence class is equal
 715             std::vector< Node > eq_terms;
 716             NodeBuilder<> nb(kind::AND);
 717             for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 718               nb << (*i);
 719               if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){
 720                 eq_terms.push_back( (*i)[0][0] );
 721                 if( (*i)[0][0]!=tt[0] ){
 722                   nb << (*i)[0][0].eqNode( tt[0] );
 723                 }
 724               }
 725             }
 726             Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] );
 727             Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
 728             d_pending.push_back( t_concl );
 729             d_pending_exp[ t_concl ] = t_concl_exp;
 730             Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl;
 731             d_infer.push_back( t_concl );
 732             d_infer_exp.push_back( t_concl_exp );
 733             return;
 734           }
 735         }
 736       }
 737     }
 738     if( d_conflict ){
 739       std::vector< TNode > assumptions;
 740       explain( j, assumptions );
 741       explain( t, assumptions );
 742       explain( jt[0].eqNode( tt[0] ), assumptions );
 743       d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions );
 744       Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
 745       d_out->conflict( d_conflictNode );
 746     }
 747   }
 748 }
 749
 750 EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
 751   if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
 752     if (d_equalityEngine.areEqual(a, b)) {
 753       // The terms are implied to be equal
 754       return EQUALITY_TRUE;
 755     }
 756     if (d_equalityEngine.areDisequal(a, b, false)) {
 757       // The terms are implied to be dis-equal
 758       return EQUALITY_FALSE;
 759     }
 760   }
 761   return EQUALITY_UNKNOWN;
 762 }
 763
 764 void TheoryDatatypes::computeCareGraph(){
 765   Theory::computeCareGraph();
 766 }
 767
 768 void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
 769   Trace("dt-model") << std::endl;
 770   printModelDebug( "dt-model" );
 771   m->assertEqualityEngine( &d_equalityEngine );
 772   //must choose proper representatives
 773   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 774   while( !eqcs_i.isFinished() ){
 775     Node eqc = (*eqcs_i);
 776     //for all equivalence classes that are datatypes
 777     if( DatatypesRewriter::isTermDatatype( eqc ) ){
 778       EqcInfo* ei = getOrMakeEqcInfo( eqc );
 779       if( ei ){
 780         if( !ei->d_constructor.get().isNull() ){
 781           //specify that we should use the constructor as the representative
 782           m->assertRepresentative( ei->d_constructor.get() );
 783         }else{
 784           Trace("model-warn") << "WARNING: Datatypes: no constructor in equivalence class " << eqc << std::endl;
 785           Trace("model-warn") << "   Type : " << eqc.getType() << std::endl;
 786         }
 787       }else{
 788         Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl;
 789         Trace("model-warn") << "   Type : " << eqc.getType() << std::endl;
 790       }
 791     }
 792     ++eqcs_i;
 793   }
 794 }
 795
 796
 797 void TheoryDatatypes::collectTerms( Node n ) {
 798   if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
 799     d_collectTermsCache[n] = true;
 800     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
 801       collectTerms( n[i] );
 802     }
 803     if( n.getKind() == APPLY_CONSTRUCTOR ){
 804       //we must take into account subterm relation when checking for cycles
 805       for( int i=0; i<(int)n.getNumChildren(); i++ ) {
 806         Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl;
 807         bool result = d_cycle_check.addEdgeNode( n, n[i] );
 808         d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
 809       }
 810     }else if( n.getKind() == APPLY_SELECTOR ){
 811       if( d_selector_apps.find( n )==d_selector_apps.end() ){
 812         d_selector_apps[n] = false;
 813         //we must also record which selectors exist
 814         Debug("datatypes") << "  Found selector " << n << endl;
 815         if (n.getType().isBoolean()) {
 816           d_equalityEngine.addTriggerPredicate( n );
 817         }else{
 818           d_equalityEngine.addTerm( n );
 819         }
 820         Node rep = getRepresentative( n[0] );
 821         EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
 822         if( !eqc->d_selectors ){
 823           eqc->d_selectors = true;
 824           instantiate( eqc, rep );
 825         }
 826       }
 827     }
 828   }
 829 }
 830
 831 void TheoryDatatypes::processNewTerm( Node n ){
 832   Trace("dt-terms") << "Created term : " << n << std::endl;
 833   //see if it is rewritten to be something different
 834   Node rn = Rewriter::rewrite( n );
 835   if( rn!=n ){
 836     Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
 837     d_pending.push_back( eq );
 838     d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
 839     Trace("datatypes-infer") << "DtInfer : " << eq << ", trivial" << std::endl;
 840     d_infer.push_back( eq );
 841   }
 842 }
 843
 844 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){
 845   //if( !d_inst_map[n][index].isNull() ){
 846   //  return d_inst_map[n][index];
 847   //}else{
 848     //add constructor to equivalence class
 849     std::vector< Node > children;
 850     children.push_back( Node::fromExpr( dt[index].getConstructor() ) );
 851     for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){
 852       Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n );
 853       children.push_back( nc );
 854       processNewTerm( nc );
 855     }
 856     Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
 857     collectTerms( n_ic );
 858     //add type ascription for ambiguous constructor types
 859     if(!n_ic.getType().isComparableTo(n.getType())) {
 860       Assert( dt.isParametric() );
 861       Debug("datatypes-parametric") << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to " << n.getType() << std::endl;
 862       Debug("datatypes-parametric") << "Constructor is " << dt[index] << std::endl;
 863       Type tspec = dt[index].getSpecializedConstructorType(n.getType().toType());
 864       Debug("datatypes-parametric") << "Type specification is " << tspec << std::endl;
 865       children[0] = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION,
 866                                                      NodeManager::currentNM()->mkConst(AscriptionType(tspec)), children[0] );
 867       n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
 868       Assert( n_ic.getType()==n.getType() );
 869     }
 870     n_ic = Rewriter::rewrite( n_ic );
 871     //d_inst_map[n][index] = n_ic;
 872     return n_ic;
 873   //}
 874 }
 875
 876 void TheoryDatatypes::collapseSelectors(){
 877   //must check incorrect applications of selectors
 878   for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){
 879     if( !(*it).second ){
 880       Node n = getRepresentative( (*it).first[0] );
 881       Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n << std::endl;
 882       EqcInfo* ei = getOrMakeEqcInfo( n, true );
 883       if( ei ){
 884         if( !ei->d_constructor.get().isNull() ){
 885           Node op = (*it).first.getOperator();
 886           Node cons = ei->d_constructor;
 887           Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons );
 888           Node s = Rewriter::rewrite( sn );
 889           if( sn!=s ){
 890             Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn );
 891             d_pending.push_back( eq );
 892             d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true );
 893             Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl;
 894             d_infer.push_back( eq );
 895           }
 896           d_selector_apps[ (*it).first ] = true;
 897         }else{
 898           Trace("datatypes-collapse") << "No constructor." << std::endl;
 899         }
 900       }else{
 901         Trace("datatypes-collapse") << "No e info." << std::endl;
 902       }
 903     }
 904   }
 905 }
 906
 907 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
 908   //add constructor to equivalence class if not done so already
 909   if( hasLabel( eqc, n ) && !eqc->d_inst ){
 910     Node exp;
 911     Node tt;
 912     if( !eqc->d_constructor.get().isNull() ){
 913       exp = NodeManager::currentNM()->mkConst( true );
 914       tt = eqc->d_constructor;
 915     }else{
 916       exp = getLabel( n );
 917       tt = exp[0];
 918     }
 919     int index = getLabelIndex( eqc, n );
 920     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
 921     //must be finite or have a selector
 922     if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){
 923       //instantiate this equivalence class
 924       eqc->d_inst = true;
 925       Node tt_cons = getInstantiateCons( tt, dt, index );
 926       Node eq;
 927       if( tt!=tt_cons ){
 928         eq = tt.eqNode( tt_cons );
 929         Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
 930         d_pending.push_back( eq );
 931         d_pending_exp[ eq ] = exp;
 932         Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl;
 933         //eqc->d_inst.set( eq );
 934         d_infer.push_back( eq );
 935         d_infer_exp.push_back( exp );
 936       }
 937     }
 938   }
 939 }
 940
 941 void TheoryDatatypes::checkCycles() {
 942   Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
 943   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 944   while( !eqcs_i.isFinished() ){
 945     Node eqc = (*eqcs_i);
 946     map< Node, bool > visited;
 947     std::vector< TNode > expl;
 948     if( searchForCycle( eqc, eqc, visited, expl ) ) {
 949       Assert( expl.size()>0 );
 950       if( expl.size() == 1 ){
 951         d_conflictNode = expl[ 0 ];
 952       }else{
 953         d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl );
 954       }
 955       Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
 956       d_out->conflict( d_conflictNode );
 957       d_conflict = true;
 958       return;
 959     }
 960     ++eqcs_i;
 961   }
 962 }
 963
 964 //postcondition: if cycle detected, explanation is why n is a subterm of on
 965 bool TheoryDatatypes::searchForCycle( Node n, Node on,
 966                                       map< Node, bool >& visited,
 967                                       std::vector< TNode >& explanation, bool firstTime ) {
 968   Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl;
 969   Node ncons;
 970   Node nn;
 971   if( !firstTime ){
 972     nn = getRepresentative( n );
 973     if( nn==on ){
 974       Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn );
 975       explain( lit, explanation );
 976       return true;
 977     }
 978   }else{
 979     nn = n;
 980   }
 981   if( visited.find( nn ) == visited.end() ) {
 982     visited[nn] = true;
 983     EqcInfo* eqc = getOrMakeEqcInfo( nn );
 984     if( eqc ){
 985       Node ncons = eqc->d_constructor.get();
 986       if( !ncons.isNull() ) {
 987         for( int i=0; i<(int)ncons.getNumChildren(); i++ ) {
 988           if( searchForCycle( ncons[i], on, visited, explanation, false ) ) {
 989             if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
 990               Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
 991             }
 992             //add explanation for why the constructor is connected
 993             if( n != ncons ) {
 994               Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons );
 995               explain( lit, explanation );
 996             }
 997             return true;
 998           }
 999         }
1000       }
1001     }
1002   }
1003   return false;
1004 }
1005
1006 bool TheoryDatatypes::mustSpecifyAssignment(){
1007   //FIXME: the condition finiteModelFind is an over-approximation in this function
1008   //   we still may not want to specify assignments for datatypes that are truly infinite
1009   //   the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
1010   return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
1011   //return options::produceModels();
1012   //return false;
1013 }
1014
1015 bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
1016   //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine :
1017   //  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
1018   //  (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
1019   //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
1020   //We may need to communicate (3) outwards if the conclusions involve other theories
1021   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
1022   if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
1023     bool addLemma = false;
1024 #if 1
1025     const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype();
1026     addLemma = dt.involvesExternalType();
1027 #else
1028     for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
1029       if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
1030         addLemma = true;
1031         break;
1032       }
1033     }
1034 #endif
1035     if( addLemma ){
1036       //check if we have already added this lemma
1037       if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
1038         d_inst_lemmas[ n[0] ].push_back( n[1] );
1039         Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
1040         return true;
1041       }else{
1042         Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
1043         return false;
1044       }
1045     }
1046   }
1047   Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
1048   return false;
1049 }
1050
1051 bool TheoryDatatypes::hasTerm( Node a ){
1052   return d_equalityEngine.hasTerm( a );
1053 }
1054
1055 bool TheoryDatatypes::areEqual( Node a, Node b ){
1056   if( a==b ){
1057     return true;
1058   }else if( hasTerm( a ) && hasTerm( b ) ){
1059     return d_equalityEngine.areEqual( a, b );
1060   }else{
1061     return false;
1062   }
1063 }
1064
1065 bool TheoryDatatypes::areDisequal( Node a, Node b ){
1066   if( a==b ){
1067     return false;
1068   }else if( hasTerm( a ) && hasTerm( b ) ){
1069     return d_equalityEngine.areDisequal( a, b, false );
1070   }else{
1071     return false;
1072   }
1073 }
1074
1075 Node TheoryDatatypes::getRepresentative( Node a ){
1076   if( hasTerm( a ) ){
1077     return d_equalityEngine.getRepresentative( a );
1078   }else{
1079     return a;
1080   }
1081 }
1082
1083
1084 void TheoryDatatypes::printModelDebug( const char* c ){
1085   if(! (Trace.isOn(c))) {
1086     return;
1087   }
1088
1089   Trace( c ) << "Datatypes model : " << std::endl;
1090   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1091   while( !eqcs_i.isFinished() ){
1092     Node eqc = (*eqcs_i);
1093     if( DatatypesRewriter::isTermDatatype( eqc ) ){
1094       Trace( c ) << "DATATYPE : ";
1095     }
1096     Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
1097     Trace( c ) << "   { ";
1098     //add terms to model
1099     eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1100     while( !eqc_i.isFinished() ){
1101       Trace( c ) << (*eqc_i) << " ";
1102       ++eqc_i;
1103     }
1104     Trace( c ) << "}" << std::endl;
1105     if( DatatypesRewriter::isTermDatatype( eqc ) ){
1106       EqcInfo* ei = getOrMakeEqcInfo( eqc );
1107       if( ei ){
1108         Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
1109         if( ei->d_constructor.get().isNull() ){
1110           Trace("model-warn") << eqc << " has no constructor in equivalence class!" << std::endl;
1111           Trace("model-warn") << "  Type : " << eqc.getType() << std::endl;
1112           Trace( c ) << "   Constructor : " << std::endl;
1113           Trace( c ) << "   Labels : ";
1114           if( hasLabel( ei, eqc ) ){
1115             Trace( c ) << getLabel( eqc );
1116           }else{
1117             NodeListMap::iterator lbl_i = d_labels.find( eqc );
1118             if( lbl_i != d_labels.end() ){
1119               NodeList* lbl = (*lbl_i).second;
1120               for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
1121                 Trace( c ) << *j << " ";
1122               }
1123             }
1124           }
1125           Trace( c ) << std::endl;
1126         }else{
1127           Trace( c ) << "   Constructor : " << ei->d_constructor.get() << std::endl;
1128         }
1129         Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl;
1130       }
1131     }
1132     ++eqcs_i;
1133   }
1134 }