summaryrefslogtreecommitdiff
path: root/src/theory/sep/theory_sep.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/sep/theory_sep.cpp')
-rw-r--r--src/theory/sep/theory_sep.cpp55
1 files changed, 46 insertions, 9 deletions
diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp
index e2cd4f9dc..680bd8536 100644
--- a/src/theory/sep/theory_sep.cpp
+++ b/src/theory/sep/theory_sep.cpp
@@ -265,7 +265,8 @@ void TheorySep::postProcessModel( TheoryModel* m ){
Trace("sep-model") << std::endl;
if( sep_children.empty() ){
TypeEnumerator te_domain( it->first );
- m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain );
+ TypeEnumerator te_range( d_loc_to_data_type[it->first] );
+ m_heap = NodeManager::currentNM()->mkNode( kind::SEP_EMP, *te_domain, *te_range );
}else if( sep_children.size()==1 ){
m_heap = sep_children[0];
}else{
@@ -311,6 +312,7 @@ void TheorySep::check(Effort e) {
bool polarity = fact.getKind() != kind::NOT;
TNode atom = polarity ? fact : fact[0];
+ /*
if( atom.getKind()==kind::SEP_EMP ){
TypeNode tn = atom[0].getType();
if( d_emp_arg.find( tn )==d_emp_arg.end() ){
@@ -319,6 +321,7 @@ void TheorySep::check(Effort e) {
//normalize argument TODO
}
}
+ */
TNode s_atom = atom.getKind()==kind::SEP_LABEL ? atom[0] : atom;
TNode s_lbl = atom.getKind()==kind::SEP_LABEL ? atom[1] : TNode::null();
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;
@@ -410,7 +413,6 @@ void TheorySep::check(Effort e) {
//Node ssn = NodeManager::currentNM()->mkNode( kind::EQUAL, s_atom[0], getNilRef(s_atom[0].getType()) ).negate();
//conc = conc.isNull() ? ssn : NodeManager::currentNM()->mkNode( kind::AND, conc, ssn );
- /* TODO?
}else if( s_atom.getKind()==kind::SEP_EMP ){
//conc = s_lbl.eqNode( NodeManager::currentNM()->mkConst(EmptySet(s_lbl.getType().toType())) );
Node lem;
@@ -427,7 +429,7 @@ void TheorySep::check(Effort e) {
}
Trace("sep-lemma") << "Sep::Lemma : emp : " << lem << std::endl;
d_out->lemma( lem );
- */
+
}else{
//labeled emp should be rewritten
Assert( false );
@@ -546,6 +548,12 @@ void TheorySep::check(Effort e) {
if( d_pto_model.find( vv )==d_pto_model.end() ){
Trace("sep-process") << "Pto : " << s_atom[0] << " (" << vv << ") -> " << s_atom[1] << std::endl;
d_pto_model[vv] = s_atom[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(), s_atom[0] )!=d_type_references_all[vtn].end() ){
+ d_tmodel[vv] = s_atom[0];
+ }
}
}
}else{
@@ -991,7 +999,7 @@ TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node
return tn1;
}else if( n.getKind()==kind::SEP_EMP ){
TypeNode tn = n[0].getType();
- TypeNode tnd;
+ TypeNode tnd = n[1].getType();
registerRefDataTypes( tn, tnd, atom );
card = 1;
visited[n] = card;
@@ -1110,6 +1118,8 @@ void TheorySep::initializeBounds() {
//must include at least one constant
n_emp = 1;
}
+ Trace("sep-bound") << "Card maximums : " << d_card_max[tn] << " " << d_card_max[TypeNode::null()] << 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 = NodeManager::currentNM()->mkSkolem( "e", tn, "cardinality bound element for seplog" );
@@ -1321,6 +1331,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
std::vector< Node > children;
children.resize( n.getNumChildren() );
Assert( d_label_map[n].find( lbl )!=d_label_map[n].end() );
+ std::map< int, Node > mvals;
for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
Node sub_lbl = itl->second;
int sub_index = itl->first;
@@ -1339,6 +1350,7 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
lbl_mval = d_label_model[sub_lbl].getValue( rtn );
}
Trace("sep-inst-debug") << "Sublabel value is " << lbl_mval << std::endl;
+ mvals[sub_index] = lbl_mval;
children[sub_index] = instantiateLabel( n[sub_index], o_lbl, sub_lbl, lbl_mval, visited, pto_model, rtn, active_lbl, ind+1 );
if( children[sub_index].isNull() ){
return Node::null();
@@ -1346,14 +1358,18 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
}
Node empSet = NodeManager::currentNM()->mkConst(EmptySet(rtn.toType()));
if( n.getKind()==kind::SEP_STAR ){
+
//disjoint contraints
+ std::vector< Node > conj;
+ std::vector< Node > bchildren;
+ bchildren.insert( bchildren.end(), children.begin(), children.end() );
Node vsu;
std::vector< Node > vs;
for( std::map< int, Node >::iterator itl = d_label_map[n][lbl].begin(); itl != d_label_map[n][lbl].end(); ++itl ){
Node sub_lbl = itl->second;
Node lbl_mval = d_label_model[sub_lbl].getValue( rtn );
for( unsigned j=0; j<vs.size(); j++ ){
- children.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
+ bchildren.push_back( NodeManager::currentNM()->mkNode( kind::INTERSECTION, lbl_mval, vs[j] ).eqNode( empSet ) );
}
vs.push_back( lbl_mval );
if( vsu.isNull() ){
@@ -1362,11 +1378,32 @@ Node TheorySep::instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std:
vsu = NodeManager::currentNM()->mkNode( kind::UNION, vsu, lbl_mval );
}
}
- children.push_back( vsu.eqNode( lbl ) );
+ bchildren.push_back( vsu.eqNode( lbl ) );
- //return the lemma
- Assert( children.size()>1 );
- return NodeManager::currentNM()->mkNode( kind::AND, children );
+ Assert( bchildren.size()>1 );
+ conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) );
+
+ if( options::sepChildRefine() ){
+ //child-specific refinements (TODO: use ?)
+ for( unsigned i=0; i<children.size(); i++ ){
+ std::vector< Node > tchildren;
+ Node mval = mvals[i];
+ tchildren.push_back( NodeManager::currentNM()->mkNode( kind::SUBSET, mval, lbl ) );
+ tchildren.push_back( children[i] );
+ std::vector< Node > rem_children;
+ for( unsigned j=0; j<children.size(); j++ ){
+ if( j!=i ){
+ rem_children.push_back( n[j] );
+ }
+ }
+ std::map< Node, Node > rvisited;
+ Node rem = rem_children.size()==1 ? rem_children[0] : NodeManager::currentNM()->mkNode( kind::SEP_STAR, rem_children );
+ rem = applyLabel( rem, NodeManager::currentNM()->mkNode( kind::SETMINUS, lbl, mval ), rvisited );
+ tchildren.push_back( rem );
+ conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, tchildren ) );
+ }
+ }
+ return conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( kind::OR, conj );
}else{
std::vector< Node > wchildren;
//disjoint constraints
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback