1 /********************* */
2 /*! \file theory_sep.cpp
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
12 ** \brief Implementation of the theory of sep.
14 ** Implementation of the theory of sep.
18 #include "theory/sep/theory_sep.h"
19 #include "theory/valuation.h"
20 #include "expr/kind.h"
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"
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
),
39 d_equalityEngine(d_notify
, c
, "theory::sep::TheorySep", true),
44 d_spatial_assertions(c
)
46 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
47 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
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);
54 TheorySep::~TheorySep() {
55 for( std::map
< Node
, HeapAssertInfo
* >::iterator it
= d_eqc_info
.begin(); it
!= d_eqc_info
.end(); ++it
){
60 void TheorySep::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
61 d_equalityEngine
.setMasterEqualityEngine(eq
);
64 Node
TheorySep::mkAnd( std::vector
< TNode
>& assumptions
) {
65 if( assumptions
.empty() ){
67 }else if( assumptions
.size()==1 ){
68 return assumptions
[0];
70 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
74 /////////////////////////////////////////////////////////////////////////////
76 /////////////////////////////////////////////////////////////////////////////
80 Node
TheorySep::ppRewrite(TNode term
) {
81 Trace("sep-pp") << "ppRewrite : " << term
<< std::endl
;
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)
87 TypeNode tn = getReferenceType( s_atom, card );
88 Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl;
94 //must process assertions at preprocess so that quantified assertions are processed properly
95 void TheorySep::processAssertions( std::vector
< Node
>& assertions
) {
97 std::map
< Node
, bool > visited
;
98 for( unsigned i
=0; i
<assertions
.size(); i
++ ){
99 processAssertion( assertions
[i
], visited
);
103 void TheorySep::processAssertion( Node n
, std::map
< Node
, bool >& visited
) {
104 if( visited
.find( n
)==visited
.end() ){
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
);
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)
113 TypeNode tn
= getReferenceType( n
, card
);
114 Trace("sep-pp") << " reference type is " << tn
<< ", card is " << card
<< std::endl
;
116 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
117 processAssertion( n
[i
], visited
);
123 Theory::PPAssertStatus
TheorySep::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
125 return PP_ASSERT_STATUS_UNSOLVED
;
129 /////////////////////////////////////////////////////////////////////////////
130 // T-PROPAGATION / REGISTRATION
131 /////////////////////////////////////////////////////////////////////////////
134 bool TheorySep::propagate(TNode literal
)
136 Debug("sep") << "TheorySep::propagate(" << literal
<< ")" << std::endl
;
137 // If already in conflict, no more propagation
139 Debug("sep") << "TheorySep::propagate(" << literal
<< "): already in conflict" << std::endl
;
142 bool ok
= d_out
->propagate(literal
);
147 }/* TheorySep::propagate(TNode) */
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
);
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
);
162 d_equalityEngine
.explainPredicate( atom
, polarity
, assumptions
);
167 void TheorySep::preRegisterTermRec(TNode t
, std::map
< TNode
, bool >& visited
) {
168 if( visited
.find( t
)==visited
.end() ){
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
;
180 Node nr
= it
->second
;
181 Trace("sep-prereg") << "...reference is " << nr
<< "." << std::endl
;
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
;
192 for( unsigned i
=0; i
<t
.getNumChildren(); i
++ ){
193 preRegisterTermRec( t
[i
], visited
);
199 void TheorySep::preRegisterTerm(TNode term
){
200 std::map
< TNode
, bool > visited
;
201 preRegisterTermRec( term
, visited
);
205 void TheorySep::propagate(Effort e
){
210 Node
TheorySep::explain(TNode literal
)
212 Debug("sep") << "TheorySep::explain(" << literal
<< ")" << std::endl
;
213 std::vector
<TNode
> assumptions
;
214 explain(literal
, assumptions
);
215 return mkAnd(assumptions
);
219 /////////////////////////////////////////////////////////////////////////////
221 /////////////////////////////////////////////////////////////////////////////
224 void TheorySep::addSharedTerm(TNode t
) {
225 Debug("sep") << "TheorySep::addSharedTerm(" << t
<< ")" << std::endl
;
226 d_equalityEngine
.addTriggerTerm(t
, THEORY_SEP
);
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
;
236 else if (d_equalityEngine
.areDisequal(a
, b
, false)) {
237 // The terms are implied to be dis-equal
238 return EQUALITY_FALSE
;
240 return EQUALITY_UNKNOWN
;//FALSE_IN_MODEL;
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
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
270 /////////////////////////////////////////////////////////////////////////////
272 /////////////////////////////////////////////////////////////////////////////
275 void TheorySep::collectModelInfo( TheoryModel
* m
, bool fullModel
)
277 // Send the equality engine information to the model
278 m
->assertEqualityEngine( &d_equalityEngine
);
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
;
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") << "_";
294 Trace("sep-model") << d_pto_model
[l
];
296 Trace("sep-model") << std::endl
;
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
;
307 /////////////////////////////////////////////////////////////////////////////
309 /////////////////////////////////////////////////////////////////////////////
312 void TheorySep::presolve() {
313 Trace("sep-pp") << "Presolving" << std::endl
;
314 //TODO: cleanup if incremental?
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
);
325 /////////////////////////////////////////////////////////////////////////////
327 /////////////////////////////////////////////////////////////////////////////
330 void TheorySep::check(Effort e
) {
331 if (done() && !fullEffort(e
) && e
!= EFFORT_LAST_CALL
) {
335 getOutputChannel().spendResource(options::theoryCheckStep());
337 TimerStat::CodeTimer
checkTimer(d_checkTime
);
338 Trace("sep-check") << "Sep::check(): " << e
<< endl
;
340 while( !done() && !d_conflict
){
341 // Get all the assertions
342 Assertion assertion
= get();
343 TNode fact
= assertion
.assertion
;
345 Trace("sep-assert") << "TheorySep::check(): processing " << fact
<< std::endl
;
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];
354 //normalize argument TODO
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
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
);
372 lem
= NodeManager::currentNM()->mkNode( kind::OR
, s_atom
.negate(), s_atom_new
);
374 lem
= NodeManager::currentNM()->mkNode( kind::OR
, s_atom
, s_atom_new
.negate() );
376 Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem
<< std::endl
;
382 if( d_reduce
.find( fact
)==d_reduce
.end() ){
383 Trace("sep-lemma-debug") << "Reducing assertion " << fact
<< std::endl
;
384 d_reduce
.insert( fact
);
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
;
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() ){
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
] << " ";
403 Trace("sep-bound") << std::endl
<< " to children of " << s_atom
<< std::endl
;
405 for( unsigned j
=0; j
<s_atom
.getNumChildren(); j
++ ){
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() );
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] );
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
) );
428 Trace("sep-bound") << "Done propagate Bound(" << s_lbl
<< ")" << std::endl
;
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
] );
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
);
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
);
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
] );
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] );
471 conc
= s_lbl
.eqNode( ss
);
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
);
476 //labeled emp should be rewritten
479 d_red_conc
[s_lbl
][s_atom
] = conc
;
483 if( !conc
.isNull() ){
484 bool use_polarity
= s_atom
.getKind()==kind::SEP_WAND
? !polarity
: 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
;
501 //reduce based on implication
506 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, ant
, conc
);
507 Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem
<< std::endl
;
511 Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl
;
515 //assert to equality engine
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
);
521 d_equalityEngine
.assertPredicate(atom
, polarity
, fact
);
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
;
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
);
540 //add to spatial assertions
541 if( !d_conflict
&& is_spatial
){
542 d_spatial_assertions
.push_back( fact
);
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();
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
;
562 Trace("sep-process") << "?" << std::endl
;
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
) {
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
;
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];
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
];
595 if( getValuation().hasSatValue( guard
, value
) ) {
596 assert_active
[fact
] = value
;
601 //(recursively) set inactive sub-assertions
602 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
604 if( !assert_active
[fact
] ){
605 setInactiveAssertionRec( fact
, lbl_to_assertions
, assert_active
);
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
) {
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
);
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
) {
624 Trace("sep-process") << " " << fact
;
625 if( !assert_active
[fact
] ){
626 Trace("sep-process") << " [inactive]";
628 Trace("sep-process") << std::endl
;
630 Trace("sep-process") << "---" << std::endl
;
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
) << " ";
645 Trace("sep-eqc") << " } " << std::endl
;
648 Trace("sep-eqc") << std::endl
;
651 if( options::sepCheckNeg() ){
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
) {
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
;
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;
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
) {
680 bool polarity
= fact
.getKind() != kind::NOT
;
681 TNode atom
= polarity
? fact
: fact
[0];
682 TNode s_atom
= atom
[0];
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
;
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() ){
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
;
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
;
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() );
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
;
736 inst_success
= false;
738 inst
= Rewriter::rewrite( inst
);
739 if( inst
==( polarity
? d_true
: d_false
) ){
740 inst_success
= false;
742 conc
.push_back( polarity
? inst
: inst
.negate() );
746 std::vector
< Node
> lemc
;
747 Node pol_atom
= atom
;
749 pol_atom
= atom
.negate();
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
;
763 Trace("sep-process") << "*** repeated refinement lemma : " << lem
<< std::endl
;
767 Trace("sep-process-debug") << " no children." << std::endl
;
768 Assert( s_atom
.getKind()==kind::SEP_PTO
);
771 Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom
<< std::endl
;
777 Trace("sep-process") << "WARNING : could not find refinement lemma!!!" << std::endl
;
779 d_out
->setIncomplete();
784 Trace("sep-check") << "Sep::check(): " << e
<< " done, conflict=" << d_conflict
.get() << endl
;
788 bool TheorySep::needsCheckLastEffort() {
792 Node
TheorySep::getNextDecisionRequest() {
793 for( unsigned i
=0; i
<d_neg_guards
.size(); i
++ ){
794 Node g
= d_neg_guards
[i
];
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
);
801 //must wait to decide on counterexample literal from quantified formula
802 Node cel
= getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q
);
804 if( d_valuation
.hasSatValue( cel
, value
) ){
807 Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g
<< " until " << cel
<< " is set " << std::endl
;
814 if( !d_valuation
.hasSatValue( g
, value
) ) {
815 Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g
<< " (" << i
<< "/" << d_neg_guards
.size() << ")" << std::endl
;
820 Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl
;
824 void TheorySep::conflict(TNode a
, TNode b
) {
825 Trace("sep-conflict") << "Sep::conflict : " << a
<< " " << b
<< std::endl
;
827 if (a
.getKind() == kind::CONST_BOOLEAN
) {
828 conflictNode
= explain(a
.iffNode(b
));
830 conflictNode
= explain(a
.eqNode(b
));
833 d_out
->conflict( conflictNode
);
837 TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context
* c
) : d_pto(c
), d_has_neg_pto(c
,false) {
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() ){
845 HeapAssertInfo
* ei
= new HeapAssertInfo( getSatContext() );
852 return (*e_i
).second
;
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() ){
863 if( index
==-1 && ( atom
.getKind()==kind::SEP_STAR
|| atom
.getKind()==kind::SEP_WAND
) ){
864 for( unsigned i
=0; i
<atom
.getNumChildren(); i
++ ){
866 TypeNode ctn
= getReferenceType( atom
, cardc
, i
);
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
] );
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
);
883 if( tn
.isNull() && index
==-1 ){
884 tn
= NodeManager::currentNM()->booleanType();
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
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
] );
898 // update maximum cardinality value
899 if( card
>(int)d_card_max
[tn
] ){
900 d_card_max
[tn
] = card
;
905 Assert( d_reference_type_card
[atom
].find( index
)!=d_reference_type_card
[atom
].end() );
906 card
= d_reference_type_card
[atom
][index
];
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
;
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;
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] );
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
;
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());
940 //return n[1].getType();
941 }else if( n
.getKind()==kind::SEP_EMP
){
944 return n
[0].getType();
945 }else if( n
.getKind()==kind::SEP_STAR
|| n
.getKind()==kind::SEP_WAND
){
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
] );
960 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
962 TypeNode tn
= getReferenceType2( atom
, cardc
, index
, n
[i
], visited
);
966 card
= cardc
>card
? cardc
: card
;
972 Trace("sep-type-debug") << "already visit : " << n
<< " : " << atom
<< " " << index
<< std::endl
;
974 return TypeNode::null();
979 int TheorySep::getCardinality( Node n, std::vector< Node >& refs ) {
980 std::map< Node, int > visited;
981 return getCardinality2( n, refs, visited );
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() ){
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
;
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
;
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() );
1023 d_type_references_all
[tn
].push_back( e
);
1024 d_lbl_reference_bound
[d_base_label
[tn
]].push_back( e
);
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
;
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
);
1035 Trace("sep-bound") << "reference cannot be bound (possibly due to quantified pto)." << std::endl
;
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 );
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
;
1057 Node
TheorySep::mkUnion( TypeNode tn
, std::vector
< Node
>& locs
) {
1060 TypeNode ltn
= NodeManager::currentNM()->mkSetType(tn
);
1061 return NodeManager::currentNM()->mkConst(EmptySet(ltn
.toType()));
1063 for( unsigned i
=0; i
<locs
.size(); i
++ ){
1065 Assert( !s
.isNull() );
1066 s
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, s
);
1070 u
= NodeManager::currentNM()->mkNode( kind::UNION
, s
, u
);
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() ){
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
;
1091 return (*it
).second
;
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 ){
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() );
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
];
1116 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
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();
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
;
1139 Assert( n
.getKind()!=kind::SEP_LABEL
);
1140 if( n
.getKind()==kind::SEP_STAR
|| n
.getKind()==kind::SEP_WAND
){
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
;
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
) );
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
);
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();
1168 if( n
.getKind()==kind::SEP_STAR
){
1169 Assert( children
.size()>1 );
1170 return NodeManager::currentNM()->mkNode( kind::AND
, children
);
1172 return NodeManager::currentNM()->mkNode( kind::OR
, children
[0].negate(), children
[1] );
1175 //nested star/wand, label it and return
1176 return NodeManager::currentNM()->mkNode( kind::SEP_LABEL
, n
, lbl_v
);
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
;
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
) );
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
) );
1197 Trace("sep-inst-debug") << "Data for " << vr
<< " was not specified, do not add condition." << std::endl
;
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
;
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())) );
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() );
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
);
1218 return Node::null();
1220 children
.push_back( aln
);
1221 childChanged
= childChanged
|| aln
!=n
[i
];
1226 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1228 //careful about caching
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
);
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
){
1265 children
.push_back( lc
);
1266 labels
.push_back( lblc
);
1268 Assert( children
.size()>1 );
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;
1275 //we must get the value of lbl from the model: this is being run at last call, after the model is constructed
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] );
1285 Assert( v_val
.getKind()==kind::SINGLETON
);
1286 d_label_model
[lbl
].d_heap_locs_model
.push_back( v_val
);
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
);
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;
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];
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
);
1314 Node
TheorySep::getRepresentative( Node t
) {
1315 if( d_equalityEngine
.hasTerm( t
) ){
1316 return d_equalityEngine
.getRepresentative( t
);
1322 bool TheorySep::hasTerm( Node a
){
1323 return d_equalityEngine
.hasTerm( a
);
1326 bool TheorySep::areEqual( Node a
, Node b
){
1329 }else if( hasTerm( a
) && hasTerm( b
) ){
1330 return d_equalityEngine
.areEqual( a
, b
);
1336 bool TheorySep::areDisequal( Node a
, Node b
){
1339 }else if( hasTerm( a
) && hasTerm( b
) ){
1340 if( d_equalityEngine
.areDisequal( a
, b
, false ) ){
1348 void TheorySep::eqNotifyPreMerge(TNode t1
, TNode t2
) {
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() );
1361 e1
->d_pto
.set( e2
->d_pto
.get() );
1364 e1
->d_has_neg_pto
.set( e1
->d_has_neg_pto
.get() || e2
->d_has_neg_pto
.get() );
1366 validatePto( e1
, t1
);
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
) {
1374 bool polarity
= fact
.getKind() != kind::NOT
;
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 );
1386 //we have now processed all pending negated pto
1387 ei
->d_has_neg_pto
.set( false );
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() ){
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
);
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
;
1405 exp
.push_back( pb
[1].eqNode( p
[1] ) );
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() );
1414 conc
.push_back( pb
[1].eqNode( p
[1] ).negate() );
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" );
1422 validatePto( ei
, ei_n
);
1424 ei
->d_has_neg_pto
.set( true );
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
;
1436 Assert( areEqual( p1
[1], p2
[1] ) );
1437 exp
.push_back( p1
[1].eqNode( p2
[1] ) );
1439 exp
.push_back( p1
);
1440 exp
.push_back( p2
);
1441 sendLemma( exp
, p1
[0][1].eqNode( p2
[0][1] ), "PTO_PROP" );
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
;
1450 if( infer
&& conc
!=d_false
){
1454 }else if( ant
.size()==1 ){
1457 ant_n
= NodeManager::currentNM()->mkNode( kind::AND
, ant
);
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
);
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
);
1471 if( ant_e
.empty() ){
1473 }else if( ant_e
.size()==1 ){
1476 ant_n
= NodeManager::currentNM()->mkNode( kind::AND
, ant_e
);
1478 if( conc
==d_false
){
1479 Trace("sep-lemma") << "Sep::Conflict: " << ant_n
<< " by " << c
<< std::endl
;
1480 d_out
->conflict( ant_n
);
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 );
1492 void TheorySep::doPendingFacts() {
1493 if( d_pending_lem
.empty() ){
1494 for( unsigned i
=0; i
<d_pending
.size(); i
++ ){
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
]);
1504 d_equalityEngine
.assertPredicate(atom
, pol
, d_pending_exp
[i
]);
1508 for( unsigned i
=0; i
<d_pending_lem
.size(); i
++ ){
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
;
1518 d_pending_exp
.clear();
1520 d_pending_lem
.clear();
1523 void TheorySep::debugPrintHeap( HeapInfo
& heap
, const char * c
) {
1524 Trace(c
) << "[" << std::endl
;
1526 for( unsigned j
=0; j
<heap
.d_heap_locs
.size(); j
++ ){
1527 Trace(c
) << heap
.d_heap_locs
[j
] << " ";
1529 Trace(c
) << std::endl
;
1530 Trace(c
) << "]" << std::endl
;
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];
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
] );
1548 }/* CVC4::theory::sep namespace */
1549 }/* CVC4::theory namespace */
1550 }/* CVC4 namespace */