projects / cvc5.git / blob
? search:


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