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