src/theory/sep/theory_sep.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sep.cpp
   3  ** \verbatim
   4  ** Original author: Andrew Reynolds
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief Implementation of the theory of sep.
  13  **
  14  ** Implementation of the theory of sep.
  15  **/
  16
  17
  18 #include "theory/sep/theory_sep.h"
  19 #include "theory/valuation.h"
  20 #include "expr/kind.h"
  21 #include <map>
  22 #include "theory/rewriter.h"
  23 #include "theory/theory_model.h"
  24 #include "options/sep_options.h"
  25 #include "options/smt_options.h"
  26 #include "smt/logic_exception.h"
  27 #include "theory/quantifiers_engine.h"
  28 #include "theory/quantifiers/term_database.h"
  29 #include "options/quantifiers_options.h"
  30
  31 using namespace std;
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace sep {
  36
  37 TheorySep::TheorySep(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
  38   Theory(THEORY_SEP, c, u, out, valuation, logicInfo),
  39   d_lemmas_produced_c(u),
  40   d_notify(*this),
  41   d_equalityEngine(d_notify, c, "theory::sep::TheorySep", true),
  42   d_conflict(c, false),
  43   d_reduce(u),
  44   d_infer(c),
  45   d_infer_exp(c),
  46   d_spatial_assertions(c)
  47 {
  48   d_true = NodeManager::currentNM()->mkConst<bool>(true);
  49   d_false = NodeManager::currentNM()->mkConst<bool>(false);
  50   d_bounds_init = false;
  51
  52   // The kinds we are treating as function application in congruence
  53   d_equalityEngine.addFunctionKind(kind::SEP_PTO);
  54   //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
  55 }
  56
  57 TheorySep::~TheorySep() {
  58   for( std::map< Node, HeapAssertInfo * >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){
  59     delete it->second;
  60   }
  61 }
  62
  63 void TheorySep::setMasterEqualityEngine(eq::EqualityEngine* eq) {
  64   d_equalityEngine.setMasterEqualityEngine(eq);
  65 }
  66
  67 Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) {
  68   if( assumptions.empty() ){
  69     return d_true;
  70   }else if( assumptions.size()==1 ){
  71     return assumptions[0];
  72   }else{
  73     return NodeManager::currentNM()->mkNode( kind::AND, assumptions );
  74   }
  75 }
  76
  77 /////////////////////////////////////////////////////////////////////////////
  78 // PREPROCESSING
  79 /////////////////////////////////////////////////////////////////////////////
  80
  81
  82
  83 Node TheorySep::ppRewrite(TNode term) {
  84   Trace("sep-pp") << "ppRewrite : " << term << std::endl;
  85   return term;
  86 }
  87
  88 Theory::PPAssertStatus TheorySep::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
  89
  90   return PP_ASSERT_STATUS_UNSOLVED;
  91 }
  92
  93
  94 /////////////////////////////////////////////////////////////////////////////
  95 // T-PROPAGATION / REGISTRATION
  96 /////////////////////////////////////////////////////////////////////////////
  97
  98
  99 bool TheorySep::propagate(TNode literal)
 100 {
 101   Debug("sep") << "TheorySep::propagate(" << literal  << ")" << std::endl;
 102   // If already in conflict, no more propagation
 103   if (d_conflict) {
 104     Debug("sep") << "TheorySep::propagate(" << literal << "): already in conflict" << std::endl;
 105     return false;
 106   }
 107   bool ok = d_out->propagate(literal);
 108   if (!ok) {
 109     d_conflict = true;
 110   }
 111   return ok;
 112 }/* TheorySep::propagate(TNode) */
 113
 114
 115 void TheorySep::explain(TNode literal, std::vector<TNode>& assumptions) {
 116   if( literal.getKind()==kind::SEP_LABEL ||
 117       ( literal.getKind()==kind::NOT && literal[0].getKind()==kind::SEP_LABEL ) ){
 118     //labelled assertions are never given to equality engine and should only come from the outside
 119     assumptions.push_back( literal );
 120   }else{
 121     // Do the work
 122     bool polarity = literal.getKind() != kind::NOT;
 123     TNode atom = polarity ? literal : literal[0];
 124     if (atom.getKind() == kind::EQUAL) {
 125       d_equalityEngine.explainEquality( atom[0], atom[1], polarity, assumptions, NULL );
 126     } else {
 127       d_equalityEngine.explainPredicate( atom, polarity, assumptions );
 128     }
 129   }
 130 }
 131
 132
 133 void TheorySep::propagate(Effort e){
 134
 135 }
 136
 137
 138 Node TheorySep::explain(TNode literal)
 139 {
 140   Debug("sep") << "TheorySep::explain(" << literal << ")" << std::endl;
 141   std::vector<TNode> assumptions;
 142   explain(literal, assumptions);
 143   return mkAnd(assumptions);
 144 }
 145
 146
 147 /////////////////////////////////////////////////////////////////////////////
 148 // SHARING
 149 /////////////////////////////////////////////////////////////////////////////
 150
 151
 152 void TheorySep::addSharedTerm(TNode t) {
 153   Debug("sep") << "TheorySep::addSharedTerm(" << t << ")" << std::endl;
 154   d_equalityEngine.addTriggerTerm(t, THEORY_SEP);
 155 }
 156
 157
 158 EqualityStatus TheorySep::getEqualityStatus(TNode a, TNode b) {
 159   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
 160   if (d_equalityEngine.areEqual(a, b)) {
 161     // The terms are implied to be equal
 162     return EQUALITY_TRUE;
 163   }
 164   else if (d_equalityEngine.areDisequal(a, b, false)) {
 165     // The terms are implied to be dis-equal
 166     return EQUALITY_FALSE;
 167   }
 168   return EQUALITY_UNKNOWN;//FALSE_IN_MODEL;
 169 }
 170
 171
 172 void TheorySep::computeCareGraph() {
 173   Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
 174   for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
 175     TNode a = d_sharedTerms[i];
 176     TypeNode aType = a.getType();
 177     for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
 178       TNode b = d_sharedTerms[j];
 179       if (b.getType() != aType) {
 180         // We don't care about the terms of different types
 181         continue;
 182       }
 183       switch (d_valuation.getEqualityStatus(a, b)) {
 184       case EQUALITY_TRUE_AND_PROPAGATED:
 185       case EQUALITY_FALSE_AND_PROPAGATED:
 186         // If we know about it, we should have propagated it, so we can skip
 187         break;
 188       default:
 189         // Let's split on it
 190         addCarePair(a, b);
 191         break;
 192       }
 193     }
 194   }
 195 }
 196
 197
 198 /////////////////////////////////////////////////////////////////////////////
 199 // MODEL GENERATION
 200 /////////////////////////////////////////////////////////////////////////////
 201
 202
 203 void TheorySep::collectModelInfo( TheoryModel* m ){
 204   set<Node> termSet;
 205
 206   // Compute terms appearing in assertions and shared terms
 207   computeRelevantTerms(termSet);
 208
 209   // Send the equality engine information to the model
 210   m->assertEqualityEngine( &d_equalityEngine, &termSet );
 211 }
 212
 213 void TheorySep::postProcessModel( TheoryModel* m ){
 214   Trace("sep-model") << "Printing model for TheorySep..." << std::endl;
 215
 216   std::vector< Node > sep_children;
 217   Node m_neq;
 218   Node m_heap;
 219   for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
 220     //should only be constructing for one heap type
 221     Assert( m_heap.isNull() );
 222     Assert( d_loc_to_data_type.find( it->first )!=d_loc_to_data_type.end() );
 223     Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl;
 224     TypeNode data_type = d_loc_to_data_type[it->first];
 225     computeLabelModel( it->second );
 226     if( d_label_model[it->second].d_heap_locs_model.empty() ){
 227       Trace("sep-model") << "  [empty]" << std::endl;
 228     }else{
 229       for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
 230         Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON );
 231         std::vector< Node > pto_children;
 232         Node l = d_label_model[it->second].d_heap_locs_model[j][0];
 233         Assert( l.isConst() );
 234         pto_children.push_back( l );
 235         Trace("sep-model") << " " << l << " -> ";
 236         if( d_pto_model[l].isNull() ){
 237           Trace("sep-model") << "_";
 238           //m->d_comment_str << "_";
 239           TypeEnumerator te_range( data_type );
 240           if( data_type.isInterpretedFinite() ){
 241             pto_children.push_back( *te_range );
 242           }else{
 243             //must enumerate until we find one that is not explicitly pointed to
 244             bool success = false;
 245             Node cv;
 246             do{
 247               cv = *te_range;
 248               if( std::find( d_heap_locs_nptos[l].begin(), d_heap_locs_nptos[l].end(), cv )==d_heap_locs_nptos[l].end() ){
 249                 success = true;
 250               }else{
 251                 ++te_range;
 252               }
 253             }while( !success );
 254             pto_children.push_back( cv );
 255           }
 256         }else{
 257           Trace("sep-model") << d_pto_model[l];
 258           Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] );
 259           Assert( vpto.isConst() );
 260           pto_children.push_back( vpto );
 261         }
 262         Trace("sep-model") << std::endl;
 263         sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) );
 264       }
 265     }
 266     Node nil = getNilRef( it->first );
 267     Node vnil = d_valuation.getModel()->getRepresentative( nil );
 268     m_neq = NodeManager::currentNM()->mkNode( kind::EQUAL, nil, vnil );
 269     Trace("sep-model") << "sep.nil = " << vnil << std::endl;
 270     Trace("sep-model") << std::endl;
 271     if( sep_children.empty() ){
 272       TypeEnumerator te_domain( it->first );
 273       TypeEnumerator te_range( d_loc_to_data_type[it->first] );
 274       m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
 275     }else if( sep_children.size()==1 ){
 276       m_heap = sep_children[0];
 277     }else{
 278       m_heap = NodeManager::currentNM()->mkNode( kind::SEP_STAR, sep_children );
 279     }
 280     m->setHeapModel( m_heap, m_neq );
 281   }
 282   Trace("sep-model") << "Finished printing model for TheorySep." << std::endl;
 283 }
 284
 285 /////////////////////////////////////////////////////////////////////////////
 286 // NOTIFICATIONS
 287 /////////////////////////////////////////////////////////////////////////////
 288
 289
 290 void TheorySep::presolve() {
 291   Trace("sep-pp") << "Presolving" << std::endl;
 292   //TODO: cleanup if incremental?
 293 }
 294
 295
 296 /////////////////////////////////////////////////////////////////////////////
 297 // MAIN SOLVER
 298 /////////////////////////////////////////////////////////////////////////////
 299
 300
 301 void TheorySep::check(Effort e) {
 302   if (done() && !fullEffort(e) && e != EFFORT_LAST_CALL) {
 303     return;
 304   }
 305
 306   getOutputChannel().spendResource(options::theoryCheckStep());
 307
 308   TimerStat::CodeTimer checkTimer(d_checkTime);
 309   Trace("sep-check") << "Sep::check(): " << e << endl;
 310
 311   while( !done() && !d_conflict ){
 312     // Get all the assertions
 313     Assertion assertion = get();
 314     TNode fact = assertion.assertion;
 315
 316     Trace("sep-assert") << "TheorySep::check(): processing " << fact << std::endl;
 317
 318     bool polarity = fact.getKind() != kind::NOT;
 319     TNode atom = polarity ? fact : fact[0];
 320     /*
 321     if( atom.getKind()==kind::SEP_EMP ){
 322       TypeNode tn = atom[0].getType();
 323       if( d_emp_arg.find( tn )==d_emp_arg.end() ){
 324         d_emp_arg[tn] = atom[0];
 325       }else{
 326         //normalize argument TODO
 327       }
 328     }
 329     */
 330     TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom;
 331     TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null();
 332     bool is_spatial = s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP;
 333     if( is_spatial && s_lbl.isNull() ){
 334       if( d_reduce.find( fact )==d_reduce.end() ){
 335         Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl;
 336         d_reduce.insert( fact );
 337         //introduce top-level label, add iff
 338         TypeNode refType = getReferenceType( s_atom );
 339         Trace("sep-lemma-debug") << "...reference type is : " << refType << std::endl;
 340         Node b_lbl = getBaseLabel( refType );
 341         Node s_atom_new = NodeManager::currentNM()->mkNode( kind::SEP_LABEL, s_atom, b_lbl );
 342         Node lem;
 343         Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl;
 344         if( polarity ){
 345           lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom.negate(), s_atom_new );
 346         }else{
 347           lem = NodeManager::currentNM()->mkNode( kind::OR, s_atom, s_atom_new.negate() );
 348         }
 349         Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem << std::endl;
 350         d_out->lemma( lem );
 351       }
 352     }else{
 353       //do reductions
 354       if( is_spatial ){
 355         if( d_reduce.find( fact )==d_reduce.end() ){
 356           Trace("sep-lemma-debug") << "Reducing assertion " << fact << std::endl;
 357           d_reduce.insert( fact );
 358           Node conc;
 359           std::map< Node, Node >::iterator its = d_red_conc[s_lbl].find( s_atom );
 360           if( its==d_red_conc[s_lbl].end() ){
 361             //make conclusion based on type of assertion
 362             if( s_atom.getKind()==kind::SEP_STAR || s_atom.getKind()==kind::SEP_WAND ){
 363               std::vector< Node > children;
 364               std::vector< Node > c_lems;
 365               TypeNode tn = getReferenceType( s_atom );
 366               if( d_reference_bound_max.find( tn )!=d_reference_bound_max.end() ){
 367                 c_lems.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, s_lbl, d_reference_bound_max[tn] ) );
 368               }
 369               std::vector< Node > labels;
 370               getLabelChildren( s_atom, s_lbl, children, labels );
 371               Node empSet = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
 372               Assert( children.size()>1 );
 373               if( s_atom.getKind()==kind::SEP_STAR ){
 374                 //reduction for heap : union, pairwise disjoint
 375                 Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, labels[0], labels[1] );
 376                 for( unsigned i=2; i<labels.size(); i++ ){
 377                   ulem = NodeManager::currentNM()->mkNode( kind::UNION, ulem, labels[i] );
 378                 }
 379                 ulem = s_lbl.eqNode( ulem );
 380                 Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, union : " << ulem << std::endl;
 381                 c_lems.push_back( ulem );
 382                 for( unsigned i=0; i<labels.size(); i++ ){
 383                   for( unsigned j=(i+1); j<labels.size(); j++ ){
 384                     Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, labels[i], labels[j] );
 385                     Node ilem = s.eqNode( empSet );
 386                     Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem << std::endl;
 387                     c_lems.push_back( ilem );
 388                   }
 389                 }
 390               }else{
 391                 Node ulem = NodeManager::currentNM()->mkNode( kind::UNION, s_lbl, labels[0] );
 392                 ulem = ulem.eqNode( labels[1] );
 393                 Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem << std::endl;
 394                 c_lems.push_back( ulem );
 395                 Node s = NodeManager::currentNM()->mkNode( kind::INTERSECTION, s_lbl, labels[0] );
 396                 Node ilem = s.eqNode( empSet );
 397                 Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem << std::endl;
 398                 c_lems.push_back( ilem );
 399                 //nil does not occur in labels[0]
 400                 Node nr = getNilRef( tn );
 401                 Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, labels[0] ).negate();
 402                 Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl;
 403                 d_out->lemma( nrlem );
 404               }
 405               //send out definitional lemmas for introduced sets
 406               for( unsigned j=0; j<c_lems.size(); j++ ){
 407                 Trace("sep-lemma") << "Sep::Lemma : definition : " << c_lems[j] << std::endl;
 408                 d_out->lemma( c_lems[j] );
 409               }
 410               //children.insert( children.end(), c_lems.begin(), c_lems.end() );
 411               conc = NodeManager::currentNM()->mkNode( kind::AND, children );
 412             }else if( s_atom.getKind()==kind::SEP_PTO ){
 413               Node ss = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
 414               if( s_lbl!=ss ){
 415                 conc = s_lbl.eqNode( ss );
 416               }
 417               //not needed anymore: semantics of sep.nil is enforced globally
 418               //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate();
 419               //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
 420
 421             }else if( s_atom.getKind()==kind::SEP_EMP ){
 422               //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
 423               Node lem;
 424               Node emp_s = NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType()));
 425               if( polarity ){
 426                 lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), s_lbl.eqNode( emp_s ) );
 427               }else{
 428                 Node kl = NodeManager::currentNM()->mkSkolem( "loc", getReferenceType( s_atom ) );
 429                 Node kd = NodeManager::currentNM()->mkSkolem( "data", getDataType( s_atom ) );
 430                 Node econc = NodeManager::currentNM()->mkNode( kind::SEP_LABEL,
 431                                NodeManager::currentNM()->mkNode( kind::SEP_STAR, NodeManager::currentNM()->mkNode( kind::SEP_PTO, kl, kd ), d_true ), s_lbl );
 432                 //Node econc = NodeManager::currentNM()->mkNode( kind::AND, s_lbl.eqNode( emp_s ).negate(),
 433                 lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), econc );
 434               }
 435               Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
 436               d_out->lemma( lem );
 437
 438             }else{
 439               //labeled emp should be rewritten
 440               Assert( false );
 441             }
 442             d_red_conc[s_lbl][s_atom] = conc;
 443           }else{
 444             conc = its->second;
 445           }
 446           if( !conc.isNull() ){
 447             bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
 448             if( !use_polarity ){
 449               // introduce guard, assert positive version
 450               Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact << std::endl;
 451               Node lit = Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
 452               lit = getValuation().ensureLiteral( lit );
 453               d_neg_guard[s_lbl][s_atom] = lit;
 454               Trace("sep-lemma-debug") << "Neg guard : " << s_lbl << " " << s_atom << " " << lit << std::endl;
 455               AlwaysAssert( !lit.isNull() );
 456               d_out->requirePhase( lit, true );
 457               d_neg_guards.push_back( lit );
 458               d_guard_to_assertion[lit] = s_atom;
 459               //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
 460               Node lem = NodeManager::currentNM()->mkNode( kind::OR, lit.negate(), conc );
 461               Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem << std::endl;
 462               d_out->lemma( lem );
 463             }else{
 464               //reduce based on implication
 465               Node lem = NodeManager::currentNM()->mkNode( kind::OR, fact.negate(), conc );
 466               Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem << std::endl;
 467               d_out->lemma( lem );
 468             }
 469           }else{
 470             Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl;
 471           }
 472         }
 473       }
 474       //assert to equality engine
 475       if( !is_spatial ){
 476         Trace("sep-assert") << "Asserting " << atom << ", pol = " << polarity << " to EE..." << std::endl;
 477         if( s_atom.getKind()==kind::EQUAL ){
 478           d_equalityEngine.assertEquality(atom, polarity, fact);
 479         }else{
 480           d_equalityEngine.assertPredicate(atom, polarity, fact);
 481         }
 482         Trace("sep-assert") << "Done asserting " << atom << " to EE." << std::endl;
 483       }else if( s_atom.getKind()==kind::SEP_PTO ){
 484         Node pto_lbl = NodeManager::currentNM()->mkNode( kind::SINGLETON, s_atom[0] );
 485         Assert( s_lbl==pto_lbl );
 486         Trace("sep-assert") << "Asserting " << s_atom << std::endl;
 487         d_equalityEngine.assertPredicate(s_atom, polarity, fact);
 488         //associate the equivalence class of the lhs with this pto
 489         Node r = getRepresentative( s_lbl );
 490         HeapAssertInfo * ei = getOrMakeEqcInfo( r, true );
 491         addPto( ei, r, atom, polarity );
 492       }
 493       //maybe propagate
 494       doPendingFacts();
 495       //add to spatial assertions
 496       if( !d_conflict && is_spatial ){
 497         d_spatial_assertions.push_back( fact );
 498       }
 499     }
 500   }
 501
 502   if( e == EFFORT_LAST_CALL && !d_conflict && !d_valuation.needCheck() ){
 503     Trace("sep-process") << "Checking heap at full effort..." << std::endl;
 504     d_label_model.clear();
 505     d_tmodel.clear();
 506     d_pto_model.clear();
 507     Trace("sep-process") << "---Locations---" << std::endl;
 508     std::map< Node, int > min_id;
 509     for( std::map< TypeNode, std::vector< Node > >::iterator itt = d_type_references_all.begin(); itt != d_type_references_all.end(); ++itt ){
 510       for( unsigned k=0; k<itt->second.size(); k++ ){
 511         Node t = itt->second[k];
 512         Trace("sep-process") << "  " << t << " = ";
 513         if( d_valuation.getModel()->hasTerm( t ) ){
 514           Node v = d_valuation.getModel()->getRepresentative( t );
 515           Trace("sep-process") << v << std::endl;
 516           //take minimal id
 517           std::map< Node, unsigned >::iterator itrc = d_type_ref_card_id.find( t );
 518           int tid = itrc==d_type_ref_card_id.end() ? -1 : (int)itrc->second;
 519           bool set_term_model;
 520           if( d_tmodel.find( v )==d_tmodel.end() ){
 521             set_term_model = true;
 522           }else{
 523             set_term_model = min_id[v]>tid;
 524           }
 525           if( set_term_model ){
 526             d_tmodel[v] = t;
 527             min_id[v] = tid;
 528           }
 529         }else{
 530           Trace("sep-process") << "?" << std::endl;
 531         }
 532       }
 533     }
 534     Trace("sep-process") << "---" << std::endl;
 535     //build positive/negative assertion lists for labels
 536     std::map< Node, bool > assert_active;
 537     //get the inactive assertions
 538     std::map< Node, std::vector< Node > > lbl_to_assertions;
 539     for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 540       Node fact = (*i);
 541       bool polarity = fact.getKind() != kind::NOT;
 542       TNode atom = polarity ? fact : fact[0];
 543       Assert( atom.getKind()==kind::SEP_LABEL );
 544       TNode s_atom = atom[0];
 545       TNode s_lbl = atom[1];
 546       lbl_to_assertions[s_lbl].push_back( fact );
 547       //check whether assertion is active : either polarity=true, or guard is not asserted false
 548       assert_active[fact] = true;
 549       bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
 550       if( use_polarity ){
 551         if( s_atom.getKind()==kind::SEP_PTO ){
 552           Node vv = d_valuation.getModel()->getRepresentative( s_atom[0] );
 553           if( d_pto_model.find( vv )==d_pto_model.end() ){
 554             Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
 555             d_pto_model[vv] = s_atom[1];
 556
 557             //replace this on pto-model since this term is more relevant
 558             TypeNode vtn = vv.getType();
 559             if( std::find( d_type_references_all[vtn].begin(), d_type_references_all[vtn].end(), s_atom[0] )!=d_type_references_all[vtn].end() ){
 560               d_tmodel[vv] = s_atom[0];
 561             }
 562           }
 563         }
 564       }else{
 565         if( d_neg_guard[s_lbl].find( s_atom )!=d_neg_guard[s_lbl].end() ){
 566           //check if the guard is asserted positively
 567           Node guard = d_neg_guard[s_lbl][s_atom];
 568           bool value;
 569           if( getValuation().hasSatValue( guard, value ) ) {
 570             assert_active[fact] = value;
 571           }
 572         }
 573       }
 574     }
 575     //(recursively) set inactive sub-assertions
 576     for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 577       Node fact = (*i);
 578       if( !assert_active[fact] ){
 579         setInactiveAssertionRec( fact, lbl_to_assertions, assert_active );
 580       }
 581     }
 582     //set up model information based on active assertions
 583     for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 584       Node fact = (*i);
 585       bool polarity = fact.getKind() != kind::NOT;
 586       TNode atom = polarity ? fact : fact[0];
 587       TNode s_atom = atom[0];
 588       TNode s_lbl = atom[1];
 589       if( assert_active[fact] ){
 590         computeLabelModel( s_lbl );
 591       }
 592     }
 593     //debug print
 594     if( Trace.isOn("sep-process") ){
 595       Trace("sep-process") << "--- Current spatial assertions : " << std::endl;
 596       for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 597         Node fact = (*i);
 598         Trace("sep-process") << "  " << fact;
 599         if( !assert_active[fact] ){
 600           Trace("sep-process") << " [inactive]";
 601         }
 602         Trace("sep-process") << std::endl;
 603       }
 604       Trace("sep-process") << "---" << std::endl;
 605     }
 606     if(Trace.isOn("sep-eqc")) {
 607       eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator( &d_equalityEngine );
 608       Trace("sep-eqc") << "EQC:" << std::endl;
 609       while( !eqcs2_i.isFinished() ){
 610         Node eqc = (*eqcs2_i);
 611         eq::EqClassIterator eqc2_i = eq::EqClassIterator( eqc, &d_equalityEngine );
 612         Trace("sep-eqc") << "Eqc( " << eqc << " ) : { ";
 613         while( !eqc2_i.isFinished() ) {
 614           if( (*eqc2_i)!=eqc ){
 615             Trace("sep-eqc") << (*eqc2_i) << " ";
 616           }
 617           ++eqc2_i;
 618         }
 619         Trace("sep-eqc") << " } " << std::endl;
 620         ++eqcs2_i;
 621       }
 622       Trace("sep-eqc") << std::endl;
 623     }
 624
 625     bool addedLemma = false;
 626     bool needAddLemma = false;
 627     //check negated star / positive wand
 628     if( options::sepCheckNeg() ){
 629       //get active labels
 630       std::map< Node, bool > active_lbl;
 631       if( options::sepMinimalRefine() ){
 632         for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 633           Node fact = (*i);
 634           bool polarity = fact.getKind() != kind::NOT;
 635           TNode atom = polarity ? fact : fact[0];
 636           TNode s_atom = atom[0];
 637           bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
 638           if( !use_polarity ){
 639             Assert( assert_active.find( fact )!=assert_active.end() );
 640             if( assert_active[fact] ){
 641               Assert( atom.getKind()==kind::SEP_LABEL );
 642               TNode s_lbl = atom[1];
 643               if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
 644                 Trace("sep-process-debug") << "Active lbl : " << s_lbl << std::endl;
 645                 active_lbl[s_lbl] = true;
 646               }
 647             }
 648           }
 649         }
 650       }
 651
 652       //process spatial assertions
 653       for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
 654         Node fact = (*i);
 655         bool polarity = fact.getKind() != kind::NOT;
 656         TNode atom = polarity ? fact : fact[0];
 657         TNode s_atom = atom[0];
 658
 659         bool use_polarity = s_atom.getKind()==kind::SEP_WAND ? !polarity : polarity;
 660         Trace("sep-process-debug") << "  check atom : " << s_atom << " use polarity " << use_polarity << std::endl;
 661         if( !use_polarity ){
 662           Assert( assert_active.find( fact )!=assert_active.end() );
 663           if( assert_active[fact] ){
 664             Assert( atom.getKind()==kind::SEP_LABEL );
 665             TNode s_lbl = atom[1];
 666             Trace("sep-process") << "--> Active negated atom : " << s_atom << ", lbl = " << s_lbl << std::endl;
 667             //add refinement lemma
 668             if( d_label_map[s_atom].find( s_lbl )!=d_label_map[s_atom].end() ){
 669               needAddLemma = true;
 670               TypeNode tn = getReferenceType( s_atom );
 671               tn = NodeManager::currentNM()->mkSetType(tn);
 672               //tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
 673               Node o_b_lbl_mval = d_label_model[s_lbl].getValue( tn );
 674               Trace("sep-process") << "    Model for " << s_lbl << " : " << o_b_lbl_mval << std::endl;
 675
 676               //get model values
 677               std::map< int, Node > mvals;
 678               for( std::map< int, Node >::iterator itl = d_label_map[s_atom][s_lbl].begin(); itl != d_label_map[s_atom][s_lbl].end(); ++itl ){
 679                 Node sub_lbl = itl->second;
 680                 int sub_index = itl->first;
 681                 computeLabelModel( sub_lbl );
 682                 Node lbl_mval = d_label_model[sub_lbl].getValue( tn );
 683                 Trace("sep-process-debug") << "  child " << sub_index << " : " << sub_lbl << ", mval = " << lbl_mval << std::endl;
 684                 mvals[sub_index] = lbl_mval;
 685               }
 686
 687               // Now, assert model-instantiated implication based on the negation
 688               Assert( d_label_model.find( s_lbl )!=d_label_model.end() );
 689               std::vector< Node > conc;
 690               bool inst_success = true;
 691               //new refinement
 692               //instantiate the label
 693               std::map< Node, Node > visited;
 694               Node inst = instantiateLabel( s_atom, s_lbl, s_lbl, o_b_lbl_mval, visited, d_pto_model, tn, active_lbl );
 695               Trace("sep-inst-debug") << "    applied inst : " << inst << std::endl;
 696               if( inst.isNull() ){
 697                 inst_success = false;
 698               }else{
 699                 inst = Rewriter::rewrite( inst );
 700                 if( inst==( polarity ? d_true : d_false ) ){
 701                   inst_success = false;
 702                 }
 703                 conc.push_back( polarity ? inst : inst.negate() );
 704               }
 705               if( inst_success ){
 706                 std::vector< Node > lemc;
 707                 Node pol_atom = atom;
 708                 if( polarity ){
 709                   pol_atom = atom.negate();
 710                 }
 711                 lemc.push_back( pol_atom );
 712
 713                 //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() );
 714                 //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() );
 715                 lemc.insert( lemc.end(), conc.begin(), conc.end() );
 716                 Node lem = NodeManager::currentNM()->mkNode( kind::OR, lemc );
 717                 if( std::find( d_refinement_lem[s_atom][s_lbl].begin(), d_refinement_lem[s_atom][s_lbl].end(), lem )==d_refinement_lem[s_atom][s_lbl].end() ){
 718                   d_refinement_lem[s_atom][s_lbl].push_back( lem );
 719                   Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem[s_atom][s_lbl].size() << ") : " << lem << std::endl;
 720                   Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem << std::endl;
 721                   d_out->lemma( lem );
 722                   addedLemma = true;
 723                 }else{
 724                   //this typically should not happen, should never happen for complete base theories
 725                   Trace("sep-process") << "*** repeated refinement lemma : " << lem << std::endl;
 726                   Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " << lem << "!!!" << std::endl;
 727                 }
 728               }
 729             }else{
 730               Trace("sep-process-debug") << "  no children." << std::endl;
 731               Assert( s_atom.getKind()==kind::SEP_PTO || s_atom.getKind()==kind::SEP_EMP );
 732             }
 733           }else{
 734             Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom << std::endl;
 735           }
 736         }
 737       }
 738       Trace("sep-process") << "...finished check of negated assertions, addedLemma=" << addedLemma << ", needAddLemma=" << needAddLemma << std::endl;
 739     }
 740     if( !addedLemma ){
 741       //must witness finite data points-to
 742       for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){
 743         TypeNode data_type = d_loc_to_data_type[it->first];
 744         //if the data type is finite
 745         if( data_type.isInterpretedFinite() ){
 746           computeLabelModel( it->second );
 747           Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " << data_type << std::endl;
 748           for( unsigned j=0; j<d_label_model[it->second].d_heap_locs_model.size(); j++ ){
 749             Assert( d_label_model[it->second].d_heap_locs_model[j].getKind()==kind::SINGLETON );
 750             Node l = d_label_model[it->second].d_heap_locs_model[j][0];
 751             Trace("sep-process-debug") << "  location : " << l << std::endl;
 752             if( d_pto_model[l].isNull() ){
 753               needAddLemma = true;
 754               Node ll;
 755               std::map< Node, Node >::iterator itm = d_tmodel.find( l );
 756               if( itm!=d_tmodel.end() ) {
 757                 ll = itm->second;
 758               }else{
 759                 //try to assign arbitrary skolem?
 760               }
 761               if( !ll.isNull() ){
 762                 Trace("sep-process") << "Must witness label : " << ll << ", data type is " << data_type << std::endl;
 763                 Node dsk = NodeManager::currentNM()->mkSkolem( "dsk", data_type, "pto-data for implicit location" );
 764                 // if location is in the heap, then something must point to it
 765                 Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, NodeManager::currentNM()->mkNode( kind::MEMBER, ll, it->second ),
 766                                                                             NodeManager::currentNM()->mkNode( kind::SEP_STAR,
 767                                                                               NodeManager::currentNM()->mkNode( kind::SEP_PTO, ll, dsk ),
 768                                                                               d_true ) );
 769                 Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl;
 770                 d_out->lemma( lem );
 771                 addedLemma = true;
 772               }else{
 773                 //This should only happen if we are in an unbounded fragment
 774                 Trace("sep-warn") << "TheorySep : WARNING : no term corresponding to location " << l << " in heap!!!" << std::endl;
 775               }
 776             }else{
 777               Trace("sep-process-debug") << "  points-to data witness : " << d_pto_model[l] << std::endl;
 778             }
 779           }
 780         }
 781       }
 782       if( !addedLemma ){
 783         //set up model
 784         Trace("sep-process-debug") << "...preparing sep model..." << std::endl;
 785         d_heap_locs_nptos.clear();
 786         //collect data points that are not pointed to
 787         for( context::CDList<Assertion>::const_iterator it = facts_begin(); it != facts_end(); ++ it) {
 788           Node lit = (*it).assertion;
 789           if( lit.getKind()==kind::NOT && lit[0].getKind()==kind::SEP_PTO ){
 790             Node s_atom = lit[0];
 791             Node v1 = d_valuation.getModel()->getRepresentative( s_atom[0] );
 792             Node v2 = d_valuation.getModel()->getRepresentative( s_atom[1] );
 793             Trace("sep-process-debug") << v1 << " does not point-to " << v2 << std::endl;
 794             d_heap_locs_nptos[v1].push_back( v2 );
 795           }
 796         }
 797
 798         if( needAddLemma ){
 799           d_out->setIncomplete();
 800         }
 801       }
 802     }
 803   }
 804   Trace("sep-check") << "Sep::check(): " << e << " done, conflict=" << d_conflict.get() << endl;
 805 }
 806
 807
 808 bool TheorySep::needsCheckLastEffort() {
 809   return hasFacts();
 810 }
 811
 812 Node TheorySep::getNextDecisionRequest( unsigned& priority ) {
 813   for( unsigned i=0; i<d_neg_guards.size(); i++ ){
 814     Node g = d_neg_guards[i];
 815     bool success = true;
 816     if( getLogicInfo().isQuantified() ){
 817       Assert( d_guard_to_assertion.find( g )!= d_guard_to_assertion.end() );
 818       Node a = d_guard_to_assertion[g];
 819       Node q = quantifiers::TermDb::getInstConstAttr( a );
 820       if( !q.isNull() ){
 821         //must wait to decide on counterexample literal from quantified formula
 822         Node cel = getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q );
 823         bool value;
 824         if( d_valuation.hasSatValue( cel, value ) ){
 825           Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g << " depends on value for guard for quantified formula : " << value << std::endl;
 826           success = value;
 827         }else{
 828           Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g << " until " << cel << " is set " << std::endl;
 829           success = false;
 830         }
 831       }
 832     }
 833     if( success ){
 834       bool value;
 835       if( !d_valuation.hasSatValue( g, value ) ) {
 836         Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g << " (" << i << "/" << d_neg_guards.size() << ")" << std::endl;
 837         priority = 0;
 838         return g;
 839       }
 840     }
 841   }
 842   Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl;
 843   return Node::null();
 844 }
 845
 846 void TheorySep::conflict(TNode a, TNode b) {
 847   Trace("sep-conflict") << "Sep::conflict : " << a << " " << b << std::endl;
 848   Node conflictNode = explain(a.eqNode(b));
 849   d_conflict = true;
 850   d_out->conflict( conflictNode );
 851 }
 852
 853
 854 TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context* c ) : d_pto(c), d_has_neg_pto(c,false) {
 855
 856 }
 857
 858 TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) {
 859   std::map< Node, HeapAssertInfo* >::iterator e_i = d_eqc_info.find( n );
 860   if( e_i==d_eqc_info.end() ){
 861     if( doMake ){
 862       HeapAssertInfo* ei = new HeapAssertInfo( getSatContext() );
 863       d_eqc_info[n] = ei;
 864       return ei;
 865     }else{
 866       return NULL;
 867     }
 868   }else{
 869     return (*e_i).second;
 870   }
 871 }
 872
 873 //for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2)
 874 TypeNode TheorySep::getReferenceType( Node n ) {
 875   Assert( !d_type_ref.isNull() );
 876   return d_type_ref;
 877 }
 878
 879 TypeNode TheorySep::getDataType( Node n ) {
 880   Assert( !d_type_data.isNull() );
 881   return d_type_data;
 882 }
 883
 884 // Must process assertions at preprocess so that quantified assertions are
 885 // processed properly.
 886 void TheorySep::ppNotifyAssertions(const std::vector<Node>& assertions) {
 887   std::map<int, std::map<Node, int> > visited;
 888   std::map<int, std::map<Node, std::vector<Node> > > references;
 889   std::map<int, std::map<Node, bool> > references_strict;
 890   for (unsigned i = 0; i < assertions.size(); i++) {
 891     Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl;
 892     processAssertion(assertions[i], visited, references, references_strict,
 893                      true, true, false);
 894   }
 895   // if data type is unconstrained, assume a fresh uninterpreted sort
 896   if (!d_type_ref.isNull()) {
 897     if (d_type_data.isNull()) {
 898       d_type_data = NodeManager::currentNM()->mkSort("_sep_U");
 899       Trace("sep-type") << "Sep: assume data type " << d_type_data << std::endl;
 900       d_loc_to_data_type[d_type_ref] = d_type_data;
 901     }
 902   }
 903 }
 904
 905 //return cardinality
 906 int TheorySep::processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
 907                                  std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
 908                                  bool pol, bool hasPol, bool underSpatial ) {
 909   int index = hasPol ? ( pol ? 1 : -1 ) : 0;
 910   int card = 0;
 911   std::map< Node, int >::iterator it = visited[index].find( n );
 912   if( it==visited[index].end() ){
 913     Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl;
 914     if( n.getKind()==kind::SEP_EMP ){
 915       TypeNode tn = n[0].getType();
 916       TypeNode tnd = n[1].getType();
 917       registerRefDataTypes( tn, tnd, n );
 918       if( hasPol && pol ){
 919         references[index][n].clear();
 920         references_strict[index][n] = true;
 921       }else{
 922         card = 1;
 923       }
 924     }else if( n.getKind()==kind::SEP_PTO ){
 925       TypeNode tn1 = n[0].getType();
 926       TypeNode tn2 = n[1].getType();
 927       registerRefDataTypes( tn1, tn2, n );
 928       if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
 929         if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
 930           if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
 931             // still valid : bound on heap models will include Herbrand universe of n[0].getType()
 932             d_bound_kind[tn1] = bound_herbrand;
 933           }else{
 934             d_bound_kind[tn1] = bound_invalid;
 935             Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl;
 936           }
 937         }
 938       }else{
 939         references[index][n].push_back( n[0] );
 940       }
 941       if( hasPol && pol ){
 942         references_strict[index][n] = true;
 943       }else{
 944         card = 1;
 945       }
 946     }else{
 947       bool isSpatial = n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_STAR;
 948       bool newUnderSpatial = underSpatial || isSpatial;
 949       bool refStrict = isSpatial;
 950       for( unsigned i=0; i<n.getNumChildren(); i++ ){
 951         bool newHasPol, newPol;
 952         QuantPhaseReq::getEntailPolarity( n, i, hasPol, pol, newHasPol, newPol );
 953         int newIndex = newHasPol ? ( newPol ? 1 : -1 ) : 0;
 954         int ccard = processAssertion( n[i], visited, references, references_strict, newPol, newHasPol, newUnderSpatial );
 955         //update cardinality
 956         if( n.getKind()==kind::SEP_STAR ){
 957           card += ccard;
 958         }else if( n.getKind()==kind::SEP_WAND ){
 959           if( i==1 ){
 960             card = ccard;
 961           }
 962         }else if( ccard>card ){
 963           card = ccard;
 964         }
 965         //track references if we are or below a spatial operator
 966         if( newUnderSpatial ){
 967           bool add = true;
 968           if( references_strict[newIndex].find( n[i] )!=references_strict[newIndex].end() ){
 969             if( !isSpatial ){
 970               if( references_strict[index].find( n )==references_strict[index].end() ){
 971                 references_strict[index][n] = true;
 972               }else{
 973                 add = false;
 974                 //TODO: can derive static equality between sets
 975               }
 976             }
 977           }else{
 978             if( isSpatial ){
 979               refStrict = false;
 980             }
 981           }
 982           if( add ){
 983             for( unsigned j=0; j<references[newIndex][n[i]].size(); j++ ){
 984               if( std::find( references[index][n].begin(), references[index][n].end(), references[newIndex][n[i]][j] )==references[index][n].end() ){
 985                 references[index][n].push_back( references[newIndex][n[i]][j] );
 986               }
 987             }
 988           }
 989         }
 990       }
 991       if( isSpatial && refStrict ){
 992         if( n.getKind()==kind::SEP_WAND ){
 993           //TODO
 994         }else{
 995           Assert( n.getKind()==kind::SEP_STAR && hasPol && pol );
 996           references_strict[index][n] = true;
 997         }
 998       }
 999     }
