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"
29 #include "options/quantifiers_options.h"
37 TheorySep::TheorySep(context::Context
* c
, context::UserContext
* u
, OutputChannel
& out
, Valuation valuation
, const LogicInfo
& logicInfo
) :
38 Theory(THEORY_SEP
, c
, u
, out
, valuation
, logicInfo
),
39 d_lemmas_produced_c(u
),
41 d_equalityEngine(d_notify
, c
, "theory::sep::TheorySep", true),
46 d_spatial_assertions(c
)
48 d_true
= NodeManager::currentNM()->mkConst
<bool>(true);
49 d_false
= NodeManager::currentNM()->mkConst
<bool>(false);
50 d_bounds_init
= false;
52 // The kinds we are treating as function application in congruence
53 d_equalityEngine
.addFunctionKind(kind::SEP_PTO
);
54 //d_equalityEngine.addFunctionKind(kind::SEP_STAR);
57 TheorySep::~TheorySep() {
58 for( std::map
< Node
, HeapAssertInfo
* >::iterator it
= d_eqc_info
.begin(); it
!= d_eqc_info
.end(); ++it
){
63 void TheorySep::setMasterEqualityEngine(eq::EqualityEngine
* eq
) {
64 d_equalityEngine
.setMasterEqualityEngine(eq
);
67 Node
TheorySep::mkAnd( std::vector
< TNode
>& assumptions
) {
68 if( assumptions
.empty() ){
70 }else if( assumptions
.size()==1 ){
71 return assumptions
[0];
73 return NodeManager::currentNM()->mkNode( kind::AND
, assumptions
);
77 /////////////////////////////////////////////////////////////////////////////
79 /////////////////////////////////////////////////////////////////////////////
83 Node
TheorySep::ppRewrite(TNode term
) {
84 Trace("sep-pp") << "ppRewrite : " << term
<< std::endl
;
88 Theory::PPAssertStatus
TheorySep::ppAssert(TNode in
, SubstitutionMap
& outSubstitutions
) {
90 return PP_ASSERT_STATUS_UNSOLVED
;
94 /////////////////////////////////////////////////////////////////////////////
95 // T-PROPAGATION / REGISTRATION
96 /////////////////////////////////////////////////////////////////////////////
99 bool TheorySep::propagate(TNode literal
)
101 Debug("sep") << "TheorySep::propagate(" << literal
<< ")" << std::endl
;
102 // If already in conflict, no more propagation
104 Debug("sep") << "TheorySep::propagate(" << literal
<< "): already in conflict" << std::endl
;
107 bool ok
= d_out
->propagate(literal
);
112 }/* TheorySep::propagate(TNode) */
115 void TheorySep::explain(TNode literal
, std::vector
<TNode
>& assumptions
) {
116 if( literal
.getKind()==kind::SEP_LABEL
||
117 ( literal
.getKind()==kind::NOT
&& literal
[0].getKind()==kind::SEP_LABEL
) ){
118 //labelled assertions are never given to equality engine and should only come from the outside
119 assumptions
.push_back( literal
);
122 bool polarity
= literal
.getKind() != kind::NOT
;
123 TNode atom
= polarity
? literal
: literal
[0];
124 if (atom
.getKind() == kind::EQUAL
) {
125 d_equalityEngine
.explainEquality( atom
[0], atom
[1], polarity
, assumptions
, NULL
);
127 d_equalityEngine
.explainPredicate( atom
, polarity
, assumptions
);
133 void TheorySep::propagate(Effort e
){
138 Node
TheorySep::explain(TNode literal
)
140 Debug("sep") << "TheorySep::explain(" << literal
<< ")" << std::endl
;
141 std::vector
<TNode
> assumptions
;
142 explain(literal
, assumptions
);
143 return mkAnd(assumptions
);
147 /////////////////////////////////////////////////////////////////////////////
149 /////////////////////////////////////////////////////////////////////////////
152 void TheorySep::addSharedTerm(TNode t
) {
153 Debug("sep") << "TheorySep::addSharedTerm(" << t
<< ")" << std::endl
;
154 d_equalityEngine
.addTriggerTerm(t
, THEORY_SEP
);
158 EqualityStatus
TheorySep::getEqualityStatus(TNode a
, TNode b
) {
159 Assert(d_equalityEngine
.hasTerm(a
) && d_equalityEngine
.hasTerm(b
));
160 if (d_equalityEngine
.areEqual(a
, b
)) {
161 // The terms are implied to be equal
162 return EQUALITY_TRUE
;
164 else if (d_equalityEngine
.areDisequal(a
, b
, false)) {
165 // The terms are implied to be dis-equal
166 return EQUALITY_FALSE
;
168 return EQUALITY_UNKNOWN
;//FALSE_IN_MODEL;
172 void TheorySep::computeCareGraph() {
173 Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl
;
174 for (unsigned i
= 0; i
< d_sharedTerms
.size(); ++ i
) {
175 TNode a
= d_sharedTerms
[i
];
176 TypeNode aType
= a
.getType();
177 for (unsigned j
= i
+ 1; j
< d_sharedTerms
.size(); ++ j
) {
178 TNode b
= d_sharedTerms
[j
];
179 if (b
.getType() != aType
) {
180 // We don't care about the terms of different types
183 switch (d_valuation
.getEqualityStatus(a
, b
)) {
184 case EQUALITY_TRUE_AND_PROPAGATED
:
185 case EQUALITY_FALSE_AND_PROPAGATED
:
186 // If we know about it, we should have propagated it, so we can skip
198 /////////////////////////////////////////////////////////////////////////////
200 /////////////////////////////////////////////////////////////////////////////
203 void TheorySep::collectModelInfo( TheoryModel
* m
){
206 // Compute terms appearing in assertions and shared terms
207 computeRelevantTerms(termSet
);
209 // Send the equality engine information to the model
210 m
->assertEqualityEngine( &d_equalityEngine
, &termSet
);
213 void TheorySep::postProcessModel( TheoryModel
* m
){
214 Trace("sep-model") << "Printing model for TheorySep..." << std::endl
;
216 std::vector
< Node
> sep_children
;
219 for( std::map
< TypeNode
, Node
>::iterator it
= d_base_label
.begin(); it
!= d_base_label
.end(); ++it
){
220 //should only be constructing for one heap type
221 Assert( m_heap
.isNull() );
222 Assert( d_loc_to_data_type
.find( it
->first
)!=d_loc_to_data_type
.end() );
223 Trace("sep-model") << "Model for heap, type = " << it
->first
<< " with data type " << d_loc_to_data_type
[it
->first
] << " : " << std::endl
;
224 TypeNode data_type
= d_loc_to_data_type
[it
->first
];
225 computeLabelModel( it
->second
);
226 if( d_label_model
[it
->second
].d_heap_locs_model
.empty() ){
227 Trace("sep-model") << " [empty]" << std::endl
;
229 for( unsigned j
=0; j
<d_label_model
[it
->second
].d_heap_locs_model
.size(); j
++ ){
230 Assert( d_label_model
[it
->second
].d_heap_locs_model
[j
].getKind()==kind::SINGLETON
);
231 std::vector
< Node
> pto_children
;
232 Node l
= d_label_model
[it
->second
].d_heap_locs_model
[j
][0];
233 Assert( l
.isConst() );
234 pto_children
.push_back( l
);
235 Trace("sep-model") << " " << l
<< " -> ";
236 if( d_pto_model
[l
].isNull() ){
237 Trace("sep-model") << "_";
238 //m->d_comment_str << "_";
239 TypeEnumerator
te_range( data_type
);
240 if( data_type
.isInterpretedFinite() ){
241 pto_children
.push_back( *te_range
);
243 //must enumerate until we find one that is not explicitly pointed to
244 bool success
= false;
248 if( std::find( d_heap_locs_nptos
[l
].begin(), d_heap_locs_nptos
[l
].end(), cv
)==d_heap_locs_nptos
[l
].end() ){
254 pto_children
.push_back( cv
);
257 Trace("sep-model") << d_pto_model
[l
];
258 Node vpto
= d_valuation
.getModel()->getRepresentative( d_pto_model
[l
] );
259 Assert( vpto
.isConst() );
260 pto_children
.push_back( vpto
);
262 Trace("sep-model") << std::endl
;
263 sep_children
.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO
, pto_children
) );
266 Node nil
= getNilRef( it
->first
);
267 Node vnil
= d_valuation
.getModel()->getRepresentative( nil
);
268 m_neq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, nil
, vnil
);
269 Trace("sep-model") << "sep.nil = " << vnil
<< std::endl
;
270 Trace("sep-model") << std::endl
;
271 if( sep_children
.empty() ){
272 TypeEnumerator
te_domain( it
->first
);
273 TypeEnumerator
te_range( d_loc_to_data_type
[it
->first
] );
274 m_heap
= NodeManager::currentNM()->mkNode( kind::SEP_EMP
, *te_domain
, *te_range
);
275 }else if( sep_children
.size()==1 ){
276 m_heap
= sep_children
[0];
278 m_heap
= NodeManager::currentNM()->mkNode( kind::SEP_STAR
, sep_children
);
280 m
->setHeapModel( m_heap
, m_neq
);
282 Trace("sep-model") << "Finished printing model for TheorySep." << std::endl
;
285 /////////////////////////////////////////////////////////////////////////////
287 /////////////////////////////////////////////////////////////////////////////
290 void TheorySep::presolve() {
291 Trace("sep-pp") << "Presolving" << std::endl
;
292 //TODO: cleanup if incremental?
296 /////////////////////////////////////////////////////////////////////////////
298 /////////////////////////////////////////////////////////////////////////////
301 void TheorySep::check(Effort e
) {
302 if (done() && !fullEffort(e
) && e
!= EFFORT_LAST_CALL
) {
306 getOutputChannel().spendResource(options::theoryCheckStep());
308 TimerStat::CodeTimer
checkTimer(d_checkTime
);
309 Trace("sep-check") << "Sep::check(): " << e
<< endl
;
311 while( !done() && !d_conflict
){
312 // Get all the assertions
313 Assertion assertion
= get();
314 TNode fact
= assertion
.assertion
;
316 Trace("sep-assert") << "TheorySep::check(): processing " << fact
<< std::endl
;
318 bool polarity
= fact
.getKind() != kind::NOT
;
319 TNode atom
= polarity
? fact
: fact
[0];
321 if( atom.getKind()==kind::SEP_EMP ){
322 TypeNode tn = atom[0].getType();
323 if( d_emp_arg.find( tn )==d_emp_arg.end() ){
324 d_emp_arg[tn] = atom[0];
326 //normalize argument TODO
330 TNode s_atom
= atom
.getKind()==kind::SEP_LABEL
? atom
[0] : atom
;
331 TNode s_lbl
= atom
.getKind()==kind::SEP_LABEL
? atom
[1] : TNode::null();
332 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
;
333 if( is_spatial
&& s_lbl
.isNull() ){
334 if( d_reduce
.find( fact
)==d_reduce
.end() ){
335 Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom
<< std::endl
;
336 d_reduce
.insert( fact
);
337 //introduce top-level label, add iff
338 TypeNode refType
= getReferenceType( s_atom
);
339 Trace("sep-lemma-debug") << "...reference type is : " << refType
<< std::endl
;
340 Node b_lbl
= getBaseLabel( refType
);
341 Node s_atom_new
= NodeManager::currentNM()->mkNode( kind::SEP_LABEL
, s_atom
, b_lbl
);
343 Trace("sep-lemma-debug") << "...polarity is " << polarity
<< std::endl
;
345 lem
= NodeManager::currentNM()->mkNode( kind::OR
, s_atom
.negate(), s_atom_new
);
347 lem
= NodeManager::currentNM()->mkNode( kind::OR
, s_atom
, s_atom_new
.negate() );
349 Trace("sep-lemma-debug") << "Sep::Lemma : base reduction : " << lem
<< std::endl
;
355 if( d_reduce
.find( fact
)==d_reduce
.end() ){
356 Trace("sep-lemma-debug") << "Reducing assertion " << fact
<< std::endl
;
357 d_reduce
.insert( fact
);
359 std::map
< Node
, Node
>::iterator its
= d_red_conc
[s_lbl
].find( s_atom
);
360 if( its
==d_red_conc
[s_lbl
].end() ){
361 //make conclusion based on type of assertion
362 if( s_atom
.getKind()==kind::SEP_STAR
|| s_atom
.getKind()==kind::SEP_WAND
){
363 std::vector
< Node
> children
;
364 std::vector
< Node
> c_lems
;
365 TypeNode tn
= getReferenceType( s_atom
);
366 if( d_reference_bound_max
.find( tn
)!=d_reference_bound_max
.end() ){
367 c_lems
.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET
, s_lbl
, d_reference_bound_max
[tn
] ) );
369 std::vector
< Node
> labels
;
370 getLabelChildren( s_atom
, s_lbl
, children
, labels
);
371 Node empSet
= NodeManager::currentNM()->mkConst(EmptySet(s_lbl
.getType().toType()));
372 Assert( children
.size()>1 );
373 if( s_atom
.getKind()==kind::SEP_STAR
){
374 //reduction for heap : union, pairwise disjoint
375 Node ulem
= NodeManager::currentNM()->mkNode( kind::UNION
, labels
[0], labels
[1] );
376 for( unsigned i
=2; i
<labels
.size(); i
++ ){
377 ulem
= NodeManager::currentNM()->mkNode( kind::UNION
, ulem
, labels
[i
] );
379 ulem
= s_lbl
.eqNode( ulem
);
380 Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, union : " << ulem
<< std::endl
;
381 c_lems
.push_back( ulem
);
382 for( unsigned i
=0; i
<labels
.size(); i
++ ){
383 for( unsigned j
=(i
+1); j
<labels
.size(); j
++ ){
384 Node s
= NodeManager::currentNM()->mkNode( kind::INTERSECTION
, labels
[i
], labels
[j
] );
385 Node ilem
= s
.eqNode( empSet
);
386 Trace("sep-lemma-debug") << "Sep::Lemma : star reduction, disjoint : " << ilem
<< std::endl
;
387 c_lems
.push_back( ilem
);
391 Node ulem
= NodeManager::currentNM()->mkNode( kind::UNION
, s_lbl
, labels
[0] );
392 ulem
= ulem
.eqNode( labels
[1] );
393 Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, union : " << ulem
<< std::endl
;
394 c_lems
.push_back( ulem
);
395 Node s
= NodeManager::currentNM()->mkNode( kind::INTERSECTION
, s_lbl
, labels
[0] );
396 Node ilem
= s
.eqNode( empSet
);
397 Trace("sep-lemma-debug") << "Sep::Lemma : wand reduction, disjoint : " << ilem
<< std::endl
;
398 c_lems
.push_back( ilem
);
399 //nil does not occur in labels[0]
400 Node nr
= getNilRef( tn
);
401 Node nrlem
= NodeManager::currentNM()->mkNode( kind::MEMBER
, nr
, labels
[0] ).negate();
402 Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem
<< std::endl
;
403 d_out
->lemma( nrlem
);
405 //send out definitional lemmas for introduced sets
406 for( unsigned j
=0; j
<c_lems
.size(); j
++ ){
407 Trace("sep-lemma") << "Sep::Lemma : definition : " << c_lems
[j
] << std::endl
;
408 d_out
->lemma( c_lems
[j
] );
410 //children.insert( children.end(), c_lems.begin(), c_lems.end() );
411 conc
= NodeManager::currentNM()->mkNode( kind::AND
, children
);
412 }else if( s_atom
.getKind()==kind::SEP_PTO
){
413 Node ss
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, s_atom
[0] );
415 conc
= s_lbl
.eqNode( ss
);
417 //not needed anymore: semantics of sep.nil is enforced globally
418 //Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate();
419 //conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
421 }else if( s_atom
.getKind()==kind::SEP_EMP
){
422 //conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
424 Node emp_s
= NodeManager::currentNM()->mkConst(EmptySet(s_lbl
.getType().toType()));
426 lem
= NodeManager::currentNM()->mkNode( kind::OR
, fact
.negate(), s_lbl
.eqNode( emp_s
) );
428 Node kl
= NodeManager::currentNM()->mkSkolem( "loc", getReferenceType( s_atom
) );
429 Node kd
= NodeManager::currentNM()->mkSkolem( "data", getDataType( s_atom
) );
430 Node econc
= NodeManager::currentNM()->mkNode( kind::SEP_LABEL
,
431 NodeManager::currentNM()->mkNode( kind::SEP_STAR
, NodeManager::currentNM()->mkNode( kind::SEP_PTO
, kl
, kd
), d_true
), s_lbl
);
432 //Node econc = NodeManager::currentNM()->mkNode( kind::AND, s_lbl.eqNode( emp_s ).negate(),
433 lem
= NodeManager::currentNM()->mkNode( kind::OR
, fact
.negate(), econc
);
435 Trace("sep-lemma") << "Sep::Lemma : emp : " << lem
<< std::endl
;
439 //labeled emp should be rewritten
442 d_red_conc
[s_lbl
][s_atom
] = conc
;
446 if( !conc
.isNull() ){
447 bool use_polarity
= s_atom
.getKind()==kind::SEP_WAND
? !polarity
: polarity
;
449 // introduce guard, assert positive version
450 Trace("sep-lemma-debug") << "Negated spatial constraint asserted to sep theory: " << fact
<< std::endl
;
451 Node lit
= Rewriter::rewrite( NodeManager::currentNM()->mkSkolem( "G", NodeManager::currentNM()->booleanType() ) );
452 lit
= getValuation().ensureLiteral( lit
);
453 d_neg_guard
[s_lbl
][s_atom
] = lit
;
454 Trace("sep-lemma-debug") << "Neg guard : " << s_lbl
<< " " << s_atom
<< " " << lit
<< std::endl
;
455 AlwaysAssert( !lit
.isNull() );
456 d_out
->requirePhase( lit
, true );
457 d_neg_guards
.push_back( lit
);
458 d_guard_to_assertion
[lit
] = s_atom
;
459 //Node lem = NodeManager::currentNM()->mkNode( kind::EQUAL, lit, conc );
460 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lit
.negate(), conc
);
461 Trace("sep-lemma") << "Sep::Lemma : (neg) reduction : " << lem
<< std::endl
;
464 //reduce based on implication
465 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, fact
.negate(), conc
);
466 Trace("sep-lemma") << "Sep::Lemma : reduction : " << lem
<< std::endl
;
470 Trace("sep-lemma-debug") << "Trivial conclusion, do not add lemma." << std::endl
;
474 //assert to equality engine
476 Trace("sep-assert") << "Asserting " << atom
<< ", pol = " << polarity
<< " to EE..." << std::endl
;
477 if( s_atom
.getKind()==kind::EQUAL
){
478 d_equalityEngine
.assertEquality(atom
, polarity
, fact
);
480 d_equalityEngine
.assertPredicate(atom
, polarity
, fact
);
482 Trace("sep-assert") << "Done asserting " << atom
<< " to EE." << std::endl
;
483 }else if( s_atom
.getKind()==kind::SEP_PTO
){
484 Node pto_lbl
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, s_atom
[0] );
485 Assert( s_lbl
==pto_lbl
);
486 Trace("sep-assert") << "Asserting " << s_atom
<< std::endl
;
487 d_equalityEngine
.assertPredicate(s_atom
, polarity
, fact
);
488 //associate the equivalence class of the lhs with this pto
489 Node r
= getRepresentative( s_lbl
);
490 HeapAssertInfo
* ei
= getOrMakeEqcInfo( r
, true );
491 addPto( ei
, r
, atom
, polarity
);
495 //add to spatial assertions
496 if( !d_conflict
&& is_spatial
){
497 d_spatial_assertions
.push_back( fact
);
502 if( e
== EFFORT_LAST_CALL
&& !d_conflict
&& !d_valuation
.needCheck() ){
503 Trace("sep-process") << "Checking heap at full effort..." << std::endl
;
504 d_label_model
.clear();
507 Trace("sep-process") << "---Locations---" << std::endl
;
508 std::map
< Node
, int > min_id
;
509 for( std::map
< TypeNode
, std::vector
< Node
> >::iterator itt
= d_type_references_all
.begin(); itt
!= d_type_references_all
.end(); ++itt
){
510 for( unsigned k
=0; k
<itt
->second
.size(); k
++ ){
511 Node t
= itt
->second
[k
];
512 Trace("sep-process") << " " << t
<< " = ";
513 if( d_valuation
.getModel()->hasTerm( t
) ){
514 Node v
= d_valuation
.getModel()->getRepresentative( t
);
515 Trace("sep-process") << v
<< std::endl
;
517 std::map
< Node
, unsigned >::iterator itrc
= d_type_ref_card_id
.find( t
);
518 int tid
= itrc
==d_type_ref_card_id
.end() ? -1 : (int)itrc
->second
;
520 if( d_tmodel
.find( v
)==d_tmodel
.end() ){
521 set_term_model
= true;
523 set_term_model
= min_id
[v
]>tid
;
525 if( set_term_model
){
530 Trace("sep-process") << "?" << std::endl
;
534 Trace("sep-process") << "---" << std::endl
;
535 //build positive/negative assertion lists for labels
536 std::map
< Node
, bool > assert_active
;
537 //get the inactive assertions
538 std::map
< Node
, std::vector
< Node
> > lbl_to_assertions
;
539 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
541 bool polarity
= fact
.getKind() != kind::NOT
;
542 TNode atom
= polarity
? fact
: fact
[0];
543 Assert( atom
.getKind()==kind::SEP_LABEL
);
544 TNode s_atom
= atom
[0];
545 TNode s_lbl
= atom
[1];
546 lbl_to_assertions
[s_lbl
].push_back( fact
);
547 //check whether assertion is active : either polarity=true, or guard is not asserted false
548 assert_active
[fact
] = true;
549 bool use_polarity
= s_atom
.getKind()==kind::SEP_WAND
? !polarity
: polarity
;
551 if( s_atom
.getKind()==kind::SEP_PTO
){
552 Node vv
= d_valuation
.getModel()->getRepresentative( s_atom
[0] );
553 if( d_pto_model
.find( vv
)==d_pto_model
.end() ){
554 Trace("sep-process") << "Pto : " << s_atom
[0] << " (" << vv
<< ") -> " << s_atom
[1] << std::endl
;
555 d_pto_model
[vv
] = s_atom
[1];
557 //replace this on pto-model since this term is more relevant
558 TypeNode vtn
= vv
.getType();
559 if( std::find( d_type_references_all
[vtn
].begin(), d_type_references_all
[vtn
].end(), s_atom
[0] )!=d_type_references_all
[vtn
].end() ){
560 d_tmodel
[vv
] = s_atom
[0];
565 if( d_neg_guard
[s_lbl
].find( s_atom
)!=d_neg_guard
[s_lbl
].end() ){
566 //check if the guard is asserted positively
567 Node guard
= d_neg_guard
[s_lbl
][s_atom
];
569 if( getValuation().hasSatValue( guard
, value
) ) {
570 assert_active
[fact
] = value
;
575 //(recursively) set inactive sub-assertions
576 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
578 if( !assert_active
[fact
] ){
579 setInactiveAssertionRec( fact
, lbl_to_assertions
, assert_active
);
582 //set up model information based on active assertions
583 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
585 bool polarity
= fact
.getKind() != kind::NOT
;
586 TNode atom
= polarity
? fact
: fact
[0];
587 TNode s_atom
= atom
[0];
588 TNode s_lbl
= atom
[1];
589 if( assert_active
[fact
] ){
590 computeLabelModel( s_lbl
);
594 if( Trace
.isOn("sep-process") ){
595 Trace("sep-process") << "--- Current spatial assertions : " << std::endl
;
596 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
598 Trace("sep-process") << " " << fact
;
599 if( !assert_active
[fact
] ){
600 Trace("sep-process") << " [inactive]";
602 Trace("sep-process") << std::endl
;
604 Trace("sep-process") << "---" << std::endl
;
606 if(Trace
.isOn("sep-eqc")) {
607 eq::EqClassesIterator eqcs2_i
= eq::EqClassesIterator( &d_equalityEngine
);
608 Trace("sep-eqc") << "EQC:" << std::endl
;
609 while( !eqcs2_i
.isFinished() ){
610 Node eqc
= (*eqcs2_i
);
611 eq::EqClassIterator eqc2_i
= eq::EqClassIterator( eqc
, &d_equalityEngine
);
612 Trace("sep-eqc") << "Eqc( " << eqc
<< " ) : { ";
613 while( !eqc2_i
.isFinished() ) {
614 if( (*eqc2_i
)!=eqc
){
615 Trace("sep-eqc") << (*eqc2_i
) << " ";
619 Trace("sep-eqc") << " } " << std::endl
;
622 Trace("sep-eqc") << std::endl
;
625 bool addedLemma
= false;
626 bool needAddLemma
= false;
627 //check negated star / positive wand
628 if( options::sepCheckNeg() ){
630 std::map
< Node
, bool > active_lbl
;
631 if( options::sepMinimalRefine() ){
632 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
634 bool polarity
= fact
.getKind() != kind::NOT
;
635 TNode atom
= polarity
? fact
: fact
[0];
636 TNode s_atom
= atom
[0];
637 bool use_polarity
= s_atom
.getKind()==kind::SEP_WAND
? !polarity
: polarity
;
639 Assert( assert_active
.find( fact
)!=assert_active
.end() );
640 if( assert_active
[fact
] ){
641 Assert( atom
.getKind()==kind::SEP_LABEL
);
642 TNode s_lbl
= atom
[1];
643 if( d_label_map
[s_atom
].find( s_lbl
)!=d_label_map
[s_atom
].end() ){
644 Trace("sep-process-debug") << "Active lbl : " << s_lbl
<< std::endl
;
645 active_lbl
[s_lbl
] = true;
652 //process spatial assertions
653 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
655 bool polarity
= fact
.getKind() != kind::NOT
;
656 TNode atom
= polarity
? fact
: fact
[0];
657 TNode s_atom
= atom
[0];
659 bool use_polarity
= s_atom
.getKind()==kind::SEP_WAND
? !polarity
: polarity
;
660 Trace("sep-process-debug") << " check atom : " << s_atom
<< " use polarity " << use_polarity
<< std::endl
;
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 Trace("sep-process") << "--> Active negated atom : " << s_atom
<< ", lbl = " << s_lbl
<< std::endl
;
667 //add refinement lemma
668 if( d_label_map
[s_atom
].find( s_lbl
)!=d_label_map
[s_atom
].end() ){
670 TypeNode tn
= getReferenceType( s_atom
);
671 tn
= NodeManager::currentNM()->mkSetType(tn
);
672 //tn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
673 Node o_b_lbl_mval
= d_label_model
[s_lbl
].getValue( tn
);
674 Trace("sep-process") << " Model for " << s_lbl
<< " : " << o_b_lbl_mval
<< std::endl
;
677 std::map
< int, Node
> mvals
;
678 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
){
679 Node sub_lbl
= itl
->second
;
680 int sub_index
= itl
->first
;
681 computeLabelModel( sub_lbl
);
682 Node lbl_mval
= d_label_model
[sub_lbl
].getValue( tn
);
683 Trace("sep-process-debug") << " child " << sub_index
<< " : " << sub_lbl
<< ", mval = " << lbl_mval
<< std::endl
;
684 mvals
[sub_index
] = lbl_mval
;
687 // Now, assert model-instantiated implication based on the negation
688 Assert( d_label_model
.find( s_lbl
)!=d_label_model
.end() );
689 std::vector
< Node
> conc
;
690 bool inst_success
= true;
692 //instantiate the label
693 std::map
< Node
, Node
> visited
;
694 Node inst
= instantiateLabel( s_atom
, s_lbl
, s_lbl
, o_b_lbl_mval
, visited
, d_pto_model
, tn
, active_lbl
);
695 Trace("sep-inst-debug") << " applied inst : " << inst
<< std::endl
;
697 inst_success
= false;
699 inst
= Rewriter::rewrite( inst
);
700 if( inst
==( polarity
? d_true
: d_false
) ){
701 inst_success
= false;
703 conc
.push_back( polarity
? inst
: inst
.negate() );
706 std::vector
< Node
> lemc
;
707 Node pol_atom
= atom
;
709 pol_atom
= atom
.negate();
711 lemc
.push_back( pol_atom
);
713 //lemc.push_back( s_lbl.eqNode( o_b_lbl_mval ).negate() );
714 //lemc.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, o_b_lbl_mval, s_lbl ).negate() );
715 lemc
.insert( lemc
.end(), conc
.begin(), conc
.end() );
716 Node lem
= NodeManager::currentNM()->mkNode( kind::OR
, lemc
);
717 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() ){
718 d_refinement_lem
[s_atom
][s_lbl
].push_back( lem
);
719 Trace("sep-process") << "-----> refinement lemma (#" << d_refinement_lem
[s_atom
][s_lbl
].size() << ") : " << lem
<< std::endl
;
720 Trace("sep-lemma") << "Sep::Lemma : negated star/wand refinement : " << lem
<< std::endl
;
724 //this typically should not happen, should never happen for complete base theories
725 Trace("sep-process") << "*** repeated refinement lemma : " << lem
<< std::endl
;
726 Trace("sep-warn") << "TheorySep : WARNING : repeated refinement lemma : " << lem
<< "!!!" << std::endl
;
730 Trace("sep-process-debug") << " no children." << std::endl
;
731 Assert( s_atom
.getKind()==kind::SEP_PTO
|| s_atom
.getKind()==kind::SEP_EMP
);
734 Trace("sep-process-debug") << "--> inactive negated assertion " << s_atom
<< std::endl
;
738 Trace("sep-process") << "...finished check of negated assertions, addedLemma=" << addedLemma
<< ", needAddLemma=" << needAddLemma
<< std::endl
;
741 //must witness finite data points-to
742 for( std::map
< TypeNode
, Node
>::iterator it
= d_base_label
.begin(); it
!= d_base_label
.end(); ++it
){
743 TypeNode data_type
= d_loc_to_data_type
[it
->first
];
744 //if the data type is finite
745 if( data_type
.isInterpretedFinite() ){
746 computeLabelModel( it
->second
);
747 Trace("sep-process-debug") << "Check heap data for " << it
->first
<< " -> " << data_type
<< std::endl
;
748 for( unsigned j
=0; j
<d_label_model
[it
->second
].d_heap_locs_model
.size(); j
++ ){
749 Assert( d_label_model
[it
->second
].d_heap_locs_model
[j
].getKind()==kind::SINGLETON
);
750 Node l
= d_label_model
[it
->second
].d_heap_locs_model
[j
][0];
751 Trace("sep-process-debug") << " location : " << l
<< std::endl
;
752 if( d_pto_model
[l
].isNull() ){
755 std::map
< Node
, Node
>::iterator itm
= d_tmodel
.find( l
);
756 if( itm
!=d_tmodel
.end() ) {
759 //try to assign arbitrary skolem?
762 Trace("sep-process") << "Must witness label : " << ll
<< ", data type is " << data_type
<< std::endl
;
763 Node dsk
= NodeManager::currentNM()->mkSkolem( "dsk", data_type
, "pto-data for implicit location" );
764 // if location is in the heap, then something must point to it
765 Node lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, NodeManager::currentNM()->mkNode( kind::MEMBER
, ll
, it
->second
),
766 NodeManager::currentNM()->mkNode( kind::SEP_STAR
,
767 NodeManager::currentNM()->mkNode( kind::SEP_PTO
, ll
, dsk
),
769 Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem
<< std::endl
;
773 //This should only happen if we are in an unbounded fragment
774 Trace("sep-warn") << "TheorySep : WARNING : no term corresponding to location " << l
<< " in heap!!!" << std::endl
;
777 Trace("sep-process-debug") << " points-to data witness : " << d_pto_model
[l
] << std::endl
;
784 Trace("sep-process-debug") << "...preparing sep model..." << std::endl
;
785 d_heap_locs_nptos
.clear();
786 //collect data points that are not pointed to
787 for( context::CDList
<Assertion
>::const_iterator it
= facts_begin(); it
!= facts_end(); ++ it
) {
788 Node lit
= (*it
).assertion
;
789 if( lit
.getKind()==kind::NOT
&& lit
[0].getKind()==kind::SEP_PTO
){
790 Node s_atom
= lit
[0];
791 Node v1
= d_valuation
.getModel()->getRepresentative( s_atom
[0] );
792 Node v2
= d_valuation
.getModel()->getRepresentative( s_atom
[1] );
793 Trace("sep-process-debug") << v1
<< " does not point-to " << v2
<< std::endl
;
794 d_heap_locs_nptos
[v1
].push_back( v2
);
799 d_out
->setIncomplete();
804 Trace("sep-check") << "Sep::check(): " << e
<< " done, conflict=" << d_conflict
.get() << endl
;
808 bool TheorySep::needsCheckLastEffort() {
812 Node
TheorySep::getNextDecisionRequest( unsigned& priority
) {
813 for( unsigned i
=0; i
<d_neg_guards
.size(); i
++ ){
814 Node g
= d_neg_guards
[i
];
816 if( getLogicInfo().isQuantified() ){
817 Assert( d_guard_to_assertion
.find( g
)!= d_guard_to_assertion
.end() );
818 Node a
= d_guard_to_assertion
[g
];
819 Node q
= quantifiers::TermDb::getInstConstAttr( a
);
821 //must wait to decide on counterexample literal from quantified formula
822 Node cel
= getQuantifiersEngine()->getTermDatabase()->getCounterexampleLiteral( q
);
824 if( d_valuation
.hasSatValue( cel
, value
) ){
825 Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : dependent guard " << g
<< " depends on value for guard for quantified formula : " << value
<< std::endl
;
828 Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : wait to decide on " << g
<< " until " << cel
<< " is set " << std::endl
;
835 if( !d_valuation
.hasSatValue( g
, value
) ) {
836 Trace("sep-dec") << "TheorySep::getNextDecisionRequest : " << g
<< " (" << i
<< "/" << d_neg_guards
.size() << ")" << std::endl
;
842 Trace("sep-dec-debug") << "TheorySep::getNextDecisionRequest : null" << std::endl
;
846 void TheorySep::conflict(TNode a
, TNode b
) {
847 Trace("sep-conflict") << "Sep::conflict : " << a
<< " " << b
<< std::endl
;
848 Node conflictNode
= explain(a
.eqNode(b
));
850 d_out
->conflict( conflictNode
);
854 TheorySep::HeapAssertInfo::HeapAssertInfo( context::Context
* c
) : d_pto(c
), d_has_neg_pto(c
,false) {
858 TheorySep::HeapAssertInfo
* TheorySep::getOrMakeEqcInfo( Node n
, bool doMake
) {
859 std::map
< Node
, HeapAssertInfo
* >::iterator e_i
= d_eqc_info
.find( n
);
860 if( e_i
==d_eqc_info
.end() ){
862 HeapAssertInfo
* ei
= new HeapAssertInfo( getSatContext() );
869 return (*e_i
).second
;
873 //for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2)
874 TypeNode
TheorySep::getReferenceType( Node n
) {
875 Assert( !d_type_ref
.isNull() );
879 TypeNode
TheorySep::getDataType( Node n
) {
880 Assert( !d_type_data
.isNull() );
884 // Must process assertions at preprocess so that quantified assertions are
885 // processed properly.
886 void TheorySep::ppNotifyAssertions(const std::vector
<Node
>& assertions
) {
887 std::map
<int, std::map
<Node
, int> > visited
;
888 std::map
<int, std::map
<Node
, std::vector
<Node
> > > references
;
889 std::map
<int, std::map
<Node
, bool> > references_strict
;
890 for (unsigned i
= 0; i
< assertions
.size(); i
++) {
891 Trace("sep-pp") << "Process assertion : " << assertions
[i
] << std::endl
;
892 processAssertion(assertions
[i
], visited
, references
, references_strict
,
895 // if data type is unconstrained, assume a fresh uninterpreted sort
896 if (!d_type_ref
.isNull()) {
897 if (d_type_data
.isNull()) {
898 d_type_data
= NodeManager::currentNM()->mkSort("_sep_U");
899 Trace("sep-type") << "Sep: assume data type " << d_type_data
<< std::endl
;
900 d_loc_to_data_type
[d_type_ref
] = d_type_data
;
906 int TheorySep::processAssertion( Node n
, std::map
< int, std::map
< Node
, int > >& visited
,
907 std::map
< int, std::map
< Node
, std::vector
< Node
> > >& references
, std::map
< int, std::map
< Node
, bool > >& references_strict
,
908 bool pol
, bool hasPol
, bool underSpatial
) {
909 int index
= hasPol
? ( pol
? 1 : -1 ) : 0;
911 std::map
< Node
, int >::iterator it
= visited
[index
].find( n
);
912 if( it
==visited
[index
].end() ){
913 Trace("sep-pp-debug") << "process assertion : " << n
<< ", index = " << index
<< std::endl
;
914 if( n
.getKind()==kind::SEP_EMP
){
915 TypeNode tn
= n
[0].getType();
916 TypeNode tnd
= n
[1].getType();
917 registerRefDataTypes( tn
, tnd
, n
);
919 references
[index
][n
].clear();
920 references_strict
[index
][n
] = true;
924 }else if( n
.getKind()==kind::SEP_PTO
){
925 TypeNode tn1
= n
[0].getType();
926 TypeNode tn2
= n
[1].getType();
927 registerRefDataTypes( tn1
, tn2
, n
);
928 if( quantifiers::TermDb::hasBoundVarAttr( n
[0] ) ){
929 if( d_bound_kind
[tn1
]!=bound_strict
&& d_bound_kind
[tn1
]!=bound_invalid
){
930 if( options::quantEpr() && n
[0].getKind()==kind::BOUND_VARIABLE
){
931 // still valid : bound on heap models will include Herbrand universe of n[0].getType()
932 d_bound_kind
[tn1
] = bound_herbrand
;
934 d_bound_kind
[tn1
] = bound_invalid
;
935 Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl
;
939 references
[index
][n
].push_back( n
[0] );
942 references_strict
[index
][n
] = true;
947 bool isSpatial
= n
.getKind()==kind::SEP_WAND
|| n
.getKind()==kind::SEP_STAR
;
948 bool newUnderSpatial
= underSpatial
|| isSpatial
;
949 bool refStrict
= isSpatial
;
950 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
951 bool newHasPol
, newPol
;
952 QuantPhaseReq::getEntailPolarity( n
, i
, hasPol
, pol
, newHasPol
, newPol
);
953 int newIndex
= newHasPol
? ( newPol
? 1 : -1 ) : 0;
954 int ccard
= processAssertion( n
[i
], visited
, references
, references_strict
, newPol
, newHasPol
, newUnderSpatial
);
956 if( n
.getKind()==kind::SEP_STAR
){
958 }else if( n
.getKind()==kind::SEP_WAND
){
962 }else if( ccard
>card
){
965 //track references if we are or below a spatial operator
966 if( newUnderSpatial
){
968 if( references_strict
[newIndex
].find( n
[i
] )!=references_strict
[newIndex
].end() ){
970 if( references_strict
[index
].find( n
)==references_strict
[index
].end() ){
971 references_strict
[index
][n
] = true;
974 //TODO: can derive static equality between sets
983 for( unsigned j
=0; j
<references
[newIndex
][n
[i
]].size(); j
++ ){
984 if( std::find( references
[index
][n
].begin(), references
[index
][n
].end(), references
[newIndex
][n
[i
]][j
] )==references
[index
][n
].end() ){
985 references
[index
][n
].push_back( references
[newIndex
][n
[i
]][j
] );
991 if( isSpatial
&& refStrict
){
992 if( n
.getKind()==kind::SEP_WAND
){
995 Assert( n
.getKind()==kind::SEP_STAR
&& hasPol
&& pol
);
996 references_strict
[index
][n
] = true;
1000 visited
[index
][n
] = card
;
1005 if( !underSpatial
&& ( !references
[index
][n
].empty() || card
>0 ) ){
1006 TypeNode tn
= getReferenceType( n
);
1007 Assert( !tn
.isNull() );
1008 // add references to overall type
1009 unsigned bt
= d_bound_kind
[tn
];
1011 if( references_strict
[index
].find( n
)!=references_strict
[index
].end() ){
1012 Trace("sep-bound") << "Strict bound found based on " << n
<< ", index = " << index
<< std::endl
;
1013 if( bt
!=bound_strict
){
1014 d_bound_kind
[tn
] = bound_strict
;
1015 //d_type_references[tn].clear();
1016 d_card_max
[tn
] = card
;
1018 //TODO: derive static equality
1022 add
= bt
!=bound_strict
;
1024 for( unsigned i
=0; i
<references
[index
][n
].size(); i
++ ){
1025 if( std::find( d_type_references
[tn
].begin(), d_type_references
[tn
].end(), references
[index
][n
][i
] )==d_type_references
[tn
].end() ){
1026 d_type_references
[tn
].push_back( references
[index
][n
][i
] );
1030 //add max cardinality
1031 if( card
>(int)d_card_max
[tn
] ){
1032 d_card_max
[tn
] = card
;
1039 void TheorySep::registerRefDataTypes( TypeNode tn1
, TypeNode tn2
, Node atom
){
1040 //separation logic is effectively enabled when we find at least one spatial constraint occurs in the input
1041 if( options::incrementalSolving() ){
1042 std::stringstream ss
;
1043 ss
<< "ERROR: cannot use separation logic in incremental mode." << std::endl
;
1044 throw LogicException(ss
.str());
1046 std::map
< TypeNode
, TypeNode
>::iterator itt
= d_loc_to_data_type
.find( tn1
);
1047 if( itt
==d_loc_to_data_type
.end() ){
1048 if( !d_loc_to_data_type
.empty() ){
1049 TypeNode te1
= d_loc_to_data_type
.begin()->first
;
1050 std::stringstream ss
;
1051 ss
<< "ERROR: specifying heap constraints for two different types : " << tn1
<< " -> " << tn2
<< " and " << te1
<< " -> " << d_loc_to_data_type
[te1
] << std::endl
;
1052 throw LogicException(ss
.str());
1056 Trace("sep-type") << "Sep: assume location type " << tn1
<< " (from " << atom
<< ")" << std::endl
;
1058 Trace("sep-type") << "Sep: assume location type " << tn1
<< " is associated with data type " << tn2
<< " (from " << atom
<< ")" << std::endl
;
1060 d_loc_to_data_type
[tn1
] = tn2
;
1061 //for now, we only allow heap constraints of one type
1064 d_bound_kind
[tn1
] = bound_default
;
1066 if( !tn2
.isNull() ){
1067 if( itt
->second
!=tn2
){
1068 if( itt
->second
.isNull() ){
1069 Trace("sep-type") << "Sep: assume location type " << tn1
<< " is associated with data type " << tn2
<< " (from " << atom
<< ")" << std::endl
;
1070 //now we know data type
1071 d_loc_to_data_type
[tn1
] = tn2
;
1074 std::stringstream ss
;
1075 ss
<< "ERROR: location type " << tn1
<< " is already associated with data type " << itt
->second
<< ", offending atom is " << atom
<< " with data type " << tn2
<< std::endl
;
1076 throw LogicException(ss
.str());
1084 void TheorySep::initializeBounds() {
1085 if( !d_bounds_init
){
1086 Trace("sep-bound") << "Initialize sep bounds..." << std::endl
;
1087 d_bounds_init
= true;
1088 for( std::map
< TypeNode
, TypeNode
>::iterator it
= d_loc_to_data_type
.begin(); it
!= d_loc_to_data_type
.end(); ++it
){
1089 TypeNode tn
= it
->first
;
1090 Trace("sep-bound") << "Initialize bounds for " << tn
<< "..." << std::endl
;
1091 QuantEPR
* qepr
= getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL
;
1092 //if pto had free variable reference
1093 if( d_bound_kind
[tn
]==bound_herbrand
){
1094 //include Herbrand universe of tn
1095 if( qepr
&& qepr
->isEPR( tn
) ){
1096 for( unsigned j
=0; j
<qepr
->d_consts
[tn
].size(); j
++ ){
1097 Node k
= qepr
->d_consts
[tn
][j
];
1098 if( std::find( d_type_references
[tn
].begin(), d_type_references
[tn
].end(), k
)==d_type_references
[tn
].end() ){
1099 d_type_references
[tn
].push_back( k
);
1103 d_bound_kind
[tn
] = bound_invalid
;
1104 Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl
;
1108 if( d_bound_kind
[tn
] != bound_invalid
){
1109 n_emp
= d_card_max
[tn
];
1110 }else if( d_type_references
[tn
].empty() ){
1111 //must include at least one constant TODO: remove?
1114 Trace("sep-bound") << "Cardinality element size : " << d_card_max
[tn
] << std::endl
;
1115 Trace("sep-bound") << "Type reference size : " << d_type_references
[tn
].size() << std::endl
;
1116 Trace("sep-bound") << "Constructing " << n_emp
<< " cardinality constants." << std::endl
;
1117 for( unsigned r
=0; r
<n_emp
; r
++ ){
1118 Node e
= NodeManager::currentNM()->mkSkolem( "e", tn
, "cardinality bound element for seplog" );
1119 d_type_references_card
[tn
].push_back( e
);
1120 d_type_ref_card_id
[e
] = r
;
1121 //must include this constant back into EPR handling
1122 if( qepr
&& qepr
->isEPR( tn
) ){
1123 qepr
->addEPRConstant( tn
, e
);
1126 //EPR must include nil ref
1127 if( qepr
&& qepr
->isEPR( tn
) ){
1128 Node nr
= getNilRef( tn
);
1129 if( !qepr
->isEPRConstant( tn
, nr
) ){
1130 qepr
->addEPRConstant( tn
, nr
);
1137 Node
TheorySep::getBaseLabel( TypeNode tn
) {
1138 std::map
< TypeNode
, Node
>::iterator it
= d_base_label
.find( tn
);
1139 if( it
==d_base_label
.end() ){
1141 Trace("sep") << "Make base label for " << tn
<< std::endl
;
1142 std::stringstream ss
;
1144 TypeNode ltn
= NodeManager::currentNM()->mkSetType(tn
);
1145 //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(tn));
1146 Node n_lbl
= NodeManager::currentNM()->mkSkolem( ss
.str(), ltn
, "base label" );
1147 d_base_label
[tn
] = n_lbl
;
1148 //make reference bound
1149 Trace("sep") << "Make reference bound label for " << tn
<< std::endl
;
1150 std::stringstream ss2
;
1152 d_reference_bound
[tn
] = NodeManager::currentNM()->mkSkolem( ss2
.str(), ltn
, "" );
1153 d_type_references_all
[tn
].insert( d_type_references_all
[tn
].end(), d_type_references
[tn
].begin(), d_type_references
[tn
].end() );
1155 //check whether monotonic (elements can be added to tn without effecting satisfiability)
1156 bool tn_is_monotonic
= true;
1158 //TODO: use monotonicity inference
1159 tn_is_monotonic
= !getLogicInfo().isQuantified();
1161 tn_is_monotonic
= tn
.getCardinality().isInfinite();
1163 //add a reference type for maximum occurrences of empty in a constraint
1164 if( options::sepDisequalC() && tn_is_monotonic
){
1165 for( unsigned r
=0; r
<d_type_references_card
[tn
].size(); r
++ ){
1166 Node e
= d_type_references_card
[tn
][r
];
1167 //ensure that it is distinct from all other references so far
1168 for( unsigned j
=0; j
<d_type_references_all
[tn
].size(); j
++ ){
1169 Node eq
= NodeManager::currentNM()->mkNode( kind::EQUAL
, e
, d_type_references_all
[tn
][j
] );
1170 d_out
->lemma( eq
.negate() );
1172 d_type_references_all
[tn
].push_back( e
);
1175 //break symmetries TODO
1177 d_type_references_all
[tn
].insert( d_type_references_all
[tn
].end(), d_type_references_card
[tn
].begin(), d_type_references_card
[tn
].end() );
1179 //Assert( !d_type_references_all[tn].empty() );
1181 if( d_bound_kind
[tn
]!=bound_invalid
){
1183 d_reference_bound_max
[tn
] = mkUnion( tn
, d_type_references_all
[tn
] );
1184 Trace("sep-bound") << "overall bound for " << d_base_label
[tn
] << " : " << d_reference_bound_max
[tn
] << std::endl
;
1186 Node slem
= NodeManager::currentNM()->mkNode( kind::SUBSET
, d_base_label
[tn
], d_reference_bound_max
[tn
] );
1187 Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn
<< " : " << slem
<< std::endl
;
1188 d_out
->lemma( slem
);
1189 //slem = NodeManager::currentNM()->mkNode( kind::SUBSET, d_base_label[tn], d_reference_bound_max[tn] );
1190 //Trace("sep-lemma") << "Sep::Lemma: base reference bound for " << tn << " : " << slem << std::endl;
1191 //d_out->lemma( slem );
1194 if( d_type_references_card
[tn
].size()>1 ){
1195 std::map
< unsigned, Node
> lit_mem_map
;
1196 for( unsigned i
=0; i
<d_type_references_card
[tn
].size(); i
++ ){
1197 lit_mem_map
[i
] = NodeManager::currentNM()->mkNode( kind::MEMBER
, d_type_references_card
[tn
][i
], d_reference_bound_max
[tn
]);
1199 for( unsigned i
=0; i
<(d_type_references_card
[tn
].size()-1); i
++ ){
1200 std::vector
< Node
> children
;
1201 for( unsigned j
=(i
+1); j
<d_type_references_card
[tn
].size(); j
++ ){
1202 children
.push_back( lit_mem_map
[j
].negate() );
1204 if( !children
.empty() ){
1205 Node sym_lem
= children
.size()==1 ? children
[0] : NodeManager::currentNM()->mkNode( kind::AND
, children
);
1206 sym_lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, lit_mem_map
[i
].negate(), sym_lem
);
1207 Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem
<< std::endl
;
1208 d_out
->lemma( sym_lem
);
1214 //assert that nil ref is not in base label
1215 Node nr
= getNilRef( tn
);
1216 Node nrlem
= NodeManager::currentNM()->mkNode( kind::MEMBER
, nr
, n_lbl
).negate();
1217 Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn
<< " : " << nrlem
<< std::endl
;
1218 d_out
->lemma( nrlem
);
1226 Node
TheorySep::getNilRef( TypeNode tn
) {
1227 std::map
< TypeNode
, Node
>::iterator it
= d_nil_ref
.find( tn
);
1228 if( it
==d_nil_ref
.end() ){
1229 Node nil
= NodeManager::currentNM()->mkNullaryOperator( tn
, kind::SEP_NIL
);
1230 setNilRef( tn
, nil
);
1237 void TheorySep::setNilRef( TypeNode tn
, Node n
) {
1238 Assert( n
.getType()==tn
);
1242 Node
TheorySep::mkUnion( TypeNode tn
, std::vector
< Node
>& locs
) {
1245 TypeNode ltn
= NodeManager::currentNM()->mkSetType(tn
);
1246 return NodeManager::currentNM()->mkConst(EmptySet(ltn
.toType()));
1248 for( unsigned i
=0; i
<locs
.size(); i
++ ){
1250 Assert( !s
.isNull() );
1251 s
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, s
);
1255 u
= NodeManager::currentNM()->mkNode( kind::UNION
, s
, u
);
1262 Node
TheorySep::getLabel( Node atom
, int child
, Node lbl
) {
1263 std::map
< int, Node
>::iterator it
= d_label_map
[atom
][lbl
].find( child
);
1264 if( it
==d_label_map
[atom
][lbl
].end() ){
1265 TypeNode refType
= getReferenceType( atom
);
1266 std::stringstream ss
;
1267 ss
<< "__Lc" << child
;
1268 TypeNode ltn
= NodeManager::currentNM()->mkSetType(refType
);
1269 //TypeNode ltn = NodeManager::currentNM()->mkSetType(NodeManager::currentNM()->mkRefType(refType));
1270 Node n_lbl
= NodeManager::currentNM()->mkSkolem( ss
.str(), ltn
, "sep label" );
1271 d_label_map
[atom
][lbl
][child
] = n_lbl
;
1272 d_label_map_parent
[n_lbl
] = lbl
;
1275 return (*it
).second
;
1279 Node
TheorySep::applyLabel( Node n
, Node lbl
, std::map
< Node
, Node
>& visited
) {
1280 Assert( n
.getKind()!=kind::SEP_LABEL
);
1281 if( n
.getKind()==kind::SEP_STAR
|| n
.getKind()==kind::SEP_WAND
|| n
.getKind()==kind::SEP_PTO
|| n
.getKind()==kind::SEP_EMP
){
1282 return NodeManager::currentNM()->mkNode( kind::SEP_LABEL
, n
, lbl
);
1283 }else if( !n
.getType().isBoolean() || n
.getNumChildren()==0 ){
1286 std::map
< Node
, Node
>::iterator it
= visited
.find( n
);
1287 if( it
==visited
.end() ){
1288 std::vector
< Node
> children
;
1289 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1290 children
.push_back( n
.getOperator() );
1292 bool childChanged
= false;
1293 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1294 Node aln
= applyLabel( n
[i
], lbl
, visited
);
1295 children
.push_back( aln
);
1296 childChanged
= childChanged
|| aln
!=n
[i
];
1300 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1310 Node
TheorySep::instantiateLabel( Node n
, Node o_lbl
, Node lbl
, Node lbl_v
, std::map
< Node
, Node
>& visited
, std::map
< Node
, Node
>& pto_model
,
1311 TypeNode rtn
, std::map
< Node
, bool >& active_lbl
, unsigned ind
) {
1312 Trace("sep-inst-debug") << "Instantiate label " << n
<< " " << lbl
<< " " << lbl_v
<< std::endl
;
1313 if( options::sepMinimalRefine() && lbl
!=o_lbl
&& active_lbl
.find( lbl
)!=active_lbl
.end() ){
1314 Trace("sep-inst") << "...do not instantiate " << o_lbl
<< " since it has an active sublabel " << lbl
<< std::endl
;
1315 return Node::null();
1317 if( Trace
.isOn("sep-inst") ){
1318 if( n
.getKind()==kind::SEP_STAR
|| n
.getKind()==kind::SEP_WAND
|| n
.getKind()==kind::SEP_PTO
|| n
.getKind()==kind::SEP_EMP
){
1319 for( unsigned j
=0; j
<ind
; j
++ ){ Trace("sep-inst") << " "; }
1320 Trace("sep-inst") << n
<< "[" << lbl
<< "] :: " << lbl_v
<< std::endl
;
1323 Assert( n
.getKind()!=kind::SEP_LABEL
);
1324 if( n
.getKind()==kind::SEP_STAR
|| n
.getKind()==kind::SEP_WAND
){
1326 std::vector
< Node
> children
;
1327 children
.resize( n
.getNumChildren() );
1328 Assert( d_label_map
[n
].find( lbl
)!=d_label_map
[n
].end() );
1329 std::map
< int, Node
> mvals
;
1330 for( std::map
< int, Node
>::iterator itl
= d_label_map
[n
][lbl
].begin(); itl
!= d_label_map
[n
][lbl
].end(); ++itl
){
1331 Node sub_lbl
= itl
->second
;
1332 int sub_index
= itl
->first
;
1333 Assert( sub_index
>=0 && sub_index
<(int)children
.size() );
1334 Trace("sep-inst-debug") << "Sublabel " << sub_index
<< " is " << sub_lbl
<< std::endl
;
1336 if( n
.getKind()==kind::SEP_WAND
&& sub_index
==1 ){
1337 Assert( d_label_map
[n
][lbl
].find( 0 )!=d_label_map
[n
][lbl
].end() );
1338 Node sub_lbl_0
= d_label_map
[n
][lbl
][0];
1339 computeLabelModel( sub_lbl_0
);
1340 Assert( d_label_model
.find( sub_lbl_0
)!=d_label_model
.end() );
1341 lbl_mval
= NodeManager::currentNM()->mkNode( kind::UNION
, lbl
, d_label_model
[sub_lbl_0
].getValue( rtn
) );
1343 computeLabelModel( sub_lbl
);
1344 Assert( d_label_model
.find( sub_lbl
)!=d_label_model
.end() );
1345 lbl_mval
= d_label_model
[sub_lbl
].getValue( rtn
);
1347 Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval
<< std::endl
;
1348 mvals
[sub_index
] = lbl_mval
;
1349 children
[sub_index
] = instantiateLabel( n
[sub_index
], o_lbl
, sub_lbl
, lbl_mval
, visited
, pto_model
, rtn
, active_lbl
, ind
+1 );
1350 if( children
[sub_index
].isNull() ){
1351 return Node::null();
1354 Node empSet
= NodeManager::currentNM()->mkConst(EmptySet(rtn
.toType()));
1355 if( n
.getKind()==kind::SEP_STAR
){
1357 //disjoint contraints
1358 std::vector
< Node
> conj
;
1359 std::vector
< Node
> bchildren
;
1360 bchildren
.insert( bchildren
.end(), children
.begin(), children
.end() );
1362 std::vector
< Node
> vs
;
1363 for( std::map
< int, Node
>::iterator itl
= d_label_map
[n
][lbl
].begin(); itl
!= d_label_map
[n
][lbl
].end(); ++itl
){
1364 Node sub_lbl
= itl
->second
;
1365 Node lbl_mval
= d_label_model
[sub_lbl
].getValue( rtn
);
1366 for( unsigned j
=0; j
<vs
.size(); j
++ ){
1367 bchildren
.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION
, lbl_mval
, vs
[j
] ).eqNode( empSet
) );
1369 vs
.push_back( lbl_mval
);
1373 vsu
= NodeManager::currentNM()->mkNode( kind::UNION
, vsu
, lbl_mval
);
1376 bchildren
.push_back( vsu
.eqNode( lbl
) );
1378 Assert( bchildren
.size()>1 );
1379 conj
.push_back( NodeManager::currentNM()->mkNode( kind::AND
, bchildren
) );
1381 if( options::sepChildRefine() ){
1382 //child-specific refinements (TODO: use ?)
1383 for( unsigned i
=0; i
<children
.size(); i
++ ){
1384 std::vector
< Node
> tchildren
;
1385 Node mval
= mvals
[i
];
1386 tchildren
.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET
, mval
, lbl
) );
1387 tchildren
.push_back( children
[i
] );
1388 std::vector
< Node
> rem_children
;
1389 for( unsigned j
=0; j
<children
.size(); j
++ ){
1391 rem_children
.push_back( n
[j
] );
1394 std::map
< Node
, Node
> rvisited
;
1395 Node rem
= rem_children
.size()==1 ? rem_children
[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR
, rem_children
);
1396 rem
= applyLabel( rem
, NodeManager::currentNM()->mkNode( kind::SETMINUS
, lbl
, mval
), rvisited
);
1397 tchildren
.push_back( rem
);
1398 conj
.push_back( NodeManager::currentNM()->mkNode( kind::AND
, tchildren
) );
1401 return conj
.size()==1 ? conj
[0] : NodeManager::currentNM()->mkNode( kind::OR
, conj
);
1403 std::vector
< Node
> wchildren
;
1404 //disjoint constraints
1405 Node sub_lbl_0
= d_label_map
[n
][lbl
][0];
1406 Node lbl_mval_0
= d_label_model
[sub_lbl_0
].getValue( rtn
);
1407 wchildren
.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION
, lbl_mval_0
, lbl
).eqNode( empSet
).negate() );
1410 wchildren
.push_back( children
[0].negate() );
1411 wchildren
.push_back( children
[1] );
1412 return NodeManager::currentNM()->mkNode( kind::OR
, wchildren
);
1415 //nested star/wand, label it and return
1416 return NodeManager::currentNM()->mkNode( kind::SEP_LABEL
, n
, lbl_v
);
1418 }else if( n
.getKind()==kind::SEP_PTO
){
1419 //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption
1420 Assert( d_label_model
.find( o_lbl
)!=d_label_model
.end() );
1421 Node vr
= d_valuation
.getModel()->getRepresentative( n
[0] );
1422 Node svr
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, vr
);
1423 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();
1424 Trace("sep-inst-debug") << "Is in base (non-instantiating) heap : " << inBaseHeap
<< " for value ref " << vr
<< " in " << o_lbl
<< std::endl
;
1425 std::vector
< Node
> children
;
1427 Node s
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, n
[0] );
1428 children
.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL
, NodeManager::currentNM()->mkNode( kind::SEP_PTO
, n
[0], n
[1] ), s
) );
1430 //look up value of data
1431 std::map
< Node
, Node
>::iterator it
= pto_model
.find( vr
);
1432 if( it
!=pto_model
.end() ){
1433 if( n
[1]!=it
->second
){
1434 children
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, n
[1], it
->second
) );
1437 Trace("sep-inst-debug") << "Data for " << vr
<< " was not specified, do not add condition." << std::endl
;
1440 children
.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL
, NodeManager::currentNM()->mkNode( kind::SINGLETON
, n
[0] ), lbl_v
) );
1441 Node ret
= children
.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children
.size()==1 ? children
[0] : NodeManager::currentNM()->mkNode( kind::AND
, children
) );
1442 Trace("sep-inst-debug") << "Return " << ret
<< std::endl
;
1444 }else if( n
.getKind()==kind::SEP_EMP
){
1445 //return NodeManager::currentNM()->mkConst( lbl_v.getKind()==kind::EMPTYSET );
1446 return lbl_v
.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v
.getType().toType())) );
1448 std::map
< Node
, Node
>::iterator it
= visited
.find( n
);
1449 if( it
==visited
.end() ){
1450 std::vector
< Node
> children
;
1451 if (n
.getMetaKind() == kind::metakind::PARAMETERIZED
) {
1452 children
.push_back( n
.getOperator() );
1454 bool childChanged
= false;
1455 for( unsigned i
=0; i
<n
.getNumChildren(); i
++ ){
1456 Node aln
= instantiateLabel( n
[i
], o_lbl
, lbl
, lbl_v
, visited
, pto_model
, rtn
, active_lbl
, ind
);
1458 return Node::null();
1460 children
.push_back( aln
);
1461 childChanged
= childChanged
|| aln
!=n
[i
];
1466 ret
= NodeManager::currentNM()->mkNode( n
.getKind(), children
);
1468 //careful about caching
1478 void TheorySep::setInactiveAssertionRec( Node fact
, std::map
< Node
, std::vector
< Node
> >& lbl_to_assertions
, std::map
< Node
, bool >& assert_active
) {
1479 Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact
<< std::endl
;
1480 assert_active
[fact
] = false;
1481 bool polarity
= fact
.getKind() != kind::NOT
;
1482 TNode atom
= polarity
? fact
: fact
[0];
1483 TNode s_atom
= atom
[0];
1484 TNode s_lbl
= atom
[1];
1485 if( s_atom
.getKind()==kind::SEP_WAND
|| s_atom
.getKind()==kind::SEP_STAR
){
1486 for( unsigned j
=0; j
<s_atom
.getNumChildren(); j
++ ){
1487 Node lblc
= getLabel( s_atom
, j
, s_lbl
);
1488 for( unsigned k
=0; k
<lbl_to_assertions
[lblc
].size(); k
++ ){
1489 setInactiveAssertionRec( lbl_to_assertions
[lblc
][k
], lbl_to_assertions
, assert_active
);
1495 void TheorySep::getLabelChildren( Node s_atom
, Node lbl
, std::vector
< Node
>& children
, std::vector
< Node
>& labels
) {
1496 for( unsigned i
=0; i
<s_atom
.getNumChildren(); i
++ ){
1497 Node lblc
= getLabel( s_atom
, i
, lbl
);
1498 Assert( !lblc
.isNull() );
1499 std::map
< Node
, Node
> visited
;
1500 Node lc
= applyLabel( s_atom
[i
], lblc
, visited
);
1501 Assert( !lc
.isNull() );
1502 if( i
==1 && s_atom
.getKind()==kind::SEP_WAND
){
1505 children
.push_back( lc
);
1506 labels
.push_back( lblc
);
1508 Assert( children
.size()>1 );
1511 void TheorySep::computeLabelModel( Node lbl
) {
1512 if( !d_label_model
[lbl
].d_computed
){
1513 d_label_model
[lbl
].d_computed
= true;
1515 //we must get the value of lbl from the model: this is being run at last call, after the model is constructed
1517 Node v_val
= d_valuation
.getModel()->getRepresentative( lbl
);
1518 Trace("sep-process") << "Model value (from valuation) for " << lbl
<< " : " << v_val
<< std::endl
;
1519 if( v_val
.getKind()!=kind::EMPTYSET
){
1520 while( v_val
.getKind()==kind::UNION
){
1521 Assert( v_val
[1].getKind()==kind::SINGLETON
);
1522 d_label_model
[lbl
].d_heap_locs_model
.push_back( v_val
[1] );
1525 if( v_val
.getKind()==kind::SINGLETON
){
1526 d_label_model
[lbl
].d_heap_locs_model
.push_back( v_val
);
1528 throw Exception("Could not establish value of heap in model.");
1532 for( unsigned j
=0; j
<d_label_model
[lbl
].d_heap_locs_model
.size(); j
++ ){
1533 Node u
= d_label_model
[lbl
].d_heap_locs_model
[j
];
1534 Assert( u
.getKind()==kind::SINGLETON
);
1537 std::map
< Node
, Node
>::iterator itm
= d_tmodel
.find( u
);
1538 if( itm
==d_tmodel
.end() ) {
1539 //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl;
1542 //TypeNode tn = u.getType().getRefConstituentType();
1543 TypeNode tn
= u
.getType();
1544 Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u
<< ", cref type " << tn
<< std::endl
;
1545 Assert( d_type_references_all
.find( tn
)!=d_type_references_all
.end() );
1546 Assert( !d_type_references_all
[tn
].empty() );
1547 tt
= d_type_references_all
[tn
][0];
1551 Node stt
= NodeManager::currentNM()->mkNode( kind::SINGLETON
, tt
);
1552 Trace("sep-process-debug") << "...model : add " << tt
<< " for " << u
<< " in lbl " << lbl
<< std::endl
;
1553 d_label_model
[lbl
].d_heap_locs
.push_back( stt
);
1558 Node
TheorySep::getRepresentative( Node t
) {
1559 if( d_equalityEngine
.hasTerm( t
) ){
1560 return d_equalityEngine
.getRepresentative( t
);
1566 bool TheorySep::hasTerm( Node a
){
1567 return d_equalityEngine
.hasTerm( a
);
1570 bool TheorySep::areEqual( Node a
, Node b
){
1573 }else if( hasTerm( a
) && hasTerm( b
) ){
1574 return d_equalityEngine
.areEqual( a
, b
);
1580 bool TheorySep::areDisequal( Node a
, Node b
){
1583 }else if( hasTerm( a
) && hasTerm( b
) ){
1584 if( d_equalityEngine
.areDisequal( a
, b
, false ) ){
1592 void TheorySep::eqNotifyPreMerge(TNode t1
, TNode t2
) {
1596 void TheorySep::eqNotifyPostMerge(TNode t1
, TNode t2
) {
1597 HeapAssertInfo
* e2
= getOrMakeEqcInfo( t2
, false );
1598 if( e2
&& ( !e2
->d_pto
.get().isNull() || e2
->d_has_neg_pto
.get() ) ){
1599 HeapAssertInfo
* e1
= getOrMakeEqcInfo( t1
, true );
1600 if( !e2
->d_pto
.get().isNull() ){
1601 if( !e1
->d_pto
.get().isNull() ){
1602 Trace("sep-pto-debug") << "While merging " << t1
<< " " << t2
<< ", merge pto." << std::endl
;
1603 mergePto( e1
->d_pto
.get(), e2
->d_pto
.get() );
1605 e1
->d_pto
.set( e2
->d_pto
.get() );
1608 e1
->d_has_neg_pto
.set( e1
->d_has_neg_pto
.get() || e2
->d_has_neg_pto
.get() );
1610 validatePto( e1
, t1
);
1614 void TheorySep::validatePto( HeapAssertInfo
* ei
, Node ei_n
) {
1615 if( !ei
->d_pto
.get().isNull() && ei
->d_has_neg_pto
.get() ){
1616 for( NodeList::const_iterator i
= d_spatial_assertions
.begin(); i
!= d_spatial_assertions
.end(); ++i
) {
1618 bool polarity
= fact
.getKind() != kind::NOT
;
1620 TNode atom
= polarity
? fact
: fact
[0];
1621 Assert( atom
.getKind()==kind::SEP_LABEL
);
1622 TNode s_atom
= atom
[0];
1623 if( s_atom
.getKind()==kind::SEP_PTO
){
1624 if( areEqual( atom
[1], ei_n
) ){
1625 addPto( ei
, ei_n
, atom
, false );
1630 //we have now processed all pending negated pto
1631 ei
->d_has_neg_pto
.set( false );
1635 void TheorySep::addPto( HeapAssertInfo
* ei
, Node ei_n
, Node p
, bool polarity
) {
1636 Trace("sep-pto") << "Add pto " << p
<< ", pol = " << polarity
<< " to eqc " << ei_n
<< std::endl
;
1637 if( !ei
->d_pto
.get().isNull() ){
1639 Trace("sep-pto-debug") << "...eqc " << ei_n
<< " already has pto " << ei
->d_pto
.get() << ", merge." << std::endl
;
1640 mergePto( ei
->d_pto
.get(), p
);
1642 Node pb
= ei
->d_pto
.get();
1643 Trace("sep-pto") << "Process positive/negated pto " << " " << pb
<< " " << p
<< std::endl
;
1644 Assert( pb
.getKind()==kind::SEP_LABEL
&& pb
[0].getKind()==kind::SEP_PTO
);
1645 Assert( p
.getKind()==kind::SEP_LABEL
&& p
[0].getKind()==kind::SEP_PTO
);
1646 Assert( areEqual( pb
[1], p
[1] ) );
1647 std::vector
< Node
> exp
;
1649 //if( pb[1].getKind()==kind::SINGLETON && p[1].getKind()==kind::SINGLETON ){
1650 // exp.push_back( pb[1][0].eqNode( p[1][0] ) );
1652 exp
.push_back( pb
[1].eqNode( p
[1] ) );
1655 exp
.push_back( pb
);
1656 exp
.push_back( p
.negate() );
1657 std::vector
< Node
> conc
;
1658 if( pb
[0][1]!=p
[0][1] ){
1659 conc
.push_back( pb
[0][1].eqNode( p
[0][1] ).negate() );
1661 //if( pb[1]!=p[1] ){
1662 // conc.push_back( pb[1].eqNode( p[1] ).negate() );
1664 Node n_conc
= conc
.empty() ? d_false
: ( conc
.size()==1 ? conc
[0] : NodeManager::currentNM()->mkNode( kind::OR
, conc
) );
1665 Trace("sep-pto") << "Conclusion is " << n_conc
<< std::endl
;
1666 // propagation for (pto x y) ^ ~(pto z w) ^ x = z => y != w
1667 sendLemma( exp
, n_conc
, "PTO_NEG_PROP" );
1672 validatePto( ei
, ei_n
);
1674 ei
->d_has_neg_pto
.set( true );
1679 void TheorySep::mergePto( Node p1
, Node p2
) {
1680 Trace("sep-lemma-debug") << "Merge pto " << p1
<< " " << p2
<< std::endl
;
1681 Assert( p1
.getKind()==kind::SEP_LABEL
&& p1
[0].getKind()==kind::SEP_PTO
);
1682 Assert( p2
.getKind()==kind::SEP_LABEL
&& p2
[0].getKind()==kind::SEP_PTO
);
1683 if( !areEqual( p1
[0][1], p2
[0][1] ) ){
1684 std::vector
< Node
> exp
;
1686 Assert( areEqual( p1
[1], p2
[1] ) );
1687 exp
.push_back( p1
[1].eqNode( p2
[1] ) );
1689 exp
.push_back( p1
);
1690 exp
.push_back( p2
);
1691 //enforces injectiveness of pto : (pto x y) ^ (pto y w) ^ x = y => y = w
1692 sendLemma( exp
, p1
[0][1].eqNode( p2
[0][1] ), "PTO_PROP" );
1696 void TheorySep::sendLemma( std::vector
< Node
>& ant
, Node conc
, const char * c
, bool infer
) {
1697 Trace("sep-lemma-debug") << "Do rewrite on inference : " << conc
<< std::endl
;
1698 conc
= Rewriter::rewrite( conc
);
1699 Trace("sep-lemma-debug") << "Got : " << conc
<< std::endl
;
1701 if( infer
&& conc
!=d_false
){
1705 }else if( ant
.size()==1 ){
1708 ant_n
= NodeManager::currentNM()->mkNode( kind::AND
, ant
);
1710 Trace("sep-lemma") << "Sep::Infer: " << conc
<< " from " << ant_n
<< " by " << c
<< std::endl
;
1711 d_pending_exp
.push_back( ant_n
);
1712 d_pending
.push_back( conc
);
1713 d_infer
.push_back( ant_n
);
1714 d_infer_exp
.push_back( conc
);
1716 std::vector
< TNode
> ant_e
;
1717 for( unsigned i
=0; i
<ant
.size(); i
++ ){
1718 Trace("sep-lemma-debug") << "Explain : " << ant
[i
] << std::endl
;
1719 explain( ant
[i
], ant_e
);
1722 if( ant_e
.empty() ){
1724 }else if( ant_e
.size()==1 ){
1727 ant_n
= NodeManager::currentNM()->mkNode( kind::AND
, ant_e
);
1729 if( conc
==d_false
){
1730 Trace("sep-lemma") << "Sep::Conflict: " << ant_n
<< " by " << c
<< std::endl
;
1731 d_out
->conflict( ant_n
);
1734 Trace("sep-lemma") << "Sep::Lemma: " << conc
<< " from " << ant_n
<< " by " << c
<< std::endl
;
1735 d_pending_exp
.push_back( ant_n
);
1736 d_pending
.push_back( conc
);
1737 d_pending_lem
.push_back( d_pending
.size()-1 );
1743 void TheorySep::doPendingFacts() {
1744 if( d_pending_lem
.empty() ){
1745 for( unsigned i
=0; i
<d_pending
.size(); i
++ ){
1749 Node atom
= d_pending
[i
].getKind()==kind::NOT
? d_pending
[i
][0] : d_pending
[i
];
1750 bool pol
= d_pending
[i
].getKind()!=kind::NOT
;
1751 Trace("sep-pending") << "Sep : Assert to EE : " << atom
<< ", pol = " << pol
<< std::endl
;
1752 if( atom
.getKind()==kind::EQUAL
){
1753 d_equalityEngine
.assertEquality(atom
, pol
, d_pending_exp
[i
]);
1755 d_equalityEngine
.assertPredicate(atom
, pol
, d_pending_exp
[i
]);
1759 for( unsigned i
=0; i
<d_pending_lem
.size(); i
++ ){
1763 int index
= d_pending_lem
[i
];
1764 Node lem
= NodeManager::currentNM()->mkNode( kind::IMPLIES
, d_pending_exp
[index
], d_pending
[index
] );
1765 if( d_lemmas_produced_c
.find( lem
)==d_lemmas_produced_c
.end() ){
1766 d_lemmas_produced_c
.insert( lem
);
1767 d_out
->lemma( lem
);
1768 Trace("sep-pending") << "Sep : Lemma : " << lem
<< std::endl
;
1772 d_pending_exp
.clear();
1774 d_pending_lem
.clear();
1777 void TheorySep::debugPrintHeap( HeapInfo
& heap
, const char * c
) {
1778 Trace(c
) << "[" << std::endl
;
1780 for( unsigned j
=0; j
<heap
.d_heap_locs
.size(); j
++ ){
1781 Trace(c
) << heap
.d_heap_locs
[j
] << " ";
1783 Trace(c
) << std::endl
;
1784 Trace(c
) << "]" << std::endl
;
1787 Node
TheorySep::HeapInfo::getValue( TypeNode tn
) {
1788 Assert( d_heap_locs
.size()==d_heap_locs_model
.size() );
1789 if( d_heap_locs
.empty() ){
1790 return NodeManager::currentNM()->mkConst(EmptySet(tn
.toType()));
1791 }else if( d_heap_locs
.size()==1 ){
1792 return d_heap_locs
[0];
1794 Node curr
= NodeManager::currentNM()->mkNode( kind::UNION
, d_heap_locs
[0], d_heap_locs
[1] );
1795 for( unsigned j
=2; j
<d_heap_locs
.size(); j
++ ){
1796 curr
= NodeManager::currentNM()->mkNode( kind::UNION
, curr
, d_heap_locs
[j
] );
1802 }/* CVC4::theory::sep namespace */
1803 }/* CVC4::theory namespace */
1804 }/* CVC4 namespace */