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