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