1000     visited[index][n] = card;
1001   }else{
1002     card = it->second;
1003   }
1004
1005   if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
1006     TypeNode tn = getReferenceType( n );
1007     Assert( !tn.isNull() );
1008     // add references to overall type
1009     unsigned bt = d_bound_kind[tn];
1010     bool add = true;
1011     if( references_strict[index].find( n )!=references_strict[index].end() ){
1012       Trace("sep-bound") << "Strict bound found based on " << n << ", index = " << index << std::endl;
1013       if( bt!=bound_strict ){
1014         d_bound_kind[tn] = bound_strict;
1015         //d_type_references[tn].clear();
1016         d_card_max[tn] = card;
1017       }else{
1018         //TODO: derive static equality
1019         add = false;
1020       }
1021     }else{
1022       add = bt!=bound_strict;
1023     }
1024     for( unsigned i=0; i<references[index][n].size(); i++ ){
1025       if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), references[index][n][i] )==d_type_references[tn].end() ){
1026         d_type_references[tn].push_back( references[index][n][i] );
1027       }
1028     }
1029     if( add ){
1030       //add max cardinality
1031       if( card>(int)d_card_max[tn] ){
1032         d_card_max[tn] = card;
1033       }
1034     }
1035   }
1036   return card;
1037 }
1038
1039 void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){
1040   //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
1041   if( options::incrementalSolving() ){
1042     std::stringstream ss;
1043     ss << "ERROR: cannot use separation logic in incremental mode." << std::endl;
1044     throw LogicException(ss.str());
1045   }
1046   std::map< TypeNode, TypeNode >::iterator itt = d_loc_to_data_type.find( tn1 );
1047   if( itt==d_loc_to_data_type.end() ){
1048     if( !d_loc_to_data_type.empty() ){
1049       TypeNode te1 = d_loc_to_data_type.begin()->first;
1050       std::stringstream ss;
1051       ss << "ERROR: specifying heap constraints for two different types : " << tn1 << " -> " << tn2 << " and " << te1 << " -> " << d_loc_to_data_type[te1] << std::endl;
1052       throw LogicException(ss.str());
1053       Assert( false );
1054     }
1055     if( tn2.isNull() ){
1056       Trace("sep-type") << "Sep: assume location type " << tn1 << " (from " << atom << ")" << std::endl;
1057     }else{
1058       Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
1059     }
1060     d_loc_to_data_type[tn1] = tn2;
1061     //for now, we only allow heap constraints of one type
1062     d_type_ref = tn1;
1063     d_type_data = tn2;
1064     d_bound_kind[tn1] = bound_default;
1065   }else{
1066     if( !tn2.isNull() ){
1067       if( itt->second!=tn2 ){
1068         if( itt->second.isNull() ){
1069           Trace("sep-type") << "Sep: assume location type " << tn1 << " is associated with data type " << tn2 << " (from " << atom << ")" << std::endl;
1070           //now we know data type
1071           d_loc_to_data_type[tn1] = tn2;
1072           d_type_data = tn2;
1073         }else{
1074           std::stringstream ss;
1075           ss << "ERROR: location type " << tn1 << " is already associated with data type " << itt->second << ", offending atom is " << atom << " with data type " << tn2 << std::endl;
1076           throw LogicException(ss.str());
1077           Assert( false );
1078         }
1079       }
1080     }
1081   }
1082 }
1083
1084 void TheorySep::initializeBounds() {
1085   if( !d_bounds_init ){
1086     Trace("sep-bound")  << "Initialize sep bounds..." << std::endl;
1087     d_bounds_init = true;
1088     for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){
1089       TypeNode tn = it->first;
1090       Trace("sep-bound")  << "Initialize bounds for " << tn << "..." << std::endl;
1091       QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL;
1092       //if pto had free variable reference
1093       if( d_bound_kind[tn]==bound_herbrand ){
1094         //include Herbrand universe of tn
1095         if( qepr && qepr->isEPR( tn ) ){
1096           for( unsigned j=0; j<qepr->d_consts[tn].size(); j++ ){
1097             Node k = qepr->d_consts[tn][j];
1098             if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){
1099               d_type_references[tn].push_back( k );
1100             }
1101           }
1102         }else{
1103           d_bound_kind[tn] = bound_invalid;
1104           Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl;
1105         }
1106       }
1107       unsigned n_emp = 0;
1108       if( d_bound_kind[tn] != bound_invalid ){
1109         n_emp = d_card_max[tn];
1110       }else if( d_type_references[tn].empty() ){
1111         //must include at least one constant TODO: remove?
1112         n_emp = 1;
1113       }
1114       Trace("sep-bound") << "Cardinality element size : " << d_card_max[tn] << std::endl;
1115       Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl;
1116       Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl;
1117       for( unsigned r=0; r<n_emp; r++ ){
1118         Node e = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
1119         d_type_references_card[tn].push_back( e );
1120         d_type_ref_card_id[e] = r;
1121         //must include this constant back into EPR handling
1122         if( qepr && qepr->isEPR( tn ) ){
1123           qepr->addEPRConstant( tn, e );
1124         }
1125       }
1126       //EPR must include nil ref
1127       if( qepr && qepr->isEPR( tn ) ){
1128         Node nr = getNilRef( tn );
1129         if( !qepr->isEPRConstant( tn, nr ) ){
1130           qepr->addEPRConstant( tn, nr );
1131         }
1132       }
1133     }
1134   }
1135 }
1136
1137 Node TheorySep::getBaseLabel( TypeNode tn ) {
1138   std::map< TypeNode, Node >::iterator it = d_base_label.find( tn );
1139   if( it==d_base_label.end() ){
1140     initializeBounds();
1141     Trace("sep") << "Make base label for " << tn << std::endl;
1142     std::stringstream ss;
1143     ss << "__Lb";
1144     TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
1145     //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
1146     Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "base label" );
1147     d_base_label[tn] = n_lbl;
1148     //make reference bound
1149     Trace("sep") << "Make reference bound label for " << tn << std::endl;
1150     std::stringstream ss2;
1151     ss2 << "__Lu";
1152     d_reference_bound[tn] = NodeManager::currentNM()->mkSkolem( ss2.str(), ltn, "" );
1153     d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() );
1154
1155     //check whether monotonic (elements can be added to tn without effecting satisfiability)
1156     bool tn_is_monotonic = true;
1157     if( tn.isSort() ){
1158       //TODO: use monotonicity inference
1159       tn_is_monotonic = !getLogicInfo().isQuantified();
1160     }else{
1161       tn_is_monotonic = tn.getCardinality().isInfinite();
1162     }
1163     //add a reference type for maximum occurrences of empty in a constraint
1164     if( options::sepDisequalC() && tn_is_monotonic ){
1165       for( unsigned r=0; r<d_type_references_card[tn].size(); r++ ){
1166         Node e = d_type_references_card[tn][r];
1167         //ensure that it is distinct from all other references so far
1168         for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
1169           Node eq = NodeManager::currentNM()->mkNode( kind::EQUAL, e, d_type_references_all[tn][j] );
1170           d_out->lemma( eq.negate() );
1171         }
1172         d_type_references_all[tn].push_back( e );
1173       }
1174     }else{
1175       //break symmetries TODO
1176
1177       d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
1178     }
1179     //Assert( !d_type_references_all[tn].empty() );
1180
1181     if( d_bound_kind[tn]!=bound_invalid ){
1182       //construct bound
1183       d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] );
1184       Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl;
1185
1186       Node slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
1187       Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl;
1188       d_out->lemma( slem );
1189       //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
1190       //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
1191       //d_out->lemma( slem );
1192
1193       //symmetry breaking
1194       if( d_type_references_card[tn].size()>1 ){
1195         std::map< unsigned, Node > lit_mem_map;
1196         for( unsigned i=0; i<d_type_references_card[tn].size(); i++ ){
1197           lit_mem_map[i] = NodeManager::currentNM()->mkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound_max[tn]);
1198         }
1199         for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){
1200           std::vector< Node > children;
1201           for( unsigned j=(i+1); j<d_type_references_card[tn].size(); j++ ){
1202             children.push_back( lit_mem_map[j].negate() );
1203           }
1204           if( !children.empty() ){
1205             Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children );
1206             sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem );
1207             Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl;
1208             d_out->lemma( sym_lem );
1209           }
1210         }
1211       }
1212     }
1213
1214     //assert that nil ref is not in base label
1215     Node nr = getNilRef( tn );
1216     Node nrlem = NodeManager::currentNM()->mkNode( kind::MEMBER, nr, n_lbl ).negate();
1217     Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::endl;
1218     d_out->lemma( nrlem );
1219
1220     return n_lbl;
1221   }else{
1222     return it->second;
1223   }
1224 }
1225
1226 Node TheorySep::getNilRef( TypeNode tn ) {
1227   std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn );
1228   if( it==d_nil_ref.end() ){
1229     Node nil = NodeManager::currentNM()->mkNullaryOperator( tn, kind::SEP_NIL );
1230     setNilRef( tn, nil );
1231     return nil;
1232   }else{
1233     return it->second;
1234   }
1235 }
1236
1237 void TheorySep::setNilRef( TypeNode tn, Node n ) {
1238   Assert( n.getType()==tn );
1239   d_nil_ref[tn] = n;
1240 }
1241
1242 Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) {
1243   Node u;
1244   if( locs.empty() ){
1245     TypeNode ltn = NodeManager::currentNM()->mkSetType(tn);
1246     return NodeManager::currentNM()->mkConst(EmptySet(ltn.toType()));
1247   }else{
1248     for( unsigned i=0; i<locs.size(); i++ ){
1249       Node s = locs[i];
1250       Assert( !s.isNull() );
1251       s = NodeManager::currentNM()->mkNode( kind::SINGLETON, s );
1252       if( u.isNull() ){
1253         u = s;
1254       }else{
1255         u = NodeManager::currentNM()->mkNode( kind::UNION, s, u );
1256       }
1257     }
1258     return u;
1259   }
1260 }
1261
1262 Node TheorySep::getLabel( Node atom, int child, Node lbl ) {
1263   std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child );
1264   if( it==d_label_map[atom][lbl].end() ){
1265     TypeNode refType = getReferenceType( atom );
1266     std::stringstream ss;
1267     ss << "__Lc" << child;
1268     TypeNode ltn = NodeManager::currentNM()->mkSetType(refType);
1269     //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
1270     Node n_lbl = NodeManager::currentNM()->mkSkolem( ss.str(), ltn, "sep label" );
1271     d_label_map[atom][lbl][child] = n_lbl;
1272     d_label_map_parent[n_lbl] = lbl;
1273     return n_lbl;
1274   }else{
1275     return (*it).second;
1276   }
1277 }
1278
1279 Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) {
1280   Assert( n.getKind()!=kind::SEP_LABEL );
1281   if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
1282     return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl );
1283   }else if( !n.getType().isBoolean() || n.getNumChildren()==0 ){
1284     return n;
1285   }else{
1286     std::map< Node, Node >::iterator it = visited.find( n );
1287     if( it==visited.end() ){
1288       std::vector< Node > children;
1289       if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
1290         children.push_back( n.getOperator() );
1291       }
1292       bool childChanged = false;
1293       for( unsigned i=0; i<n.getNumChildren(); i++ ){
1294         Node aln = applyLabel( n[i], lbl, visited );
1295         children.push_back( aln );
1296         childChanged = childChanged || aln!=n[i];
1297       }
1298       Node ret = n;
1299       if( childChanged ){
1300         ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
1301       }
1302       visited[n] = ret;
1303       return ret;
1304     }else{
1305       return it->second;
1306     }
1307   }
1308 }
1309
1310 Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
1311                                   TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind ) {
1312   Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
1313   if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
1314     Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
1315     return Node::null();
1316   }else{
1317     if( Trace.isOn("sep-inst") ){
1318       if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND  || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
1319         for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << "  "; }
1320         Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl;
1321       }
1322     }
1323     Assert( n.getKind()!=kind::SEP_LABEL );
1324     if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
1325       if( lbl==o_lbl ){
1326         std::vector< Node > children;
1327         children.resize( n.getNumChildren() );
1328         Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
1329         std::map< int, Node > mvals;
1330         for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
1331           Node sub_lbl = itl->second;
1332           int sub_index = itl->first;
1333           Assert( sub_index>=0 && sub_index<(int)children.size() );
1334           Trace("sep-inst-debug") << "Sublabel " << sub_index << " is " << sub_lbl << std::endl;
1335           Node lbl_mval;
1336           if( n.getKind()==kind::SEP_WAND && sub_index==1 ){
1337             Assert( d_label_map[n][lbl].find( 0 )!=d_label_map[n][lbl].end() );
1338             Node sub_lbl_0 = d_label_map[n][lbl][0];
1339             computeLabelModel( sub_lbl_0 );
1340             Assert( d_label_model.find( sub_lbl_0 )!=d_label_model.end() );
1341             lbl_mval = NodeManager::currentNM()->mkNode( kind::UNION, lbl, d_label_model[sub_lbl_0].getValue( rtn ) );
1342           }else{
1343             computeLabelModel( sub_lbl );
1344             Assert( d_label_model.find( sub_lbl )!=d_label_model.end() );
1345             lbl_mval = d_label_model[sub_lbl].getValue( rtn );
1346           }
1347           Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval  << std::endl;
1348           mvals[sub_index] = lbl_mval;
1349           children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 );
1350           if( children[sub_index].isNull() ){
1351             return Node::null();
1352           }
1353         }
1354         Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
1355         if( n.getKind()==kind::SEP_STAR ){
1356
1357           //disjoint contraints
1358           std::vector< Node > conj;
1359           std::vector< Node > bchildren;
1360           bchildren.insert( bchildren.end(), children.begin(), children.end() );
1361           Node vsu;
1362           std::vector< Node > vs;
1363           for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
1364             Node sub_lbl = itl->second;
1365             Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
1366             for( unsigned j=0; j<vs.size(); j++ ){
1367               bchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
1368             }
1369             vs.push_back( lbl_mval );
1370             if( vsu.isNull() ){
1371               vsu = lbl_mval;
1372             }else{
1373               vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval );
1374             }
1375           }
1376           bchildren.push_back( vsu.eqNode( lbl ) );
1377
1378           Assert( bchildren.size()>1 );
1379           conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) );
1380
1381           if( options::sepChildRefine() ){
1382             //child-specific refinements (TODO: use ?)
1383             for( unsigned i=0; i<children.size(); i++ ){
1384               std::vector< Node > tchildren;
1385               Node mval = mvals[i];
1386               tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );
1387               tchildren.push_back( children[i] );
1388               std::vector< Node > rem_children;
1389               for( unsigned j=0; j<children.size(); j++ ){
1390                 if( j!=i ){
1391                   rem_children.push_back( n[j] );
1392                 }
1393               }
1394               std::map< Node, Node > rvisited;
1395               Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children );
1396               rem = applyLabel( rem, NodeManager::currentNM()->mkNode( kind::SETMINUS, lbl, mval ), rvisited );
1397               tchildren.push_back( rem );
1398               conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) );
1399             }
1400           }
1401           return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj );
1402         }else{
1403           std::vector< Node > wchildren;
1404           //disjoint constraints
1405           Node sub_lbl_0 = d_label_map[n][lbl][0];
1406           Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn );
1407           wchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval_0, lbl ).eqNode( empSet ).negate() );
1408
1409           //return the lemma
1410           wchildren.push_back( children[0].negate() );
1411           wchildren.push_back( children[1] );
1412           return NodeManager::currentNM()->mkNode( kind::OR, wchildren );
1413         }
1414       }else{
1415         //nested star/wand, label it and return
1416         return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v );
1417       }
1418     }else if( n.getKind()==kind::SEP_PTO ){
1419       //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
1420       Assert( d_label_model.find( o_lbl )!=d_label_model.end() );
1421       Node vr = d_valuation.getModel()->getRepresentative( n[0] );
1422       Node svr = NodeManager::currentNM()->mkNode( kind::SINGLETON, vr );
1423       bool inBaseHeap = std::find( d_label_model[o_lbl].d_heap_locs_model.begin(), d_label_model[o_lbl].d_heap_locs_model.end(), svr )!=d_label_model[o_lbl].d_heap_locs_model.end();
1424       Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap << " for value ref " << vr << " in " << o_lbl << std::endl;
1425       std::vector< Node > children;
1426       if( inBaseHeap ){
1427         Node s = NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] );
1428         children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) );
1429       }else{
1430         //look up value of data
1431         std::map< Node, Node >::iterator it = pto_model.find( vr );
1432         if( it!=pto_model.end() ){
1433           if( n[1]!=it->second ){
1434             children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], it->second ) );
1435           }
1436         }else{
1437           Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl;
1438         }
1439       }
1440       children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, NodeManager::currentNM()->mkNode( kind::SINGLETON, n[0] ), lbl_v ) );
1441       Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) );
1442       Trace("sep-inst-debug") << "Return " << ret << std::endl;
1443       return ret;
1444     }else if( n.getKind()==kind::SEP_EMP ){
1445       //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
1446       return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType().toType())) );
1447     }else{
1448       std::map< Node, Node >::iterator it = visited.find( n );
1449       if( it==visited.end() ){
1450         std::vector< Node > children;
1451         if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
1452           children.push_back( n.getOperator() );
1453         }
1454         bool childChanged = false;
1455         for( unsigned i=0; i<n.getNumChildren(); i++ ){
1456           Node aln = instantiateLabel( n[i], o_lbl, lbl, lbl_v, visited, pto_model, rtn, active_lbl, ind );
1457           if( aln.isNull() ){
1458             return Node::null();
1459           }else{
1460             children.push_back( aln );
1461             childChanged = childChanged || aln!=n[i];
1462           }
1463         }
1464         Node ret = n;
1465         if( childChanged ){
1466           ret = NodeManager::currentNM()->mkNode( n.getKind(), children );
1467         }
1468         //careful about caching
1469         //visited[n] = ret;
1470         return ret;
1471       }else{
1472         return it->second;
1473       }
1474     }
1475   }
1476 }
1477
1478 void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ) {
1479   Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact << std::endl;
1480   assert_active[fact] = false;
1481   bool polarity = fact.getKind() != kind::NOT;
1482   TNode atom = polarity ? fact : fact[0];
1483   TNode s_atom = atom[0];
1484   TNode s_lbl = atom[1];
1485   if( s_atom.getKind()==kind::SEP_WAND || s_atom.getKind()==kind::SEP_STAR ){
1486     for( unsigned j=0; j<s_atom.getNumChildren(); j++ ){
1487       Node lblc = getLabel( s_atom, j, s_lbl );
1488       for( unsigned k=0; k<lbl_to_assertions[lblc].size(); k++ ){
1489         setInactiveAssertionRec( lbl_to_assertions[lblc][k], lbl_to_assertions, assert_active );
1490       }
1491     }
1492   }
1493 }
1494
1495 void TheorySep::getLabelChildren( Node s_atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels ) {
1496   for( unsigned i=0; i<s_atom.getNumChildren(); i++ ){
1497     Node lblc = getLabel( s_atom, i, lbl );
1498     Assert( !lblc.isNull() );
1499     std::map< Node, Node > visited;
1500     Node lc = applyLabel( s_atom[i], lblc, visited );
1501     Assert( !lc.isNull() );
1502     if( i==1 && s_atom.getKind()==kind::SEP_WAND ){
1503       lc = lc.negate();
1504     }
1505     children.push_back( lc );
1506     labels.push_back( lblc );
1507   }
1508   Assert( children.size()>1 );
1509 }
1510
1511 void TheorySep::computeLabelModel( Node lbl ) {
1512   if( !d_label_model[lbl].d_computed ){
1513     d_label_model[lbl].d_computed = true;
1514
1515     //we must get the value of lbl from the model: this is being run at last call, after the model is constructed
1516     //Assert(...); TODO
1517     Node v_val = d_valuation.getModel()->getRepresentative( lbl );
1518     Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl;
1519     if( v_val.getKind()!=kind::EMPTYSET ){
1520       while( v_val.getKind()==kind::UNION ){
1521         Assert( v_val[1].getKind()==kind::SINGLETON );
1522         d_label_model[lbl].d_heap_locs_model.push_back( v_val[1] );
1523         v_val = v_val[0];
1524       }
1525       if( v_val.getKind()==kind::SINGLETON ){
1526         d_label_model[lbl].d_heap_locs_model.push_back( v_val );
1527       }else{
1528         throw Exception("Could not establish value of heap in model.");
1529         Assert( false );
1530       }
1531     }
1532     for( unsigned j=0; j<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
1533       Node u = d_label_model[lbl].d_heap_locs_model[j];
1534       Assert( u.getKind()==kind::SINGLETON );
1535       u = u[0];
1536       Node tt;
1537       std::map< Node, Node >::iterator itm = d_tmodel.find( u );
1538       if( itm==d_tmodel.end() ) {
1539         //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl;
1540         //Assert( false );
1541         //tt = u;
1542         //TypeNode tn = u.getType().getRefConstituentType();
1543         TypeNode tn = u.getType();
1544         Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl;
1545         Assert( d_type_references_all.find( tn )!=d_type_references_all.end() );
1546         Assert( !d_type_references_all[tn].empty() );
1547         tt = d_type_references_all[tn][0];
1548       }else{
1549         tt = itm->second;
1550       }
1551       Node stt = NodeManager::currentNM()->mkNode( kind::SINGLETON, tt );
1552       Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl;
1553       d_label_model[lbl].d_heap_locs.push_back( stt );
1554     }
1555   }
1556 }
1557
1558 Node TheorySep::getRepresentative( Node t ) {
1559   if( d_equalityEngine.hasTerm( t ) ){
1560     return d_equalityEngine.getRepresentative( t );
1561   }else{
1562     return t;
1563   }
1564 }
1565
1566 bool TheorySep::hasTerm( Node a ){
1567   return d_equalityEngine.hasTerm( a );
1568 }
1569
1570 bool TheorySep::areEqual( Node a, Node b ){
1571   if( a==b ){
1572     return true;
1573   }else if( hasTerm( a ) && hasTerm( b ) ){
1574     return d_equalityEngine.areEqual( a, b );
1575   }else{
1576     return false;
1577   }
1578 }
1579
1580 bool TheorySep::areDisequal( Node a, Node b ){
1581   if( a==b ){
1582     return false;
1583   }else if( hasTerm( a ) && hasTerm( b ) ){
1584     if( d_equalityEngine.areDisequal( a, b, false ) ){
1585       return true;
1586     }
1587   }
1588   return false;
1589 }
1590
1591
1592 void TheorySep::eqNotifyPreMerge(TNode t1, TNode t2) {
1593
1594 }
1595
1596 void TheorySep::eqNotifyPostMerge(TNode t1, TNode t2) {
1597   HeapAssertInfo * e2 = getOrMakeEqcInfo( t2, false );
1598   if( e2 && ( !e2->d_pto.get().isNull() || e2->d_has_neg_pto.get() ) ){
1599     HeapAssertInfo * e1 = getOrMakeEqcInfo( t1, true );
1600     if( !e2->d_pto.get().isNull() ){
1601       if( !e1->d_pto.get().isNull() ){
1602         Trace("sep-pto-debug") << "While merging " << t1 << " " << t2 << ", merge pto." << std::endl;
1603         mergePto( e1->d_pto.get(), e2->d_pto.get() );
1604       }else{
1605         e1->d_pto.set( e2->d_pto.get() );
1606       }
1607     }
1608     e1->d_has_neg_pto.set( e1->d_has_neg_pto.get() || e2->d_has_neg_pto.get() );
1609     //validate
1610     validatePto( e1, t1 );
1611   }
1612 }
1613
1614 void TheorySep::validatePto( HeapAssertInfo * ei, Node ei_n ) {
1615   if( !ei->d_pto.get().isNull() && ei->d_has_neg_pto.get() ){
1616     for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
1617       Node fact = (*i);
1618       bool polarity = fact.getKind() != kind::NOT;
1619       if( !polarity ){
1620         TNode atom = polarity ? fact : fact[0];
1621         Assert( atom.getKind()==kind::SEP_LABEL );
1622         TNode s_atom = atom[0];
1623         if( s_atom.getKind()==kind::SEP_PTO ){
1624           if( areEqual( atom[1], ei_n ) ){
1625             addPto( ei, ei_n, atom, false );
1626           }
1627         }
1628       }
1629     }
1630     //we have now processed all pending negated pto
1631     ei->d_has_neg_pto.set( false );
1632   }
1633 }
1634
1635 void TheorySep::addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity ) {
1636   Trace("sep-pto") << "Add pto " << p << ", pol = " << polarity << " to eqc " << ei_n << std::endl;
1637   if( !ei->d_pto.get().isNull() ){
1638     if( polarity ){
1639       Trace("sep-pto-debug") << "...eqc " << ei_n << " already has pto " << ei->d_pto.get() << ", merge." << std::endl;
1640       mergePto( ei->d_pto.get(), p );
1641     }else{
1642       Node pb = ei->d_pto.get();
1643       Trace("sep-pto") << "Process positive/negated pto " << " " << pb << " " << p << std::endl;
1644       Assert( pb.getKind()==kind::SEP_LABEL && pb[0].getKind()==kind::SEP_PTO );
1645       Assert( p.getKind()==kind::SEP_LABEL && p[0].getKind()==kind::SEP_PTO );
1646       Assert( areEqual( pb[1], p[1] ) );
1647       std::vector< Node > exp;
1648       if( pb[1]!=p[1] ){
1649         //if( pb[1].getKind()==kind::SINGLETON && p[1].getKind()==kind::SINGLETON ){
1650         //  exp.push_back( pb[1][0].eqNode( p[1][0] ) );
1651         //}else{
1652         exp.push_back( pb[1].eqNode( p[1] ) );
1653         //}
1654       }
1655       exp.push_back( pb );
1656       exp.push_back( p.negate() );
1657       std::vector< Node > conc;
1658       if( pb[0][1]!=p[0][1] ){
1659         conc.push_back( pb[0][1].eqNode( p[0][1] ).negate() );
1660       }
1661       //if( pb[1]!=p[1] ){
1662       //  conc.push_back( pb[1].eqNode( p[1] ).negate() );
1663       //}
1664       Node n_conc = conc.empty() ? d_false : ( conc.size()==1 ? conc[0] : NodeManager::currentNM()->mkNode( kind::OR, conc ) );
1665       Trace("sep-pto")  << "Conclusion is " << n_conc << std::endl;
1666       // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w
1667       sendLemma( exp, n_conc, "PTO_NEG_PROP" );
1668     }
1669   }else{
1670     if( polarity ){
1671       ei->d_pto.set( p );
1672       validatePto( ei, ei_n );
1673     }else{
1674       ei->d_has_neg_pto.set( true );
1675     }
1676   }
1677 }
1678
1679 void TheorySep::mergePto( Node p1, Node p2 ) {
1680   Trace("sep-lemma-debug") << "Merge pto " << p1 << " " << p2 << std::endl;
1681   Assert( p1.getKind()==kind::SEP_LABEL && p1[0].getKind()==kind::SEP_PTO );
1682   Assert( p2.getKind()==kind::SEP_LABEL && p2[0].getKind()==kind::SEP_PTO );
1683   if( !areEqual( p1[0][1], p2[0][1] ) ){
1684     std::vector< Node > exp;
1685     if( p1[1]!=p2[1] ){
1686       Assert( areEqual( p1[1], p2[1] ) );
1687       exp.push_back( p1[1].eqNode( p2[1] ) );
1688     }
1689     exp.push_back( p1 );
1690     exp.push_back( p2 );
1691     //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w
1692     sendLemma( exp, p1[0][1].eqNode( p2[0][1] ), "PTO_PROP" );
1693   }
1694 }
1695
1696 void TheorySep::sendLemma( std::vector< Node >& ant, Node conc, const char * c, bool infer ) {
1697   Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc << std::endl;
1698   conc = Rewriter::rewrite( conc );
1699   Trace("sep-lemma-debug") << "Got : " << conc << std::endl;
1700   if( conc!=d_true ){
1701     if( infer && conc!=d_false ){
1702       Node ant_n;
1703       if( ant.empty() ){
1704         ant_n = d_true;
1705       }else if( ant.size()==1 ){
1706         ant_n = ant[0];
1707       }else{
1708         ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant );
1709       }
1710       Trace("sep-lemma") << "Sep::Infer: " << conc << " from " << ant_n << " by " << c << std::endl;
1711       d_pending_exp.push_back( ant_n );
1712       d_pending.push_back( conc );
1713       d_infer.push_back( ant_n );
1714       d_infer_exp.push_back( conc );
1715     }else{
1716       std::vector< TNode > ant_e;
1717       for( unsigned i=0; i<ant.size(); i++ ){
1718         Trace("sep-lemma-debug") << "Explain : " << ant[i] << std::endl;
1719         explain( ant[i], ant_e );
1720       }
1721       Node ant_n;
1722       if( ant_e.empty() ){
1723         ant_n = d_true;
1724       }else if( ant_e.size()==1 ){
1725         ant_n = ant_e[0];
1726       }else{
1727         ant_n = NodeManager::currentNM()->mkNode( kind::AND, ant_e );
1728       }
1729       if( conc==d_false ){
1730         Trace("sep-lemma") << "Sep::Conflict: " << ant_n << " by " << c << std::endl;
1731         d_out->conflict( ant_n );
1732         d_conflict = true;
1733       }else{
1734         Trace("sep-lemma") << "Sep::Lemma: " << conc << " from " << ant_n << " by " << c << std::endl;
1735         d_pending_exp.push_back( ant_n );
1736         d_pending.push_back( conc );
1737         d_pending_lem.push_back( d_pending.size()-1 );
1738       }
1739     }
1740   }
1741 }
1742
1743 void TheorySep::doPendingFacts() {
1744   if( d_pending_lem.empty() ){
1745     for( unsigned i=0; i<d_pending.size(); i++ ){
1746       if( d_conflict ){
1747         break;
1748       }
1749       Node atom = d_pending[i].getKind()==kind::NOT ? d_pending[i][0] : d_pending[i];
1750       bool pol = d_pending[i].getKind()!=kind::NOT;
1751       Trace("sep-pending") << "Sep : Assert to EE : " << atom << ", pol = " << pol << std::endl;
1752       if( atom.getKind()==kind::EQUAL ){
1753         d_equalityEngine.assertEquality(atom, pol, d_pending_exp[i]);
1754       }else{
1755         d_equalityEngine.assertPredicate(atom, pol, d_pending_exp[i]);
1756       }
1757     }
1758   }else{
1759     for( unsigned i=0; i<d_pending_lem.size(); i++ ){
1760       if( d_conflict ){
1761         break;
1762       }
1763       int index = d_pending_lem[i];
1764       Node lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, d_pending_exp[index], d_pending[index] );
1765       if( d_lemmas_produced_c.find( lem )==d_lemmas_produced_c.end() ){
1766         d_lemmas_produced_c.insert( lem );
1767         d_out->lemma( lem );
1768         Trace("sep-pending") << "Sep : Lemma : " << lem << std::endl;
1769       }
1770     }
1771   }
1772   d_pending_exp.clear();
1773   d_pending.clear();
1774   d_pending_lem.clear();
1775 }
1776
1777 void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
1778   Trace(c) << "[" << std::endl;
1779   Trace(c) << "  ";
1780   for( unsigned j=0; j<heap.d_heap_locs.size(); j++ ){
1781     Trace(c) << heap.d_heap_locs[j] << " ";
1782   }
1783   Trace(c) << std::endl;
1784   Trace(c) << "]" << std::endl;
1785 }
1786
1787 Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
1788   Assert( d_heap_locs.size()==d_heap_locs_model.size() );
1789   if( d_heap_locs.empty() ){
1790     return NodeManager::currentNM()->mkConst(EmptySet(tn.toType()));
1791   }else if( d_heap_locs.size()==1 ){
1792     return d_heap_locs[0];
1793   }else{
1794     Node curr = NodeManager::currentNM()->mkNode( kind::UNION, d_heap_locs[0], d_heap_locs[1] );
1795     for( unsigned j=2; j<d_heap_locs.size(); j++ ){
1796       curr = NodeManager::currentNM()->mkNode( kind::UNION, curr, d_heap_locs[j] );
1797     }
1798     return curr;
1799   }
1800 }
1801
1802 }/* CVC4::theory::sep namespace */
1803 }/* CVC4::theory namespace */
1804 }/* CVC4 namespace */