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