summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/quantifiers/quant_util.cpp4
-rw-r--r--src/theory/sep/theory_sep.cpp313
-rw-r--r--src/theory/sep/theory_sep.h22
-rw-r--r--src/theory/sets/theory_sets_private.cpp112
-rw-r--r--src/theory/sets/theory_sets_private.h1
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.size(); i++ ){
Trace("sep-pp") << "Process assertion : " << assertions[i] << std::endl;
- processAssertion( assertions[i], visited );
+ 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() ){
@@ -898,148 +900,138 @@ void TheorySep::ppNotifyAssertions( std::vector< Node >& 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<n.getNumChildren(); i++ ){
- processAssertion( n[i], visited );
+//return cardinality
+int TheorySep::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 ) {
+ 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<atom.getNumChildren(); i++ ){
- int cardc = 0;
- TypeNode ctn = computeReferenceType( atom, cardc, i );
- if( !ctn.isNull() ){
- tn = ctn;
- }
- for( unsigned j=0; j<d_references[atom][i].size(); j++ ){
- if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[atom][i][j] )==d_references[atom][index].end() ){
- d_references[atom][index].push_back( d_references[atom][i][j] );
+ }else if( n.getKind()==kind::SEP_PTO ){
+ TypeNode tn1 = n[0].getType();
+ TypeNode tn2 = n[1].getType();
+ registerRefDataTypes( tn1, tn2, n );
+ if( quantifiers::TermDb::hasBoundVarAttr( n[0] ) ){
+ if( d_bound_kind[tn1]!=bound_strict && d_bound_kind[tn1]!=bound_invalid ){
+ if( options::quantEpr() && n[0].getKind()==kind::BOUND_VARIABLE ){
+ // still valid : bound on heap models will include Herbrand universe of n[0].getType()
+ d_bound_kind[tn1] = bound_herbrand;
+ }else{
+ d_bound_kind[tn1] = bound_invalid;
+ Trace("sep-bound") << "reference cannot be bound (due to quantified pto)." << std::endl;
}
}
- card = card + cardc;
+ }else{
+ references[index][n].push_back( n[0] );
+ }
+ if( hasPol && pol ){
+ references_strict[index][n] = true;
+ }else{
+ card = 1;
}
}else{
- Node n = index==-1 ? atom : atom[index];
- //will compute d_references as well
- std::map< Node, int > 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; i<d_references[atom][index].size(); i++ ){
- Assert( !d_references[atom][index][i].isNull() );
- if( std::find( d_type_references[tn].begin(), d_type_references[tn].end(), d_references[atom][index][i] )==d_type_references[tn].end() ){
- d_type_references[tn].push_back( d_references[atom][index][i] );
+ bool isSpatial = n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_STAR;
+ bool newUnderSpatial = underSpatial || isSpatial;
+ bool refStrict = isSpatial;
+ for( unsigned i=0; i<n.getNumChildren(); 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 );
+ //update cardinality
+ if( n.getKind()==kind::SEP_STAR ){
+ card += ccard;
+ }else if( n.getKind()==kind::SEP_WAND ){
+ if( i==1 ){
+ card = ccard;
+ }
+ }else if( ccard>card ){
+ 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<references[newIndex][n[i]].size(); j++ ){
+ if( std::find( references[index][n].begin(), references[index][n].end(), references[newIndex][n[i]][j] )==references[index][n].end() ){
+ references[index][n].push_back( references[newIndex][n[i]][j] );
+ }
+ }
+ }
}
}
- // update maximum cardinality value
- if( card>(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; j<d_references[n][-1].size(); j++ ){
- if( std::find( d_references[atom][index].begin(), d_references[atom][index].end(), d_references[n][-1][j] )==d_references[atom][index].end() ){
- d_references[atom][index].push_back( d_references[n][-1][j] );
- }
+ //TODO: derive static equality
+ add = false;
}
- visited[n] = card;
- return tn;
- }else if( n.getKind()==kind::SEP_NIL ){
- TypeNode tn = n.getType();
- TypeNode tnd;
- registerRefDataTypes( tn, tnd, n );
- return tn;
}else{
- card = 0;
- TypeNode otn;
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- int cardc = 0;
- TypeNode tn = computeReferenceType2( atom, cardc, index, n[i], visited );
- if( !tn.isNull() ){
- otn = tn;
- }
- card = cardc>card ? cardc : card;
+ 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] );
+ }
+ }
+ if( add ){
+ //add max cardinality
+ if( card>(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; j<qepr->d_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; j<qepr->d_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; r<n_emp; r++ ){
@@ -1183,9 +1174,9 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
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() );
+ //Assert( !d_type_references_all[tn].empty() );
- if( d_reference_bound_invalid.find( tn )==d_reference_bound_invalid.end() ){
+ if( d_bound_kind[tn]!=bound_invalid ){
//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;
@@ -1198,20 +1189,23 @@ Node TheorySep::getBaseLabel( TypeNode tn ) {
//d_out->lemma( slem );
//symmetry breaking
- 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::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); j<d_type_references_card[tn].size(); j++ ){
- children.push_back( lit_mem_map[j].negate() );
+ 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::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); 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_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; k<prev.size(); k++ ){
+ if( ee_areDisequal( itm->first, 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 );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback