diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 13:59:13 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-05-20 13:59:20 -0500 |
commit | d5d05e4723581c86808a866af1a9f20343ed36dc (patch) | |
tree | b8b6985db8c361f4ad8a0a004ebb4596fca32824 /src/theory/uf | |
parent | 8b57c18d24caced0744d8624b3e0208aeba923ef (diff) |
Improvements to theory combination + strings: do not return trivial care graph, split on length terms for disequal strings. Term indexing for TheoryDatatypes::computeCareGraph. Minor fix in quantifiers rewriter for entailed conditions, strings cardinality.
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 96 | ||||
-rw-r--r-- | src/theory/uf/theory_uf.h | 7 |
2 files changed, 103 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 0c7bed773..5c28e4ab5 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -26,6 +26,8 @@ #include "theory/theory_model.h" #include "theory/type_enumerator.h" #include "theory/uf/theory_uf_strong_solver.h" +#include "theory/quantifiers/term_database.h" +#include "options/theory_options.h" using namespace std; @@ -431,10 +433,104 @@ void TheoryUF::addSharedTerm(TNode t) { d_equalityEngine.addTriggerTerm(t, THEORY_UF); } +/* +void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ){ + if( depth==arity ){ + if( t2!=NULL ){ + Node f1 = t1->getNodeData(); + Node f2 = t2->getNodeData(); + if( !d_equalityEngine.areEqual( f1, f2 ) ){ + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; + vector< pair<TNode, TNode> > currentPairs; + for (unsigned k = 0; k < f1.getNumChildren(); ++ k) { + TNode x = f1[k]; + TNode y = f2[k]; + Assert( d_equalityEngine.hasTerm(x) ); + Assert( d_equalityEngine.hasTerm(y) ); + Assert( !d_equalityEngine.areDisequal( x, y, false ) ); + 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)); + } + } + } + } + for (unsigned c = 0; c < currentPairs.size(); ++ c) { + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl; + addCarePair(currentPairs[c].first, currentPairs[c].second); + } + } + } + }else{ + if( t2==NULL ){ + if( depth<(arity-1) ){ + //add care pairs internal to each child + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ + addCarePairs( &it->second, NULL, arity, depth+1 ); + } + } + //add care pairs based on each pair of non-disequal arguments + for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it ){ + std::map< TNode, quantifiers::TermArgTrie >::iterator it2 = it; + ++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 ); + } + } + } + }else{ + //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( !d_equalityEngine.areDisequal(it->first, it2->first, false) ){ + addCarePairs( &it->second, &it2->second, arity, depth+1 ); + } + } + } + } + } +} +*/ + void TheoryUF::computeCareGraph() { if (d_sharedTerms.size() > 0) { +/* TODO : this does (almost) the same as below, and is 1-2 order of magnitudes faster + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; + std::map< Node, quantifiers::TermArgTrie > index; + std::map< Node, unsigned > arity; + unsigned functionTerms = d_functionsTerms.size(); + for (unsigned i = 0; i < functionTerms; ++ i) { + TNode f1 = d_functionsTerms[i]; + Node op = f1.getOperator(); + std::vector< TNode > reps; + bool has_trigger_arg = false; + for( unsigned j=0; j<f1.getNumChildren(); j++ ){ + reps.push_back( d_equalityEngine.getRepresentative( f1[j] ) ); + if( d_equalityEngine.isTriggerTerm( f1[j], THEORY_UF ) ){ + has_trigger_arg = true; + } + } + if( has_trigger_arg ){ + index[op].addTerm( f1, reps ); + arity[op] = reps.size(); + } + } + //for each index + for( std::map< Node, quantifiers::TermArgTrie >::iterator itii = index.begin(); itii != index.end(); ++itii ){ + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " << itii->first << "..." << std::endl; + addCarePairs( &itii->second, NULL, arity[ itii->first ], 0 ); + } + */ vector< pair<TNode, TNode> > currentPairs; // Go through the function terms and see if there are any to split on diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 42a804c09..ff7d7419a 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -32,6 +32,11 @@ namespace CVC4 { namespace theory { + +namespace quantifiers{ + class TermArgTrie; +} + namespace uf { class UfTermDb; @@ -204,6 +209,8 @@ public: StrongSolverTheoryUF* getStrongSolver() { return d_thss; } +//private: + //void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth ); };/* class TheoryUF */ }/* CVC4::theory::uf namespace */ |