From: Andrew Reynolds Date: Wed, 18 May 2022 15:35:51 +0000 (-0500) Subject: Basic cleanup of sep theory (#8790) X-Git-Tag: cvc5-1.0.1~117 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=244fc0d5f79148ec34b6dfb821d4427d470136bf;p=cvc5.git Basic cleanup of sep theory (#8790) Most of the simplifications are due to the fact that we only handle a single heap type. (The solver was initially designed to potentially handle more than one heap type). --- diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 8e930bea6..048d93e80 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -50,7 +50,9 @@ TheorySep::TheorySep(Env& env, OutputChannel& out, Valuation valuation) d_im(env, *this, d_state, "theory::sep::"), d_notify(*this), d_reduce(userContext()), - d_spatial_assertions(context()) + d_spatial_assertions(context()), + d_bound_kind(bound_invalid), + d_card_max(0) { d_true = NodeManager::currentNM()->mkConst(true); d_false = NodeManager::currentNM()->mkConst(false); @@ -78,11 +80,11 @@ void TheorySep::initializeHeapTypes() // otherwise set it Trace("sep-type") << "Sep: assume location type " << locT << " is associated with data type " << dataT << std::endl; - d_loc_to_data_type[locT] = dataT; // for now, we only allow heap constraints of one type d_type_ref = locT; d_type_data = dataT; - d_bound_kind[locT] = bound_default; + d_nil_ref = NodeManager::currentNM()->mkNullaryOperator(locT, SEP_NIL); + d_bound_kind = bound_default; } } @@ -121,21 +123,6 @@ void TheorySep::preRegisterTerm(TNode n) } } -Node TheorySep::mkAnd( std::vector< TNode >& assumptions ) { - if( assumptions.empty() ){ - return d_true; - }else if( assumptions.size()==1 ){ - return assumptions[0]; - }else{ - return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); - } -} - - -///////////////////////////////////////////////////////////////////////////// -// T-PROPAGATION / REGISTRATION -///////////////////////////////////////////////////////////////////////////// - bool TheorySep::propagateLit(TNode literal) { return d_im.propagateLit(literal); @@ -184,76 +171,95 @@ void TheorySep::computeCareGraph() { void TheorySep::postProcessModel( TheoryModel* m ){ Trace("sep-model") << "Printing model for TheorySep..." << std::endl; - + if (d_type_ref.isNull()) + { + return; + } NodeManager* nm = NodeManager::currentNM(); std::vector< Node > sep_children; Node m_neq; Node m_heap; - for( std::map< TypeNode, Node >::iterator it = d_base_label.begin(); it != d_base_label.end(); ++it ){ - //should only be constructing for one heap type - Assert(m_heap.isNull()); - Assert(d_loc_to_data_type.find(it->first) != d_loc_to_data_type.end()); - Trace("sep-model") << "Model for heap, type = " << it->first << " with data type " << d_loc_to_data_type[it->first] << " : " << std::endl; - TypeNode data_type = d_loc_to_data_type[it->first]; - computeLabelModel( it->second ); - if( d_label_model[it->second].d_heap_locs_model.empty() ){ - Trace("sep-model") << " [empty]" << std::endl; - }else{ - for( unsigned j=0; jsecond].d_heap_locs_model.size(); j++ ){ - Assert(d_label_model[it->second].d_heap_locs_model[j].getKind() - == kind::SET_SINGLETON); - std::vector< Node > pto_children; - Node l = d_label_model[it->second].d_heap_locs_model[j][0]; - Assert(l.isConst()); - pto_children.push_back( l ); - Trace("sep-model") << " " << l << " -> "; - if( d_pto_model[l].isNull() ){ - Trace("sep-model") << "_"; - TypeEnumerator te_range( data_type ); - if (d_env.isFiniteType(data_type)) - { - pto_children.push_back( *te_range ); - }else{ - //must enumerate until we find one that is not explicitly pointed to - bool success = false; - Node cv; - do{ - cv = *te_range; - if( std::find( d_heap_locs_nptos[l].begin(), d_heap_locs_nptos[l].end(), cv )==d_heap_locs_nptos[l].end() ){ - success = true; - }else{ - ++te_range; - } - }while( !success ); - pto_children.push_back( cv ); - } + // should only be constructing for one heap type + Assert(m_heap.isNull()); + Trace("sep-model") << "Model for heap, type = " << d_type_ref + << " with data type " << d_type_data << " : " << std::endl; + computeLabelModel(d_base_label); + HeapInfo& hm = d_label_model[d_base_label]; + if (hm.d_heap_locs_model.empty()) + { + Trace("sep-model") << " [empty]" << std::endl; + } + else + { + for (const Node& hv : hm.d_heap_locs_model) + { + Assert(hv.getKind() == SET_SINGLETON); + std::vector pto_children; + Node l = hv[0]; + Assert(l.isConst()); + pto_children.push_back(l); + Trace("sep-model") << " " << l << " -> "; + if (d_pto_model[l].isNull()) + { + Trace("sep-model") << "_"; + TypeEnumerator te_range(d_type_data); + if (d_env.isFiniteType(d_type_data)) + { + pto_children.push_back(*te_range); }else{ - Trace("sep-model") << d_pto_model[l]; - Node vpto = d_valuation.getModel()->getRepresentative( d_pto_model[l] ); - Assert(vpto.isConst()); - pto_children.push_back( vpto ); + // must enumerate until we find one that is not explicitly pointed to + bool success = false; + Node cv; + do + { + cv = *te_range; + if (std::find(d_heap_locs_nptos[l].begin(), + d_heap_locs_nptos[l].end(), + cv) + == d_heap_locs_nptos[l].end()) + { + success = true; + } + else + { + ++te_range; + } + } while (!success); + pto_children.push_back(cv); } - Trace("sep-model") << std::endl; - sep_children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_PTO, pto_children ) ); } + else + { + Trace("sep-model") << d_pto_model[l]; + Node vpto = d_valuation.getModel()->getRepresentative(d_pto_model[l]); + Assert(vpto.isConst()); + pto_children.push_back(vpto); + } + Trace("sep-model") << std::endl; + sep_children.push_back( + NodeManager::currentNM()->mkNode(SEP_PTO, pto_children)); } - Node nil = getNilRef( it->first ); - Node vnil = d_valuation.getModel()->getRepresentative( nil ); - m_neq = nm->mkNode(kind::EQUAL, nil, vnil); - Trace("sep-model") << "sep.nil = " << vnil << std::endl; - Trace("sep-model") << std::endl; - if( sep_children.empty() ){ - TypeEnumerator te_domain( it->first ); - TypeEnumerator te_range( d_loc_to_data_type[it->first] ); - TypeNode boolType = nm->booleanType(); - m_heap = nm->mkNullaryOperator(boolType, kind::SEP_EMP); - }else if( sep_children.size()==1 ){ - m_heap = sep_children[0]; - }else{ - m_heap = nm->mkNode(kind::SEP_STAR, sep_children); - } - m->setHeapModel( m_heap, m_neq ); } + Assert(!d_nil_ref.isNull()); + Node vnil = d_valuation.getModel()->getRepresentative(d_nil_ref); + m_neq = nm->mkNode(EQUAL, d_nil_ref, vnil); + Trace("sep-model") << "sep.nil = " << vnil << std::endl; + Trace("sep-model") << std::endl; + if (sep_children.empty()) + { + TypeNode boolType = nm->booleanType(); + m_heap = nm->mkNullaryOperator(boolType, SEP_EMP); + } + else if (sep_children.size() == 1) + { + m_heap = sep_children[0]; + } + else + { + m_heap = nm->mkNode(SEP_STAR, sep_children); + } + m->setHeapModel(m_heap, m_neq); + Trace("sep-model") << "Finished printing model for TheorySep." << std::endl; } @@ -350,10 +356,9 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) Trace("sep-lemma-debug") << "Reducing unlabelled assertion " << atom << std::endl; // introduce top-level label, add iff - TypeNode refType = getReferenceType(); Trace("sep-lemma-debug") - << "...reference type is : " << refType << std::endl; - Node b_lbl = getBaseLabel(refType); + << "...reference type is : " << d_type_ref << std::endl; + Node b_lbl = getBaseLabel(); Node satom_new = nm->mkNode(SEP_LABEL, satom, b_lbl); Node lem; Trace("sep-lemma-debug") << "...polarity is " << polarity << std::endl; @@ -381,10 +386,9 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) // make conclusion based on type of assertion if (satom.getKind() == SEP_STAR || satom.getKind() == SEP_WAND) { - TypeNode tn = getReferenceType(); - if (d_reference_bound_max.find(tn) != d_reference_bound_max.end()) + if (!d_reference_bound_max.isNull()) { - Node blem = nm->mkNode(SET_SUBSET, slbl, d_reference_bound_max[tn]); + Node blem = nm->mkNode(SET_SUBSET, slbl, d_reference_bound_max); d_im.lemma(blem, InferenceId::SEP_LABEL_DEF); } std::vector children; @@ -401,8 +405,8 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) { Assert(satom.getKind() == SEP_WAND); // nil does not occur in labels[0] - Node nr = getNilRef(tn); - Node nrlem = nm->mkNode(SET_MEMBER, nr, labels[0]).negate(); + Assert(!d_nil_ref.isNull()); + Node nrlem = nm->mkNode(SET_MEMBER, d_nil_ref, labels[0]).negate(); Trace("sep-lemma") << "Sep::Lemma: sep.nil not in wand antecedant heap : " << nrlem << std::endl; @@ -431,8 +435,9 @@ void TheorySep::reduceFact(TNode atom, bool polarity, TNode fact) } else { - Node kl = sm->mkDummySkolem("loc", getReferenceType()); - Node kd = sm->mkDummySkolem("data", getDataType()); + Assert(!d_type_ref.isNull()); + Node kl = sm->mkDummySkolem("loc", d_type_ref); + Node kd = sm->mkDummySkolem("data", d_type_data); Node econc = nm->mkNode( SEP_LABEL, nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, kl, kd), d_true), @@ -510,50 +515,43 @@ void TheorySep::postCheck(Effort level) d_pto_model.clear(); Trace("sep-process") << "---Locations---" << std::endl; std::map min_id; - for (std::map >::iterator itt = - d_type_references_all.begin(); - itt != d_type_references_all.end(); - ++itt) + for (const Node& t : d_type_references) { - for (const Node& t : itt->second) + Trace("sep-process") << " " << t << " = "; + if (d_valuation.getModel()->hasTerm(t)) { - Trace("sep-process") << " " << t << " = "; - if (d_valuation.getModel()->hasTerm(t)) + Node v = d_valuation.getModel()->getRepresentative(t); + Trace("sep-process") << v << std::endl; + // take minimal id + std::map::iterator itrc = d_type_ref_card_id.find(t); + int tid = itrc == d_type_ref_card_id.end() ? -1 : (int)itrc->second; + bool set_term_model; + if (d_tmodel.find(v) == d_tmodel.end()) { - Node v = d_valuation.getModel()->getRepresentative(t); - Trace("sep-process") << v << std::endl; - // take minimal id - std::map::iterator itrc = d_type_ref_card_id.find(t); - int tid = itrc == d_type_ref_card_id.end() ? -1 : (int)itrc->second; - bool set_term_model; - if (d_tmodel.find(v) == d_tmodel.end()) - { - set_term_model = true; - }else{ - set_term_model = min_id[v] > tid; - } - if (set_term_model) - { - d_tmodel[v] = t; - min_id[v] = tid; - } + set_term_model = true; } else { - Trace("sep-process") << "?" << std::endl; + set_term_model = min_id[v] > tid; + } + if (set_term_model) + { + d_tmodel[v] = t; + min_id[v] = tid; } } + else + { + Trace("sep-process") << "?" << std::endl; + } } Trace("sep-process") << "---" << std::endl; // build positive/negative assertion lists for labels std::map assert_active; // get the inactive assertions std::map > lbl_to_assertions; - for (NodeList::const_iterator i = d_spatial_assertions.begin(); - i != d_spatial_assertions.end(); - ++i) + for (const Node& fact : d_spatial_assertions) { - Node fact = (*i); bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; Assert(atom.getKind() == SEP_LABEL); @@ -576,11 +574,10 @@ void TheorySep::postCheck(Effort level) d_pto_model[vv] = satom[1]; // replace this on pto-model since this term is more relevant - TypeNode vtn = vv.getType(); - if (std::find(d_type_references_all[vtn].begin(), - d_type_references_all[vtn].end(), - satom[0]) - != d_type_references_all[vtn].end()) + Assert(vv.getType() == d_type_ref); + if (std::find( + d_type_references.begin(), d_type_references.end(), satom[0]) + != d_type_references.end()) { d_tmodel[vv] = satom[0]; } @@ -602,22 +599,16 @@ void TheorySep::postCheck(Effort level) } } //(recursively) set inactive sub-assertions - for (NodeList::const_iterator i = d_spatial_assertions.begin(); - i != d_spatial_assertions.end(); - ++i) + for (const Node& fact : d_spatial_assertions) { - Node fact = (*i); if (!assert_active[fact]) { setInactiveAssertionRec(fact, lbl_to_assertions, assert_active); } } // set up model information based on active assertions - for (NodeList::const_iterator i = d_spatial_assertions.begin(); - i != d_spatial_assertions.end(); - ++i) + for (const Node& fact : d_spatial_assertions) { - Node fact = (*i); bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; TNode satom = atom[0]; @@ -631,8 +622,8 @@ void TheorySep::postCheck(Effort level) if (TraceIsOn("sep-process")) { Trace("sep-process") << "--- Current spatial assertions : " << std::endl; - for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) { - Node fact = (*i); + for (const Node& fact : d_spatial_assertions) + { Trace("sep-process") << " " << fact; if (!assert_active[fact]) { @@ -655,11 +646,8 @@ void TheorySep::postCheck(Effort level) std::map active_lbl; if (options().sep.sepMinimalRefine) { - for (NodeList::const_iterator i = d_spatial_assertions.begin(); - i != d_spatial_assertions.end(); - ++i) + for (const Node& fact : d_spatial_assertions) { - Node fact = (*i); bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; TNode satom = atom[0]; @@ -683,11 +671,8 @@ void TheorySep::postCheck(Effort level) } // process spatial assertions - for (NodeList::const_iterator i = d_spatial_assertions.begin(); - i != d_spatial_assertions.end(); - ++i) + for (const Node& fact : d_spatial_assertions) { - Node fact = (*i); bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; TNode satom = atom[0]; @@ -718,8 +703,8 @@ void TheorySep::postCheck(Effort level) continue; } needAddLemma = true; - TypeNode tn = getReferenceType(); - tn = nm->mkSetType(tn); + Assert(!d_type_ref.isNull()); + TypeNode tn = nm->mkSetType(d_type_ref); // tn = nm->mkSetType(nm->mkRefType(tn)); Node o_b_lbl_mval = d_label_model[slbl].getValue(tn); Trace("sep-process") << " Model for " << slbl << " : " << o_b_lbl_mval @@ -805,20 +790,13 @@ void TheorySep::postCheck(Effort level) return; } // must witness finite data points-to - for (std::map::iterator it = d_base_label.begin(); - it != d_base_label.end(); - ++it) + // if the data type is finite + if (d_env.isFiniteType(d_type_data)) { - TypeNode data_type = d_loc_to_data_type[it->first]; - // if the data type is finite - if (!d_env.isFiniteType(data_type)) - { - continue; - } - computeLabelModel(it->second); - Trace("sep-process-debug") << "Check heap data for " << it->first << " -> " - << data_type << std::endl; - std::vector& hlmodel = d_label_model[it->second].d_heap_locs_model; + computeLabelModel(d_base_label); + Trace("sep-process-debug") << "Check heap data for " << d_type_data + << " -> " << d_type_data << std::endl; + std::vector& hlmodel = d_label_model[d_base_label].d_heap_locs_model; for (size_t j = 0, hsize = hlmodel.size(); j < hsize; j++) { Assert(hlmodel[j].getKind() == SET_SINGLETON); @@ -841,13 +819,13 @@ void TheorySep::postCheck(Effort level) if (!ll.isNull()) { Trace("sep-process") << "Must witness label : " << ll - << ", data type is " << data_type << std::endl; + << ", data type is " << d_type_data << std::endl; Node dsk = sm->mkDummySkolem( - "dsk", data_type, "pto-data for implicit location"); + "dsk", d_type_data, "pto-data for implicit location"); // if location is in the heap, then something must point to it Node lem = nm->mkNode( IMPLIES, - nm->mkNode(SET_MEMBER, ll, it->second), + nm->mkNode(SET_MEMBER, ll, d_base_label), nm->mkNode(SEP_STAR, nm->mkNode(SEP_PTO, ll, dsk), d_true)); Trace("sep-lemma") << "Sep::Lemma : witness finite data-pto : " << lem << std::endl; @@ -863,6 +841,7 @@ void TheorySep::postCheck(Effort level) } } } + if (addedLemma) { return; @@ -925,23 +904,10 @@ TheorySep::HeapAssertInfo * TheorySep::getOrMakeEqcInfo( Node n, bool doMake ) { } } -//for now, assume all constraints are for the same heap type (ensured by logic exceptions thrown in computeReferenceType2) -TypeNode TheorySep::getReferenceType() const -{ - Assert(!d_type_ref.isNull()); - return d_type_ref; -} - -TypeNode TheorySep::getDataType() const -{ - Assert(!d_type_data.isNull()); - return d_type_data; -} - // Must process assertions at preprocess so that quantified assertions are // processed properly. void TheorySep::ppNotifyAssertions(const std::vector& assertions) { - std::map > visited; + std::map > visited; std::map > > references; std::map > references_strict; for (unsigned i = 0; i < assertions.size(); i++) { @@ -949,20 +915,12 @@ void TheorySep::ppNotifyAssertions(const std::vector& assertions) { processAssertion(assertions[i], visited, references, references_strict, true, true, false); } - // if data type is unconstrained, assume a fresh uninterpreted sort - if (!d_type_ref.isNull()) { - if (d_type_data.isNull()) { - d_type_data = NodeManager::currentNM()->mkSort("_sep_U"); - Trace("sep-type") << "Sep: assume data type " << d_type_data << std::endl; - d_loc_to_data_type[d_type_ref] = d_type_data; - } - } } //return cardinality -int TheorySep::processAssertion( +size_t TheorySep::processAssertion( Node n, - std::map >& visited, + std::map >& visited, std::map > >& references, std::map >& references_strict, bool pol, @@ -970,11 +928,12 @@ int TheorySep::processAssertion( bool underSpatial) { int index = hasPol ? ( pol ? 1 : -1 ) : 0; - int card = 0; - std::map< Node, int >::iterator it = visited[index].find( n ); + size_t card = 0; + std::map::iterator it = visited[index].find(n); if( it==visited[index].end() ){ Trace("sep-pp-debug") << "process assertion : " << n << ", index = " << index << std::endl; - if( n.getKind()==kind::SEP_EMP ){ + if (n.getKind() == SEP_EMP) + { ensureHeapTypesFor(n); if( hasPol && pol ){ references[index][n].clear(); @@ -982,12 +941,15 @@ int TheorySep::processAssertion( }else{ card = 1; } - }else if( n.getKind()==kind::SEP_PTO ){ + } + else if (n.getKind() == SEP_PTO) + { ensureHeapTypesFor(n); if( quantifiers::TermUtil::hasBoundVarAttr( n[0] ) ){ - TypeNode tn1 = n[0].getType(); - if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){ - d_bound_kind[tn1] = bound_invalid; + Assert(n[0].getType() == d_type_ref); + if (d_bound_kind != bound_strict && d_bound_kind != bound_invalid) + { + d_bound_kind = bound_invalid; Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl; @@ -1001,18 +963,28 @@ int TheorySep::processAssertion( card = 1; } }else{ - bool isSpatial = n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_STAR; + bool isSpatial = n.getKind() == SEP_WAND || n.getKind() == SEP_STAR; bool newUnderSpatial = underSpatial || isSpatial; bool refStrict = isSpatial; - for( unsigned i=0; i0 ) ){ - TypeNode tn = getReferenceType(); - Assert(!tn.isNull()); + Assert(!d_type_ref.isNull()); // add references to overall type - unsigned bt = d_bound_kind[tn]; + unsigned bt = d_bound_kind; bool add = true; if( references_strict[index].find( n )!=references_strict[index].end() ){ Trace("sep-bound") << "Strict bound found based on " << n << ", index = " << index << std::endl; if( bt!=bound_strict ){ - d_bound_kind[tn] = bound_strict; - //d_type_references[tn].clear(); - d_card_max[tn] = card; + d_bound_kind = bound_strict; + d_card_max = card; }else{ //TODO: derive static equality add = false; @@ -1078,15 +1049,19 @@ int TheorySep::processAssertion( }else{ add = bt!=bound_strict; } - for( unsigned i=0; i(int)d_card_max[tn] ){ - d_card_max[tn] = card; + if (card > d_card_max) + { + d_card_max = card; } } } @@ -1131,147 +1106,149 @@ void TheorySep::ensureHeapTypesFor(Node atom) const } void TheorySep::initializeBounds() { - if( !d_bounds_init ){ - Trace("sep-bound") << "Initialize sep bounds..." << std::endl; - d_bounds_init = true; - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - for( std::map< TypeNode, TypeNode >::iterator it = d_loc_to_data_type.begin(); it != d_loc_to_data_type.end(); ++it ){ - TypeNode tn = it->first; - Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; - unsigned n_emp = 0; - if( d_bound_kind[tn] != bound_invalid ){ - n_emp = d_card_max[tn]; - }else if( d_type_references[tn].empty() ){ - //must include at least one constant TODO: remove? - n_emp = 1; - } - Trace("sep-bound") << "Cardinality element size : " << d_card_max[tn] << std::endl; - Trace("sep-bound") << "Type reference size : " << d_type_references[tn].size() << std::endl; - Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." << std::endl; - for( unsigned r=0; rmkDummySkolem("e", tn, "cardinality bound element for seplog"); - d_type_references_card[tn].push_back( e ); - d_type_ref_card_id[e] = r; - } - } + if (d_bounds_init) + { + return; + } + Trace("sep-bound") << "Initialize sep bounds..." << std::endl; + d_bounds_init = true; + if (d_type_ref.isNull()) + { + return; + } + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + Trace("sep-bound") << "Initialize bounds for " << d_type_ref << "..." + << std::endl; + size_t n_emp = 0; + if (d_bound_kind != bound_invalid) + { + n_emp = d_card_max; + } + else if (d_type_references.empty()) + { + // must include at least one constant TODO: remove? + n_emp = 1; + } + Trace("sep-bound") << "Cardinality element size : " << d_card_max + << std::endl; + Trace("sep-bound") << "Type reference size : " << d_type_references.size() + << std::endl; + Trace("sep-bound") << "Constructing " << n_emp << " cardinality constants." + << std::endl; + for (size_t r = 0; r < n_emp; r++) + { + Node e = sm->mkDummySkolem( + "e", d_type_ref, "cardinality bound element for seplog"); + d_type_references_card.push_back(e); + d_type_ref_card_id[e] = r; } } -Node TheorySep::getBaseLabel( TypeNode tn ) { - std::map< TypeNode, Node >::iterator it = d_base_label.find( tn ); - if( it==d_base_label.end() ){ - NodeManager* nm = NodeManager::currentNM(); - SkolemManager* sm = nm->getSkolemManager(); - initializeBounds(); - Trace("sep") << "Make base label for " << tn << std::endl; - std::stringstream ss; - ss << "__Lb"; - TypeNode ltn = nm->mkSetType(tn); - Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label"); - d_base_label[tn] = n_lbl; - //make reference bound - Trace("sep") << "Make reference bound label for " << tn << std::endl; - std::stringstream ss2; - ss2 << "__Lu"; - d_reference_bound[tn] = sm->mkDummySkolem(ss2.str(), ltn, ""); - d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references[tn].begin(), d_type_references[tn].end() ); - - //check whether monotonic (elements can be added to tn without effecting satisfiability) - bool tn_is_monotonic = true; - if (tn.isUninterpretedSort()) - { - //TODO: use monotonicity inference - tn_is_monotonic = !logicInfo().isQuantified(); - } - else - { - tn_is_monotonic = tn.getCardinality().isInfinite(); - } - //add a reference type for maximum occurrences of empty in a constraint - if (tn_is_monotonic) +Node TheorySep::getBaseLabel() +{ + if (!d_base_label.isNull()) + { + return d_base_label; + } + NodeManager* nm = NodeManager::currentNM(); + SkolemManager* sm = nm->getSkolemManager(); + initializeBounds(); + Trace("sep") << "Make base label for " << d_type_ref << std::endl; + std::stringstream ss; + ss << "__Lb"; + TypeNode ltn = nm->mkSetType(d_type_ref); + Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "base label"); + d_base_label = n_lbl; + // make reference bound + Trace("sep") << "Make reference bound label for " << d_type_ref << std::endl; + std::stringstream ss2; + ss2 << "__Lu"; + d_reference_bound = sm->mkDummySkolem(ss2.str(), ltn, ""); + + // check whether monotonic (elements can be added to tn without effecting + // satisfiability) + bool tn_is_monotonic = true; + if (d_type_ref.isUninterpretedSort()) + { + // TODO: use monotonicity inference + tn_is_monotonic = !logicInfo().isQuantified(); + } + else + { + tn_is_monotonic = d_type_ref.getCardinality().isInfinite(); + } + // add a reference type for maximum occurrences of empty in a constraint + if (tn_is_monotonic) + { + for (const Node& e : d_type_references_card) { - for( unsigned r=0; rmkNode( kind::EQUAL, e, d_type_references_all[tn][j] ); - d_im.lemma(eq.negate(), InferenceId::SEP_DISTINCT_REF); - } - d_type_references_all[tn].push_back( e ); + // ensure that it is distinct from all other references so far + for (const Node& r : d_type_references) + { + Node eq = nm->mkNode(EQUAL, e, r); + d_im.lemma(eq.negate(), InferenceId::SEP_DISTINCT_REF); } + d_type_references.push_back(e); } - else - { - //break symmetries TODO - - d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() ); - } - //Assert( !d_type_references_all[tn].empty() ); + } + else + { + d_type_references.insert(d_type_references.end(), + d_type_references_card.begin(), + d_type_references_card.end()); + } - if (d_bound_kind[tn] != bound_invalid) + if (d_bound_kind != bound_invalid) + { + // construct bound + d_reference_bound_max = mkUnion(d_type_ref, d_type_references); + Trace("sep-bound") << "overall bound for " << d_base_label << " : " + << d_reference_bound_max << std::endl; + + Node slem = nm->mkNode(SET_SUBSET, d_base_label, d_reference_bound_max); + Trace("sep-lemma") << "Sep::Lemma: reference bound for " << d_type_ref + << " : " << slem << std::endl; + d_im.lemma(slem, InferenceId::SEP_REF_BOUND); + + // symmetry breaking + size_t trcSize = d_type_references_card.size(); + if (trcSize > 1) { - //construct bound - d_reference_bound_max[tn] = mkUnion( tn, d_type_references_all[tn] ); - Trace("sep-bound") << "overall bound for " << d_base_label[tn] << " : " << d_reference_bound_max[tn] << std::endl; - - Node slem = NodeManager::currentNM()->mkNode( - kind::SET_SUBSET, d_base_label[tn], d_reference_bound_max[tn]); - Trace("sep-lemma") << "Sep::Lemma: reference bound for " << tn << " : " << slem << std::endl; - d_im.lemma(slem, InferenceId::SEP_REF_BOUND); - - //symmetry breaking - if( d_type_references_card[tn].size()>1 ){ - std::map< unsigned, Node > lit_mem_map; - for( unsigned i=0; imkNode(kind::SET_MEMBER, - d_type_references_card[tn][i], - d_reference_bound_max[tn]); + std::map lit_mem_map; + for (size_t i = 0; i < trcSize; i++) + { + lit_mem_map[i] = nm->mkNode( + SET_MEMBER, d_type_references_card[i], d_reference_bound_max); + } + for (size_t i = 0; i < (trcSize - 1); i++) + { + std::vector children; + for (size_t j = (i + 1); j < trcSize; j++) + { + children.push_back(lit_mem_map[j].negate()); } - for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){ - std::vector< Node > children; - for( unsigned j=(i+1); jmkNode( kind::AND, children ); - sym_lem = NodeManager::currentNM()->mkNode( kind::IMPLIES, lit_mem_map[i].negate(), sym_lem ); - Trace("sep-lemma") << "Sep::Lemma: symmetry breaking lemma : " << sym_lem << std::endl; - d_im.lemma(sym_lem, InferenceId::SEP_SYM_BREAK); - } + if (!children.empty()) + { + Node sym_lem = nm->mkAnd(children); + sym_lem = nm->mkNode(IMPLIES, lit_mem_map[i].negate(), sym_lem); + Trace("sep-lemma") + << "Sep::Lemma: symmetry breaking lemma : " << sym_lem + << std::endl; + d_im.lemma(sym_lem, InferenceId::SEP_SYM_BREAK); } } } - - //assert that nil ref is not in base label - Node nr = getNilRef( tn ); - Node nrlem = - NodeManager::currentNM()->mkNode(kind::SET_MEMBER, nr, n_lbl).negate(); - Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << tn << " : " << nrlem << std::endl; - d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP); - - return n_lbl; - }else{ - return it->second; } -} -Node TheorySep::getNilRef( TypeNode tn ) { - std::map< TypeNode, Node >::iterator it = d_nil_ref.find( tn ); - if( it==d_nil_ref.end() ){ - Node nil = NodeManager::currentNM()->mkNullaryOperator( tn, kind::SEP_NIL ); - setNilRef( tn, nil ); - return nil; - }else{ - return it->second; - } -} + // assert that nil ref is not in base label + Assert(!d_nil_ref.isNull()); + Node nrlem = nm->mkNode(SET_MEMBER, d_nil_ref, n_lbl).negate(); + Trace("sep-lemma") << "Sep::Lemma: sep.nil not in base label " << d_type_ref + << " : " << nrlem << std::endl; + d_im.lemma(nrlem, InferenceId::SEP_NIL_NOT_IN_HEAP); -void TheorySep::setNilRef( TypeNode tn, Node n ) { - Assert(n.getType() == tn); - d_nil_ref[tn] = n; + return n_lbl; } Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { @@ -1287,7 +1264,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { if( u.isNull() ){ u = s; }else{ - u = NodeManager::currentNM()->mkNode(kind::SET_UNION, s, u); + u = NodeManager::currentNM()->mkNode(SET_UNION, s, u); } } return u; @@ -1299,10 +1276,10 @@ Node TheorySep::getLabel( Node atom, int child, Node lbl ) { if( it==d_label_map[atom][lbl].end() ){ NodeManager* nm = NodeManager::currentNM(); SkolemManager* sm = nm->getSkolemManager(); - TypeNode refType = getReferenceType(); + Assert(!d_type_ref.isNull()); std::stringstream ss; ss << "__Lc" << child; - TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); + TypeNode ltn = NodeManager::currentNM()->mkSetType(d_type_ref); Node n_lbl = sm->mkDummySkolem(ss.str(), ltn, "sep label"); d_label_map[atom][lbl][child] = n_lbl; return n_lbl; @@ -1398,7 +1375,7 @@ bool TheorySep::sharesRootLabel(Node p, Node q) const } Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) { - Assert(n.getKind() != kind::SEP_LABEL); + Assert(n.getKind() != SEP_LABEL); NodeManager* nm = NodeManager::currentNM(); Kind k = n.getKind(); std::map::iterator it = visited.find(n); @@ -1407,11 +1384,11 @@ Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) return it->second; } Node ret; - if (k == kind::SEP_STAR || k == kind::SEP_WAND || k == kind::SEP_PTO) + if (k == SEP_STAR || k == SEP_WAND || k == SEP_PTO) { - ret = nm->mkNode(kind::SEP_LABEL, n, lbl); + ret = nm->mkNode(SEP_LABEL, n, lbl); } - else if (k == kind::SEP_EMP) + else if (k == SEP_EMP) { // (SEP_LABEL sep.emp L) is the same as (= L set.empty) ret = lbl.eqNode(nm->mkConst(EmptySet(lbl.getType()))); @@ -1420,7 +1397,7 @@ Node TheorySep::applyLabel( Node n, Node lbl, std::map< Node, Node >& visited ) { ret = n; std::vector children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + if (n.getMetaKind() == metakind::PARAMETERIZED) { children.push_back(n.getOperator()); } @@ -1465,13 +1442,16 @@ Node TheorySep::instantiateLabel(Node n, else { if( TraceIsOn("sep-inst") ){ - if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){ + if (n.getKind() == SEP_STAR || n.getKind() == SEP_WAND + || n.getKind() == SEP_PTO || n.getKind() == SEP_EMP) + { for( unsigned j=0; j children; children.resize( n.getNumChildren() ); @@ -1483,13 +1463,14 @@ Node TheorySep::instantiateLabel(Node n, Assert(sub_index >= 0 && sub_index < (int)children.size()); Trace("sep-inst-debug") << "Sublabel " << sub_index << " is " << sub_lbl << std::endl; Node lbl_mval; - if( n.getKind()==kind::SEP_WAND && sub_index==1 ){ + if (n.getKind() == SEP_WAND && sub_index == 1) + { Assert(d_label_map[n][lbl].find(0) != d_label_map[n][lbl].end()); Node sub_lbl_0 = d_label_map[n][lbl][0]; computeLabelModel( sub_lbl_0 ); Assert(d_label_model.find(sub_lbl_0) != d_label_model.end()); lbl_mval = NodeManager::currentNM()->mkNode( - kind::SET_UNION, lbl, d_label_model[sub_lbl_0].getValue(rtn)); + SET_UNION, lbl, d_label_model[sub_lbl_0].getValue(rtn)); }else{ computeLabelModel( sub_lbl ); Assert(d_label_model.find(sub_lbl) != d_label_model.end()); @@ -1503,8 +1484,8 @@ Node TheorySep::instantiateLabel(Node n, } } Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn)); - if( n.getKind()==kind::SEP_STAR ){ - + if (n.getKind() == SEP_STAR) + { //disjoint contraints std::vector< Node > conj; std::vector< Node > bchildren; @@ -1516,21 +1497,20 @@ Node TheorySep::instantiateLabel(Node n, Node lbl_mval = d_label_model[sub_lbl].getValue( rtn ); for( unsigned j=0; jmkNode(kind::SET_INTER, lbl_mval, vs[j]) + ->mkNode(SET_INTER, lbl_mval, vs[j]) .eqNode(empSet)); } vs.push_back( lbl_mval ); if( vsu.isNull() ){ vsu = lbl_mval; }else{ - vsu = NodeManager::currentNM()->mkNode( - kind::SET_UNION, vsu, lbl_mval); + vsu = NodeManager::currentNM()->mkNode(SET_UNION, vsu, lbl_mval); } } bchildren.push_back( vsu.eqNode( lbl ) ); Assert(bchildren.size() > 1); - conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) ); + conj.push_back(NodeManager::currentNM()->mkNode(AND, bchildren)); return NodeManager::currentNM()->mkOr(conj); }else{ std::vector< Node > wchildren; @@ -1538,20 +1518,22 @@ Node TheorySep::instantiateLabel(Node n, Node sub_lbl_0 = d_label_map[n][lbl][0]; Node lbl_mval_0 = d_label_model[sub_lbl_0].getValue( rtn ); wchildren.push_back(NodeManager::currentNM() - ->mkNode(kind::SET_INTER, lbl_mval_0, lbl) + ->mkNode(SET_INTER, lbl_mval_0, lbl) .eqNode(empSet) .negate()); //return the lemma wchildren.push_back( children[0].negate() ); wchildren.push_back( children[1] ); - return NodeManager::currentNM()->mkNode( kind::OR, wchildren ); + return NodeManager::currentNM()->mkNode(OR, wchildren); } }else{ //nested star/wand, label it and return - return NodeManager::currentNM()->mkNode( kind::SEP_LABEL, n, lbl_v ); + return NodeManager::currentNM()->mkNode(SEP_LABEL, n, lbl_v); } - }else if( n.getKind()==kind::SEP_PTO ){ + } + else if (n.getKind() == SEP_PTO) + { //check if this pto reference is in the base label, if not, then it does not need to be added as an assumption Assert(d_label_model.find(o_lbl) != d_label_model.end()); Node vr = d_valuation.getModel()->getRepresentative( n[0] ); @@ -1561,13 +1543,16 @@ Node TheorySep::instantiateLabel(Node n, std::vector< Node > children; if( inBaseHeap ){ Node s = nm->mkNode(SET_SINGLETON, n[0]); - children.push_back( NodeManager::currentNM()->mkNode( kind::SEP_LABEL, NodeManager::currentNM()->mkNode( kind::SEP_PTO, n[0], n[1] ), s ) ); + children.push_back(NodeManager::currentNM()->mkNode( + SEP_LABEL, + NodeManager::currentNM()->mkNode(SEP_PTO, n[0], n[1]), + s)); }else{ //look up value of data std::map< Node, Node >::iterator it = pto_model.find( vr ); if( it!=pto_model.end() ){ if( n[1]!=it->second ){ - children.push_back( NodeManager::currentNM()->mkNode( kind::EQUAL, n[1], it->second ) ); + children.push_back(nm->mkNode(EQUAL, n[1], it->second)); } }else{ Trace("sep-inst-debug") << "Data for " << vr << " was not specified, do not add condition." << std::endl; @@ -1575,19 +1560,20 @@ Node TheorySep::instantiateLabel(Node n, } Node singleton = nm->mkNode(SET_SINGLETON, n[0]); children.push_back(singleton.eqNode(lbl_v)); - Node ret = children.empty() ? NodeManager::currentNM()->mkConst( true ) : ( children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( kind::AND, children ) ); + Node ret = nm->mkAnd(children); Trace("sep-inst-debug") << "Return " << ret << std::endl; return ret; - }else if( n.getKind()==kind::SEP_EMP ){ - // return NodeManager::currentNM()->mkConst( - // lbl_v.getKind()==kind::SET_EMPTY ); + } + else if (n.getKind() == SEP_EMP) + { return lbl_v.eqNode( NodeManager::currentNM()->mkConst(EmptySet(lbl_v.getType()))); }else{ std::map< Node, Node >::iterator it = visited.find( n ); if( it==visited.end() ){ std::vector< Node > children; - if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + if (n.getMetaKind() == metakind::PARAMETERIZED) + { children.push_back( n.getOperator() ); } bool childChanged = false; @@ -1617,7 +1603,7 @@ Node TheorySep::instantiateLabel(Node n, void TheorySep::setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active ) { Trace("sep-process-debug") << "setInactiveAssertionRec::inactive : " << fact << std::endl; assert_active[fact] = false; - bool polarity = fact.getKind() != kind::NOT; + bool polarity = fact.getKind() != NOT; TNode atom = polarity ? fact : fact[0]; TNode satom = atom[0]; TNode slbl = atom[1]; @@ -1656,55 +1642,59 @@ void TheorySep::getLabelChildren(Node satom, } void TheorySep::computeLabelModel( Node lbl ) { - if( !d_label_model[lbl].d_computed ){ - d_label_model[lbl].d_computed = true; - NodeManager* nm = NodeManager::currentNM(); - //we must get the value of lbl from the model: this is being run at last call, after the model is constructed - //Assert(...); TODO - Node v_val = d_valuation.getModel()->getRepresentative( lbl ); - Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " << v_val << std::endl; - if (v_val.getKind() != kind::SET_EMPTY) + if (d_label_model[lbl].d_computed) + { + return; + } + d_label_model[lbl].d_computed = true; + NodeManager* nm = NodeManager::currentNM(); + // we must get the value of lbl from the model: this is being run at last + // call, after the model is constructed Assert(...); TODO + Node v_val = d_valuation.getModel()->getRepresentative(lbl); + Trace("sep-process") << "Model value (from valuation) for " << lbl << " : " + << v_val << std::endl; + if (v_val.getKind() != SET_EMPTY) + { + while (v_val.getKind() == SET_UNION) { - while (v_val.getKind() == kind::SET_UNION) - { - Assert(v_val[0].getKind() == kind::SET_SINGLETON); - d_label_model[lbl].d_heap_locs_model.push_back(v_val[0]); - v_val = v_val[1]; - } - if (v_val.getKind() == kind::SET_SINGLETON) - { - d_label_model[lbl].d_heap_locs_model.push_back( v_val ); - } - else - { - throw Exception("Could not establish value of heap in model."); - Assert(false); - } + Assert(v_val[0].getKind() == SET_SINGLETON); + d_label_model[lbl].d_heap_locs_model.push_back(v_val[0]); + v_val = v_val[1]; } - for( unsigned j=0; j::iterator itm = d_tmodel.find( u ); - if( itm==d_tmodel.end() ) { - //Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << std::endl; - //Assert( false ); - //tt = u; - //TypeNode tn = u.getType().getRefConstituentType(); - TypeNode tn = u.getType(); - Trace("sep-process") << "WARNING: could not find symbolic term in model for " << u << ", cref type " << tn << std::endl; - Assert(d_type_references_all.find(tn) != d_type_references_all.end()); - Assert(!d_type_references_all[tn].empty()); - tt = d_type_references_all[tn][0]; - }else{ - tt = itm->second; - } - Node stt = nm->mkNode(SET_SINGLETON, tt); - Trace("sep-process-debug") << "...model : add " << tt << " for " << u << " in lbl " << lbl << std::endl; - d_label_model[lbl].d_heap_locs.push_back( stt ); + if (v_val.getKind() == SET_SINGLETON) + { + d_label_model[lbl].d_heap_locs_model.push_back(v_val); + } + else + { + throw Exception("Could not establish value of heap in model."); + Assert(false); } } + for (const Node& s : d_label_model[lbl].d_heap_locs_model) + { + Assert(s.getKind() == SET_SINGLETON); + Node u = s[0]; + Node tt; + std::map::iterator itm = d_tmodel.find(u); + if (itm == d_tmodel.end()) + { + TypeNode tn = u.getType(); + Trace("sep-process") + << "WARNING: could not find symbolic term in model for " << u + << ", cref type " << tn << std::endl; + Assert(!d_type_references.empty()); + tt = d_type_references[0]; + } + else + { + tt = itm->second; + } + Node stt = nm->mkNode(SET_SINGLETON, tt); + Trace("sep-process-debug") << "...model : add " << tt << " for " << u + << " in lbl " << lbl << std::endl; + d_label_model[lbl].d_heap_locs.push_back(stt); + } } Node TheorySep::getRepresentative( Node t ) { @@ -1903,16 +1893,6 @@ void TheorySep::doPending() d_im.doPendingLemmas(); } -void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) { - Trace(c) << "[" << std::endl; - Trace(c) << " "; - for( unsigned j=0; jmkNode(kind::SET_UNION, d_heap_locs[j], curr); + curr = NodeManager::currentNM()->mkNode(SET_UNION, d_heap_locs[j], curr); } return curr; } diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index aee92dcba..8abfd5a5a 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -65,11 +65,9 @@ class TheorySep : public Theory { /** A buffered inference manager */ InferenceManagerBuffered d_im; - Node mkAnd( std::vector< TNode >& assumptions ); - - int processAssertion( + size_t processAssertion( Node n, - std::map >& visited, + std::map >& visited, std::map > >& references, std::map >& references_strict, bool pol, @@ -221,29 +219,27 @@ class TheorySep : public Theory { //data,ref type (globally fixed) TypeNode d_type_ref; TypeNode d_type_data; - //currently fix one data type for each location type, throw error if using more than one - std::map< TypeNode, TypeNode > d_loc_to_data_type; //information about types - std::map< TypeNode, Node > d_base_label; - std::map< TypeNode, Node > d_nil_ref; + Node d_base_label; + Node d_nil_ref; //reference bound - std::map< TypeNode, Node > d_reference_bound; - std::map< TypeNode, Node > d_reference_bound_max; - std::map< TypeNode, std::vector< Node > > d_type_references; + Node d_reference_bound; + Node d_reference_bound_max; + std::vector d_type_references; //kind of bound for reference types enum { bound_strict, bound_default, bound_invalid, }; - std::map< TypeNode, unsigned > d_bound_kind; + unsigned d_bound_kind; - std::map< TypeNode, std::vector< Node > > d_type_references_card; + std::vector d_type_references_card; std::map< Node, unsigned > d_type_ref_card_id; - std::map< TypeNode, std::vector< Node > > d_type_references_all; - std::map< TypeNode, unsigned > d_card_max; + std::vector d_type_references_all; + size_t d_card_max; //for empty argument - std::map< TypeNode, Node > d_emp_arg; + Node d_emp_arg; //map from ( atom, label, child index ) -> label std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map; @@ -301,9 +297,6 @@ class TheorySep : public Theory { * non-null, and compatible with separation logic constraint atom. */ void ensureHeapTypesFor(Node atom) const; - // get global reference/data type - TypeNode getReferenceType() const; - TypeNode getDataType() const; /** * This is called either when: * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or @@ -314,9 +307,7 @@ class TheorySep : public Theory { void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom); //get location/data type //get the base label for the spatial assertion - Node getBaseLabel( TypeNode tn ); - Node getNilRef( TypeNode tn ); - void setNilRef( TypeNode tn, Node n ); + Node getBaseLabel(); Node getLabel( Node atom, int child, Node lbl ); /** * Apply label lbl to all top-level spatial assertions, recursively, in n. @@ -338,8 +329,6 @@ class TheorySep : public Theory { std::map< Node, HeapInfo > d_label_model; // loc -> { data_1, ..., data_n } where (not (pto loc data_1))...(not (pto loc data_n))). std::map< Node, std::vector< Node > > d_heap_locs_nptos; - - void debugPrintHeap( HeapInfo& heap, const char * c ); /** * This checks the impact of adding the pto assertion p to heap assert info e, * where p has been asserted with the given polarity.