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<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
// 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;
}
}
}
}
-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);
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; j<d_label_model[it->second].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<Node> 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;
}
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;
// 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<Node> children;
{
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;
}
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),
d_pto_model.clear();
Trace("sep-process") << "---Locations---" << std::endl;
std::map<Node, int> min_id;
- for (std::map<TypeNode, std::vector<Node> >::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<Node, unsigned>::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<Node, unsigned>::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<Node, bool> assert_active;
// get the inactive assertions
std::map<Node, std::vector<Node> > 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);
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];
}
}
}
//(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];
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])
{
std::map<Node, bool> 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];
}
// 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];
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
return;
}
// must witness finite data points-to
- for (std::map<TypeNode, Node>::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<Node>& 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<Node>& 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);
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;
}
}
}
+
if (addedLemma)
{
return;
}
}
-//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<Node>& assertions) {
- std::map<int, std::map<Node, int> > visited;
+ std::map<int, std::map<Node, size_t> > visited;
std::map<int, std::map<Node, std::vector<Node> > > references;
std::map<int, std::map<Node, bool> > references_strict;
for (unsigned i = 0; i < assertions.size(); i++) {
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<int, std::map<Node, int> >& visited,
+ std::map<int, std::map<Node, size_t> >& visited,
std::map<int, std::map<Node, std::vector<Node> > >& references,
std::map<int, std::map<Node, bool> >& references_strict,
bool pol,
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<Node, size_t>::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();
}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;
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; i<n.getNumChildren(); i++ ){
+ for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
+ {
bool newHasPol, newPol;
QuantPhaseReq::getEntailPolarity( n, i, hasPol, pol, newHasPol, newPol );
int newIndex = newHasPol ? ( newPol ? 1 : -1 ) : 0;
- int ccard = processAssertion( n[i], visited, references, references_strict, newPol, newHasPol, newUnderSpatial );
+ size_t ccard = processAssertion(n[i],
+ visited,
+ references,
+ references_strict,
+ newPol,
+ newHasPol,
+ newUnderSpatial);
//update cardinality
- if( n.getKind()==kind::SEP_STAR ){
+ if (n.getKind() == SEP_STAR)
+ {
card += ccard;
- }else if( n.getKind()==kind::SEP_WAND ){
+ }
+ else if (n.getKind() == SEP_WAND)
+ {
if( i==1 ){
card = ccard;
}
}
}
if( isSpatial && refStrict ){
- if( n.getKind()==kind::SEP_WAND ){
+ if (n.getKind() == SEP_WAND)
+ {
//TODO
}else{
- Assert(n.getKind() == kind::SEP_STAR && hasPol && pol);
+ Assert(n.getKind() == SEP_STAR && hasPol && pol);
references_strict[index][n] = true;
}
}
}
if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){
- 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;
}else{
add = bt!=bound_strict;
}
- for( unsigned i=0; i<references[index][n].size(); i++ ){
- if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), references[index][n][i] )==d_type_references[tn].end() ){
- d_type_references[tn].push_back( references[index][n][i] );
+ for (const Node& r : references[index][n])
+ {
+ if (std::find(d_type_references.begin(), d_type_references.end(), r)
+ == d_type_references.end())
+ {
+ d_type_references.push_back(r);
}
}
if( add ){
//add max cardinality
- if( card>(int)d_card_max[tn] ){
- d_card_max[tn] = card;
+ if (card > d_card_max)
+ {
+ d_card_max = card;
}
}
}
}
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; r<n_emp; r++ ){
- Node e =
- sm->mkDummySkolem("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; r<d_type_references_card[tn].size(); r++ ){
- Node e = d_type_references_card[tn][r];
- //ensure that it is distinct from all other references so far
- for( unsigned j=0; j<d_type_references_all[tn].size(); j++ ){
- Node eq = NodeManager::currentNM()->mkNode( 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; i<d_type_references_card[tn].size(); i++ ){
- lit_mem_map[i] =
- NodeManager::currentNM()->mkNode(kind::SET_MEMBER,
- d_type_references_card[tn][i],
- d_reference_bound_max[tn]);
+ std::map<size_t, Node> 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<Node> 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); j<d_type_references_card[tn].size(); j++ ){
- children.push_back( lit_mem_map[j].negate() );
- }
- if( !children.empty() ){
- Node sym_lem = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( 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 ) {
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;
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;
}
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<Node, Node>::iterator it = visited.find(n);
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())));
{
ret = n;
std::vector<Node> children;
- if (n.getMetaKind() == kind::metakind::PARAMETERIZED)
+ if (n.getMetaKind() == metakind::PARAMETERIZED)
{
children.push_back(n.getOperator());
}
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<ind; j++ ){ Trace("sep-inst") << " "; }
Trace("sep-inst") << n << "[" << lbl << "] :: " << lbl_v << std::endl;
}
}
- Assert(n.getKind() != kind::SEP_LABEL);
- if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){
+ Assert(n.getKind() != SEP_LABEL);
+ if (n.getKind() == SEP_STAR || n.getKind() == SEP_WAND)
+ {
if( lbl==o_lbl ){
std::vector< Node > children;
children.resize( n.getNumChildren() );
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());
}
}
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;
Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
for( unsigned j=0; j<vs.size(); j++ ){
bchildren.push_back(NodeManager::currentNM()
- ->mkNode(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;
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] );
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;
}
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;
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];
}
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<d_label_model[lbl].d_heap_locs_model.size(); j++ ){
- Node u = d_label_model[lbl].d_heap_locs_model[j];
- Assert(u.getKind() == kind::SET_SINGLETON);
- u = u[0];
- Node tt;
- std::map< Node, Node >::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<Node, Node>::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 ) {
d_im.doPendingLemmas();
}
-void TheorySep::debugPrintHeap( HeapInfo& heap, const char * c ) {
- Trace(c) << "[" << std::endl;
- Trace(c) << " ";
- for( unsigned j=0; j<heap.d_heap_locs.size(); j++ ){
- Trace(c) << heap.d_heap_locs[j] << " ";
- }
- Trace(c) << std::endl;
- Trace(c) << "]" << std::endl;
-}
-
Node TheorySep::HeapInfo::getValue( TypeNode tn ) {
Assert(d_heap_locs.size() == d_heap_locs_model.size());
if( d_heap_locs.empty() ){
Node curr = d_heap_locs[0];
for (unsigned j = 1; j < d_heap_locs.size(); j++)
{
- curr =
- NodeManager::currentNM()->mkNode(kind::SET_UNION, d_heap_locs[j], curr);
+ curr = NodeManager::currentNM()->mkNode(SET_UNION, d_heap_locs[j], curr);
}
return curr;
}
projects / cvc5.git / commitdiff