GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sep/theory_sep.cpp Lines: 912 1077 84.7 %
Date: 2021-03-23 Branches: 2273 5448 41.7 %

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