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-2014  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/theory_model.h"
  26 #include "smt/options.h"
  27 #include "smt/boolean_terms.h"
  28 #include "theory/quantifiers/options.h"
  29 #include "theory/datatypes/options.h"
  30 #include "theory/type_enumerator.h"
  31
  32 #include <map>
  33
  34 using namespace std;
  35 using namespace CVC4;
  36 using namespace CVC4::kind;
  37 using namespace CVC4::context;
  38 using namespace CVC4::theory;
  39 using namespace CVC4::theory::datatypes;
  40
  41
  42 TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
  43   Theory(THEORY_DATATYPES, c, u, out, valuation, logicInfo),
  44   //d_cycle_check(c),
  45   d_hasSeenCycle(c, false),
  46   d_infer(c),
  47   d_infer_exp(c),
  48   d_notify( *this ),
  49   d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"),
  50   d_labels( c ),
  51   d_selector_apps( c ),
  52   d_consEqc( c ),
  53   d_conflict( c, false ),
  54   d_collectTermsCache( c ),
  55   d_consTerms( c ),
  56   d_selTerms( c ){
  57
  58   // The kinds we are treating as function application in congruence
  59   d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR);
  60   d_equalityEngine.addFunctionKind(kind::APPLY_SELECTOR_TOTAL);
  61   d_equalityEngine.addFunctionKind(kind::APPLY_TESTER);
  62   d_equalityEngine.addFunctionKind(kind::APPLY_UF);
  63
  64   d_true = NodeManager::currentNM()->mkConst( true );
  65   d_dtfCounter = 0;
  66 }
  67
  68 TheoryDatatypes::~TheoryDatatypes() {
  69 }
  70
  71 void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  72   d_equalityEngine.setMasterEqualityEngine(eq);
  73 }
  74
  75 TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMake ){
  76   if( !hasEqcInfo( n ) ){
  77     if( doMake ){
  78       //add to labels
  79       NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
  80                                                              ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
  81       d_labels.insertDataFromContextMemory( n, lbl );
  82
  83       std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
  84       EqcInfo* ei;
  85       if( eqc_i!=d_eqc_info.end() ){
  86         ei = eqc_i->second;
  87       }else{
  88         ei = new EqcInfo( getSatContext() );
  89         d_eqc_info[n] = ei;
  90       }
  91       if( n.getKind()==APPLY_CONSTRUCTOR ){
  92         ei->d_constructor = n;
  93       }
  94       //add to selectors
  95       NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false,
  96                                                                ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) );
  97       d_selector_apps.insertDataFromContextMemory( n, sel );
  98       return ei;
  99     }else{
 100       return NULL;
 101     }
 102   }else{
 103     std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
 104     return (*eqc_i).second;
 105   }
 106 }
 107
 108 TNode TheoryDatatypes::getEqcConstructor( TNode r ) {
 109   if( r.getKind()==APPLY_CONSTRUCTOR ){
 110     return r;
 111   }else{
 112     EqcInfo * ei = getOrMakeEqcInfo( r, false );
 113     if( ei && !ei->d_constructor.get().isNull() ){
 114       return ei->d_constructor.get();
 115     }else{
 116       return r;
 117     }
 118   }
 119 }
 120
 121 void TheoryDatatypes::check(Effort e) {
 122   Trace("datatypes-debug") << "Check effort " << e << std::endl;
 123   while(!done() && !d_conflict) {
 124     // Get all the assertions
 125     Assertion assertion = get();
 126     TNode fact = assertion.assertion;
 127     Trace("datatypes-assert") << "Assert " << fact << std::endl;
 128
 129     TNode atom CVC4_UNUSED = fact.getKind() == kind::NOT ? fact[0] : fact;
 130
 131     // extra debug check to make sure that the rewriter did its job correctly
 132     Assert( atom.getKind() != kind::EQUAL ||
 133             ( atom[0].getKind() != kind::TUPLE && atom[1].getKind() != kind::TUPLE &&
 134               atom[0].getKind() != kind::RECORD && atom[1].getKind() != kind::RECORD &&
 135               atom[0].getKind() != kind::TUPLE_UPDATE && atom[1].getKind() != kind::TUPLE_UPDATE &&
 136               atom[0].getKind() != kind::RECORD_UPDATE && atom[1].getKind() != kind::RECORD_UPDATE &&
 137               atom[0].getKind() != kind::TUPLE_SELECT && atom[1].getKind() != kind::TUPLE_SELECT &&
 138               atom[0].getKind() != kind::RECORD_SELECT && atom[1].getKind() != kind::RECORD_SELECT ),
 139             "tuple/record escaped into datatypes decision procedure; should have been rewritten away" );
 140
 141     //assert the fact
 142     assertFact( fact, fact );
 143     flushPendingFacts();
 144   }
 145
 146   if( e == EFFORT_FULL && !d_conflict ) {
 147     //check for cycles
 148     bool addedFact;
 149     do {
 150       checkCycles();
 151       addedFact = !d_pending.empty() || !d_pending_merge.empty();
 152       flushPendingFacts();
 153       if( d_conflict ){
 154         return;
 155       }
 156     }while( addedFact );
 157
 158     //check for splits
 159     Debug("datatypes-split") << "Check for splits " << e << endl;
 160     addedFact = false;
 161     do {
 162       eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 163       while( !eqcs_i.isFinished() ){
 164         Node n = (*eqcs_i);
 165         TypeNode tn = n.getType();
 166         if( DatatypesRewriter::isTypeDatatype( tn ) ){
 167           Trace("datatypes-debug") << "Process equivalence class " << n << std::endl;
 168           EqcInfo* eqc = getOrMakeEqcInfo( n, true );
 169           //if there are more than 1 possible constructors for eqc
 170           if( eqc->d_constructor.get().isNull() && !hasLabel( eqc, n ) ) {
 171             Trace("datatypes-debug") << "No constructor..." << std::endl;
 172             const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
 173
 174             std::vector< bool > pcons;
 175             getPossibleCons( eqc, n, pcons );
 176             //std::cout << "pcons " << n << " = ";
 177             //for( int i=0; i<(int)pcons.size(); i++ ){ //std::cout << pcons[i] << " "; }
 178             //std::cout << std::endl;
 179             //check if we do not need to resolve the constructor type for this equivalence class.
 180             // this is if there are no selectors for this equivalence class, its possible values are infinite,
 181             //  and we are not producing a model, then do not split.
 182             int consIndex = -1;
 183             bool needSplit = true;
 184             for( unsigned int j=0; j<pcons.size(); j++ ) {
 185               if( pcons[j] ) {
 186                 if( consIndex==-1 ){
 187                   consIndex = j;
 188                 }
 189                 if( !dt[ j ].isFinite() && !eqc->d_selectors ) {
 190                   needSplit = false;
 191                 }
 192               }
 193             }
 194             //d_dtfCounter++;
 195             if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
 196               //for the sake of termination, we must choose the constructor of a ground term
 197               //NEED GUARENTEE: groundTerm should not contain any subterms of the same type
 198               // TODO: this is probably not good enough, actually need fair enumeration strategy
 199               if( !n.getType().isRecord() ){ //FIXME
 200                 Node groundTerm = n.getType().mkGroundTerm();
 201                 if( groundTerm.getOperator().getType().isConstructor() ){ //FIXME
 202                   int index = Datatype::indexOf( groundTerm.getOperator().toExpr() );
 203                   if( pcons[index] ){
 204                     consIndex = index;
 205                   }
 206                   needSplit = true;
 207                 }
 208               }
 209             }
 210
 211             if( needSplit && consIndex!=-1 ) {
 212               //if only one constructor, then this term must be this constructor
 213               if( dt.getNumConstructors()==1 ){
 214                 Node t = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[0].getTester() ), n );
 215                 d_pending.push_back( t );
 216                 d_pending_exp[ t ] = d_true;
 217                 Trace("datatypes-infer") << "DtInfer : 1-cons : " << t << std::endl;
 218                 d_infer.push_back( t );
 219               }else{
 220                   Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n );
 221                   Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n <<  endl;
 222                   test = Rewriter::rewrite( test );
 223                   NodeBuilder<> nb(kind::OR);
 224                   nb << test << test.notNode();
 225                   Node lemma = nb;
 226                   d_out->lemma( lemma );
 227                   d_out->requirePhase( test, true );
 228                   return;
 229               }
 230             }else{
 231               Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl;
 232             }
 233
 234           }else{
 235             Trace("datatypes-debug") << "Has constructor " << eqc->d_constructor.get() << std::endl;
 236           }
 237         }
 238         ++eqcs_i;
 239       }
 240       Trace("datatypes-debug") << "Flush pending facts..."  << std::endl;
 241       addedFact = !d_pending.empty() || !d_pending_merge.empty();
 242       flushPendingFacts();
 243       /*
 244       if( !d_conflict ){
 245         if( options::dtRewriteErrorSel() ){
 246           bool innerAddedFact = false;
 247           do {
 248             collapseSelectors();
 249             innerAddedFact = !d_pending.empty() || !d_pending_merge.empty();
 250             flushPendingFacts();
 251           }while( !d_conflict && innerAddedFact );
 252         }
 253       }
 254       */
 255     }while( !d_conflict && addedFact );
 256     Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl;
 257     if( !d_conflict ){
 258       Trace("dt-model-test") << std::endl;
 259       printModelDebug("dt-model-test");
 260     }
 261   }
 262
 263   if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") ) {
 264     Notice() << "TheoryDatatypes::check(): done" << endl;
 265   }
 266 }
 267
 268 void TheoryDatatypes::flushPendingFacts(){
 269   doPendingMerges();
 270   if( !d_pending.empty() ){
 271     int i = 0;
 272     while( !d_conflict && i<(int)d_pending.size() ){
 273       Node fact = d_pending[i];
 274       Node exp = d_pending_exp[ fact ];
 275       //check to see if we have to communicate it to the rest of the system
 276       if( mustCommunicateFact( fact, exp ) ){
 277         Trace("dt-lemma-debug") << "Assert fact " << fact << " " << exp << std::endl;
 278         Node lem = fact;
 279         if( exp.isNull() || exp==d_true ){
 280           lem = fact;
 281         }else{
 282           Trace("dt-lemma-debug") << "Get explanation..." << std::endl;
 283           Node ee_exp = explain( exp );
 284           Trace("dt-lemma-debug") << "Explanation : " << ee_exp << std::endl;
 285           lem = NodeManager::currentNM()->mkNode( IMPLIES, ee_exp, fact );
 286           lem = Rewriter::rewrite( lem );
 287         }
 288         Trace("dt-lemma") << "Datatypes lemma : " << lem << std::endl;
 289         d_out->lemma( lem );
 290       }else{
 291         assertFact( fact, exp );
 292       }
 293       i++;
 294     }
 295     d_pending.clear();
 296     d_pending_exp.clear();
 297   }
 298 }
 299
 300 void TheoryDatatypes::doPendingMerges(){
 301   //do all pending merges
 302   int i=0;
 303   while( i<(int)d_pending_merge.size() ){
 304     Assert( d_pending_merge[i].getKind()==EQUAL || d_pending_merge[i].getKind()==IFF );
 305     merge( d_pending_merge[i][0], d_pending_merge[i][1] );
 306     i++;
 307   }
 308   d_pending_merge.clear();
 309 }
 310
 311 void TheoryDatatypes::assertFact( Node fact, Node exp ){
 312   Assert( d_pending_merge.empty() );
 313   bool polarity = fact.getKind() != kind::NOT;
 314   TNode atom = polarity ? fact : fact[0];
 315   if (atom.getKind() == kind::EQUAL) {
 316     d_equalityEngine.assertEquality( atom, polarity, exp );
 317   }else{
 318     d_equalityEngine.assertPredicate( atom, polarity, exp );
 319   }
 320   doPendingMerges();
 321   //add to tester if applicable
 322   if( atom.getKind()==kind::APPLY_TESTER ){
 323     Node rep = getRepresentative( atom[0] );
 324     EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
 325     addTester( fact, eqc, rep );
 326   }
 327   doPendingMerges();
 328 }
 329
 330 void TheoryDatatypes::preRegisterTerm(TNode n) {
 331   Debug("datatypes-prereg") << "TheoryDatatypes::preRegisterTerm() " << n << endl;
 332   collectTerms( n );
 333   switch (n.getKind()) {
 334   case kind::EQUAL:
 335     // Add the trigger for equality
 336     d_equalityEngine.addTriggerEquality(n);
 337     break;
 338   case kind::APPLY_TESTER:
 339     // Get triggered for both equal and dis-equal
 340     d_equalityEngine.addTriggerPredicate(n);
 341     break;
 342   default:
 343     // Maybe it's a predicate
 344     if (n.getType().isBoolean()) {
 345       // Get triggered for both equal and dis-equal
 346       d_equalityEngine.addTriggerPredicate(n);
 347     } else {
 348       // Function applications/predicates
 349       d_equalityEngine.addTerm(n);
 350     }
 351     break;
 352   }
 353   flushPendingFacts();
 354 }
 355
 356 Node TheoryDatatypes::expandDefinition(LogicRequest &logicRequest, Node n) {
 357   switch( n.getKind() ){
 358   case kind::APPLY_SELECTOR: {
 359     Node selector = n.getOperator();
 360     Expr selectorExpr = selector.toExpr();
 361     Node sel = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, Node::fromExpr( selectorExpr ), n[0] );
 362     if( options::dtRewriteErrorSel() ){
 363       return sel;
 364     }else{
 365       size_t selectorIndex = Datatype::cindexOf(selectorExpr);
 366       const Datatype& dt = Datatype::datatypeOf(selectorExpr);
 367       const DatatypeConstructor& c = dt[selectorIndex];
 368       Expr tester = c.getTester();
 369       Node tst = NodeManager::currentNM()->mkNode( kind::APPLY_TESTER, Node::fromExpr( tester ), n[0] );
 370       tst = Rewriter::rewrite( tst );
 371       Node n_ret;
 372       if( tst==d_true ){
 373         n_ret = sel;
 374       }else{
 375         if( d_exp_def_skolem.find( selector )==d_exp_def_skolem.end() ){
 376           std::stringstream ss;
 377           ss << selector << "_uf";
 378           d_exp_def_skolem[ selector ] = NodeManager::currentNM()->mkSkolem( ss.str().c_str(),
 379                                             NodeManager::currentNM()->mkFunctionType( n[0].getType(), n.getType() ) );
 380         }
 381         Node sk = NodeManager::currentNM()->mkNode( kind::APPLY_UF, d_exp_def_skolem[ selector ], n[0]  );
 382         if( tst==NodeManager::currentNM()->mkConst( false ) ){
 383           n_ret = sk;
 384         }else{
 385           n_ret = NodeManager::currentNM()->mkNode( kind::ITE, tst, sel, sk );
 386         }
 387       }
 388       //n_ret = Rewriter::rewrite( n_ret );
 389       Trace("dt-expand") << "Expand def : " << n << " to " << n_ret << std::endl;
 390       return n_ret;
 391     }
 392   }
 393     break;
 394   default:
 395     return n;
 396     break;
 397   }
 398   Unreachable();
 399 }
 400
 401 void TheoryDatatypes::presolve() {
 402   Debug("datatypes") << "TheoryDatatypes::presolve()" << endl;
 403 }
 404
 405 Node TheoryDatatypes::ppRewrite(TNode in) {
 406   Debug("tuprec") << "TheoryDatatypes::ppRewrite(" << in << ")" << endl;
 407
 408   if(in.getKind() == kind::TUPLE_SELECT) {
 409     TypeNode t = in[0].getType();
 410     if(t.hasAttribute(expr::DatatypeTupleAttr())) {
 411       t = t.getAttribute(expr::DatatypeTupleAttr());
 412     }
 413     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
 414     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 415     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<TupleSelect>().getIndex()].getSelector()), in[0]);
 416   } else if(in.getKind() == kind::RECORD_SELECT) {
 417     TypeNode t = in[0].getType();
 418     if(t.hasAttribute(expr::DatatypeRecordAttr())) {
 419       t = t.getAttribute(expr::DatatypeRecordAttr());
 420     }
 421     TypeNode dtt = NodeManager::currentNM()->getDatatypeForTupleRecord(t);
 422     const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 423     return NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][in.getOperator().getConst<RecordSelect>().getField()].getSelector()), in[0]);
 424   }
 425
 426   TypeNode t = in.getType();
 427
 428   // we only care about tuples and records here
 429   if(in.getKind() != kind::TUPLE && in.getKind() != kind::TUPLE_UPDATE &&
 430      in.getKind() != kind::RECORD && in.getKind() != kind::RECORD_UPDATE) {
 431     if((t.isTuple() || t.isRecord()) && in.hasAttribute(smt::BooleanTermAttr())) {
 432       Debug("tuprec") << "should map " << in << " of type " << t << " back to " << in.getAttribute(smt::BooleanTermAttr()).getType() << endl;
 433       Debug("tuprec") << "so " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getDatatype() << " goes to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getDatatype() << endl;
 434       if(t.isTuple()) {
 435         Debug("tuprec") << "current datatype-tuple-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeTupleAttr()) << endl;
 436         Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()) << endl;
 437         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeTupleAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeTupleAttr()));
 438       } else {
 439         Debug("tuprec") << "current datatype-record-attr is " << NodeManager::currentNM()->getDatatypeForTupleRecord(t).getAttribute(expr::DatatypeRecordAttr()) << endl;
 440         Debug("tuprec") << "setting to " << NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()) << endl;
 441         NodeManager::currentNM()->getDatatypeForTupleRecord(t).setAttribute(expr::DatatypeRecordAttr(), NodeManager::currentNM()->getDatatypeForTupleRecord(in.getAttribute(smt::BooleanTermAttr()).getType()).getAttribute(expr::DatatypeRecordAttr()));
 442       }
 443     }
 444
 445     if( in.getKind()==EQUAL ){
 446       Node nn;
 447       std::vector< Node > rew;
 448       if( DatatypesRewriter::checkClash(in[0], in[1], rew) ){
 449         nn = NodeManager::currentNM()->mkConst(false);
 450       }else{
 451         nn = rew.size()==0 ? d_true :
 452                   ( rew.size()==1 ? rew[0] : NodeManager::currentNM()->mkNode( kind::AND, rew ) );
 453       }
 454       return nn;
 455     }
 456
 457     // nothing to do
 458     return in;
 459   }
 460
 461   if(t.hasAttribute(expr::DatatypeTupleAttr())) {
 462     t = t.getAttribute(expr::DatatypeTupleAttr());
 463   } else if(t.hasAttribute(expr::DatatypeRecordAttr())) {
 464     t = t.getAttribute(expr::DatatypeRecordAttr());
 465   }
 466
 467   // if the type doesn't have an associated datatype, then make one for it
 468   TypeNode dtt = (t.isTuple() || t.isRecord()) ? NodeManager::currentNM()->getDatatypeForTupleRecord(t) : t;
 469
 470   const Datatype& dt = DatatypeType(dtt.toType()).getDatatype();
 471
 472   // now rewrite the expression
 473   Node n;
 474   if(in.getKind() == kind::TUPLE || in.getKind() == kind::RECORD) {
 475     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 476     b << Node::fromExpr(dt[0].getConstructor());
 477     b.append(in.begin(), in.end());
 478     n = b;
 479   } else if(in.getKind() == kind::TUPLE_UPDATE || in.getKind() == kind::RECORD_UPDATE) {
 480     NodeBuilder<> b(kind::APPLY_CONSTRUCTOR);
 481     b << Node::fromExpr(dt[0].getConstructor());
 482     size_t size, updateIndex;
 483     if(in.getKind() == kind::TUPLE_UPDATE) {
 484       size = t.getNumChildren();
 485       updateIndex = in.getOperator().getConst<TupleUpdate>().getIndex();
 486     } else { // kind::RECORD_UPDATE
 487       const Record& record = t.getConst<Record>();
 488       size = record.getNumFields();
 489       updateIndex = record.getIndex(in.getOperator().getConst<RecordUpdate>().getField());
 490     }
 491     Debug("tuprec") << "expr is " << in << std::endl;
 492     Debug("tuprec") << "updateIndex is " << updateIndex << std::endl;
 493     Debug("tuprec") << "t is " << t << std::endl;
 494     Debug("tuprec") << "t has arity " << size << std::endl;
 495     for(size_t i = 0; i < size; ++i) {
 496       if(i == updateIndex) {
 497         b << in[1];
 498         Debug("tuprec") << "arg " << i << " gets updated to " << in[1] << std::endl;
 499       } else {
 500         b << NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, Node::fromExpr(dt[0][i].getSelector()), in[0]);
 501         Debug("tuprec") << "arg " << i << " copies " << b[b.getNumChildren() - 1] << std::endl;
 502       }
 503     }
 504     Debug("tuprec") << "builder says " << b << std::endl;
 505     n = b;
 506   }
 507
 508   Assert(!n.isNull());
 509
 510
 511   Debug("tuprec") << "REWROTE " << in << " to " << n << std::endl;
 512
 513   return n;
 514 }
 515
 516 void TheoryDatatypes::addSharedTerm(TNode t) {
 517   Debug("datatypes") << "TheoryDatatypes::addSharedTerm(): "
 518                      << t << " " << t.getType().isBoolean() << endl;
 519   if( t.getType().isBoolean() ){
 520     //d_equalityEngine.addTriggerPredicate(t, THEORY_DATATYPES);
 521   }else{
 522     d_equalityEngine.addTriggerTerm(t, THEORY_DATATYPES);
 523   }
 524   Debug("datatypes") << "TheoryDatatypes::addSharedTerm() finished" << std::endl;
 525 }
 526
 527 /** propagate */
 528 void TheoryDatatypes::propagate(Effort effort){
 529
 530 }
 531
 532 /** propagate */
 533 bool TheoryDatatypes::propagate(TNode literal){
 534   Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal  << ")" << std::endl;
 535   // If already in conflict, no more propagation
 536   if (d_conflict) {
 537     Debug("dt::propagate") << "TheoryDatatypes::propagate(" << literal << "): already in conflict" << std::endl;
 538     return false;
 539   }
 540   Trace("dt-prop") << "dtPropagate " << literal << std::endl;
 541   // Propagate out
 542   bool ok = d_out->propagate(literal);
 543   if (!ok) {
 544     d_conflict = true;
 545   }
 546   return ok;
 547 }
 548
 549 void TheoryDatatypes::addAssumptions( std::vector<TNode>& assumptions, std::vector<TNode>& tassumptions ) {
 550   for( unsigned i=0; i<tassumptions.size(); i++ ){
 551     if( std::find( assumptions.begin(), assumptions.end(), tassumptions[i] )==assumptions.end() ){
 552       assumptions.push_back( tassumptions[i] );
 553     }
 554   }
 555 }
 556
 557 void TheoryDatatypes::explainEquality( TNode a, TNode b, bool polarity, std::vector<TNode>& assumptions ) {
 558   if( a!=b ){
 559     std::vector<TNode> tassumptions;
 560     d_equalityEngine.explainEquality(a, b, polarity, tassumptions);
 561     addAssumptions( assumptions, tassumptions );
 562   }
 563 }
 564
 565 void TheoryDatatypes::explainPredicate( TNode p, bool polarity, std::vector<TNode>& assumptions ) {
 566   std::vector<TNode> tassumptions;
 567   d_equalityEngine.explainPredicate(p, polarity, tassumptions);
 568   addAssumptions( assumptions, tassumptions );
 569 }
 570
 571 /** explain */
 572 void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
 573   Debug("datatypes-explain") << "Explain " << literal << std::endl;
 574   bool polarity = literal.getKind() != kind::NOT;
 575   TNode atom = polarity ? literal : literal[0];
 576   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 577     explainEquality( atom[0], atom[1], polarity, assumptions );
 578   } else if( atom.getKind() == kind::AND && polarity ){
 579     for( unsigned i=0; i<atom.getNumChildren(); i++ ){
 580       explain( atom[i], assumptions );
 581     }
 582   } else {
 583     Assert( atom.getKind()!=kind::AND );
 584     explainPredicate( atom, polarity, assumptions );
 585   }
 586 }
 587
 588 Node TheoryDatatypes::explain( TNode literal ){
 589   std::vector< TNode > assumptions;
 590   explain( literal, assumptions );
 591   return mkAnd( assumptions );
 592 }
 593
 594 Node TheoryDatatypes::explain( std::vector< Node >& lits ) {
 595   std::vector< TNode > assumptions;
 596   for( unsigned i=0; i<lits.size(); i++ ){
 597     explain( lits[i], assumptions );
 598   }
 599   return mkAnd( assumptions );
 600 }
 601
 602 /** Conflict when merging two constants */
 603 void TheoryDatatypes::conflict(TNode a, TNode b){
 604   if (a.getKind() == kind::CONST_BOOLEAN) {
 605     d_conflictNode = explain( a.iffNode(b) );
 606   } else {
 607     d_conflictNode = explain( a.eqNode(b) );
 608   }
 609   Trace("dt-conflict") << "CONFLICT: Eq engine conflict : " << d_conflictNode << std::endl;
 610   d_out->conflict( d_conflictNode );
 611   d_conflict = true;
 612 }
 613
 614 /** called when a new equivalance class is created */
 615 void TheoryDatatypes::eqNotifyNewClass(TNode t){
 616   if( t.getKind()==APPLY_CONSTRUCTOR ){
 617     getOrMakeEqcInfo( t, true );
 618     //look at all equivalence classes with constructor terms
 619 /*
 620     for( BoolMap::const_iterator it = d_consEqc.begin(); it != d_consEqc.end(); ++it ){
 621       if( (*it).second ){
 622         TNode r = (*it).first;
 623         if( r.getType()==t.getType() ){
 624           EqcInfo * ei = getOrMakeEqcInfo( r, false );
 625           if( ei && !ei->d_constructor.get().isNull() && ei->d_constructor.get().getOperator()!=t.getOperator() ){
 626             Node deq = ei->d_constructor.get().eqNode( t ).negate();
 627             d_pending.push_back( deq );
 628             d_pending_exp[ deq ] = d_true;
 629             Trace("datatypes-infer") << "DtInfer : diff constructor : " << deq << std::endl;
 630             d_infer.push_back( deq );
 631           }
 632         }
 633       }
 634     }
 635 */
 636     d_consEqc[t] = true;
 637   }
 638 }
 639
 640 /** called when two equivalance classes will merge */
 641 void TheoryDatatypes::eqNotifyPreMerge(TNode t1, TNode t2){
 642
 643 }
 644
 645 /** called when two equivalance classes have merged */
 646 void TheoryDatatypes::eqNotifyPostMerge(TNode t1, TNode t2){
 647   if( DatatypesRewriter::isTermDatatype( t1 ) ){
 648     d_pending_merge.push_back( t1.eqNode( t2 ) );
 649   }
 650 }
 651
 652 void TheoryDatatypes::merge( Node t1, Node t2 ){
 653   if( !d_conflict ){
 654     TNode trep1 = t1;
 655     TNode trep2 = t2;
 656     Debug("datatypes-debug") << "Merge " << t1 << " " << t2 << std::endl;
 657     EqcInfo* eqc2 = getOrMakeEqcInfo( t2 );
 658     if( eqc2 ){
 659       bool checkInst = false;
 660       if( !eqc2->d_constructor.get().isNull() ){
 661         trep2 = eqc2->d_constructor.get();
 662       }
 663       EqcInfo* eqc1 = getOrMakeEqcInfo( t1 );
 664       if( eqc1 ){
 665         if( !eqc1->d_constructor.get().isNull() ){
 666           trep1 = eqc1->d_constructor.get();
 667         }
 668         //check for clash
 669         TNode cons1 = eqc1->d_constructor.get();
 670         TNode cons2 = eqc2->d_constructor.get();
 671         //if both have constructor, then either clash or unification
 672         if( !cons1.isNull() && !cons2.isNull() ){
 673           Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl;
 674           Node unifEq = cons1.eqNode( cons2 );
 675 #if 0
 676           std::vector< Node > exp;
 677           std::vector< std::pair< TNode, TNode > > deq_cand;
 678           bool conf = checkClashModEq( cons1, cons2, exp, deq_cand );
 679           if( !conf ){
 680             for( unsigned i=0; i<deq_cand.size(); i++ ){
 681               if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
 682                 conf = true;
 683                 Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
 684                                                             deq_cand[i].first, deq_cand[i].second );
 685                 exp.push_back( eq.negate() );
 686               }
 687             }
 688           }
 689           if( conf ){
 690             exp.push_back( unifEq );
 691             d_conflictNode = explain( exp );
 692 #else
 693           std::vector< Node > rew;
 694           if( DatatypesRewriter::checkClash( cons1, cons2, rew ) ){
 695             d_conflictNode = explain( unifEq );
 696 #endif
 697             Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl;
 698             d_out->conflict( d_conflictNode );
 699             d_conflict = true;
 700             return;
 701           }else{
 702
 703             //do unification
 704             for( int i=0; i<(int)cons1.getNumChildren(); i++ ) {
 705               if( !areEqual( cons1[i], cons2[i] ) ){
 706                 Node eq = cons1[i].getType().isBoolean() ? cons1[i].iffNode( cons2[i] ) : cons1[i].eqNode( cons2[i] );
 707                 d_pending.push_back( eq );
 708                 d_pending_exp[ eq ] = unifEq;
 709                 Trace("datatypes-infer") << "DtInfer : cons-inj : " << eq << " by " << unifEq << std::endl;
 710                 d_infer.push_back( eq );
 711                 d_infer_exp.push_back( unifEq );
 712               }
 713             }
 714 /*
 715             for( unsigned i=0; i<rew.size(); i++ ){
 716               d_pending.push_back( rew[i] );
 717               d_pending_exp[ rew[i] ] = unifEq;
 718               Trace("datatypes-infer") << "DtInfer : cons-inj : " << rew[i] << " by " << unifEq << std::endl;
 719               d_infer.push_back( rew[i] );
 720               d_infer_exp.push_back( unifEq );
 721             }
 722 */
 723           }
 724         }
 725         if( !eqc1->d_inst && eqc2->d_inst ){
 726           eqc1->d_inst = true;
 727         }
 728         if( !cons2.isNull() ){
 729           if( cons1.isNull() ){
 730             Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl;
 731             checkInst = true;
 732             addConstructor( eqc2->d_constructor.get(), eqc1, t1 );
 733             if( d_conflict ){
 734               return;
 735             }
 736             d_consEqc[t1] = true;
 737           }
 738           d_consEqc[t2] = false;
 739         }
 740       }else{
 741         Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl;
 742         //just copy the equivalence class information
 743         eqc1 = getOrMakeEqcInfo( t1, true );
 744         eqc1->d_inst.set( eqc2->d_inst );
 745         eqc1->d_constructor.set( eqc2->d_constructor );
 746         eqc1->d_selectors.set( eqc2->d_selectors );
 747       }
 748
 749
 750       //merge labels
 751       NodeListMap::iterator lbl_i = d_labels.find( t2 );
 752       if( lbl_i != d_labels.end() ){
 753         Debug("datatypes-debug") << "Merge labels from " << eqc2 << " " << t2 << std::endl;
 754         NodeList* lbl = (*lbl_i).second;
 755         for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){
 756           addTester( *j, eqc1, t1 );
 757           if( d_conflict ){
 758             Debug("datatypes-debug") << "Conflict!" << std::endl;
 759             return;
 760           }
 761         }
 762       }
 763       //merge selectors
 764       if( !eqc1->d_selectors && eqc2->d_selectors ){
 765         eqc1->d_selectors = true;
 766         checkInst = true;
 767       }
 768       NodeListMap::iterator sel_i = d_selector_apps.find( t2 );
 769       if( sel_i != d_selector_apps.end() ){
 770         Debug("datatypes-debug") << "Merge selectors from " << eqc2 << " " << t2 << std::endl;
 771         NodeList* sel = (*sel_i).second;
 772         for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
 773           addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() );
 774         }
 775       }
 776       if( checkInst ){
 777         instantiate( eqc1, t1 );
 778         if( d_conflict ){
 779           return;
 780         }
 781       }
 782     }
 783     //add this to the transitive closure module
 784     Node oldRep = trep2;
 785     Node newRep = trep1;
 786     if( trep1.getKind()!=APPLY_CONSTRUCTOR && trep2.getKind()==APPLY_CONSTRUCTOR ){
 787       oldRep = trep1;
 788       newRep = trep2;
 789     }
 790     /*
 791     bool result = d_cycle_check.addEdgeNode( oldRep, newRep );
 792     //d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
 793     Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl;
 794     if( result ){
 795       checkCycles();
 796       if( d_conflict ){
 797         Debug("datatypes-cycles-find") << "Cycle found." << std::endl;
 798         return;
 799       }else{
 800         Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl;
 801         d_cycle_check.debugPrint();
 802       }
 803     }
 804     */
 805   }
 806 }
 807
 808 /** called when two equivalence classes are made disequal */
 809 void TheoryDatatypes::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 810
 811 }
 812
 813 TheoryDatatypes::EqcInfo::EqcInfo( context::Context* c ) :
 814 d_inst( c, false ), d_constructor( c, Node::null() ), d_selectors( c, false ){
 815
 816 }
 817
 818 bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){
 819   return !eqc->d_constructor.get().isNull() || !getLabel( n ).isNull();
 820 }
 821
 822 Node TheoryDatatypes::getLabel( Node n ) {
 823   NodeListMap::iterator lbl_i = d_labels.find( n );
 824   if( lbl_i != d_labels.end() ){
 825     NodeList* lbl = (*lbl_i).second;
 826     if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()==kind::APPLY_TESTER ){
 827       return (*lbl)[ (*lbl).size() - 1 ];
 828     }
 829   }
 830   return Node::null();
 831 }
 832
 833 int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){
 834   if( !eqc->d_constructor.get().isNull() ){
 835     return Datatype::indexOf( eqc->d_constructor.get().getOperator().toExpr() );
 836   }else{
 837     return Datatype::indexOf( getLabel( n ).getOperator().toExpr() );
 838   }
 839 }
 840
 841 void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){
 842   const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
 843   pcons.resize( dt.getNumConstructors(), !hasLabel( eqc, n ) );
 844   if( hasLabel( eqc, n ) ){
 845     pcons[ getLabelIndex( eqc, n ) ] = true;
 846   }else{
 847     NodeListMap::iterator lbl_i = d_labels.find( n );
 848     if( lbl_i != d_labels.end() ){
 849       NodeList* lbl = (*lbl_i).second;
 850       for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 851         Assert( (*i).getKind()==NOT );
 852         pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false;
 853       }
 854     }
 855   }
 856 }
 857
 858 void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){
 859   Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl;
 860   Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl;
 861   bool tpolarity = t.getKind()!=NOT;
 862   Node tt = ( t.getKind() == NOT ) ? t[0] : t;
 863   int ttindex = Datatype::indexOf( tt.getOperator().toExpr() );
 864   Node j, jt;
 865   bool makeConflict = false;
 866   if( hasLabel( eqc, n ) ){
 867     //if we already know the constructor type, check whether it is in conflict or redundant
 868     int jtindex = getLabelIndex( eqc, n );
 869     if( (jtindex==ttindex)!=tpolarity ){
 870       if( !eqc->d_constructor.get().isNull() ){
 871         //conflict because equivalence class contains a constructor
 872         std::vector< TNode > assumptions;
 873         explain( t, assumptions );
 874         explainEquality( eqc->d_constructor.get(), tt[0], true, assumptions );
 875         d_conflictNode = mkAnd( assumptions );
 876         Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl;
 877         d_out->conflict( d_conflictNode );
 878         d_conflict = true;
 879         return;
 880       }else{
 881         makeConflict = true;
 882         //conflict because the existing label is contradictory
 883         j = getLabel( n );
 884         jt = j;
 885       }
 886     }else{
 887       return;
 888     }
 889   }else{
 890     //otherwise, scan list of labels
 891     NodeListMap::iterator lbl_i = d_labels.find( n );
 892     Assert( lbl_i != d_labels.end() );
 893     NodeList* lbl = (*lbl_i).second;
 894     for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 895       Assert( (*i).getKind()==NOT );
 896       j = *i;
 897       jt = j[0];
 898       int jtindex = Datatype::indexOf( jt.getOperator().toExpr() );
 899       if( jtindex==ttindex ){
 900         if( tpolarity ){  //we are in conflict
 901           makeConflict = true;
 902           break;
 903         }else{            //it is redundant
 904           return;
 905         }
 906       }
 907     }
 908     if( !makeConflict ){
 909       Debug("datatypes-labels") << "Add to labels " << t << std::endl;
 910       lbl->push_back( t );
 911       const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype();
 912       Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl;
 913       if( tpolarity ){
 914         instantiate( eqc, n );
 915       }else{
 916         //check if we have reached the maximum number of testers
 917         // in this case, add the positive tester
 918         if( lbl->size()==dt.getNumConstructors()-1 ){
 919           std::vector< bool > pcons;
 920           getPossibleCons( eqc, n, pcons );
 921           int testerIndex = -1;
 922           for( int i=0; i<(int)pcons.size(); i++ ) {
 923             if( pcons[i] ){
 924               testerIndex = i;
 925               break;
 926             }
 927           }
 928           Assert( testerIndex!=-1 );
 929           //we must explain why each term in the set of testers for this equivalence class is equal
 930           std::vector< Node > eq_terms;
 931           NodeBuilder<> nb(kind::AND);
 932           for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 933             nb << (*i);
 934             if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){
 935               eq_terms.push_back( (*i)[0][0] );
 936               if( (*i)[0][0]!=tt[0] ){
 937                 nb << (*i)[0][0].eqNode( tt[0] );
 938               }
 939             }
 940           }
 941           Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] );
 942           Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb;
 943           d_pending.push_back( t_concl );
 944           d_pending_exp[ t_concl ] = t_concl_exp;
 945           Trace("datatypes-infer") << "DtInfer : label : " << t_concl << " by " << t_concl_exp << std::endl;
 946           d_infer.push_back( t_concl );
 947           d_infer_exp.push_back( t_concl_exp );
 948           return;
 949         }
 950       }
 951     }
 952   }
 953   if( makeConflict ){
 954     d_conflict = true;
 955     Debug("datatypes-labels") << "Explain " << j << " " << t << std::endl;
 956     std::vector< TNode > assumptions;
 957     explain( j, assumptions );
 958     explain( t, assumptions );
 959     explainEquality( jt[0], tt[0], true, assumptions );
 960     d_conflictNode = mkAnd( assumptions );
 961     Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl;
 962     d_out->conflict( d_conflictNode );
 963   }
 964 }
 965
 966 void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) {
 967   Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl;
 968   //check to see if it is redundant
 969   NodeListMap::iterator sel_i = d_selector_apps.find( n );
 970   Assert( sel_i != d_selector_apps.end() );
 971   if( sel_i != d_selector_apps.end() ){
 972     NodeList* sel = (*sel_i).second;
 973     for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
 974       Node ss = *j;
 975       if( s.getOperator()==ss.getOperator() ){
 976         return;
 977       }
 978     }
 979     //add it to the vector
 980     sel->push_back( s );
 981     eqc->d_selectors = true;
 982   }
 983   if( assertFacts && !eqc->d_constructor.get().isNull() ){
 984     //conclude the collapsed merge
 985     collapseSelector( s, eqc->d_constructor.get() );
 986   }
 987 }
 988
 989 void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){
 990   Debug("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl;
 991   Assert( eqc->d_constructor.get().isNull() );
 992   //check labels
 993   NodeListMap::iterator lbl_i = d_labels.find( n );
 994   if( lbl_i != d_labels.end() ){
 995     size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr());
 996     NodeList* lbl = (*lbl_i).second;
 997     for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) {
 998       if( (*i).getKind()==NOT ){
 999         if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){
1000           Node n = *i;
1001           std::vector< TNode > assumptions;
1002           explain( *i, assumptions );
1003           explainEquality( c, (*i)[0][0], true, assumptions );
1004           d_conflictNode = mkAnd( assumptions );
1005           Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl;
1006           d_out->conflict( d_conflictNode );
1007           d_conflict = true;
1008           return;
1009         }
1010       }
1011     }
1012   }
1013   //check selectors
1014   NodeListMap::iterator sel_i = d_selector_apps.find( n );
1015   if( sel_i != d_selector_apps.end() ){
1016     NodeList* sel = (*sel_i).second;
1017     for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){
1018       //collapse the selector
1019       collapseSelector( *j, c );
1020     }
1021   }
1022   eqc->d_constructor.set( c );
1023 }
1024
1025 void TheoryDatatypes::collapseSelector( Node s, Node c ) {
1026   Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR_TOTAL, s.getOperator(), c );
1027   Node rr = Rewriter::rewrite( r );
1028   //if( r!=rr ){
1029     //Node eq_exp = NodeManager::currentNM()->mkConst(true);
1030     //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr );
1031   if( s!=rr ){::
1032     Node eq_exp = c.eqNode( s[0] );
1033     Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr );
1034
1035
1036     d_pending.push_back( eq );
1037     d_pending_exp[ eq ] = eq_exp;
1038     Trace("datatypes-infer") << "DtInfer : collapse sel : " << eq << " by " << eq_exp << std::endl;
1039     d_infer.push_back( eq );
1040     d_infer_exp.push_back( eq_exp );
1041   }
1042 }
1043
1044 EqualityStatus TheoryDatatypes::getEqualityStatus(TNode a, TNode b){
1045   if( d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b) ){
1046     if (d_equalityEngine.areEqual(a, b)) {
1047       // The terms are implied to be equal
1048       return EQUALITY_TRUE;
1049     }
1050     if (d_equalityEngine.areDisequal(a, b, false)) {
1051       // The terms are implied to be dis-equal
1052       return EQUALITY_FALSE;
1053     }
1054   }
1055   return EQUALITY_UNKNOWN;
1056 }
1057
1058 void TheoryDatatypes::computeCareGraph(){
1059   Trace("dt-cg") << "Compute graph for dt..." << std::endl;
1060   vector< pair<TNode, TNode> > currentPairs;
1061   for( unsigned r=0; r<2; r++ ){
1062     unsigned functionTerms = r==0 ? d_consTerms.size() : d_selTerms.size();
1063     for( unsigned i=0; i<functionTerms; i++ ){
1064       TNode f1 = r==0 ? d_consTerms[i] : d_selTerms[i];
1065       for( unsigned j=i+1; j<functionTerms; j++ ){
1066         TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j];
1067         if( f1.getOperator()==f2.getOperator() && !areEqual( f1, f2 ) ){
1068           Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl;
1069           bool somePairIsDisequal = false;
1070           currentPairs.clear();
1071           for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1072             TNode x = f1[k];
1073             TNode y = f2[k];
1074             if( areDisequal(x, y) ){
1075               somePairIsDisequal = true;
1076               break;
1077             }else if( !areEqual( x, y ) ){
1078               Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1079               //check if they are definately disequal
1080               bool defDiseq = false;
1081 /*
1082               TNode rx = getRepresentative( x );
1083               EqcInfo* eix = getOrMakeEqcInfo( rx, false );
1084               if( eix ){
1085                 TNode ry = getRepresentative( y );
1086                 EqcInfo* eiy = getOrMakeEqcInfo( ry, false );
1087                 if( eiy ){
1088                   if( !eix->d_constructor.get().isNull() && !eiy->d_constructor.get().isNull() ){
1089                     defDiseq = eix->d_constructor.get().getOperator()!=eiy->d_constructor.get().getOperator();
1090                   }else{
1091                   }
1092                 }
1093               }
1094 */
1095               if( !defDiseq && d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
1096                 EqualityStatus eqStatus = d_valuation.getEqualityStatus(x, y);
1097                 if( eqStatus!=EQUALITY_UNKNOWN ){
1098                   TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
1099                   TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
1100                   Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
1101                   currentPairs.push_back(make_pair(x_shared, y_shared));
1102                 }
1103               }
1104             }
1105           }
1106           if (!somePairIsDisequal) {
1107             for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1108               Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1109               addCarePair(currentPairs[c].first, currentPairs[c].second);
1110             }
1111           }
1112         }
1113       }
1114     }
1115   }
1116   Trace("dt-cg") << "Done Compute graph for dt." << std::endl;
1117 }
1118
1119 void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
1120   Trace("dt-cmi") << "Datatypes : Collect model info " << d_equalityEngine.consistent() << std::endl;
1121   Trace("dt-model") << std::endl;
1122   printModelDebug( "dt-model" );
1123   Trace("dt-model") << std::endl;
1124
1125   /*
1126   bool eq_merged = false;
1127   std::vector< Node > all_eqc;
1128   eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine );
1129   while( !eqcs1_i.isFinished() ){
1130     Node eqc = (*eqcs1_i);
1131     all_eqc.push_back( eqc );
1132     ++eqcs1_i;
1133   }
1134   //check if equivalence classes have merged
1135   for( unsigned i=0; i<all_eqc.size(); i++ ){
1136     for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
1137       if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
1138         Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
1139         eq_merged = true;
1140       }
1141     }
1142   }
1143   Assert( !eq_merged );
1144   */
1145
1146   //combine the equality engine
1147   m->assertEqualityEngine( &d_equalityEngine );
1148
1149   /*
1150   //check again if equivalence classes have merged
1151   for( unsigned i=0; i<all_eqc.size(); i++ ){
1152     for( unsigned j=(i+1); j<all_eqc.size(); j++ ){
1153       if( m->areEqual( all_eqc[i], all_eqc[j] ) ){
1154         Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl;
1155         eq_merged = true;
1156       }
1157     }
1158   }
1159   Assert( !eq_merged );
1160   */
1161
1162   //get all constructors
1163   eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine );
1164   std::vector< Node > cons;
1165   std::vector< Node > nodes;
1166   std::map< Node, Node > eqc_cons;
1167   while( !eqccs_i.isFinished() ){
1168     Node eqc = (*eqccs_i);
1169     //for all equivalence classes that are datatypes
1170     if( DatatypesRewriter::isTermDatatype( eqc ) ){
1171       EqcInfo* ei = getOrMakeEqcInfo( eqc );
1172       if( !ei->d_constructor.get().isNull() ){
1173         cons.push_back( ei->d_constructor.get() );
1174         eqc_cons[ eqc ] = ei->d_constructor.get();
1175       }else{
1176         nodes.push_back( eqc );
1177       }
1178     }
1179     ++eqccs_i;
1180   }
1181
1182   //unsigned orig_size = nodes.size();
1183   std::map< TypeNode, int > typ_enum_map;
1184   std::vector< TypeEnumerator > typ_enum;
1185   unsigned index = 0;
1186   while( index<nodes.size() ){
1187     Node eqc = nodes[index];
1188     Node neqc;
1189     bool addCons = false;
1190     const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
1191     if( !d_equalityEngine.hasTerm( eqc ) ){
1192       if( !dt.isCodatatype() ){
1193         Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
1194         Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
1195         TypeNode tn = eqc.getType();
1196         //if it is infinite, make sure it is fresh
1197         if( eqc.getType().getCardinality().isInfinite() ){
1198           std::map< TypeNode, int >::iterator it = typ_enum_map.find( tn );
1199           int teIndex;
1200           if( it==typ_enum_map.end() ){
1201             teIndex = (int)typ_enum.size();
1202             typ_enum_map[tn] = teIndex;
1203             typ_enum.push_back( TypeEnumerator(tn) );
1204           }else{
1205             teIndex = it->second;
1206           }
1207           bool success;
1208           do{
1209             success = true;
1210             Assert( !typ_enum[teIndex].isFinished() );
1211             neqc = *typ_enum[teIndex];
1212             Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
1213             ++typ_enum[teIndex];
1214             for( unsigned i=0; i<cons.size(); i++ ){
1215               //check if it is modulo equality the same
1216               if( cons[i].getOperator()==neqc.getOperator() ){
1217                 bool diff = false;
1218                 for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
1219                   if( !m->areEqual( cons[i][j], neqc[j] ) ){
1220                     diff = true;
1221                     break;
1222                   }
1223                 }
1224                 if( !diff ){
1225                   Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl;
1226                   success = false;
1227                   break;
1228                 }
1229               }
1230             }
1231           }while( !success );
1232         }else{
1233           TypeEnumerator te(tn);
1234           neqc = *te;
1235         }
1236       }
1237     }else{
1238       Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl;
1239       Trace("dt-cmi") << "   Type : " << eqc.getType() << std::endl;
1240       EqcInfo* ei = getOrMakeEqcInfo( eqc );
1241       std::vector< bool > pcons;
1242       getPossibleCons( ei, eqc, pcons );
1243       Trace("dt-cmi") << "Possible constructors : ";
1244       for( unsigned i=0; i<pcons.size(); i++ ){
1245         Trace("dt-cmi") << pcons[i] << " ";
1246       }
1247       Trace("dt-cmi") << std::endl;
1248       /*
1249       std::map< int, std::map< int, bool > > sels;
1250       Trace("dt-cmi") << "Existing selectors : ";
1251       NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
1252       if( sel_i != d_selector_apps.end() ){
1253         NodeList* sel = (*sel_i).second;
1254         for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
1255           Expr selectorExpr = (*j).getOperator().toExpr();
1256           unsigned cindex = Datatype::cindexOf( selectorExpr );
1257           unsigned index = Datatype::indexOf( selectorExpr );
1258           sels[cindex][index] = true;
1259           Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") ";
1260         }
1261       }
1262       Trace("dt-cmi") << std::endl;
1263       */
1264       for( unsigned r=0; r<2; r++ ){
1265         if( neqc.isNull() ){
1266           for( unsigned i=0; i<pcons.size(); i++ ){
1267             //must try the infinite ones first
1268             if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
1269               neqc = getInstantiateCons( eqc, dt, i, false, false );
1270               for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
1271                 //if( sels[i].find( j )==sels[i].end() && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
1272                 if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
1273                   nodes.push_back( neqc[j] );
1274                 }
1275               }
1276               break;
1277             }
1278           }
1279         }
1280       }
1281       addCons = true;
1282     }
1283     if( !neqc.isNull() ){
1284       Trace("dt-cmi") << "Assign : " << neqc << std::endl;
1285       m->assertEquality( eqc, neqc, true );
1286       eqc_cons[ eqc ] = neqc;
1287     }
1288     /*
1289     for( unsigned kk=0; kk<all_eqc.size(); kk++ ){
1290       for( unsigned ll=(kk+1); ll<all_eqc.size(); ll++ ){
1291         if( m->areEqual( all_eqc[kk], all_eqc[ll] ) ){
1292           Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl;
1293           Node r = m->getRepresentative( all_eqc[kk] );
1294           Trace("dt-cmi") << "  { ";
1295           eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine );
1296           while( !eqc_i.isFinished() ){
1297             Trace("dt-cmi") << (*eqc_i) << " ";
1298             ++eqc_i;
1299           }
1300           Trace("dt-cmi") << "} " << std::endl;
1301         }
1302         Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) );
1303       }
1304     }
1305     */
1306     //m->assertRepresentative( neqc );
1307     if( addCons ){
1308       cons.push_back( neqc );
1309     }
1310     ++index;
1311   }
1312
1313   //assign MU for each codatatype eqc
1314   std::map< Node, Node > eqc_mu;
1315   for( std::map< Node, Node >::iterator it = eqc_cons.begin(); it != eqc_cons.end(); ++it ){
1316     Node eqc = it->first;
1317     const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
1318     if( dt.isCodatatype() ){
1319       std::map< Node, Node > vmap;
1320       Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap );
1321       Trace("dt-cmi-cod") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << std::endl;
1322     }
1323   }
1324 }
1325
1326
1327 Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, Node >& eqc_mu, std::map< Node, Node >& vmap ){
1328   std::map< Node, Node >::iterator itv = vmap.find( n );
1329   if( itv!=vmap.end() ){
1330     return itv->second;
1331   }else if( DatatypesRewriter::isTermDatatype( n ) ){
1332     Node nv = NodeManager::currentNM()->mkBoundVar( n.getType() );
1333     vmap[n] = nv;
1334     Trace("dt-cmi-cod-debug") << "    map " << n << " -> " << nv << std::endl;
1335     Node nc = eqc_cons[n];
1336     Assert( nc.getKind()==APPLY_CONSTRUCTOR );
1337     std::vector< Node > children;
1338     children.push_back( nc.getOperator() );
1339     for( unsigned i=0; i<nc.getNumChildren(); i++ ){
1340       Node r = getRepresentative( nc[i] );
1341       Node rv = getCodatatypesValue( r, eqc_cons, eqc_mu, vmap );
1342       children.push_back( rv );
1343     }
1344     vmap.erase( n );
1345     return NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children );
1346   }else{
1347     return n;
1348   }
1349 }
1350
1351 void TheoryDatatypes::collectTerms( Node n ) {
1352   if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){
1353     d_collectTermsCache[n] = true;
1354     for( int i=0; i<(int)n.getNumChildren(); i++ ) {
1355       collectTerms( n[i] );
1356     }
1357     if( n.getKind() == APPLY_CONSTRUCTOR ){
1358       d_consTerms.push_back( n );
1359       /*
1360       //we must take into account subterm relation when checking for cycles
1361       for( int i=0; i<(int)n.getNumChildren(); i++ ) {
1362         bool result = d_cycle_check.addEdgeNode( n, n[i] );
1363         Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl;
1364         if( result && !d_hasSeenCycle.get() ){
1365           Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl;
1366         }
1367         d_hasSeenCycle.set( d_hasSeenCycle.get() || result );
1368         //Node r = getRepresentative( n[i] );
1369         //EqcInfo* eqc = getOrMakeEqcInfo( r, true );
1370         //eqc->d_selectors = true;
1371       }
1372       */
1373     }else if( n.getKind() == APPLY_SELECTOR_TOTAL ){
1374       d_selTerms.push_back( n );
1375       //we must also record which selectors exist
1376       Debug("datatypes") << "  Found selector " << n << endl;
1377       if (n.getType().isBoolean()) {
1378         d_equalityEngine.addTriggerPredicate( n );
1379       }else{
1380         d_equalityEngine.addTerm( n );
1381       }
1382       Node rep = getRepresentative( n[0] );
1383       //record it in the selectors
1384       EqcInfo* eqc = getOrMakeEqcInfo( rep, true );
1385       //add it to the eqc info
1386       addSelector( n, eqc, rep );
1387     }
1388   }
1389 }
1390
1391 void TheoryDatatypes::processNewTerm( Node n ){
1392   Trace("dt-terms") << "Created term : " << n << std::endl;
1393   //see if it is rewritten to be something different
1394   Node rn = Rewriter::rewrite( n );
1395   if( rn!=n && !areEqual( rn, n ) ){
1396     Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n );
1397     d_pending.push_back( eq );
1398     d_pending_exp[ eq ] = d_true;
1399     Trace("datatypes-infer") << "DtInfer : rewrite : " << eq << std::endl;
1400     d_infer.push_back( eq );
1401   }
1402 }
1403
1404 Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){
1405   std::map< int, Node >::iterator it = d_inst_map[n].find( index );
1406   if( it!=d_inst_map[n].end() ){
1407     return it->second;
1408   }else{
1409     //add constructor to equivalence class
1410     Node n_ic = DatatypesRewriter::getInstCons( n, dt, index, mkVar );
1411     if( isActive ){
1412       for( unsigned i = 0; i<n_ic.getNumChildren(); i++ ){
1413         processNewTerm( n_ic[i] );
1414       }
1415       collectTerms( n_ic );
1416     }
1417     n_ic = Rewriter::rewrite( n_ic );
1418     Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl;
1419     d_inst_map[n][index] = n_ic;
1420     return n_ic;
1421   }
1422 }
1423
1424 void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){
1425   //add constructor to equivalence class if not done so already
1426   if( hasLabel( eqc, n ) && !eqc->d_inst ){
1427     Node exp;
1428     Node tt;
1429     if( !eqc->d_constructor.get().isNull() ){
1430       exp = d_true;
1431       tt = eqc->d_constructor;
1432     }else{
1433       exp = getLabel( n );
1434       tt = exp[0];
1435     }
1436     int index = getLabelIndex( eqc, n );
1437     const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype();
1438     //must be finite or have a selector
1439     //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment()
1440     //instantiate this equivalence class
1441     eqc->d_inst = true;
1442     Node tt_cons = getInstantiateCons( tt, dt, index, false, true );
1443     Node eq;
1444     if( tt!=tt_cons ){
1445       eq = tt.eqNode( tt_cons );
1446       Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl;
1447       d_pending.push_back( eq );
1448       d_pending_exp[ eq ] = exp;
1449       Trace("datatypes-infer") << "DtInfer : instantiate : " << eq << " by " << exp << std::endl;
1450       //eqc->d_inst.set( eq );
1451       d_infer.push_back( eq );
1452       d_infer_exp.push_back( exp );
1453     }
1454     //}
1455     //else{
1456     //  Debug("datatypes-inst") << "Do not instantiate" << std::endl;
1457     //}
1458   }
1459 }
1460
1461 void TheoryDatatypes::checkCycles() {
1462   Debug("datatypes-cycle-check") << "Check cycles" << std::endl;
1463   std::vector< Node > cod_eqc;
1464   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1465   while( !eqcs_i.isFinished() ){
1466     Node eqc = (*eqcs_i);
1467     TypeNode tn = eqc.getType();
1468     if( DatatypesRewriter::isTypeDatatype( tn ) ) {
1469       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
1470       if( !dt.isCodatatype() ){
1471         //do cycle checks
1472         std::map< TNode, bool > visited;
1473         std::vector< TNode > expl;
1474         Node cn = searchForCycle( eqc, eqc, visited, expl );
1475         //if we discovered a different cycle while searching this one
1476         if( !cn.isNull() && cn!=eqc ){
1477           visited.clear();
1478           expl.clear();
1479           Node prev = cn;
1480           cn = searchForCycle( cn, cn, visited, expl );
1481           Assert( prev==cn );
1482         }
1483
1484         if( !cn.isNull() ) {
1485           Assert( expl.size()>0 );
1486           d_conflictNode = mkAnd( expl );
1487           Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl;
1488           d_out->conflict( d_conflictNode );
1489           d_conflict = true;
1490           return;
1491         }
1492       }else{
1493         //indexing
1494         cod_eqc.push_back( eqc );
1495       }
1496     }
1497     ++eqcs_i;
1498   }
1499   //process codatatypes
1500   if( cod_eqc.size()>1 ){
1501     Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl;
1502     std::vector< std::vector< Node > > part_out;
1503     std::vector< TNode > exp;
1504     std::map< Node, Node > cn;
1505     std::map< Node, std::map< Node, int > > dni;
1506     for( unsigned i=0; i<cod_eqc.size(); i++ ){
1507       cn[cod_eqc[i]] = cod_eqc[i];
1508     }
1509     separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false );
1510     Trace("dt-cod-debug") << "Done separate bisimilar." << std::endl;
1511     if( !part_out.empty() ){
1512       Trace("dt-cod-debug") << "Process partition size " << part_out.size() << std::endl;
1513       for( unsigned i=0; i<part_out.size(); i++ ){
1514         std::vector< Node > part;
1515         part.push_back( part_out[i][0] );
1516         for( unsigned j=1; j<part_out[i].size(); j++ ){
1517           Trace("dt-cod") << "Codatatypes : " << part_out[i][0] << " and " << part_out[i][j] << " must be equal!!" << std::endl;
1518           part.push_back( part_out[i][j] );
1519           std::vector< std::vector< Node > > tpart_out;
1520           exp.clear();
1521           cn.clear();
1522           cn[part_out[i][0]] = part_out[i][0];
1523           cn[part_out[i][j]] = part_out[i][j];
1524           dni.clear();
1525           separateBisimilar( part, tpart_out, exp, cn, dni, 0, true );
1526           Assert( tpart_out.size()==1 && tpart_out[0].size()==2 );
1527           part.pop_back();
1528           //merge based on explanation
1529           Trace("dt-cod") << "  exp is : ";
1530           for( unsigned k=0; k<exp.size(); k++ ){
1531             Trace("dt-cod") << exp[k] << " ";
1532           }
1533           Trace("dt-cod") << std::endl;
1534           Node eq = part_out[i][0].eqNode( part_out[i][j] );
1535           Node eqExp = mkAnd( exp );
1536           d_pending.push_back( eq );
1537           d_pending_exp[ eq ] = eqExp;
1538           Trace("datatypes-infer") << "DtInfer : cod-bisimilar : " << eq << " by " << eqExp << std::endl;
1539           d_infer.push_back( eq );
1540           d_infer_exp.push_back( eqExp );
1541         }
1542       }
1543     }
1544   }
1545 }
1546
1547 //everything is in terms of representatives
1548 void TheoryDatatypes::separateBisimilar( std::vector< Node >& part, std::vector< std::vector< Node > >& part_out,
1549                                          std::vector< TNode >& exp,
1550                                          std::map< Node, Node >& cn,
1551                                          std::map< Node, std::map< Node, int > >& dni, int dniLvl, bool mkExp ){
1552   if( !mkExp ){
1553     Trace("dt-cod-debug") << "Separate bisimilar : " << std::endl;
1554     for( unsigned i=0; i<part.size(); i++ ){
1555       Trace("dt-cod-debug") << "   " << part[i] << ", current = " << cn[part[i]] << std::endl;
1556     }
1557   }
1558   Assert( part.size()>1 );
1559   std::map< Node, std::vector< Node > > new_part;
1560   std::map< Node, std::vector< Node > > new_part_c;
1561   std::map< int, std::vector< Node > > new_part_rec;
1562
1563   std::map< Node, Node > cn_cons;
1564   for( unsigned j=0; j<part.size(); j++ ){
1565     Node c = cn[part[j]];
1566     std::map< Node, int >::iterator it_rec = dni[part[j]].find( c );
1567     if( it_rec!=dni[part[j]].end() ){
1568       //looped
1569       if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is looping at index " << it_rec->second << std::endl; }
1570       new_part_rec[ it_rec->second ].push_back( part[j] );
1571     }else{
1572       if( DatatypesRewriter::isTermDatatype( c ) ){
1573         Node ncons = getEqcConstructor( c );
1574         if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
1575           Node cc = ncons.getOperator();
1576           cn_cons[part[j]] = ncons;
1577           if( mkExp ){
1578             explainEquality( c, ncons, true, exp );
1579           }
1580           new_part[cc].push_back( part[j] );
1581           if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is datatype " << ncons << "." << std::endl; }
1582         }else{
1583           new_part_c[c].push_back( part[j] );
1584           if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is unspecified datatype." << std::endl; }
1585         }
1586       }else{
1587         //add equivalences
1588         if( !mkExp ){ Trace("dt-cod-debug") << "  - " << part[j] << " is term " << c << "." << std::endl; }
1589         new_part_c[c].push_back( part[j] );
1590       }
1591     }
1592   }
1593   //direct add for constants
1594   for( std::map< Node, std::vector< Node > >::iterator it = new_part_c.begin(); it != new_part_c.end(); ++it ){
1595     if( it->second.size()>1 ){
1596       std::vector< Node > vec;
1597       vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1598       part_out.push_back( vec );
1599     }
1600   }
1601   //direct add for recursive
1602   for( std::map< int, std::vector< Node > >::iterator it = new_part_rec.begin(); it != new_part_rec.end(); ++it ){
1603     if( it->second.size()>1 ){
1604       std::vector< Node > vec;
1605       vec.insert( vec.begin(), it->second.begin(), it->second.end() );
1606       part_out.push_back( vec );
1607     }else{
1608       //add back : could match a datatype?
1609     }
1610   }
1611   //recurse for the datatypes
1612   for( std::map< Node, std::vector< Node > >::iterator it = new_part.begin(); it != new_part.end(); ++it ){
1613     if( it->second.size()>1 ){
1614       //set dni to check for loops
1615       std::map< Node, Node > dni_rem;
1616       for( unsigned i=0; i<it->second.size(); i++ ){
1617         Node n = it->second[i];
1618         dni[n][cn[n]] = dniLvl;
1619         dni_rem[n] = cn[n];
1620       }
1621
1622       //we will split based on the arguments of the datatype
1623       std::vector< std::vector< Node > > split_new_part;
1624       split_new_part.push_back( it->second );
1625
1626       unsigned nChildren = cn_cons[it->second[0]].getNumChildren();
1627       //for each child of constructor
1628       unsigned cindex = 0;
1629       while( cindex<nChildren && !split_new_part.empty() ){
1630         if( !mkExp ){ Trace("dt-cod-debug") << "Split argument #" << cindex << " of " << it->first << "..." << std::endl; }
1631         std::vector< std::vector< Node > > next_split_new_part;
1632         for( unsigned j=0; j<split_new_part.size(); j++ ){
1633           //set current node
1634           for( unsigned k=0; k<split_new_part[j].size(); k++ ){
1635             Node n = split_new_part[j][k];
1636             cn[n] = getRepresentative( cn_cons[n][cindex] );
1637             if( mkExp ){
1638               explainEquality( cn[n], cn_cons[n][cindex], true, exp );
1639             }
1640           }
1641           std::vector< std::vector< Node > > c_part_out;
1642           separateBisimilar( split_new_part[j], c_part_out, exp, cn, dni, dniLvl+1, mkExp );
1643           next_split_new_part.insert( next_split_new_part.end(), c_part_out.begin(), c_part_out.end() );
1644         }
1645         split_new_part.clear();
1646         split_new_part.insert( split_new_part.end(), next_split_new_part.begin(), next_split_new_part.end() );
1647         cindex++;
1648       }
1649       part_out.insert( part_out.end(), split_new_part.begin(), split_new_part.end() );
1650
1651       for( std::map< Node, Node >::iterator it2 = dni_rem.begin(); it2 != dni_rem.end(); ++it2 ){
1652         dni[it2->first].erase( it2->second );
1653       }
1654     }
1655   }
1656 }
1657
1658 //postcondition: if cycle detected, explanation is why n is a subterm of on
1659 Node TheoryDatatypes::searchForCycle( TNode n, TNode on,
1660                                       std::map< TNode, bool >& visited,
1661                                       std::vector< TNode >& explanation, bool firstTime ) {
1662   Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl;
1663   TNode ncons;
1664   TNode nn;
1665   if( !firstTime ){
1666     nn = getRepresentative( n );
1667     if( nn==on ){
1668       explainEquality( n, nn, true, explanation );
1669       return on;
1670     }
1671   }else{
1672     nn = n;
1673   }
1674   if( visited.find( nn ) == visited.end() ) {
1675     visited[nn] = true;
1676     TNode ncons = getEqcConstructor( nn );
1677     if( ncons.getKind()==APPLY_CONSTRUCTOR ) {
1678       for( int i=0; i<(int)ncons.getNumChildren(); i++ ) {
1679         TNode cn = searchForCycle( ncons[i], on, visited, explanation, false );
1680         if( cn==on ) {
1681           //if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){
1682           //  Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl;
1683           //}
1684           //add explanation for why the constructor is connected
1685           if( n != ncons ) {
1686             explainEquality( n, ncons, true, explanation );
1687           }
1688           return on;
1689         }else if( !cn.isNull() ){
1690           return cn;
1691         }
1692       }
1693     }
1694     visited.erase( nn );
1695     return Node::null();
1696   }else{
1697     TypeNode tn = nn.getType();
1698     if( DatatypesRewriter::isTypeDatatype( tn ) ) {
1699       const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
1700       if( !dt.isCodatatype() ){
1701         return nn;
1702       }
1703     }
1704     return Node::null();
1705   }
1706 }
1707
1708 bool TheoryDatatypes::mustSpecifyAssignment(){
1709   //FIXME: the condition finiteModelFind is an over-approximation in this function
1710   //   we still may not want to specify assignments for datatypes that are truly infinite
1711   //   the fix for this is to correctly compute the cardinality for datatypes containing uninterpered sorts in fmf (i.e. by assuming they are finite)
1712   return options::finiteModelFind() || options::produceModels() || options::dtForceAssignment();
1713   //return options::produceModels();
1714   //return false;
1715 }
1716
1717 bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){
1718   //the datatypes decision procedure makes 3 "internal" inferences apart from the equality engine :
1719   //  (1) Unification : C( t1...tn ) = C( s1...sn ) => ti = si
1720   //  (2) Label : ~is_C1( t ) ... ~is_C{i-1}( t ) ~is_C{i+1}( t ) ... ~is_Cn( t ) => is_Ci( t )
1721   //  (3) Instantiate : is_C( t ) => t = C( sel_1( t ) ... sel_n( t ) )
1722   //We may need to communicate (3) outwards if the conclusions involve other theories
1723   Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl;
1724   bool addLemma = false;
1725   if( ( n.getKind()==EQUAL || n.getKind()==IFF) && n[1].getKind()==APPLY_CONSTRUCTOR && exp.getKind()!=EQUAL  ){
1726 #if 1
1727     const Datatype& dt = ((DatatypeType)(n[1].getType()).toType()).getDatatype();
1728     addLemma = dt.involvesExternalType();
1729 #else
1730     for( int j=0; j<(int)n[1].getNumChildren(); j++ ){
1731       if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){
1732         addLemma = true;
1733         break;
1734       }
1735     }
1736 #endif
1737     if( addLemma ){
1738       //check if we have already added this lemma
1739       if( std::find( d_inst_lemmas[ n[0] ].begin(), d_inst_lemmas[ n[0] ].end(), n[1] )==d_inst_lemmas[ n[0] ].end() ){
1740         d_inst_lemmas[ n[0] ].push_back( n[1] );
1741         Trace("dt-lemma-debug") << "Communicate " << n << std::endl;
1742         return true;
1743       }else{
1744         Trace("dt-lemma-debug") << "Already communicated " << n << std::endl;
1745         return false;
1746       }
1747     }
1748   }
1749   //else if( exp.getKind()==APPLY_TESTER ){
1750     //if( n.getKind()==EQUAL && !DatatypesRewriter::isTermDatatype( n[0] ) ){
1751     //  return true;
1752     //}
1753   //}
1754   Trace("dt-lemma-debug") << "Do not need to communicate " << n << std::endl;
1755   return false;
1756 }
1757
1758 bool TheoryDatatypes::hasTerm( TNode a ){
1759   return d_equalityEngine.hasTerm( a );
1760 }
1761
1762 bool TheoryDatatypes::areEqual( TNode a, TNode b ){
1763   if( a==b ){
1764     return true;
1765   }else if( hasTerm( a ) && hasTerm( b ) ){
1766     return d_equalityEngine.areEqual( a, b );
1767   }else{
1768     return false;
1769   }
1770 }
1771
1772 bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
1773   if( a==b ){
1774     return false;
1775   }else if( hasTerm( a ) && hasTerm( b ) ){
1776     return d_equalityEngine.areDisequal( a, b, false );
1777   }else{
1778     return false;
1779   }
1780 }
1781
1782 TNode TheoryDatatypes::getRepresentative( TNode a ){
1783   if( hasTerm( a ) ){
1784     return d_equalityEngine.getRepresentative( a );
1785   }else{
1786     return a;
1787   }
1788 }
1789
1790
1791 void TheoryDatatypes::printModelDebug( const char* c ){
1792   if(! (Trace.isOn(c))) {
1793     return;
1794   }
1795
1796   Trace( c ) << "Datatypes model : " << std::endl;
1797   eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
1798   while( !eqcs_i.isFinished() ){
1799     Node eqc = (*eqcs_i);
1800     if( !eqc.getType().isBoolean() ){
1801       if( DatatypesRewriter::isTermDatatype( eqc ) ){
1802         Trace( c ) << "DATATYPE : ";
1803       }
1804       Trace( c ) << eqc << " : " << eqc.getType() << " : " << std::endl;
1805       Trace( c ) << "   { ";
1806       //add terms to model
1807       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
1808       while( !eqc_i.isFinished() ){
1809         Trace( c ) << (*eqc_i) << " ";
1810         ++eqc_i;
1811       }
1812       Trace( c ) << "}" << std::endl;
1813       if( DatatypesRewriter::isTermDatatype( eqc ) ){
1814         EqcInfo* ei = getOrMakeEqcInfo( eqc );
1815         if( ei ){
1816           Trace( c ) << "   Instantiated : " << ei->d_inst.get() << std::endl;
1817           Trace( c ) << "   Constructor : ";
1818           if( !ei->d_constructor.get().isNull() ){
1819             Trace( c )<< ei->d_constructor.get();
1820           }
1821           Trace( c ) << std::endl << "   Labels : ";
1822           if( hasLabel( ei, eqc ) ){
1823             Trace( c ) << getLabel( eqc );
1824           }else{
1825             NodeListMap::iterator lbl_i = d_labels.find( eqc );
1826             if( lbl_i != d_labels.end() ){
1827               NodeList* lbl = (*lbl_i).second;
1828               for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){
1829                 Trace( c ) << *j << " ";
1830               }
1831             }
1832           }
1833           Trace( c ) << std::endl;
1834           Trace( c ) << "   Selectors : " << ( ei->d_selectors ? "yes, " : "no " );
1835           NodeListMap::iterator sel_i = d_selector_apps.find( eqc );
1836           if( sel_i != d_selector_apps.end() ){
1837             NodeList* sel = (*sel_i).second;
1838             for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){
1839               Trace( c ) << *j << " ";
1840             }
1841           }
1842           Trace( c ) << std::endl;
1843         }
1844       }
1845     }
1846     ++eqcs_i;
1847   }
1848 }
1849
1850 Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) {
1851   if( assumptions.empty() ){
1852     return d_true;
1853   }else if( assumptions.size()==1 ){
1854     return assumptions[0];
1855   }else{
1856     return NodeManager::currentNM()->mkNode( AND, assumptions );
1857   }
1858 }
1859
1860 bool TheoryDatatypes::checkClashModEq( TNode n1, TNode n2, std::vector< Node >& exp, std::vector< std::pair< TNode, TNode > >& deq_cand ) {
1861   if( (n1.getKind() == kind::APPLY_CONSTRUCTOR && n2.getKind() == kind::APPLY_CONSTRUCTOR) ||
1862       (n1.getKind() == kind::TUPLE && n2.getKind() == kind::TUPLE) ||
1863       (n1.getKind() == kind::RECORD && n2.getKind() == kind::RECORD) ) {
1864     if( n1.getOperator() != n2.getOperator() ) {
1865       return true;
1866     } else {
1867       Assert( n1.getNumChildren() == n2.getNumChildren() );
1868       for( int i=0; i<(int)n1.getNumChildren(); i++ ) {
1869         TNode nc1 = getEqcConstructor( n1[i] );
1870         TNode nc2 = getEqcConstructor( n2[i] );
1871         if( checkClashModEq( nc1, nc2, exp, deq_cand ) ) {
1872           if( nc1!=n1[i] ){
1873             exp.push_back( nc1.eqNode( n1[i] ) );
1874           }
1875           if( nc2!=n2[i] ){
1876             exp.push_back( nc2.eqNode( n2[i] ) );
1877           }
1878           return true;
1879         }
1880       }
1881     }
1882   }else if( n1!=n2 ){
1883     if( n1.isConst() && n2.isConst() ){
1884       return true;
1885     }else{
1886       if( !areEqual( n1, n2 ) ){
1887         deq_cand.push_back( std::pair< TNode, TNode >( n1, n2 ) );
1888       }
1889     }
1890   }
1891   return false;
1892 }
1893