From: ajreynol Date: Tue, 21 Mar 2017 21:39:25 +0000 (-0500) Subject: Improve computeCareGraph functions to check shared term equality status once per... X-Git-Tag: cvc5-1.0.0~5879 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=18d2fd549d5058a6ea3ee782568bbc3ce00189ea;p=cvc5.git Improve computeCareGraph functions to check shared term equality status once per equivalence class pair. --- 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 */