summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp38
-rw-r--r--src/theory/datatypes/theory_datatypes.h1
-rw-r--r--src/theory/sets/theory_sets_private.cpp37
-rw-r--r--src/theory/sets/theory_sets_private.h1
-rw-r--r--src/theory/strings/theory_strings.cpp31
-rw-r--r--src/theory/strings/theory_strings.h1
-rw-r--r--src/theory/uf/theory_uf.cpp31
-rw-r--r--src/theory/uf/theory_uf.h1
8 files changed, 96 insertions, 45 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index d285f292a..11903f863 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1316,20 +1316,13 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::
Assert( d_equalityEngine.hasTerm(x) );
Assert( d_equalityEngine.hasTerm(y) );
Assert( !areDisequal( x, y ) );
+ Assert( !areCareDisequal( x, y ) );
if( !d_equalityEngine.areEqual( x, y ) ){
Trace("dt-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
- Trace("dt-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
- EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- Trace("dt-cg") << "...eq status is " << eqStatus << std::endl;
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- //an argument is disequal, we are done
- return;
- }else{
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
+ currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
}
@@ -1353,8 +1346,10 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::
std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !areDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ }
}
}
}
@@ -1362,8 +1357,10 @@ void TheoryDatatypes::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::
//add care pairs based on product of indices, non-disequal arguments
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !areDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ }
}
}
}
@@ -2032,10 +2029,25 @@ bool TheoryDatatypes::areDisequal( TNode a, TNode b ){
}else if( hasTerm( a ) && hasTerm( b ) ){
return d_equalityEngine.areDisequal( a, b, false );
}else{
+ //TODO : constants here?
return false;
}
}
+bool TheoryDatatypes::areCareDisequal( TNode x, TNode y ) {
+ Assert( d_equalityEngine.hasTerm( x ) );
+ Assert( d_equalityEngine.hasTerm( y ) );
+ if( d_equalityEngine.isTriggerTerm(x, THEORY_DATATYPES) && d_equalityEngine.isTriggerTerm(y, THEORY_DATATYPES) ){
+ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_DATATYPES);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_DATATYPES);
+ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
+ return true;
+ }
+ }
+ return false;
+}
+
TNode TheoryDatatypes::getRepresentative( TNode a ){
if( hasTerm( a ) ){
return d_equalityEngine.getRepresentative( a );
diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h
index 770c3a9d4..fffc4bdd7 100644
--- a/src/theory/datatypes/theory_datatypes.h
+++ b/src/theory/datatypes/theory_datatypes.h
@@ -317,6 +317,7 @@ private:
bool hasTerm( TNode a );
bool areEqual( TNode a, TNode b );
bool areDisequal( TNode a, TNode b );
+ bool areCareDisequal( TNode x, TNode y );
TNode getRepresentative( TNode a );
};/* class TheoryDatatypes */
diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e53fec02f..7662f1544 100644
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -243,6 +243,18 @@ bool TheorySetsPrivate::ee_areDisequal( Node a, Node b ) {
}
}
+bool TheorySetsPrivate::ee_areCareDisequal( Node a, Node b ) {
+ if( d_equalityEngine.isTriggerTerm(a, THEORY_SETS) && d_equalityEngine.isTriggerTerm(b, THEORY_SETS) ){
+ TNode a_shared = d_equalityEngine.getTriggerTermRepresentative(a, THEORY_SETS);
+ TNode b_shared = d_equalityEngine.getTriggerTermRepresentative(b, THEORY_SETS);
+ EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
+ return true;
+ }
+ }
+ return false;
+}
+
bool TheorySetsPrivate::isEntailed( Node n, bool polarity ) {
if( n.getKind()==kind::NOT ){
return isEntailed( n[0], !polarity );
@@ -332,7 +344,7 @@ bool TheorySetsPrivate::isSetDisequalityEntailed( Node r1, Node r2 ) {
break;
}
}
- //TODO: this can be generalized : maintain map to abstract domain ( set -> cardinality )
+ //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 ){
@@ -1617,20 +1629,13 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers
Assert( d_equalityEngine.hasTerm(x) );
Assert( d_equalityEngine.hasTerm(y) );
Assert( !ee_areDisequal( x, y ) );
+ Assert( !ee_areCareDisequal( x, y ) );
if( !d_equalityEngine.areEqual( x, y ) ){
Trace("sets-cg") << "Arg #" << k << " is " << x << " " << y << std::endl;
if( d_equalityEngine.isTriggerTerm(x, THEORY_SETS) && d_equalityEngine.isTriggerTerm(y, THEORY_SETS) ){
TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_SETS);
TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_SETS);
- Trace("sets-cg") << "Arg #" << k << " shared term is " << x_shared << " " << y_shared << std::endl;
- EqualityStatus eqStatus = d_external.d_valuation.getEqualityStatus(x_shared, y_shared);
- Trace("sets-cg") << "...eq status is " << eqStatus << std::endl;
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- //an argument is disequal, we are done
- return;
- }else{
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
+ currentPairs.push_back(make_pair(x_shared, y_shared));
}else if( isCareArg( f1, k ) && isCareArg( f2, k ) ){
//splitting on sets (necessary for handling set of sets properly)
if( x.getType().isSet() ){
@@ -1663,8 +1668,10 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers
std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it;
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
- if( !ee_areDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if( !ee_areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ }
}
}
}
@@ -1672,8 +1679,10 @@ void TheorySetsPrivate::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers
//add care pairs based on product of indices, non-disequal arguments
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
- if( !ee_areDisequal(it->first, it2->first) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
+ if( !ee_areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs );
+ }
}
}
}
diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h
index 6d7b57cc6..affc09fb9 100644
--- a/src/theory/sets/theory_sets_private.h
+++ b/src/theory/sets/theory_sets_private.h
@@ -56,6 +56,7 @@ public:
private:
bool ee_areEqual( Node a, Node b );
bool ee_areDisequal( Node a, Node b );
+ bool ee_areCareDisequal( Node a, Node b );
NodeIntMap d_members;
std::map< Node, std::vector< Node > > d_members_data;
bool assertFact( Node fact, Node exp );
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp
index 45a6a93d1..b0a9e6a1f 100644
--- a/src/theory/strings/theory_strings.cpp
+++ b/src/theory/strings/theory_strings.cpp
@@ -183,6 +183,20 @@ bool TheoryStrings::areDisequal( Node a, Node b ){
}
}
+bool TheoryStrings::areCareDisequal( TNode x, TNode y ) {
+ Assert( d_equalityEngine.hasTerm(x) );
+ Assert( d_equalityEngine.hasTerm(y) );
+ if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
+ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
+ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
+ return true;
+ }
+ }
+ return false;
+}
+
Node TheoryStrings::getLengthExp( Node t, std::vector< Node >& exp, Node te ){
Assert( areEqual( t, te ) );
Node lt = mkLength( te );
@@ -894,17 +908,12 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
Assert( d_equalityEngine.hasTerm(x) );
Assert( d_equalityEngine.hasTerm(y) );
Assert( !d_equalityEngine.areDisequal( x, y, false ) );
+ Assert( !areCareDisequal( x, y ) );
if( !d_equalityEngine.areEqual( x, y ) ){
if( d_equalityEngine.isTriggerTerm(x, THEORY_STRINGS) && d_equalityEngine.isTriggerTerm(y, THEORY_STRINGS) ){
TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_STRINGS);
TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_STRINGS);
- EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- //an argument is disequal, we are done
- return;
- }else{
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
+ currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
}
@@ -928,7 +937,9 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ }
}
}
}
@@ -937,7 +948,9 @@ void TheoryStrings::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::Te
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ }
}
}
}
diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h
index 0294c3884..ab0256237 100644
--- a/src/theory/strings/theory_strings.h
+++ b/src/theory/strings/theory_strings.h
@@ -141,6 +141,7 @@ private:
bool hasTerm( Node a );
bool areEqual( Node a, Node b );
bool areDisequal( Node a, Node b );
+ bool areCareDisequal( TNode x, TNode y );
// t is representative, te = t, add lt = te to explanation exp
Node getLengthExp( Node t, std::vector< Node >& exp, Node te );
Node getLength( Node t, std::vector< Node >& exp );
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 35aee5305..1b47b0245 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -438,6 +438,20 @@ void TheoryUF::addSharedTerm(TNode t) {
d_equalityEngine.addTriggerTerm(t, THEORY_UF);
}
+bool TheoryUF::areCareDisequal(TNode x, TNode y){
+ Assert( d_equalityEngine.hasTerm(x) );
+ Assert( d_equalityEngine.hasTerm(y) );
+ if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
+ TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
+ TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
+ EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
+ if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
+ return true;
+ }
+ }
+ return false;
+}
+
//TODO: move quantifiers::TermArgTrie to src/theory/
void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){
if( depth==arity ){
@@ -453,17 +467,12 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
Assert( d_equalityEngine.hasTerm(x) );
Assert( d_equalityEngine.hasTerm(y) );
Assert( !d_equalityEngine.areDisequal( x, y, false ) );
+ Assert( !areCareDisequal( x, y ) );
if( !d_equalityEngine.areEqual( x, y ) ){
if( d_equalityEngine.isTriggerTerm(x, THEORY_UF) && d_equalityEngine.isTriggerTerm(y, THEORY_UF) ){
TNode x_shared = d_equalityEngine.getTriggerTermRepresentative(x, THEORY_UF);
TNode y_shared = d_equalityEngine.getTriggerTermRepresentative(y, THEORY_UF);
- EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
- if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
- //an argument is disequal, we are done
- return;
- }else{
- currentPairs.push_back(make_pair(x_shared, y_shared));
- }
+ currentPairs.push_back(make_pair(x_shared, y_shared));
}
}
}
@@ -487,7 +496,9 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
++it2;
for( ; it2 != t1->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ }
}
}
}
@@ -496,7 +507,9 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){
for( std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = t2->d_data.begin(); it2 != t2->d_data.end(); ++it2 ){
if( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){
- addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ if( !areCareDisequal(it->first, it2->first) ){
+ addCarePairs( &it->second, &it2->second, arity, depth+1 );
+ }
}
}
}
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index ce9c70ca2..41bafcb84 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -210,6 +210,7 @@ public:
return d_thss;
}
private:
+ bool areCareDisequal(TNode x, TNode y);
void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
};/* class TheoryUF */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback