From 4db65cbaf87f87dba3682e88563f5a923f265152 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Tue, 6 Dec 2016 11:16:35 -0600 Subject: [PATCH] Improve bounds for global heap in sep, refactor preprocessing. Minor improvement to sets. --- src/theory/quantifiers/quant_util.cpp | 4 +- src/theory/sep/theory_sep.cpp | 313 ++++++++++++------------ src/theory/sep/theory_sep.h | 22 +- src/theory/sets/theory_sets_private.cpp | 112 +++++---- src/theory/sets/theory_sets_private.h | 1 + 5 files changed, 235 insertions(+), 217 deletions(-) diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp index f4284a8ab..c0595d3d9 100644 --- a/src/theory/quantifiers/quant_util.cpp +++ b/src/theory/quantifiers/quant_util.cpp @@ -404,8 +404,8 @@ void QuantPhaseReq::getPolarity( Node n, int child, bool hasPol, bool pol, bool& } void QuantPhaseReq::getEntailPolarity( Node n, int child, bool hasPol, bool pol, bool& newHasPol, bool& newPol ) { - if( n.getKind()==AND || n.getKind()==OR ){ - newHasPol = hasPol && pol==( n.getKind()==AND ); + if( n.getKind()==AND || n.getKind()==OR || n.getKind()==SEP_STAR ){ + newHasPol = hasPol && pol!=( n.getKind()==OR ); newPol = pol; }else if( n.getKind()==IMPLIES ){ newHasPol = hasPol && !pol; diff --git a/src/theory/sep/theory_sep.cpp b/src/theory/sep/theory_sep.cpp index 680bd8536..55279e485 100644 --- a/src/theory/sep/theory_sep.cpp +++ b/src/theory/sep/theory_sep.cpp @@ -883,10 +883,12 @@ TypeNode TheorySep::getDataType( Node n ) { //must process assertions at preprocess so that quantified assertions are processed properly void TheorySep::ppNotifyAssertions( std::vector< Node >& assertions ) { - std::map< Node, bool > visited; + std::map< int, std::map< Node, int > > 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 ) { } } -void TheorySep::processAssertion( Node n, std::map< Node, bool >& visited ) { - if( visited.find( n )==visited.end() ){ - visited[n] = true; - Trace("sep-pp-debug") << "process assertion : " << n << std::endl; - if( n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_EMP ){ - //get the reference type (will compute d_type_references) - int card = 0; - TypeNode tn = computeReferenceType( n, card ); - Trace("sep-pp") << " reference type is " << tn << ", card is " << card << std::endl; - }else{ - for( unsigned i=0; i >& visited, + std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, + bool pol, bool hasPol, bool underSpatial ) { + int index = hasPol ? ( pol ? 1 : -1 ) : 0; + int card = 0; + std::map< Node, int >::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 ){ + TypeNode tn = n[0].getType(); + TypeNode tnd = n[1].getType(); + registerRefDataTypes( tn, tnd, n ); + if( hasPol && pol ){ + references[index][n].clear(); + references_strict[index][n] = true; + }else{ + card = 1; } - } - } -} - -TypeNode TheorySep::computeReferenceType( Node atom, int& card, int index ) { - Trace("sep-pp-debug") << "getReference type " << atom << " " << index << std::endl; - Assert( atom.getKind()==kind::SEP_PTO || atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND || atom.getKind()==kind::SEP_EMP || index!=-1 ); - std::map< int, TypeNode >::iterator it = d_reference_type[atom].find( index ); - if( it==d_reference_type[atom].end() ){ - card = 0; - TypeNode tn; - if( index==-1 && ( atom.getKind()==kind::SEP_STAR || atom.getKind()==kind::SEP_WAND ) ){ - for( unsigned i=0; i visited; - tn = computeReferenceType2( atom, card, index, n, visited ); - } - if( tn.isNull() && index==-1 ){ - tn = NodeManager::currentNM()->booleanType(); - } - d_reference_type[atom][index] = tn; - d_reference_type_card[atom][index] = card; - Trace("sep-type") << "...ref type return " << card << " for " << atom << " " << index << std::endl; - //add to d_type_references - if( index==-1 ){ - //only contributes if top-level (index=-1) - for( unsigned i=0; icard ){ + card = ccard; + } + //track references if we are or below a spatial operator + if( newUnderSpatial ){ + bool add = true; + if( references_strict[newIndex].find( n[i] )!=references_strict[newIndex].end() ){ + if( !isSpatial ){ + if( references_strict[index].find( n )==references_strict[index].end() ){ + references_strict[index][n] = true; + }else{ + add = false; + //TODO: can derive static equality between sets + } + } + }else{ + if( isSpatial ){ + refStrict = false; + } + } + if( add ){ + for( unsigned j=0; j(int)d_card_max[tn] ){ - d_card_max[tn] = card; + if( isSpatial && refStrict ){ + if( n.getKind()==kind::SEP_WAND ){ + //TODO + }else{ + Assert( n.getKind()==kind::SEP_STAR && hasPol && pol ); + references_strict[index][n] = true; + } } } - return tn; + visited[index][n] = card; }else{ - Assert( d_reference_type_card[atom].find( index )!=d_reference_type_card[atom].end() ); - card = d_reference_type_card[atom][index]; - return it->second; + card = it->second; } -} - -TypeNode TheorySep::computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited ) { - if( visited.find( n )==visited.end() ){ - Trace("sep-pp-debug") << "visit : " << n << " : " << atom << " " << index << std::endl; - visited[n] = -1; - if( n.getKind()==kind::SEP_PTO ){ - //TODO: when THEORY_SETS supports mixed Int/Real sets - //TypeNode tn1 = n[0].getType().getBaseType(); - //TypeNode tn2 = n[1].getType().getBaseType(); - TypeNode tn1 = n[0].getType(); - TypeNode tn2 = n[1].getType(); - if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){ - if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){ - // still valid : bound on heap models will include Herbrand universe of n[0].getType() - d_reference_bound_fv[tn1] = true; - }else{ - d_reference_bound_invalid[tn1] = true; - Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl; - } + + if( !underSpatial && ( !references[index][n].empty() || card>0 ) ){ + TypeNode tn = getReferenceType( n ); + Assert( !tn.isNull() ); + // add references to overall type + unsigned bt = d_bound_kind[tn]; + 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; }else{ - if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), n[0] )==d_references[atom][index].end() ){ - d_references[atom][index].push_back( n[0] ); - } - } - registerRefDataTypes( tn1, tn2, atom ); - card = 1; - visited[n] = card; - return tn1; - }else if( n.getKind()==kind::SEP_EMP ){ - TypeNode tn = n[0].getType(); - TypeNode tnd = n[1].getType(); - registerRefDataTypes( tn, tnd, atom ); - card = 1; - visited[n] = card; - return tn; - }else if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND ){ - Assert( n!=atom ); - //get the references - card = 0; - TypeNode tn = computeReferenceType( n, card ); - for( unsigned j=0; jcard ? cardc : card; + add = bt!=bound_strict; + } + for( unsigned i=0; i(int)d_card_max[tn] ){ + d_card_max[tn] = card; } - visited[n] = card; - return otn; } - }else{ - Trace("sep-type-debug") << "already visit : " << n << " : " << atom << " " << index << std::endl; - card = 0; - return TypeNode::null(); } + return card; } void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){ @@ -1067,6 +1059,7 @@ void TheorySep::registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ){ //for now, we only allow heap constraints of one type d_type_ref = tn1; d_type_data = tn2; + d_bound_kind[tn1] = bound_default; }else{ if( !tn2.isNull() ){ if( itt->second!=tn2 ){ @@ -1095,30 +1088,28 @@ void TheorySep::initializeBounds() { Trace("sep-bound") << "Initialize bounds for " << tn << "..." << std::endl; QuantEPR * qepr = getLogicInfo().isQuantified() ? getQuantifiersEngine()->getQuantEPR() : NULL; //if pto had free variable reference - if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ - if( d_reference_bound_fv.find( tn )!=d_reference_bound_fv.end() ){ - //include Herbrand universe of tn - if( qepr && qepr->isEPR( tn ) ){ - for( unsigned j=0; jd_consts[tn].size(); j++ ){ - Node k = qepr->d_consts[tn][j]; - if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){ - d_type_references[tn].push_back( k ); - } + if( d_bound_kind[tn]==bound_herbrand ){ + //include Herbrand universe of tn + if( qepr && qepr->isEPR( tn ) ){ + for( unsigned j=0; jd_consts[tn].size(); j++ ){ + Node k = qepr->d_consts[tn][j]; + if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), k )==d_type_references[tn].end() ){ + d_type_references[tn].push_back( k ); } - }else{ - d_reference_bound_invalid[tn] = true; - Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl; } + }else{ + d_bound_kind[tn] = bound_invalid; + Trace("sep-bound") << "reference cannot be bound (due to non-EPR variable)." << std::endl; } } unsigned n_emp = 0; - if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){ - n_emp = d_card_max[tn]>d_card_max[TypeNode::null()] ? d_card_max[tn] : d_card_max[TypeNode::null()]; + 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 + //must include at least one constant TODO: remove? n_emp = 1; } - Trace("sep-bound") << "Card maximums : " << d_card_max[tn] << " " << d_card_max[TypeNode::null()] << std::endl; + 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; rlemma( slem ); //symmetry breaking - std::map< unsigned, Node > lit_mem_map; - for( unsigned i=0; imkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound_max[tn]); - } - for( unsigned i=0; i<(d_type_references_card[tn].size()-1); i++ ){ - std::vector< Node > children; - for( unsigned j=(i+1); j1 ){ + std::map< unsigned, Node > lit_mem_map; + for( unsigned i=0; imkNode( kind::MEMBER, d_type_references_card[tn][i], d_reference_bound_max[tn]); + } + 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_out->lemma( sym_lem ); + } } - Assert( !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_out->lemma( sym_lem ); } } @@ -1266,8 +1260,7 @@ Node TheorySep::mkUnion( TypeNode tn, std::vector< Node >& locs ) { Node TheorySep::getLabel( Node atom, int child, Node lbl ) { std::map< int, Node >::iterator it = d_label_map[atom][lbl].find( child ); if( it==d_label_map[atom][lbl].end() ){ - int card; - TypeNode refType = computeReferenceType( atom, card ); + TypeNode refType = getReferenceType( atom ); std::stringstream ss; ss << "__Lc" << child; TypeNode ltn = NodeManager::currentNM()->mkSetType(refType); diff --git a/src/theory/sep/theory_sep.h b/src/theory/sep/theory_sep.h index e00e075f5..816f91c5f 100644 --- a/src/theory/sep/theory_sep.h +++ b/src/theory/sep/theory_sep.h @@ -58,7 +58,9 @@ class TheorySep : public Theory { Node mkAnd( std::vector< TNode >& assumptions ); - void processAssertion( Node n, std::map< Node, bool >& visited ); + int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited, + std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict, + bool pol, bool hasPol, bool underSpatial ); public: @@ -200,10 +202,6 @@ class TheorySep : public Theory { std::map< Node, std::map< Node, Node > > d_neg_guard; std::vector< Node > d_neg_guards; std::map< Node, Node > d_guard_to_assertion; - //cache for references - std::map< Node, std::map< int, TypeNode > > d_reference_type; - std::map< Node, std::map< int, int > > d_reference_type_card; - std::map< Node, std::map< int, std::vector< Node > > > d_references; /** inferences: maintained to ensure ref count for internally introduced nodes */ NodeList d_infer; NodeList d_infer_exp; @@ -220,9 +218,16 @@ class TheorySep : public Theory { //reference bound std::map< TypeNode, Node > d_reference_bound; std::map< TypeNode, Node > d_reference_bound_max; - std::map< TypeNode, bool > d_reference_bound_invalid; - std::map< TypeNode, bool > d_reference_bound_fv; std::map< TypeNode, std::vector< Node > > d_type_references; + //kind of bound for reference types + enum { + bound_strict, + bound_default, + bound_herbrand, + bound_invalid, + }; + std::map< TypeNode, unsigned > d_bound_kind; + std::map< TypeNode, std::vector< Node > > d_type_references_card; std::map< Node, unsigned > d_type_ref_card_id; std::map< TypeNode, std::vector< Node > > d_type_references_all; @@ -250,9 +255,6 @@ class TheorySep : public Theory { //get global reference/data type TypeNode getReferenceType( Node n ); TypeNode getDataType( Node n ); - //calculate the element type of the heap for spatial assertions - TypeNode computeReferenceType( Node atom, int& card, int index = -1 ); - TypeNode computeReferenceType2( Node atom, int& card, int index, Node n, std::map< Node, int >& visited); void registerRefDataTypes( TypeNode tn1, TypeNode tn2, Node atom ); //get location/data type //get the base label for the spatial assertion diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 51e3fe703..b52c225aa 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -285,6 +285,72 @@ bool TheorySetsPrivate::isMember( Node x, Node s ) { } return false; } + +bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) { + Assert( d_equalityEngine.hasTerm( r1 ) && d_equalityEngine.getRepresentative( r1 )==r1 ); + Assert( d_equalityEngine.hasTerm( r2 ) && d_equalityEngine.getRepresentative( r2 )==r2 ); + TypeNode tn = r1.getType(); + Node eqc_es = d_eqc_emptyset[tn]; + bool is_sat = false; + for( unsigned e=0; e<2; e++ ){ + Node a = e==0 ? r1 : r2; + Node b = e==0 ? r2 : r1; + //if there are members in a + std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a ); + if( itpma!=d_pol_mems[0].end() ){ + Assert( !itpma->second.empty() ); + //if b is empty + if( b==eqc_es ){ + if( !itpma->second.empty() ){ + is_sat = true; + Trace("sets-deq") << "Disequality is satisfied because members are in " << a << " and " << b << " is empty" << std::endl; + }else{ + //a should not be singleton + Assert( d_eqc_singleton.find( a )==d_eqc_singleton.end() ); + } + }else{ + std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b ); + std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b ); + std::vector< Node > prev; + for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){ + //if b is a singleton + if( itsb!=d_eqc_singleton.end() ){ + if( ee_areDisequal( itm->first, itsb->second[0] ) ){ + Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << ", singleton eq " << itsb->second[0] << std::endl; + is_sat = true; + } + //or disequal with another member + for( unsigned k=0; kfirst, prev[k] ) ){ + Trace("sets-deq") << "Disequality is satisfied because of disequal members " << itm->first << " " << prev[k] << ", singleton eq " << std::endl; + is_sat = true; + break; + } + } + //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality ) + //if a has positive member that is negative member in b + }else if( itpmb!=d_pol_mems[1].end() ){ + for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){ + if( ee_areEqual( itm->first, itnm->first ) ){ + Trace("sets-deq") << "Disequality is satisfied because of " << itm->second << " " << itnm->second << std::endl; + is_sat = true; + break; + } + } + } + if( is_sat ){ + break; + } + prev.push_back( itm->first ); + } + } + if( is_sat ){ + break; + } + } + } + return is_sat; +} bool TheorySetsPrivate::assertFact( Node fact, Node exp ){ Trace("sets-assert") << "TheorySets::assertFact : " << fact << ", exp = " << exp << std::endl; @@ -757,62 +823,18 @@ void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { for(NodeBoolMap::const_iterator it=d_deq.begin(); it !=d_deq.end(); ++it) { if( (*it).second ){ Node deq = (*it).first; - bool is_sat = false; //check if it is already satisfied Assert( d_equalityEngine.hasTerm( deq[0] ) && d_equalityEngine.hasTerm( deq[1] ) ); Node r1 = d_equalityEngine.getRepresentative( deq[0] ); Node r2 = d_equalityEngine.getRepresentative( deq[1] ); - TypeNode tn = r1.getType(); - Node eqc_es = d_eqc_emptyset[tn]; - for( unsigned e=0; e<2; e++ ){ - Node a = e==0 ? r1 : r2; - Node b = e==0 ? r2 : r1; - //if there are members in a - std::map< Node, std::map< Node, Node > >::iterator itpma = d_pol_mems[0].find( a ); - if( itpma!=d_pol_mems[0].end() ){ - Assert( !itpma->second.empty() ); - //if b is empty - if( b==eqc_es ){ - if( !itpma->second.empty() ){ - is_sat = true; - Trace("sets-deq") << "Disequality " << deq << " is satisfied because members are in " << a << " and " << b << " is empty" << std::endl; - } - }else{ - std::map< Node, Node >::iterator itsb = d_eqc_singleton.find( b ); - std::map< Node, std::map< Node, Node > >::iterator itpmb = d_pol_mems[1].find( b ); - for( std::map< Node, Node >::iterator itm = itpma->second.begin(); itm != itpma->second.end(); ++itm ){ - //if b is a singleton - if( false && itsb!=d_eqc_singleton.end() ){ - //TODO? - //if a has positive member that is negative member in b - }else if( itpmb!=d_pol_mems[1].end() ){ - for( std::map< Node, Node >::iterator itnm = itpmb->second.begin(); itnm != itpmb->second.end(); ++itnm ){ - if( ee_areEqual( itm->first, itnm->first ) ){ - Trace("sets-deq") << "Disequality " << deq << " is satisfied because of " << itm->second << " " << itnm->second << std::endl; - is_sat = true; - break; - } - } - } - if( is_sat ){ - break; - } - } - } - if( is_sat ){ - break; - } - } - } + bool is_sat = isSetDisequalityEntailed( r1, r2 ); /* if( !is_sat ){ //try to make one of them empty for( unsigned e=0; e<2; e++ ){ - } } */ - Trace("sets-debug") << "Check disequality " << deq << ", is_sat = " << is_sat << std::endl; //will process regardless of sat/processed/unprocessed d_deq[deq] = false; diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 25a15a84a..8a6eaac2f 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -73,6 +73,7 @@ private: void checkUpwardsClosure( std::vector< Node >& lemmas ); void checkDisequalities( std::vector< Node >& lemmas ); bool isMember( Node x, Node s ); + bool isSetDisequalityEntailed( Node s, Node t ); void flushLemmas( std::vector< Node >& lemmas ); Node getProxy( Node n ); -- 2.30.2