src/theory/sets/theory_sets_private.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_private.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Kshitij Bansal, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Sets theory implementation.
  13  **
  14  ** Sets theory implementation.
  15  **/
  16
  17 #include <algorithm>
  18 #include "theory/sets/theory_sets_private.h"
  19
  20 #include <boost/foreach.hpp>
  21
  22 #include "expr/emptyset.h"
  23 #include "options/sets_options.h"
  24 #include "smt/smt_statistics_registry.h"
  25 #include "theory/sets/theory_sets.h"
  26 #include "theory/sets/normal_form.h"
  27 #include "theory/theory_model.h"
  28 #include "util/result.h"
  29 #include "theory/quantifiers/term_database.h"
  30
  31 #define AJR_IMPLEMENTATION
  32
  33 using namespace std;
  34
  35 namespace CVC4 {
  36 namespace theory {
  37 namespace sets {
  38
  39 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
  40                                      context::Context* c,
  41                                      context::UserContext* u):
  42   d_rels(NULL),
  43   d_members(c),
  44   d_deq(c),
  45   d_deq_processed(u),
  46   d_keep(c),
  47   d_proxy(u),
  48   d_proxy_to_term(u),
  49   d_lemmas_produced(u),
  50   d_card_processed(u),
  51   d_external(external),
  52   d_notify(*this),
  53   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", true),
  54   d_conflict(c)
  55 {
  56
  57   d_rels = new TheorySetsRels(c, u, &d_equalityEngine, &d_conflict, external);
  58
  59   d_true = NodeManager::currentNM()->mkConst( true );
  60   d_false = NodeManager::currentNM()->mkConst( false );
  61   d_zero = NodeManager::currentNM()->mkConst( Rational(0) );
  62
  63   d_equalityEngine.addFunctionKind(kind::SINGLETON);
  64   d_equalityEngine.addFunctionKind(kind::UNION);
  65   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
  66   d_equalityEngine.addFunctionKind(kind::SETMINUS);
  67
  68   d_equalityEngine.addFunctionKind(kind::MEMBER);
  69   d_equalityEngine.addFunctionKind(kind::SUBSET);
  70
  71   // If cardinality is on.
  72   d_equalityEngine.addFunctionKind(kind::CARD);
  73
  74   d_card_enabled = false;
  75   d_rels_enabled = false;
  76
  77 }/* TheorySetsPrivate::TheorySetsPrivate() */
  78
  79 TheorySetsPrivate::~TheorySetsPrivate(){
  80   delete d_rels;
  81   for(std::map< Node, EqcInfo* >::iterator i = d_eqc_info.begin(), iend = d_eqc_info.end(); i != iend; ++i){
  82     EqcInfo* current = (*i).second;
  83     delete current;
  84   }
  85 }/* TheorySetsPrivate::~TheorySetsPrivate() */
  86
  87
  88 void TheorySetsPrivate::eqNotifyNewClass(TNode t) {
  89   if( t.getKind()==kind::SINGLETON || t.getKind()==kind::EMPTYSET ){
  90     EqcInfo * e = getOrMakeEqcInfo( t, true );
  91     e->d_singleton = t;
  92   }
  93   if( options::setsRelEager() ){
  94     d_rels->eqNotifyNewClass( t );
  95   }
  96 }
  97
  98 void TheorySetsPrivate::eqNotifyPreMerge(TNode t1, TNode t2){
  99
 100 }
 101
 102 void TheorySetsPrivate::eqNotifyPostMerge(TNode t1, TNode t2){
 103   if( !d_conflict ){
 104     Trace("sets-prop-debug") << "Merge " << t1 << " and " << t2 << "..." << std::endl;
 105     Node s1, s2;
 106     EqcInfo * e2 = getOrMakeEqcInfo( t2 );
 107     if( e2 ){
 108       s2 = e2->d_singleton;
 109       EqcInfo * e1 = getOrMakeEqcInfo( t1 );
 110       Node s1;
 111       Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
 112       if( e1 ){
 113         s1 = e1->d_singleton;
 114         if( !s1.isNull() && !s2.isNull() ){
 115           if( s1.getKind()==s2.getKind() ){
 116             Trace("sets-prop") << "Propagate eq inference : " << s1 << " == " << s2 << std::endl;
 117             //infer equality between elements of singleton
 118             Node exp = s1.eqNode( s2 );
 119             Node eq = s1[0].eqNode( s2[0] );
 120             d_keep.insert( exp );
 121             d_keep.insert( eq );
 122             assertFact( eq, exp );
 123           }else{
 124             //singleton equal to emptyset, conflict
 125             Trace("sets-prop") << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
 126             conflict( s1, s2 );
 127             return;
 128           }
 129         }
 130       }else{
 131         //copy information
 132         e1 = getOrMakeEqcInfo( t1, true );
 133         e1->d_singleton.set( e2->d_singleton );
 134       }
 135     }
 136     //merge membership list
 137     Trace("sets-prop-debug") << "Copying membership list..." << std::endl;
 138     NodeIntMap::iterator mem_i2 = d_members.find( t2 );
 139     if( mem_i2 != d_members.end() ) {
 140       NodeIntMap::iterator mem_i1 = d_members.find( t1 );
 141       int n_members = 0;
 142       if( mem_i1 != d_members.end() ) {
 143         n_members = (*mem_i1).second;
 144       }
 145       for( int i=0; i<(*mem_i2).second; i++ ){
 146         Assert( i<(int)d_members_data[t2].size() && d_members_data[t2][i].getKind()==kind::MEMBER );
 147         Node m2 = d_members_data[t2][i];
 148         //check if redundant
 149         bool add = true;
 150         for( int j=0; j<n_members; j++ ){
 151           Assert( j<(int)d_members_data[t1].size() && d_members_data[t1][j].getKind()==kind::MEMBER );
 152           if( ee_areEqual( m2[0], d_members_data[t1][j][0] ) ){
 153             add = false;
 154             break;
 155           }
 156         }
 157         if( add ){
 158           if( !s1.isNull() && s2.isNull() ){
 159             Assert( m2[1].getType()==s1.getType() );
 160             Assert( ee_areEqual( m2[1], s1 ) );
 161             Node exp = NodeManager::currentNM()->mkNode( kind::AND, m2[1].eqNode( s1 ), m2 );
 162             if( s1.getKind()==kind::SINGLETON ){
 163               if( s1[0]!=m2[0] ){
 164                 Node eq = s1[0].eqNode( m2[0] );
 165                 d_keep.insert( exp );
 166                 d_keep.insert( eq );
 167                 Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp << " => " << eq << std::endl;
 168                 assertFact( eq, exp );
 169               }
 170             }else{
 171               //conflict
 172               Trace("sets-prop") << "Propagate eq-mem conflict : " << exp << std::endl;
 173               d_conflict = true;
 174               d_external.d_out->conflict( exp );
 175               return;
 176             }
 177           }
 178           if( n_members<(int)d_members_data[t1].size() ){
 179             d_members_data[t1][n_members] = m2;
 180           }else{
 181             d_members_data[t1].push_back( m2 );
 182           }
 183           n_members++;
 184         }
 185       }
 186       d_members[t1] = n_members;
 187     }
 188     if( options::setsRelEager() ){
 189       d_rels->eqNotifyPostMerge( t1, t2 );
 190     }
 191   }
 192 }
 193
 194 void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason){
 195   if( t1.getType().isSet() ){
 196     Node eq = t1.eqNode( t2 );
 197     if( d_deq.find( eq )==d_deq.end() ){
 198       d_deq[eq] = true;
 199     }
 200   }
 201 }
 202
 203 TheorySetsPrivate::EqcInfo::EqcInfo( context::Context* c ) : d_singleton( c ){
 204
 205 }
 206
 207 TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo( TNode n, bool doMake ){
 208   std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n );
 209   if( eqc_i==d_eqc_info.end() ){
 210     EqcInfo* ei = NULL;
 211     if( doMake ){
 212       ei = new EqcInfo( d_external.getSatContext() );
 213       d_eqc_info[n] = ei;
 214     }
 215     return ei;
 216   }else{
 217     return eqc_i->second;
 218   }
 219 }
 220
 221
 222 bool TheorySetsPrivate::ee_areEqual( Node a, Node b ) {
 223   if( a==b ){
 224     return true;
 225   }else{
 226     if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
 227       return d_equalityEngine.areEqual( a, b );
 228     }else{
 229       return false;
 230     }
 231   }
 232 }
 233
 234 bool TheorySetsPrivate::ee_areDisequal( Node a, Node b ) {
 235   if( a==b ){
 236     return false;
 237   }else{
 238     if( d_equalityEngine.hasTerm( a ) && d_equalityEngine.hasTerm( b ) ){
 239       return d_equalityEngine.areDisequal( a, b, false );
 240     }else{
 241       return a.isConst() && b.isConst();
 242     }
 243   }
 244 }
 245
 246 bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
 247   if( n.getKind()==kind::NOT ){
 248     return isEntailed( n[0], !polarity );
 249   }else if( n.getKind()==kind::EQUAL ){
 250     if( polarity ){
 251       return ee_areEqual( n[0], n[1] );
 252     }else{
 253       return ee_areDisequal( n[0], n[1] );
 254     }
 255   }else if( n.getKind()==kind::MEMBER ){
 256     if( ee_areEqual( n, polarity ? d_true : d_false ) ){
 257       return true;
 258     }
 259     //check members cache
 260     if( polarity && d_equalityEngine.hasTerm( n[1] ) ){
 261       Node r = d_equalityEngine.getRepresentative( n[1] );
 262       if( isMember( n[0], r ) ){
 263         return true;
 264       }
 265     }
 266   }else if( n.getKind()==kind::AND || n.getKind()==kind::OR ){
 267     bool conj = (n.getKind()==kind::AND)==polarity;
 268     for( unsigned i=0; i<n.getNumChildren(); i++ ){
 269       bool isEnt = isEntailed( n[i], polarity );
 270       if( isEnt!=conj ){
 271         return !conj;
 272       }
 273     }
 274     return conj;
 275   }else if( n.isConst() ){
 276     return ( polarity && n==d_true ) || ( !polarity && n==d_false );
 277   }
 278   return false;
 279 }
 280
 281 bool TheorySetsPrivate::isMember( Node x, Node s ) {
 282   Assert( d_equalityEngine.hasTerm( s ) && d_equalityEngine.getRepresentative( s )==s );
 283   NodeIntMap::iterator mem_i = d_members.find( s );
 284   if( mem_i != d_members.end() ) {
 285     for( int i=0; i<(*mem_i).second; i++ ){
 286       if( ee_areEqual( d_members_data[s][i][0], x ) ){
 287         return true;
 288       }
 289     }
 290   }
 291   return false;
 292 }
 293
 294 bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) {
 295   Assert( d_equalityEngine.hasTerm( r1 ) && d_equalityEngine.getRepresentative( r1 )==r1 );
 296   Assert( d_equalityEngine.hasTerm( r2 ) && d_equalityEngine.getRepresentative( r2 )==r2 );
 297   TypeNode tn = r1.getType();
 298   Node eqc_es = d_eqc_emptyset[tn];
 299   bool is_sat = false;
 300   for( unsigned e=0; e<2; e++ ){
 301     Node a = e==0 ? r1 : r2;
 302     Node b = e==0 ? r2 : r1;
 303     //if there are members in a
 304     std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a );
 305     if( itpma!=d_pol_mems[0].end() ){
 306       Assert( !itpma->second.empty() );
 307       //if b is empty
 308       if( b==eqc_es ){
 309         if( !itpma->second.empty() ){
 310           is_sat = true;
 311           Trace("sets-deq") << "Disequality is satisfied because members are in " << a << " and " << b << " is empty" << std::endl;
 312         }else{
 313           //a should not be singleton
 314           Assert( d_eqc_singleton.find( a )==d_eqc_singleton.end() );
 315         }
 316       }else{
 317         std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b );
 318         std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b );
 319         std::vector< Node > prev;
 320         for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){
 321           //if b is a singleton
 322           if( itsb!=d_eqc_singleton.end() ){
 323             if( ee_areDisequal( itm->first, itsb->second[0] ) ){
 324               Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << ", singleton eq " << itsb->second[0] << std::endl;
 325               is_sat = true;
 326             }
 327             //or disequal with another member
 328             for( unsigned k=0; k<prev.size(); k++ ){
 329               if( ee_areDisequal( itm->first, prev[k] ) ){
 330                 Trace("sets-deq") << "Disequality is satisfied because of disequal members " << itm->first << " " << prev[k] << ", singleton eq " << std::endl;
 331                 is_sat = true;
 332                 break;
 333               }
 334             }
 335             //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality )
 336           //if a has positive member that is negative member in b
 337           }else if( itpmb!=d_pol_mems[1].end() ){
 338             for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){
 339               if( ee_areEqual( itm->first, itnm->first ) ){
 340                 Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << " " << itnm->second << std::endl;
 341                 is_sat = true;
 342                 break;
 343               }
 344             }
 345           }
 346           if( is_sat ){
 347             break;
 348           }
 349           prev.push_back( itm->first );
 350         }
 351       }
 352       if( is_sat ){
 353         break;
 354       }
 355     }
 356   }
 357   return is_sat;
 358 }
 359
 360 bool TheorySetsPrivate::assertFact( Node fact, Node exp ){
 361   Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl;
 362   bool polarity = fact.getKind() != kind::NOT;
 363   TNode atom = polarity ? fact : fact[0];
 364   if( !isEntailed( atom, polarity ) ){
 365     if( atom.getKind()==kind::EQUAL ){
 366       d_equalityEngine.assertEquality( atom, polarity, exp );
 367     }else{
 368       d_equalityEngine.assertPredicate( atom, polarity, exp );
 369     }
 370     if( !d_conflict ){
 371       if( atom.getKind()==kind::MEMBER && polarity ){
 372         //check if set has a value, if so, we can propagate
 373         Node r = d_equalityEngine.getRepresentative( atom[1] );
 374         EqcInfo * e = getOrMakeEqcInfo( r, true );
 375         if( e ){
 376           Node s = e->d_singleton;
 377           if( !s.isNull() ){
 378             Node exp = NodeManager::currentNM()->mkNode( kind::AND, atom, atom[1].eqNode( s ) );
 379             d_keep.insert( exp );
 380             if( s.getKind()==kind::SINGLETON ){
 381               if( s[0]!=atom[0] ){
 382                 Trace("sets-prop") << "Propagate mem-eq : " << exp << std::endl;
 383                 Node eq = s[0].eqNode( atom[0] );
 384                 d_keep.insert( eq );
 385                 assertFact( eq, exp );
 386               }
 387             }else{
 388               Trace("sets-prop") << "Propagate mem-eq conflict : " << exp << std::endl;
 389               d_conflict = true;
 390               d_external.d_out->conflict( exp );
 391             }
 392           }
 393         }
 394         //add to membership list
 395         NodeIntMap::iterator mem_i = d_members.find( r );
 396         int n_members = 0;
 397         if( mem_i != d_members.end() ) {
 398           n_members = (*mem_i).second;
 399         }
 400         d_members[r] = n_members + 1;
 401         if( n_members<(int)d_members_data[r].size() ){
 402           d_members_data[r][n_members] = atom;
 403         }else{
 404           d_members_data[r].push_back( atom );
 405         }
 406       }
 407     }
 408     return true;
 409   }else{
 410     return false;
 411   }
 412 }
 413
 414 bool TheorySetsPrivate::assertFactRec( Node fact, Node exp, std::vector< Node >& lemma, int inferType ) {
 415   if( ( options::setsInferAsLemmas() && inferType!=-1 ) || inferType==1 ){
 416     if( !isEntailed( fact, true ) ){
 417       lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
 418       return true;
 419     }
 420   }else{
 421     Trace("sets-fact") << "Assert fact rec : " << fact << ", exp = " << exp << std::endl;
 422     if( fact.isConst() ){
 423       //either trivial or a conflict
 424       if( fact==d_false ){
 425         Trace("sets-lemma") << "Conflict : " << exp << std::endl;
 426         d_conflict = true;
 427         d_external.d_out->conflict( exp );
 428         return true;
 429       }
 430     }else if( fact.getKind()==kind::AND || ( fact.getKind()==kind::NOT && fact[0].getKind()==kind::OR ) ){
 431       bool ret = false;
 432       Node f = fact.getKind()==kind::NOT ? fact[0] : fact;
 433       for( unsigned i=0; i<f.getNumChildren(); i++ ){
 434         Node factc = fact.getKind()==kind::NOT ? f[i].negate() : f[i];
 435         bool tret = assertFactRec( factc, exp, lemma, inferType );
 436         ret = ret || tret;
 437         if( d_conflict ){
 438           return true;
 439         }
 440       }
 441       return ret;
 442     }else{
 443       bool polarity = fact.getKind() != kind::NOT;
 444       TNode atom = polarity ? fact : fact[0];
 445       //things we can assert to equality engine
 446       if( atom.getKind()==kind::MEMBER || ( atom.getKind()==kind::EQUAL && atom[0].getType().isSet() ) ){
 447         //send to equality engine
 448         if( assertFact( fact, exp ) ){
 449           d_addedFact = true;
 450           return true;
 451         }
 452       }else{
 453         if( !isEntailed( fact, true ) ){
 454           //must send as lemma
 455           lemma.push_back( exp==d_true ? fact : NodeManager::currentNM()->mkNode( kind::IMPLIES, exp, fact ) );
 456           return true;
 457         }
 458       }
 459     }
 460   }
 461   return false;
 462 }
 463 void TheorySetsPrivate::assertInference( Node fact, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
 464   d_keep.insert( exp );
 465   d_keep.insert( fact );
 466   if( assertFactRec( fact, exp, lemmas, inferType ) ){
 467     Trace("sets-lemma") << "Sets::Lemma : " << fact << " from " << exp << " by " << c << std::endl;
 468     Trace("sets-assertion") << "(assert (=> " << exp << " " << fact << ")) ; by " << c << std::endl;
 469   }
 470 }
 471
 472 void TheorySetsPrivate::assertInference( Node fact, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ){
 473   Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
 474   assertInference( fact, exp_n, lemmas, c, inferType );
 475 }
 476
 477 void TheorySetsPrivate::assertInference( std::vector< Node >& conc, Node exp, std::vector< Node >& lemmas, const char * c, int inferType ){
 478   if( !conc.empty() ){
 479     Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
 480     assertInference( fact, exp, lemmas, c, inferType );
 481   }
 482 }
 483 void TheorySetsPrivate::assertInference( std::vector< Node >& conc, std::vector< Node >& exp, std::vector< Node >& lemmas, const char * c, int inferType ) {
 484   Node exp_n = exp.empty() ? d_true : ( exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ) );
 485   assertInference( conc, exp_n, lemmas, c, inferType );
 486 }
 487
 488 void TheorySetsPrivate::split( Node n, int reqPol ) {
 489   n = Rewriter::rewrite( n );
 490   Node lem = NodeManager::currentNM()->mkNode( kind::OR, n, n.negate() );
 491   std::vector< Node > lemmas;
 492   lemmas.push_back( lem );
 493   flushLemmas( lemmas );
 494   Trace("sets-lemma") << "Sets::Lemma split : " << lem << std::endl;
 495   if( reqPol!=0 ){
 496     Trace("sets-lemma") << "Sets::Require phase "  << n << " " << (reqPol>0) << std::endl;
 497     d_external.getOutputChannel().requirePhase( n, reqPol>0 );
 498   }
 499 }
 500
 501 void TheorySetsPrivate::fullEffortCheck(){
 502   Trace("sets") << "----- Full effort check ------" << std::endl;
 503   do{
 504     Trace("sets") << "...iterate full effort check..." << std::endl;
 505     Assert( d_equalityEngine.consistent() );
 506     d_sentLemma = false;
 507     d_addedFact = false;
 508     d_set_eqc.clear();
 509     d_set_eqc_list.clear();
 510     d_eqc_emptyset.clear();
 511     d_eqc_univset.clear();
 512     d_eqc_singleton.clear();
 513     d_congruent.clear();
 514     d_nvar_sets.clear();
 515     d_pol_mems[0].clear();
 516     d_pol_mems[1].clear();
 517     d_members_index.clear();
 518     d_singleton_index.clear();
 519     d_bop_index.clear();
 520     d_op_list.clear();
 521     d_card_enabled = false;
 522     d_rels_enabled = false;
 523     d_eqc_to_card_term.clear();
 524
 525     std::vector< Node > lemmas;
 526     Trace("sets-eqc") << "Equality Engine:" << std::endl;
 527     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine );
 528     while( !eqcs_i.isFinished() ){
 529       Node eqc = (*eqcs_i);
 530       bool isSet = false;
 531       TypeNode tn = eqc.getType();
 532       if( tn.isSet() ){
 533         isSet = true;
 534         d_set_eqc.push_back( eqc );
 535       }
 536       Trace("sets-eqc") << "[" << eqc << "] : ";
 537       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );
 538       while( !eqc_i.isFinished() ) {
 539         Node n = (*eqc_i);
 540         if( n!=eqc ){
 541           Trace("sets-eqc") << n << " ";
 542         }
 543         if( n.getKind()==kind::MEMBER ){
 544           if( eqc.isConst() ){
 545             Node s = d_equalityEngine.getRepresentative( n[1] );
 546             Node x = d_equalityEngine.getRepresentative( n[0] );
 547             int pindex = eqc==d_true ? 0 : ( eqc==d_false ? 1 : -1 );
 548             if( pindex!=-1  ){
 549               if( d_pol_mems[pindex][s].find( x )==d_pol_mems[pindex][s].end() ){
 550                 d_pol_mems[pindex][s][x] = n;
 551                 Trace("sets-debug2") << "Membership[" << x << "][" << s << "] : " << n << ", pindex = " << pindex << std::endl;
 552               }
 553               if( d_members_index[s].find( x )==d_members_index[s].end() ){
 554                 d_members_index[s][x] = n;
 555                 d_op_list[kind::MEMBER].push_back( n );
 556               }
 557             }else{
 558               Assert( false );
 559             }
 560           }
 561         }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION ||
 562                   n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){
 563           if( n.getKind()==kind::SINGLETON ){
 564             //singleton lemma
 565             getProxy( n );
 566             Node r = d_equalityEngine.getRepresentative( n[0] );
 567             if( d_singleton_index.find( r )==d_singleton_index.end() ){
 568               d_singleton_index[r] = n;
 569               d_eqc_singleton[eqc] = n;
 570               d_op_list[kind::SINGLETON].push_back( n );
 571             }else{
 572               d_congruent[n] = d_singleton_index[r];
 573             }
 574           }else if( n.getKind()==kind::EMPTYSET ){
 575             d_eqc_emptyset[tn] = eqc;
 576           }else if( n.getKind()==kind::UNIVERSE_SET ){
 577             d_eqc_univset[tn] = eqc;
 578           }else{
 579             Node r1 = d_equalityEngine.getRepresentative( n[0] );
 580             Node r2 = d_equalityEngine.getRepresentative( n[1] );
 581             if( d_bop_index[n.getKind()][r1].find( r2 )==d_bop_index[n.getKind()][r1].end() ){
 582               d_bop_index[n.getKind()][r1][r2] = n;
 583               d_op_list[n.getKind()].push_back( n );
 584             }else{
 585               d_congruent[n] = d_bop_index[n.getKind()][r1][r2];
 586             }
 587           }
 588           d_nvar_sets[eqc].push_back( n );
 589           Trace("sets-debug2") << "Non-var-set[" << eqc << "] : " << n << std::endl;
 590           d_set_eqc_list[eqc].push_back( n );
 591         }else if( n.getKind()==kind::CARD ){
 592           d_card_enabled = true;
 593           TypeNode tn = n[0].getType().getSetElementType();
 594           if( tn.isInterpretedFinite() ){
 595             std::stringstream ss;
 596             ss << "ERROR: cannot use cardinality on sets with finite element type." << std::endl;
 597             throw LogicException(ss.str());
 598             //TODO: extend approach for this case
 599           }
 600           Node r = d_equalityEngine.getRepresentative( n[0] );
 601           if( d_eqc_to_card_term.find( r )==d_eqc_to_card_term.end() ){
 602             d_eqc_to_card_term[ r ] = n;
 603             registerCardinalityTerm( n[0], lemmas );
 604           }
 605         }else{
 606           if( d_rels->isRelationKind( n.getKind() ) ){
 607             d_rels_enabled = true;
 608           }
 609           if( isSet ){
 610             d_set_eqc_list[eqc].push_back( n );
 611           }
 612         }
 613         ++eqc_i;
 614       }
 615       Trace("sets-eqc") << std::endl;
 616       ++eqcs_i;
 617     }
 618
 619     flushLemmas( lemmas );
 620     if( !hasProcessed() ){
 621       if( Trace.isOn("sets-mem") ){
 622         for( unsigned i=0; i<d_set_eqc.size(); i++ ){
 623           Node s = d_set_eqc[i];
 624           Trace("sets-mem") << "Eqc " << s << " : ";
 625           std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].find( s );
 626           if( it!=d_pol_mems[0].end() ){
 627             Trace("sets-mem") << "Memberships : ";
 628             for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 629               Trace("sets-mem") << it2->first << " ";
 630             }
 631           }
 632           std::map< Node, Node >::iterator its = d_eqc_singleton.find( s );
 633           if( its!=d_eqc_singleton.end() ){
 634             Trace("sets-mem") << " : Singleton : " << its->second;
 635           }
 636           Trace("sets-mem") << std::endl;
 637         }
 638       }
 639
 640       checkDownwardsClosure( lemmas );
 641       if( options::setsInferAsLemmas() ){
 642         flushLemmas( lemmas );
 643       }
 644       if( !hasProcessed() ){
 645         checkUpwardsClosure( lemmas );
 646         flushLemmas( lemmas );
 647         if( !hasProcessed() ){
 648           std::vector< Node > intro_sets;
 649           //for cardinality
 650           if( d_card_enabled ){
 651             checkCardBuildGraph( lemmas );
 652             flushLemmas( lemmas );
 653             if( !hasProcessed() ){
 654               checkMinCard( lemmas );
 655               flushLemmas( lemmas );
 656               if( !hasProcessed() ){
 657                 checkCardCycles( lemmas );
 658                 flushLemmas( lemmas );
 659                 if( !hasProcessed() ){
 660                   checkNormalForms( lemmas, intro_sets );
 661                   flushLemmas( lemmas );
 662                 }
 663               }
 664             }
 665           }
 666           if( !hasProcessed() ){
 667             checkDisequalities( lemmas );
 668             flushLemmas( lemmas );
 669             if( !hasProcessed() ){
 670               //introduce splitting on venn regions (absolute last resort)
 671               if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){
 672                 Assert( intro_sets.size()==1 );
 673                 Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
 674                 Trace("sets-intro") << "  Actual Intro : ";
 675                 debugPrintSet( intro_sets[0], "sets-nf" );
 676                 Trace("sets-nf") << std::endl;
 677                 Node k = getProxy( intro_sets[0] );
 678                 d_sentLemma = true;
 679               }
 680             }
 681           }
 682         }
 683       }
 684     }
 685   }while( !d_sentLemma && !d_conflict && d_addedFact );
 686   Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl;
 687 }
 688
 689 void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) {
 690   Trace("sets") << "Downwards closure..." << std::endl;
 691   //downwards closure
 692   for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
 693     std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( it->first );
 694     if( itn!=d_nvar_sets.end() ){
 695       for( unsigned j=0; j<itn->second.size(); j++ ){
 696         if( d_congruent.find( itn->second[j] )==d_congruent.end() ){
 697           for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 698             Node mem = it2->second;
 699             Node eq_set = itn->second[j];
 700             Assert( d_equalityEngine.areEqual( mem[1], eq_set ) );
 701             if( mem[1]!=eq_set ){
 702               Trace("sets-debug") << "Downwards closure based on " << mem << ", eq_set = " << eq_set << std::endl;
 703               if( !options::setsProxyLemmas() ){
 704                 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
 705                 nmem = Rewriter::rewrite( nmem );
 706                 std::vector< Node > exp;
 707                 exp.push_back( mem );
 708                 exp.push_back( mem[1].eqNode( eq_set ) );
 709                 assertInference( nmem, exp, lemmas, "downc" );
 710                 if( d_conflict ){
 711                   return;
 712                 }
 713               }else{
 714                 //use proxy set
 715                 Node k = getProxy( eq_set );
 716                 Node pmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], k );
 717                 Node nmem = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], eq_set );
 718                 nmem = Rewriter::rewrite( nmem );
 719                 std::vector< Node > exp;
 720                 if( ee_areEqual( mem, pmem ) ){
 721                   exp.push_back( pmem );
 722                 }else{
 723                   nmem = NodeManager::currentNM()->mkNode( kind::OR, pmem.negate(), nmem );
 724                 }
 725                 assertInference( nmem, exp, lemmas, "downc" );
 726               }
 727             }
 728           }
 729         }
 730       }
 731     }
 732   }
 733 }
 734
 735 void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) {
 736   //upwards closure
 737   for( std::map< Kind, std::map< Node, std::map< Node, Node > > >::iterator itb = d_bop_index.begin(); itb != d_bop_index.end(); ++itb ){
 738     Kind k = itb->first;
 739     Trace("sets") << "Upwards closure " << k << "..." << std::endl;
 740     for( std::map< Node, std::map< Node, Node > >::iterator it = itb->second.begin(); it != itb->second.end(); ++it ){
 741       Node r1 = it->first;
 742       //see if there are members in first argument r1
 743       std::map< Node, std::map< Node, Node > >::iterator itm1 = d_pol_mems[0].find( r1 );
 744       if( itm1!=d_pol_mems[0].end() || k==kind::UNION ){
 745         for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 746           Node r2 = it2->first;
 747           //see if there are members in second argument
 748           std::map< Node, std::map< Node, Node > >::iterator itm2 = d_pol_mems[0].find( r2 );
 749           if( itm2!=d_pol_mems[0].end() || k!=kind::INTERSECTION ){
 750             Trace("sets-debug") << "Checking " << it2->second << ", members = " << (itm1!=d_pol_mems[0].end()) << ", " << (itm2!=d_pol_mems[0].end()) << std::endl;
 751             //for all members of r1
 752             if( itm1!=d_pol_mems[0].end() ){
 753               for( std::map< Node, Node >::iterator itm1m = itm1->second.begin(); itm1m != itm1->second.end(); ++itm1m ){
 754                 Node xr = itm1m->first;
 755                 Node x = itm1m->second[0];
 756                 Trace("sets-debug") << "checking membership " << xr << " " << itm1m->second << std::endl;
 757                 std::vector< Node > exp;
 758                 exp.push_back( itm1m->second );
 759                 addEqualityToExp( it2->second[0], itm1m->second[1], exp );
 760                 bool valid = false;
 761                 int inferType = 0;
 762                 if( k==kind::UNION ){
 763                   valid = true;
 764                 }else if( k==kind::INTERSECTION ){
 765                   //conclude x is in it2->second
 766                   //if also existing in members of r2
 767                   bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
 768                   if( in_r2 ){
 769                     exp.push_back( itm2->second[xr] );
 770                     addEqualityToExp( it2->second[1], itm2->second[xr][1], exp );
 771                     addEqualityToExp( x, itm2->second[xr][0], exp );
 772                     valid = true;
 773                   }
 774                 }else{
 775                   Assert( k==kind::SETMINUS );
 776                   /*
 777                   std::map< Node, std::map< Node, Node > >::iterator itnm2 = d_pol_mems[1].find( r2 );
 778                   if( itnm2!=d_pol_mems[1].end() ){
 779                     bool not_in_r2 = itnm2->second.find( xr )!=itnm2->second.end();
 780                     if( not_in_r2 ){
 781                       exp.push_back( itnm2->second[xr] );
 782                       if( it2->second[1]!=itnm2->second[xr][1] ){
 783                         Assert( d_equalityEngine.areEqual( it2->second[1], itnm2->second[xr][1] ) );
 784                         exp.push_back( it2->second[1].eqNode( itnm2->second[xr][1] ) );
 785                       }
 786                       if( x!=itnm2->second[xr][0] ){
 787                         Assert( d_equalityEngine.areEqual( x, itnm2->second[xr][0] ) );
 788                         exp.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, x, itnm2->second[xr][0] ) );
 789                       }
 790                       valid = true;
 791                     }
 792                   }
 793                   */
 794                   if( !valid ){
 795                     bool in_r2 = itm2!=d_pol_mems[0].end() && itm2->second.find( xr )!=itm2->second.end();
 796                     if( !in_r2 ){
 797                       // must add lemma for set minus since non-membership in this case is not explained
 798                       exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, x, it2->second[1] ).negate() );
 799                       valid = true;
 800                       inferType = 1;
 801                     }
 802                   }
 803                 }
 804                 if( valid ){
 805                   Node rr = d_equalityEngine.getRepresentative( it2->second );
 806                   if( !isMember( x, rr ) ){
 807                     Node kk = getProxy( it2->second );
 808                     Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, kk );
 809                     assertInference( fact, exp, lemmas, "upc", inferType );
 810                     if( d_conflict ){
 811                       return;
 812                     }
 813                   }
 814                 }
 815                 Trace("sets-debug") << "done checking membership " << xr << " " << itm1m->second << std::endl;
 816               }
 817             }
 818             if( k==kind::UNION ){
 819               if( itm2!=d_pol_mems[0].end() ){
 820                 //for all members of r2
 821                 for( std::map< Node, Node >::iterator itm2m = itm2->second.begin(); itm2m != itm2->second.end(); ++itm2m ){
 822                   Node x = itm2m->second[0];
 823                   Node rr = d_equalityEngine.getRepresentative( it2->second );
 824                   if( !isMember( x, rr ) ){
 825                     std::vector< Node > exp;
 826                     exp.push_back( itm2m->second );
 827                     addEqualityToExp( it2->second[1], itm2m->second[1], exp );
 828                     Node k = getProxy( it2->second );
 829                     Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, x, k );
 830                     assertInference( fact, exp, lemmas, "upc2" );
 831                     if( d_conflict ){
 832                       return;
 833                     }
 834                   }
 835                 }
 836               }
 837             }
 838           }
 839         }
 840       }
 841     }
 842   }
 843   if( !hasProcessed() ){
 844     //universal sets
 845     Trace("sets-debug") << "Check universe sets..." << std::endl;
 846     //all elements must be in universal set
 847     for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){
 848       TypeNode tn = it->first.getType();
 849       std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn );
 850       if( itu==d_eqc_univset.end() || itu->second!=it->first ){
 851         Node u = getUnivSet( tn );
 852         for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){
 853           Node mem = it2->second;
 854           Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], u );
 855           assertInference( fact, mem, lemmas, "upuniv" );
 856           if( d_conflict ){
 857             return;
 858           }
 859         }
 860       }
 861     }
 862   }
 863 }
 864
 865 void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) {
 866   //disequalities
 867   Trace("sets") << "Disequalities..." << std::endl;
 868   for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) {
 869     if( (*it).second ){
 870       Node deq = (*it).first;
 871       //check if it is already satisfied
 872       Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) );
 873       Node r1 = d_equalityEngine.getRepresentative( deq[0] );
 874       Node r2 = d_equalityEngine.getRepresentative( deq[1] );
 875       bool is_sat = isSetDisequalityEntailed( r1, r2 );
 876       /*
 877       if( !is_sat ){
 878         //try to make one of them empty
 879         for( unsigned e=0; e<2; e++ ){
 880         }
 881       }
 882       */
 883       Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl;
 884       //will process regardless of sat/processed/unprocessed
 885       d_deq[deq] = false;
 886
 887       if( !is_sat ){
 888         if( d_deq_processed.find( deq )==d_deq_processed.end() ){
 889           d_deq_processed.insert( deq );
 890           d_deq_processed.insert( deq[1].eqNode( deq[0] ) );
 891           Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
 892           TypeNode elementType = deq[0].getType().getSetElementType();
 893           Node x = NodeManager::currentNM()->mkSkolem("sde_", elementType);
 894           Node mem1 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[0] );
 895           Node mem2 = NodeManager::currentNM()->mkNode( kind::MEMBER, x, deq[1] );
 896           Node lem = NodeManager::currentNM()->mkNode( kind::OR, deq, NodeManager::currentNM()->mkNode( kind::EQUAL, mem1, mem2 ).negate() );
 897           lem = Rewriter::rewrite( lem );
 898           assertInference( lem, d_emp_exp, lemmas, "diseq", 1 );
 899           flushLemmas( lemmas );
 900           if( hasProcessed() ){
 901             return;
 902           }
 903         }
 904       }
 905     }
 906   }
 907 }
 908
 909 void TheorySetsPrivate::checkCardBuildGraph( std::vector< Node >& lemmas ) {
 910   Trace("sets") << "Cardinality graph..." << std::endl;
 911   //first, ensure cardinality relationships are added as lemmas for all non-basic set terms
 912   for( unsigned i=0; i<d_set_eqc.size(); i++ ){
 913     Node eqc = d_set_eqc[i];
 914     std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
 915     if( itn!=d_nvar_sets.end() ){
 916       for( unsigned j=0; j<itn->second.size(); j++ ){
 917         Node n = itn->second[j];
 918         if( d_congruent.find( n )==d_congruent.end() ){
 919           //if setminus, do for intersection instead
 920           if( n.getKind()==kind::SETMINUS ){
 921             n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
 922           }
 923           registerCardinalityTerm( n, lemmas );
 924         }
 925       }
 926     }
 927   }
 928   Trace("sets") << "Done cardinality graph" << std::endl;
 929 }
 930
 931 void TheorySetsPrivate::registerCardinalityTerm( Node n, std::vector< Node >& lemmas ){
 932   if( d_card_processed.find( n )==d_card_processed.end() ){
 933     d_card_processed.insert( n );
 934     Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
 935     std::vector< Node > cterms;
 936     if( n.getKind()==kind::INTERSECTION ){
 937       for( unsigned e=0; e<2; e++ ){
 938         Node s = NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] );
 939         cterms.push_back( s );
 940       }
 941       Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, n ), d_zero );
 942       assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
 943     }else{
 944       cterms.push_back( n );
 945     }
 946     for( unsigned k=0; k<cterms.size(); k++ ){
 947       Node nn = cterms[k];
 948       Node nk = getProxy( nn );
 949       Node pos_lem = NodeManager::currentNM()->mkNode( kind::GEQ, NodeManager::currentNM()->mkNode( kind::CARD, nk ), d_zero );
 950       assertInference( pos_lem, d_emp_exp, lemmas, "pcard", 1 );
 951       if( nn!=nk ){
 952         Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::CARD, nk ),
 953                                                                   NodeManager::currentNM()->mkNode( kind::CARD, nn ) );
 954         lem = Rewriter::rewrite( lem );
 955         Trace("sets-card") << "  " << k << " : " << lem << std::endl;
 956         assertInference( lem, d_emp_exp, lemmas, "card", 1 );
 957       }
 958     }
 959   }
 960 }
 961
 962 void TheorySetsPrivate::checkCardCycles( std::vector< Node >& lemmas ) {
 963   Trace("sets") << "Check cardinality cycles..." << std::endl;
 964   //build order of equivalence classes, also build cardinality graph
 965   std::vector< Node > set_eqc_tmp;
 966   set_eqc_tmp.insert( set_eqc_tmp.end(), d_set_eqc.begin(), d_set_eqc.end() );
 967   d_set_eqc.clear();
 968   d_card_parent.clear();
 969   for( unsigned i=0; i<set_eqc_tmp.size(); i++ ){
 970     std::vector< Node > curr;
 971     std::vector< Node > exp;
 972     checkCardCyclesRec( set_eqc_tmp[i], curr, exp, lemmas );
 973     flushLemmas( lemmas );
 974     if( hasProcessed() ){
 975       return;
 976     }
 977   }
 978   Trace("sets") << "Done check cardinality cycles" << std::endl;
 979 }
 980
 981 void TheorySetsPrivate::checkCardCyclesRec( Node eqc, std::vector< Node >& curr, std::vector< Node >& exp, std::vector< Node >& lemmas ) {
 982   if( std::find( curr.begin(), curr.end(), eqc )!=curr.end() ){
 983     Trace("sets-debug") << "Found venn region loop..." << std::endl;
 984     if( curr.size()>1 ){
 985       //all regions must be equal
 986       std::vector< Node > conc;
 987       for( unsigned i=1; i<curr.size(); i++ ){
 988         conc.push_back( curr[0].eqNode( curr[i] ) );
 989       }
 990       Node fact = conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::AND, conc );
 991       assertInference( fact, exp, lemmas, "card_cycle" );
 992       flushLemmas( lemmas );
 993     }else{
 994       //should be guaranteed based on not exploring equal parents
 995       Assert( false );
 996     }
 997   }else if( std::find( d_set_eqc.begin(), d_set_eqc.end(), eqc )==d_set_eqc.end() ){
 998     curr.push_back( eqc );
 999     TypeNode tn = eqc.getType();
1000     bool is_empty = eqc==d_eqc_emptyset[tn];
1001     Node emp_set = getEmptySet( tn );
1002     std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1003     if( itn!=d_nvar_sets.end() ){
1004       for( unsigned j=0; j<itn->second.size(); j++ ){
1005         Node n = itn->second[j];
1006         if( n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS ){
1007           Trace("sets-debug") << "Build cardinality parents for " << n << "..." << std::endl;
1008           std::vector< Node > sib;
1009           unsigned true_sib = 0;
1010           if( n.getKind()==kind::INTERSECTION ){
1011             d_card_base[n] = n;
1012             for( unsigned e=0; e<2; e++ ){
1013               Node sm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[e], n[1-e] ) );
1014               sib.push_back( sm );
1015             }
1016             true_sib = 2;
1017           }else{
1018             Node si = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, n[0], n[1] ) );
1019             sib.push_back( si );
1020             d_card_base[n] = si;
1021             Node osm = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::SETMINUS, n[1], n[0] ) );
1022             sib.push_back( osm );
1023             true_sib = 1;
1024           }
1025           Node u = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::UNION, n[0], n[1] ) );
1026           if( !d_equalityEngine.hasTerm( u ) ){
1027             u = Node::null();
1028           }
1029           unsigned n_parents = true_sib + ( u.isNull() ? 0 : 1 );
1030           //if this set is empty
1031           if( is_empty ){
1032             Assert( ee_areEqual( n, emp_set ) );
1033             Trace("sets-debug") << "  empty, parents equal siblings" << std::endl;
1034             std::vector< Node > conc;
1035             //parent equal siblings
1036             for( unsigned e=0; e<true_sib; e++ ){
1037               if( d_equalityEngine.hasTerm( sib[e] ) && !ee_areEqual( n[e], sib[e] ) ){
1038                 conc.push_back( n[e].eqNode( sib[e] ) );
1039               }
1040             }
1041             assertInference( conc, n.eqNode( emp_set ), lemmas, "cg_emp" );
1042             flushLemmas( lemmas );
1043             if( hasProcessed() ){
1044               return;
1045             }else{
1046               //justify why there is no edge to parents (necessary?)
1047               for( unsigned e=0; e<n_parents; e++ ){
1048                 Node p = (e==true_sib) ? u : n[e];
1049
1050               }
1051             }
1052           }else{
1053             std::vector< Node > card_parents;
1054             std::vector< int > card_parent_ids;
1055             //check if equal to a parent
1056             for( unsigned e=0; e<n_parents; e++ ){
1057               Trace("sets-debug") << "  check parent " << e << "/" << n_parents << std::endl;
1058               bool is_union = e==true_sib;
1059               Node p = (e==true_sib) ? u : n[e];
1060               Trace("sets-debug") << "  check relation to parent " << p << ", isu=" << is_union << "..." << std::endl;
1061               //if parent is empty
1062               if( ee_areEqual( p, emp_set ) ){
1063                 Trace("sets-debug") << "  it is empty..." << std::endl;
1064                 Assert( !ee_areEqual( n, emp_set ) );
1065                 assertInference( n.eqNode( emp_set ), p.eqNode( emp_set ), lemmas, "cg_emppar" );
1066                 if( hasProcessed() ){
1067                   return;
1068                 }
1069               //if we are equal to a parent
1070               }else if( ee_areEqual( p, n ) ){
1071                 Trace("sets-debug") << "  it is equal to this..." << std::endl;
1072                 std::vector< Node > conc;
1073                 std::vector< int > sib_emp_indices;
1074                 if( is_union ){
1075                   for( unsigned s=0; s<sib.size(); s++ ){
1076                     sib_emp_indices.push_back( s );
1077                   }
1078                 }else{
1079                   sib_emp_indices.push_back( e );
1080                 }
1081                 //sibling(s) are empty
1082                 for( unsigned s=0; s<sib_emp_indices.size(); s++ ){
1083                   unsigned si = sib_emp_indices[s];
1084                   if( !ee_areEqual( sib[si], emp_set ) ){
1085                     conc.push_back( sib[si].eqNode( emp_set ) );
1086                   }else{
1087                     Trace("sets-debug") << "Sibling " << sib[si] << " is already empty." << std::endl;
1088                   }
1089                 }
1090                 if( !is_union && n.getKind()==kind::INTERSECTION && !u.isNull() ){
1091                   //union is equal to other parent
1092                   if( !ee_areEqual( u, n[1-e] ) ){
1093                     conc.push_back( u.eqNode( n[1-e] ) );
1094                   }
1095                 }
1096                 Trace("sets-debug") << "...derived " << conc.size() << " conclusions" << std::endl;
1097                 assertInference( conc, n.eqNode( p ), lemmas, "cg_eqpar" );
1098                 flushLemmas( lemmas );
1099                 if( hasProcessed() ){
1100                   return;
1101                 }
1102               }else{
1103                 Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
1104                 //otherwise, we a syntactic subset of p
1105                 card_parents.push_back( p );
1106                 card_parent_ids.push_back( is_union ? 2 : e );
1107               }
1108             }
1109             Assert( d_card_parent[n].empty() );
1110             Trace("sets-debug") << "get parent representatives..." << std::endl;
1111             //for each parent, take their representatives
1112             for( unsigned k=0; k<card_parents.size(); k++ ){
1113               Node eqcc = d_equalityEngine.getRepresentative( card_parents[k] );
1114               Trace("sets-debug") << "Check card parent " << k << "/" << card_parents.size() << std::endl;
1115
1116               //if parent is singleton, then we should either be empty to equal to it
1117               std::map< Node, Node >::iterator itps = d_eqc_singleton.find( eqcc );
1118               if( itps!=d_eqc_singleton.end() ){
1119                 bool eq_parent = false;
1120                 std::vector< Node > exp;
1121                 addEqualityToExp( card_parents[k], itps->second, exp );
1122                 if( ee_areDisequal( n, emp_set ) ){
1123                   exp.push_back( n.eqNode( emp_set ).negate() );
1124                   eq_parent = true;
1125                 }else{
1126                   std::map< Node, std::map< Node, Node > >::iterator itpm = d_pol_mems[0].find( eqc );
1127                   if( itpm!=d_pol_mems[0].end() && !itpm->second.empty() ){
1128                     Node pmem = itpm->second.begin()->second;
1129                     exp.push_back( pmem );
1130                     addEqualityToExp( n, pmem[1], exp );
1131                     eq_parent = true;
1132                   }
1133                 }
1134                 //must be equal to parent
1135                 if( eq_parent ){
1136                   Node conc = n.eqNode(  card_parents[k] );
1137                   assertInference( conc, exp, lemmas, "cg_par_sing" );
1138                   flushLemmas( lemmas );
1139                 }else{
1140                   //split on empty
1141                   Trace("sets-nf") << "Split empty : " << n << std::endl;
1142                   split( n.eqNode( emp_set ), 1 );
1143                 }
1144                 Assert( hasProcessed() );
1145                 return;
1146               }else{
1147                 bool dup = false;
1148                 for( unsigned l=0; l<d_card_parent[n].size(); l++ ){
1149                   if( eqcc==d_card_parent[n][l] ){
1150                     Trace("sets-debug") << "  parents " << l << " and " << k << " are equal, ids = " << card_parent_ids[l] << " " << card_parent_ids[k] << std::endl;
1151                     dup = true;
1152                     if( n.getKind()==kind::INTERSECTION ){
1153                       Assert( card_parent_ids[l]!=2 );
1154                       std::vector< Node > conc;
1155                       if( card_parent_ids[k]==2 ){
1156                         //intersection is equal to other parent
1157                         unsigned pid = 1-card_parent_ids[l];
1158                         if( !ee_areEqual( n[pid], n ) ){
1159                           Trace("sets-debug") << "  one of them is union, make equal to other..." << std::endl;
1160                           conc.push_back( n[pid].eqNode( n ) );
1161                         }
1162                       }else{
1163                         if( !ee_areEqual( card_parents[k], n ) ){
1164                           Trace("sets-debug") << "  neither is union, make equal to one parent..." << std::endl;
1165                           //intersection is equal to one of the parents
1166                           conc.push_back( card_parents[k].eqNode( n ) );
1167                         }
1168                       }
1169                       assertInference( conc, card_parents[k].eqNode( d_card_parent[n][l] ), lemmas, "cg_pareq" );
1170                       flushLemmas( lemmas );
1171                       if( hasProcessed() ){
1172                         return;
1173                       }
1174                     }
1175                   }
1176                 }
1177                 if( !dup ){
1178                   d_card_parent[n].push_back( eqcc );
1179                 }
1180               }
1181             }
1182             //now recurse on parents (to ensure their normal will be computed after this eqc)
1183             exp.push_back( eqc.eqNode( n ) );
1184             for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1185               checkCardCyclesRec( d_card_parent[n][k], curr, exp, lemmas );
1186               if( hasProcessed() ){
1187                 return;
1188               }
1189             }
1190             exp.pop_back();
1191           }
1192         }
1193       }
1194     }
1195     curr.pop_back();
1196     //parents now processed, can add to ordered list
1197     d_set_eqc.push_back( eqc );
1198   }else{
1199     //already processed
1200   }
1201 }
1202
1203 void TheorySetsPrivate::checkNormalForms( std::vector< Node >& lemmas, std::vector< Node >& intro_sets ){
1204   Trace("sets") << "Check normal forms..." << std::endl;
1205   // now, build normal form for each equivalence class
1206   //   d_set_eqc is now sorted such that for each d_set_eqc[i], d_set_eqc[j],
1207   //      if d_set_eqc[i] is a strict syntactic subterm of d_set_eqc[j], then i<j.
1208   d_ff.clear();
1209   d_nf.clear();
1210   for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1211     checkNormalForm( d_set_eqc[i], intro_sets );
1212     if( hasProcessed() || !intro_sets.empty() ){
1213       return;
1214     }
1215   }
1216   Trace("sets") << "Done check normal forms" << std::endl;
1217 }
1218
1219 void TheorySetsPrivate::checkNormalForm( Node eqc, std::vector< Node >& intro_sets ){
1220   TypeNode tn = eqc.getType();
1221   Trace("sets") << "Compute normal form for " << eqc << std::endl;
1222   Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
1223   if( eqc==d_eqc_emptyset[tn] ){
1224     d_nf[eqc].clear();
1225     Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
1226   }else{
1227     //flat/normal forms are sets of equivalence classes
1228     Node base;
1229     std::vector< Node > comps;
1230     std::map< Node, std::map< Node, std::vector< Node > > >::iterator it = d_ff.find( eqc );
1231     if( it!=d_ff.end() ){
1232       for( std::map< Node, std::vector< Node > >::iterator itf = it->second.begin(); itf != it->second.end(); ++itf ){
1233         std::sort( itf->second.begin(), itf->second.end() );
1234         if( base.isNull() ){
1235           base = itf->first;
1236         }else{
1237           comps.push_back( itf->first );
1238         }
1239         Trace("sets-nf") << "  F " << itf->first << " : ";
1240         if( Trace.isOn("sets-nf") ){
1241           Trace("sets-nf") << "{ ";
1242           for( unsigned k=0; k<itf->second.size(); k++ ){
1243             if( k>0 ){ Trace("sets-nf") << ", "; }
1244             Trace("sets-nf") << "[" << itf->second[k] << "]";
1245           }
1246           Trace("sets-nf") << " }" << std::endl;
1247         }
1248         Trace("sets-nf-debug") << " ...";
1249         debugPrintSet( itf->first, "sets-nf-debug" );
1250         Trace("sets-nf-debug") << std::endl;
1251       }
1252     }else{
1253       Trace("sets-nf") << "(no flat forms)" << std::endl;
1254     }
1255
1256     Assert( d_nf.find( eqc )==d_nf.end() );
1257     bool success = true;
1258     if( !base.isNull() ){
1259       Node emp_set = getEmptySet( tn );
1260       for( unsigned j=0; j<comps.size(); j++ ){
1261         //compare if equal
1262         std::vector< Node > c;
1263         c.push_back( base );
1264         c.push_back( comps[j] );
1265         std::vector< Node > only[2];
1266         std::vector< Node > common;
1267         Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs " << comps[j] << std::endl;
1268         unsigned k[2] = { 0, 0 };
1269         while( k[0]<d_ff[eqc][c[0]].size() || k[1]<d_ff[eqc][c[1]].size() ){
1270           bool proc = true;
1271           for( unsigned e=0; e<2; e++ ){
1272             if( k[e]==d_ff[eqc][c[e]].size() ){
1273               for( ; k[1-e]<d_ff[eqc][c[1-e]].size(); ++k[1-e] ){
1274                 only[1-e].push_back( d_ff[eqc][c[1-e]][k[1-e]] );
1275               }
1276               proc = false;
1277             }
1278           }
1279           if( proc ){
1280             if( d_ff[eqc][c[0]][k[0]]==d_ff[eqc][c[1]][k[1]] ){
1281               common.push_back( d_ff[eqc][c[0]][k[0]] );
1282               k[0]++;
1283               k[1]++;
1284             }else if( d_ff[eqc][c[0]][k[0]]<d_ff[eqc][c[1]][k[1]] ){
1285               only[0].push_back( d_ff[eqc][c[0]][k[0]] );
1286               k[0]++;
1287             }else{
1288               only[1].push_back( d_ff[eqc][c[1]][k[1]] );
1289               k[1]++;
1290             }
1291           }
1292         }
1293         if( !only[0].empty() || !only[1].empty() ){
1294           if( Trace.isOn("sets-nf-debug") ){
1295             Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
1296             for( unsigned e=0; e<2; e++ ){
1297               Trace("sets-nf-debug") << "  " << c[e] << " : { ";
1298               for( unsigned l=0; l<only[e].size(); l++ ){
1299                 if( l>0 ){ Trace("sets-nf-debug") << ", "; }
1300                 Trace("sets-nf-debug") << "[" << only[e][l] << "]";
1301               }
1302               Trace("sets-nf-debug") << " }" << std::endl;
1303             }
1304           }
1305           //try to make one empty, prefer the unique ones first
1306           for( unsigned e=0; e<3; e++ ){
1307             unsigned sz = e==2 ? common.size() : only[e].size();
1308             for( unsigned l=0; l<sz; l++ ){
1309               Node r = e==2 ? common[l] : only[e][l];
1310               Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
1311               Trace("sets-nf-debug") << "         actual : ";
1312               debugPrintSet( r, "sets-nf-debug" );
1313               Trace("sets-nf-debug") << std::endl;
1314               Assert( !ee_areEqual( r, emp_set ) );
1315               if( !ee_areDisequal( r, emp_set ) && ( d_pol_mems[0].find( r )==d_pol_mems[0].end() || d_pol_mems[0][r].empty() ) ){
1316                 //guess that its equal empty if it has no explicit members
1317                 Trace("sets-nf") << " Split empty : " << r << std::endl;
1318                 Trace("sets-nf") << "Actual Split : ";
1319                 debugPrintSet( r, "sets-nf" );
1320                 Trace("sets-nf") << std::endl;
1321                 split( r.eqNode( emp_set ), 1 );
1322                 Assert( hasProcessed() );
1323                 return;
1324               }
1325             }
1326           }
1327           for( unsigned l=0; l<only[0].size(); l++ ){
1328             for( unsigned m=0; m<only[1].size(); m++ ){
1329               bool disjoint = false;
1330               Trace("sets-nf-debug") << "Try split " << only[0][l] << " against " << only[1][m] << std::endl;
1331               //split them
1332               for( unsigned e=0; e<2; e++ ){
1333                 Node r1 = e==0 ? only[0][l] : only[1][m];
1334                 Node r2 = e==0 ? only[1][m] : only[0][l];
1335                 //check if their intersection exists modulo equality
1336                 std::map< Node, Node >::iterator itb = d_bop_index[kind::INTERSECTION][r1].find( r2 );
1337                 if( itb!=d_bop_index[kind::INTERSECTION][r1].end() ){
1338                   Trace("sets-nf-debug") << "Split term already exists, but not in cardinality graph : " << itb->second << ", should be empty." << std::endl;
1339                   //their intersection is empty (probably?)
1340                   // e.g. these are two disjoint venn regions, proceed to next pair
1341                   Assert( ee_areEqual( emp_set, itb->second ) );
1342                   disjoint = true;
1343                   break;
1344                 }
1345               }
1346               if( !disjoint ){
1347                 //simply introduce their intersection
1348                 Assert( only[0][l]!=only[1][m] );
1349                 Node kca = getProxy( only[0][l] );
1350                 Node kcb = getProxy( only[1][m] );
1351                 Node intro = Rewriter::rewrite( NodeManager::currentNM()->mkNode( kind::INTERSECTION, kca, kcb ) );
1352                 Trace("sets-nf") << "   Intro split : " << only[0][l] << " against " << only[1][m] << ", term is " << intro << std::endl;
1353                 intro_sets.push_back( intro );
1354                 Assert( !d_equalityEngine.hasTerm( intro ) );
1355                 return;
1356               }
1357             }
1358           }
1359           //should never get here
1360           success = false;
1361         }
1362       }
1363       if( success ){
1364         //normal form is flat form of base
1365         d_nf[eqc].insert( d_nf[eqc].end(), d_ff[eqc][base].begin(), d_ff[eqc][base].end() );
1366         Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
1367       }else{
1368         Trace("sets-nf") << "failed to build N " << eqc << std::endl;
1369         Assert( false );
1370       }
1371     }else{
1372       //normal form is this equivalence class
1373       d_nf[eqc].push_back( eqc );
1374       Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }" << std::endl;
1375     }
1376     if( success ){
1377       //send to parents
1378       std::map< Node, std::vector< Node > >::iterator itn = d_nvar_sets.find( eqc );
1379       if( itn!=d_nvar_sets.end() ){
1380         std::map< Node, std::map< Node, bool > > parents_proc;
1381         for( unsigned j=0; j<itn->second.size(); j++ ){
1382           Node n = itn->second[j];
1383           Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
1384           if( !d_card_parent[n].empty() ){
1385             Assert( d_card_base.find( n )!=d_card_base.end() );
1386             Node cbase = d_card_base[n];
1387             Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
1388             for( unsigned k=0; k<d_card_parent[n].size(); k++ ){
1389               Node p = d_card_parent[n][k];
1390               Trace("sets-nf-debug") << "Check parent " << p << std::endl;
1391               if( parents_proc[cbase].find( p )==parents_proc[cbase].end() ){
1392                 parents_proc[cbase][p] = true;
1393                 Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p << "] ), from " << n << "..." << std::endl;
1394                 //for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1395                 //  Assert( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() );
1396                 //}
1397                 for( unsigned i=0; i<d_nf[eqc].size(); i++ ){
1398                   if( std::find( d_ff[p][cbase].begin(), d_ff[p][cbase].end(), d_nf[eqc][i] )==d_ff[p][cbase].end() ){
1399                     d_ff[p][cbase].insert( d_ff[p][cbase].end(), d_nf[eqc].begin(), d_nf[eqc].end() );
1400                   }else{
1401                     //if it is a duplicate venn region, it must be empty since it is coming from syntactically disjoint siblings TODO?
1402                   }
1403                 }
1404               }else{
1405                 Trace("sets-nf-debug") << "..already processed parent " << p << " for " << cbase << std::endl;
1406               }
1407             }
1408           }
1409         }
1410       }
1411     }else{
1412       Assert( hasProcessed() );
1413     }
1414   }
1415 }
1416
1417 void TheorySetsPrivate::checkMinCard( std::vector< Node >& lemmas ) {
1418
1419   for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1420     Node eqc = d_set_eqc[i];
1421     //get members in class
1422     std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1423     if( itm!=d_pol_mems[0].end() ){
1424       std::vector< Node > exp;
1425       std::vector< Node > members;
1426       Node cardTerm;
1427       std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1428       if( it!=d_eqc_to_card_term.end() ){
1429         cardTerm = it->second;
1430       }else{
1431         cardTerm = NodeManager::currentNM()->mkNode( kind::CARD, eqc );
1432       }
1433       for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1434       /*
1435         for( unsigned j=0; j<members.size(); j++ ){
1436           if( !ee_areDisequal( members[j], itmm->second ) ){
1437             Assert( !ee_areEqual( members[j], itmm->second ) );
1438
1439           }
1440         }
1441       */
1442         members.push_back( itmm->first );
1443         exp.push_back( NodeManager::currentNM()->mkNode( kind::MEMBER, itmm->first, cardTerm[0] ) );
1444       }
1445       if( members.size()>1 ){
1446         exp.push_back( NodeManager::currentNM()->mkNode( kind::DISTINCT, members ) );
1447       }
1448       if( !members.empty() ){
1449         Node conc = NodeManager::currentNM()->mkNode( kind::GEQ, cardTerm, NodeManager::currentNM()->mkConst( Rational( members.size() ) ) );
1450         Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, exp.size()==1 ? exp[0] : NodeManager::currentNM()->mkNode( kind::AND, exp ), conc );
1451         Trace("sets-lemma") << "Sets::Lemma : " << lem << " by mincard" << std::endl;
1452         lemmas.push_back( lem );
1453       }
1454     }
1455   }
1456 }
1457
1458 void TheorySetsPrivate::flushLemmas( std::vector< Node >& lemmas ) {
1459   //do lemmas
1460   for( unsigned i=0; i<lemmas.size(); i++ ){
1461     Node lem = lemmas[i];
1462     if( d_lemmas_produced.find(lem)==d_lemmas_produced.end() ){
1463       Trace("sets-lemma-debug") << "Send lemma : " << lem << std::endl;
1464       d_lemmas_produced.insert(lem);
1465       d_external.d_out->lemma(lem);
1466       d_sentLemma = true;
1467     }else{
1468       Trace("sets-lemma-debug") << "Already sent lemma : " << lem << std::endl;
1469     }
1470   }
1471   lemmas.clear();
1472 }
1473
1474 Node TheorySetsPrivate::getProxy( Node n ) {
1475   if( n.getKind()==kind::EMPTYSET || n.getKind()==kind::SINGLETON || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::UNION ){
1476     NodeMap::const_iterator it = d_proxy.find( n );
1477     if( it==d_proxy.end() ){
1478       Node k = NodeManager::currentNM()->mkSkolem( "sp", n.getType(), "proxy for set" );
1479       d_proxy[n] = k;
1480       d_proxy_to_term[k] = n;
1481       Node eq = k.eqNode( n );
1482       Trace("sets-lemma") << "Sets::Lemma : " << eq << " by proxy" << std::endl;
1483       d_external.d_out->lemma( eq );
1484       if( n.getKind()==kind::SINGLETON ){
1485         Node slem = NodeManager::currentNM()->mkNode( kind::MEMBER, n[0], k );
1486         Trace("sets-lemma") << "Sets::Lemma : " << slem << " by singleton" << std::endl;
1487         d_external.d_out->lemma( slem );
1488         d_sentLemma = true;
1489       }
1490       return k;
1491     }else{
1492       return (*it).second;
1493     }
1494   }else{
1495     return n;
1496   }
1497 }
1498
1499 Node TheorySetsPrivate::getCongruent( Node n ) {
1500   Assert( d_equalityEngine.hasTerm( n ) );
1501   std::map< Node, Node >::iterator it = d_congruent.find( n );
1502   if( it==d_congruent.end() ){
1503     return n;
1504   }else{
1505     return it->second;
1506   }
1507 }
1508
1509 Node TheorySetsPrivate::getEmptySet( TypeNode tn ) {
1510   std::map< TypeNode, Node >::iterator it = d_emptyset.find( tn );
1511   if( it==d_emptyset.end() ){
1512     Node n = NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
1513     d_emptyset[tn] = n;
1514     return n;
1515   }else{
1516     return it->second;
1517   }
1518 }
1519 Node TheorySetsPrivate::getUnivSet( TypeNode tn ) {
1520   std::map< TypeNode, Node >::iterator it = d_univset.find( tn );
1521   if( it==d_univset.end() ){
1522     Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET);
1523     d_univset[tn] = n;
1524     return n;
1525   }else{
1526     return it->second;
1527   }
1528 }
1529
1530 bool TheorySetsPrivate::hasLemmaCached( Node lem ) {
1531   return d_lemmas_produced.find(lem)!=d_lemmas_produced.end();
1532 }
1533
1534 bool TheorySetsPrivate::hasProcessed() {
1535   return d_conflict || d_sentLemma || d_addedFact;
1536 }
1537
1538 void TheorySetsPrivate::debugPrintSet( Node s, const char * c ) {
1539   if( s.getNumChildren()==0 ){
1540     NodeMap::const_iterator it = d_proxy_to_term.find( s );
1541     if( it!=d_proxy_to_term.end() ){
1542       debugPrintSet( (*it).second, c );
1543     }else{
1544       Trace(c) << s;
1545     }
1546   }else{
1547     Trace(c) << "(" << s.getOperator();
1548     for( unsigned i=0; i<s.getNumChildren(); i++ ){
1549       Trace(c) << " ";
1550       debugPrintSet( s[i], c );
1551     }
1552     Trace(c) << ")";
1553   }
1554 }
1555
1556 /**************************** TheorySetsPrivate *****************************/
1557 /**************************** TheorySetsPrivate *****************************/
1558 /**************************** TheorySetsPrivate *****************************/
1559
1560 void TheorySetsPrivate::check(Theory::Effort level) {
1561   Trace("sets-check") << "Sets check effort " << level << std::endl;
1562   while(!d_external.done() && !d_conflict) {
1563     // Get all the assertions
1564     Assertion assertion = d_external.get();
1565     TNode fact = assertion.assertion;
1566     Trace("sets-assert") << "Assert from input " << fact << std::endl;
1567     //assert the fact
1568     assertFact( fact, fact );
1569   }
1570   d_sentLemma = false;
1571   Trace("sets-check") << "Sets finished assertions effort " << level << std::endl;
1572   //invoke full effort check, relations check
1573   if( !d_conflict ){
1574     if( level == Theory::EFFORT_FULL ){
1575       if( !d_external.d_valuation.needCheck() ){
1576         fullEffortCheck();
1577         if( !d_conflict && !d_sentLemma ){
1578           //invoke relations solver
1579           d_rels->check(level);
1580           if( d_card_enabled && d_rels_enabled ){
1581             //incomplete if we have both cardinality constraints and relational operators?
1582             // TODO: should internally check model, return unknown if fail
1583             d_external.d_out->setIncomplete();
1584           }
1585         }
1586       }
1587     }else{
1588       if( options::setsRelEager() ){
1589         d_rels->check(level);
1590       }
1591     }
1592   }
1593   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
1594 }/* TheorySetsPrivate::check() */
1595
1596
1597 /************************ Sharing ************************/
1598 /************************ Sharing ************************/
1599 /************************ Sharing ************************/
1600
1601 void TheorySetsPrivate::addSharedTerm(TNode n) {
1602   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
1603   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
1604 }
1605
1606 void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth, unsigned& n_pairs ){
1607   if( depth==arity ){
1608     if( t2!=NULL ){
1609       Node f1 = t1->getNodeData();
1610       Node f2 = t2->getNodeData();
1611       if( !ee_areEqual( f1, f2 ) ){
1612         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
1613         vector< pair<TNode, TNode> > currentPairs;
1614         for (unsigned k = 0; k < f1.getNumChildren(); ++ k) {
1615           TNode x = f1[k];
1616           TNode y = f2[k];
1617           Assert( d_equalityEngine.hasTerm(x) );
1618           Assert( d_equalityEngine.hasTerm(y) );
1619           Assert( !ee_areDisequal( x, y ) );
1620           if( !d_equalityEngine.areEqual( x, y ) ){
1621             Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
1622             if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
1623               TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
1624               TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
1625               Trace("sets-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
1626               EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(x_shared, y_shared);
1627               Trace("sets-cg") << "...eq status is " << eqStatus << std::endl;
1628               if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
1629                 //an argument is disequal, we are done
1630                 return;
1631               }else{
1632                 currentPairs.push_back(make_pair(x_shared, y_shared));
1633               }
1634             }else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
1635               //splitting on sets (necessary for handling set of sets properly)
1636               if( x.getType().isSet() ){
1637                 Assert( y.getType().isSet() );
1638                 if( !ee_areDisequal( x, y ) ){
1639                   Trace("sets-cg-lemma") << "Should split on : " << x << "==" << y << std::endl;
1640                   split( x.eqNode( y ) );
1641                 }
1642               }
1643             }
1644           }
1645         }
1646         for (unsigned c = 0; c < currentPairs.size(); ++ c) {
1647           Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl;
1648           d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
1649           n_pairs++;
1650         }
1651       }
1652     }
1653   }else{
1654     if( t2==NULL ){
1655       if( depth<(arity-1) ){
1656         //add care pairs internal to each child
1657         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1658           addCarePairs( &it->second, NULL, arity, depth+1, n_pairs );
1659         }
1660       }
1661       //add care pairs based on each pair of non-disequal arguments
1662       for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1663         std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
1664         ++it2;
1665         for( ; it2 != t1->d_data.end(); ++it2 ){
1666           if( !ee_areDisequal(it->first, it2->first) ){
1667             addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1668           }
1669         }
1670       }
1671     }else{
1672       //add care pairs based on product of indices, non-disequal arguments
1673       for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
1674         for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
1675           if( !ee_areDisequal(it->first, it2->first) ){
1676             addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
1677           }
1678         }
1679       }
1680     }
1681   }
1682 }
1683
1684 void TheorySetsPrivate::computeCareGraph() {
1685   for( std::map< Kind, std::vector< Node > >::iterator it = d_op_list.begin(); it != d_op_list.end(); ++it ){
1686     if( it->first==kind::SINGLETON || it->first==kind::MEMBER ){
1687       unsigned n_pairs = 0;
1688       Trace("sets-cg-summary") << "Compute graph for sets, op=" << it->first << "..." << it->second.size() << std::endl;
1689       Trace("sets-cg") << "Build index for " << it->first << "..." << std::endl;
1690       std::map< TypeNode, quantifiers::TermArgTrie > index;
1691       unsigned arity = 0;
1692       //populate indices
1693       for( unsigned i=0; i<it->second.size(); i++ ){
1694         TNode f1 = it->second[i];
1695         Assert(d_equalityEngine.hasTerm(f1));
1696         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
1697         //break into index based on operator, and type of first argument (since some operators are parametric)
1698         TypeNode tn = f1[0].getType();
1699         std::vector< TNode > reps;
1700         bool hasCareArg = false;
1701         for( unsigned j=0; j<f1.getNumChildren(); j++ ){
1702           reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) );
1703           if( isCareArg( f1, j ) ){
1704             hasCareArg = true;
1705           }
1706         }
1707         if( hasCareArg ){
1708           index[tn].addTerm( f1, reps );
1709           arity = reps.size();
1710         }
1711       }
1712       if( arity>0 ){
1713         //for each index
1714         for( std::map< TypeNode, quantifiers::TermArgTrie >::iterator iti = index.begin(); iti != index.end(); ++iti ){
1715           Trace("sets-cg") << "Process index " << iti->first << "..." << std::endl;
1716           addCarePairs( &iti->second, NULL, arity, 0, n_pairs );
1717         }
1718       }
1719       Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1720     }
1721   }
1722 }
1723
1724 bool TheorySetsPrivate::isCareArg( Node n, unsigned a ) {
1725   if( d_equalityEngine.isTriggerTerm( n[a], THEORY_SETS ) ){
1726     return true;
1727   }else if( ( n.getKind()==kind::MEMBER || n.getKind()==kind::SINGLETON ) && a==0 && n[0].getType().isSet() ){
1728     return true;
1729   }else{
1730     return false;
1731   }
1732 }
1733
1734 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
1735   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
1736   if (d_equalityEngine.areEqual(a, b)) {
1737     // The terms are implied to be equal
1738     return EQUALITY_TRUE;
1739   }
1740   if (d_equalityEngine.areDisequal(a, b, false)) {
1741     // The terms are implied to be dis-equal
1742     return EQUALITY_FALSE;
1743   }
1744   return EQUALITY_UNKNOWN;
1745   /*
1746   Node aModelValue = d_external.d_valuation.getModelValue(a);
1747   if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1748   Node bModelValue = d_external.d_valuation.getModelValue(b);
1749   if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1750   if( aModelValue == bModelValue ) {
1751     // The term are true in current model
1752     return EQUALITY_TRUE_IN_MODEL;
1753   } else {
1754     return EQUALITY_FALSE_IN_MODEL;
1755   }
1756   */
1757   // }
1758   // //TODO: can we be more precise sometimes?
1759   // return EQUALITY_UNKNOWN;
1760 }
1761
1762 /******************** Model generation ********************/
1763 /******************** Model generation ********************/
1764 /******************** Model generation ********************/
1765
1766
1767 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) {
1768   Trace("sets-model") << "Set collect model info" << std::endl;
1769   set<Node> termSet;
1770   // Compute terms appearing in assertions and shared terms
1771   d_external.computeRelevantTerms(termSet);
1772
1773   // Assert equalities and disequalities to the model
1774   m->assertEqualityEngine(&d_equalityEngine,&termSet);
1775
1776   std::map< Node, Node > mvals;
1777   for( int i=(int)(d_set_eqc.size()-1); i>=0; i-- ){
1778     Node eqc = d_set_eqc[i];
1779     if( termSet.find( eqc )==termSet.end() ){
1780       Trace("sets-model") << "* Do not assign value for " << eqc << " since is not relevant." << std::endl;
1781     }else{
1782       std::vector< Node > els;
1783       bool is_base = !d_card_enabled || ( d_nf[eqc].size()==1 && d_nf[eqc][0]==eqc );
1784       if( is_base ){
1785         Trace("sets-model") << "Collect elements of base eqc " << eqc << std::endl;
1786         // members that must be in eqc
1787         std::map< Node, std::map< Node, Node > >::iterator itm = d_pol_mems[0].find( eqc );
1788         if( itm!=d_pol_mems[0].end() ){
1789           for( std::map< Node, Node >::iterator itmm = itm->second.begin(); itmm != itm->second.end(); ++itmm ){
1790             Node t = NodeManager::currentNM()->mkNode( kind::SINGLETON, itmm->first );
1791             els.push_back( t );
1792           }
1793         }
1794       }
1795       if( d_card_enabled ){
1796         TypeNode elementType = eqc.getType().getSetElementType();
1797         if( is_base ){
1798           std::map< Node, Node >::iterator it = d_eqc_to_card_term.find( eqc );
1799           if( it!=d_eqc_to_card_term.end() ){
1800             //slack elements from cardinality value
1801             Node v = d_external.d_valuation.getModelValue(it->second);
1802             Trace("sets-model") << "Cardinality of " << eqc << " is " << v << std::endl;
1803             Assert(v.getConst<Rational>() <= LONG_MAX, "Exceeded LONG_MAX in sets model");
1804             unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
1805             Assert( els.size()<=vu );
1806             while( els.size()<vu ){
1807               els.push_back( NodeManager::currentNM()->mkNode( kind::SINGLETON, NodeManager::currentNM()->mkSkolem( "msde", elementType ) ) );
1808             }
1809           }else{
1810             Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1811           }
1812         }else{
1813           Trace("sets-model") << "Build value for " << eqc << " based on normal form, size = " << d_nf[eqc].size() << std::endl;
1814           //it is union of venn regions
1815           for( unsigned j=0; j<d_nf[eqc].size(); j++ ){
1816             Assert( mvals.find( d_nf[eqc][j] )!=mvals.end() );
1817             els.push_back( mvals[d_nf[eqc][j]] );
1818           }
1819         }
1820       }
1821       Node rep = NormalForm::mkBop( kind::UNION, els, eqc.getType() );
1822       rep = Rewriter::rewrite( rep );
1823       Trace("sets-model") << "* Assign representative of " << eqc << " to " << rep << std::endl;
1824       mvals[eqc] = rep;
1825       m->assertEquality( eqc, rep, true );
1826       m->assertRepresentative( rep );
1827     }
1828   }
1829 }
1830
1831 /********************** Helper functions ***************************/
1832 /********************** Helper functions ***************************/
1833 /********************** Helper functions ***************************/
1834
1835 void TheorySetsPrivate::addEqualityToExp( Node a, Node b, std::vector< Node >& exp ) {
1836   if( a!=b ){
1837     Assert( ee_areEqual( a, b ) );
1838     exp.push_back( a.eqNode( b ) );
1839   }
1840 }
1841
1842 Node mkAnd(const std::vector<TNode>& conjunctions) {
1843   Assert(conjunctions.size() > 0);
1844
1845   std::set<TNode> all;
1846   for (unsigned i = 0; i < conjunctions.size(); ++i) {
1847     TNode t = conjunctions[i];
1848     if (t.getKind() == kind::AND) {
1849       for(TNode::iterator child_it = t.begin();
1850           child_it != t.end(); ++child_it) {
1851         Assert((*child_it).getKind() != kind::AND);
1852         all.insert(*child_it);
1853       }
1854     }
1855     else {
1856       all.insert(t);
1857     }
1858   }
1859
1860   Assert(all.size() > 0);
1861   if (all.size() == 1) {
1862     // All the same, or just one
1863     return conjunctions[0];
1864   }
1865
1866   NodeBuilder<> conjunction(kind::AND);
1867   std::set<TNode>::const_iterator it = all.begin();
1868   std::set<TNode>::const_iterator it_end = all.end();
1869   while (it != it_end) {
1870     conjunction << *it;
1871     ++ it;
1872   }
1873
1874   return conjunction;
1875 }/* mkAnd() */
1876
1877
1878 TheorySetsPrivate::Statistics::Statistics() :
1879   d_getModelValueTime("theory::sets::getModelValueTime")
1880   , d_mergeTime("theory::sets::merge_nodes::time")
1881   , d_processCard2Time("theory::sets::processCard2::time")
1882   , d_memberLemmas("theory::sets::lemmas::member", 0)
1883   , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
1884   , d_numVertices("theory::sets::vertices", 0)
1885   , d_numVerticesMax("theory::sets::vertices-max", 0)
1886   , d_numMergeEq1or2("theory::sets::merge1or2", 0)
1887   , d_numMergeEq3("theory::sets::merge3", 0)
1888   , d_numLeaves("theory::sets::leaves", 0)
1889   , d_numLeavesMax("theory::sets::leaves-max", 0)
1890 {
1891   smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
1892   smtStatisticsRegistry()->registerStat(&d_mergeTime);
1893   smtStatisticsRegistry()->registerStat(&d_processCard2Time);
1894   smtStatisticsRegistry()->registerStat(&d_memberLemmas);
1895   smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
1896   smtStatisticsRegistry()->registerStat(&d_numVertices);
1897   smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
1898   smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
1899   smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
1900   smtStatisticsRegistry()->registerStat(&d_numLeaves);
1901   smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
1902 }
1903
1904
1905 TheorySetsPrivate::Statistics::~Statistics() {
1906   smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
1907   smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
1908   smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
1909   smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
1910   smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
1911   smtStatisticsRegistry()->unregisterStat(&d_numVertices);
1912   smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
1913   smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
1914   smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
1915   smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
1916   smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
1917 }
1918
1919 void TheorySetsPrivate::propagate(Theory::Effort effort) {
1920
1921 }
1922
1923 bool TheorySetsPrivate::propagate(TNode literal) {
1924   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
1925
1926   // If already in conflict, no more propagation
1927   if (d_conflict) {
1928     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
1929     return false;
1930   }
1931
1932   // Propagate out
1933   bool ok = d_external.d_out->propagate(literal);
1934   if (!ok) {
1935     d_conflict = true;
1936   }
1937
1938   return ok;
1939 }/* TheorySetsPrivate::propagate(TNode) */
1940
1941
1942 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
1943   d_equalityEngine.setMasterEqualityEngine(eq);
1944 }
1945
1946
1947 void TheorySetsPrivate::conflict(TNode a, TNode b)
1948 {
1949   d_conflictNode = explain(a.eqNode(b));
1950   d_external.d_out->conflict(d_conflictNode);
1951   Debug("sets") << "[sets] conflict: " << a << " iff " << b
1952                 << ", explaination " << d_conflictNode << std::endl;
1953   Trace("sets-lemma") << "Equality Conflict : " << d_conflictNode << std::endl;
1954   d_conflict = true;
1955 }
1956
1957 Node TheorySetsPrivate::explain(TNode literal)
1958 {
1959   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
1960                 << std::endl;
1961
1962   bool polarity = literal.getKind() != kind::NOT;
1963   TNode atom = polarity ? literal : literal[0];
1964   std::vector<TNode> assumptions;
1965
1966   if(atom.getKind() == kind::EQUAL) {
1967     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
1968   } else if(atom.getKind() == kind::MEMBER) {
1969     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
1970   } else {
1971     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1972                   << polarity << "); kind" << atom.getKind() << std::endl;
1973     Unhandled();
1974   }
1975
1976   return mkAnd(assumptions);
1977 }
1978
1979 void TheorySetsPrivate::preRegisterTerm(TNode node)
1980 {
1981   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1982                 << std::endl;
1983   switch(node.getKind()) {
1984   case kind::EQUAL:
1985     // TODO: what's the point of this
1986     d_equalityEngine.addTriggerEquality(node);
1987     break;
1988   case kind::MEMBER:
1989     // TODO: what's the point of this
1990     d_equalityEngine.addTriggerPredicate(node);
1991     break;
1992   case kind::CARD:
1993     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1994     break;
1995   default:
1996     //if( node.getType().isSet() ){
1997     //  d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1998     //}else{
1999     d_equalityEngine.addTerm(node);
2000     //}
2001     break;
2002   }
2003 }
2004
2005
2006 void TheorySetsPrivate::presolve() {
2007
2008 }
2009
2010 /**************************** eq::NotifyClass *****************************/
2011 /**************************** eq::NotifyClass *****************************/
2012 /**************************** eq::NotifyClass *****************************/
2013
2014
2015 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
2016 {
2017   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
2018                    << " value = " << value << std::endl;
2019   if (value) {
2020     return d_theory.propagate(equality);
2021   } else {
2022     // We use only literal triggers so taking not is safe
2023     return d_theory.propagate(equality.notNode());
2024   }
2025 }
2026
2027 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
2028 {
2029   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
2030                    << " value = " << value << std::endl;
2031   if (value) {
2032     return d_theory.propagate(predicate);
2033   } else {
2034     return d_theory.propagate(predicate.notNode());
2035   }
2036 }
2037
2038 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
2039 {
2040   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
2041                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
2042   d_theory.propagate( value ? t1.eqNode( t2 ) : t1.eqNode( t2 ).negate() );
2043   return true;
2044 }
2045
2046 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
2047 {
2048   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2049   d_theory.conflict(t1, t2);
2050 }
2051
2052 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
2053 {
2054   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
2055   d_theory.eqNotifyNewClass(t);
2056 }
2057
2058 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
2059 {
2060   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2061   d_theory.eqNotifyPreMerge(t1, t2);
2062 }
2063
2064 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
2065 {
2066   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
2067   d_theory.eqNotifyPostMerge(t1, t2);
2068 }
2069
2070 void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
2071 {
2072   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
2073   d_theory.eqNotifyDisequal(t1, t2, reason);
2074 }
2075
2076 }/* CVC4::theory::sets namespace */
2077 }/* CVC4::theory namespace */
2078 }/* CVC4 namespace */