From 905dc2b51fd0145e0bb69a166c06a1731ef4c44b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 09:48:01 -0500 Subject: Simplify and fix care graph for ufHo (#4924) We now separate APPLY_UF and HO_APPLY. We do not generate care pairs based on comparing APPLY_UF terms with HO_APPLY terms, which led to type errors previously. Fixes #4990. --- src/theory/uf/theory_uf.cpp | 113 ++++++++++++++++++++++++-------------------- src/theory/uf/theory_uf.h | 13 +---- 2 files changed, 63 insertions(+), 63 deletions(-) (limited to 'src/theory') diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index c8ae3d844..0b97d8a5d 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -200,20 +200,6 @@ void TheoryUF::check(Effort level) { } }/* TheoryUF::check() */ -Node TheoryUF::getOperatorForApplyTerm( TNode node ) { - Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY); - if( node.getKind()==kind::APPLY_UF ){ - return node.getOperator(); - }else{ - return d_equalityEngine->getRepresentative(node[0]); - } -} - -unsigned TheoryUF::getArgumentStartIndexForApplyTerm( TNode node ) { - Assert(node.getKind() == kind::APPLY_UF || node.getKind() == kind::HO_APPLY); - return node.getKind()==kind::APPLY_UF ? 0 : 1; -} - TrustNode TheoryUF::expandDefinition(Node node) { Trace("uf-exp-def") << "TheoryUF::expandDefinition: expanding definition : " @@ -543,8 +529,8 @@ bool TheoryUF::areCareDisequal(TNode x, TNode y){ return false; } -void TheoryUF::addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, +void TheoryUF::addCarePairs(const TNodeTrie* t1, + const TNodeTrie* t2, unsigned arity, unsigned depth) { @@ -556,8 +542,8 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, { Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl; vector< pair > currentPairs; - unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 ); - for (unsigned k = arg_start_index; k < f1.getNumChildren(); ++ k) { + for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k) + { TNode x = f1[k]; TNode y = f2[k]; Assert(d_equalityEngine->hasTerm(x)); @@ -587,17 +573,17 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, if( t2==NULL ){ if( depth<(arity-1) ){ //add care pairs internal to each child - for (std::pair& tt : t1->d_data) + for (const std::pair& tt : t1->d_data) { addCarePairs(&tt.second, NULL, arity, depth + 1); } } //add care pairs based on each pair of non-disequal arguments - for (std::map::iterator it = t1->d_data.begin(); + for (std::map::const_iterator it = t1->d_data.begin(); it != t1->d_data.end(); ++it) { - std::map::iterator it2 = it; + std::map::const_iterator it2 = it; ++it2; for( ; it2 != t1->d_data.end(); ++it2 ){ if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) @@ -610,9 +596,9 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, } }else{ //add care pairs based on product of indices, non-disequal arguments - for (std::pair& tt1 : t1->d_data) + for (const std::pair& tt1 : t1->d_data) { - for (std::pair& tt2 : t2->d_data) + for (const std::pair& tt2 : t2->d_data) { if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) { @@ -628,40 +614,63 @@ void TheoryUF::addCarePairs(TNodeTrie* t1, } void TheoryUF::computeCareGraph() { - - if (d_sharedTerms.size() > 0) { - //use term indexing - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl; - std::map 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 = getOperatorForApplyTerm( f1 ); - unsigned arg_start_index = getArgumentStartIndexForApplyTerm( f1 ); - std::vector< TNode > reps; - bool has_trigger_arg = false; - for( unsigned j=arg_start_index; jgetRepresentative(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(); + if (d_sharedTerms.empty()) + { + return; + } + // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY. + // We maintain indices per operator for the former, and indices per + // function type for the latter. + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." + << std::endl; + std::map index; + std::map hoIndex; + std::map arity; + for (TNode app : d_functionsTerms) + { + std::vector reps; + bool has_trigger_arg = false; + for (const Node& j : app) + { + reps.push_back(d_equalityEngine->getRepresentative(j)); + if (d_equalityEngine->isTriggerTerm(j, THEORY_UF)) + { + has_trigger_arg = true; } } - //for each index - for (std::pair& tt : index) + if (has_trigger_arg) { - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " - << tt.first << "..." << std::endl; - addCarePairs(&tt.second, nullptr, arity[tt.first], 0); + if (app.getKind() == kind::APPLY_UF) + { + Node op = app.getOperator(); + index[op].addTerm(app, reps); + arity[op] = reps.size(); + } + else + { + Assert(app.getKind() == kind::HO_APPLY); + // add it to the hoIndex for the function type + hoIndex[app[0].getType()].addTerm(app, reps); + } } - Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." << std::endl; } + // for each index + for (std::pair& tt : index) + { + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index " + << tt.first << "..." << std::endl; + Assert(arity.find(tt.first) != arity.end()); + addCarePairs(&tt.second, nullptr, arity[tt.first], 0); + } + for (std::pair& tt : hoIndex) + { + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index " + << tt.first << "..." << std::endl; + // the arity of HO_APPLY is always two + addCarePairs(&tt.second, nullptr, 2, 0); + } + Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished." + << std::endl; }/* TheoryUF::computeCareGraph() */ void TheoryUF::conflict(TNode a, TNode b) { diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 4d0a3126f..7d17fdb86 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -150,15 +150,6 @@ private: /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); - private: - /** get the operator for this node (node should be either APPLY_UF or - * HO_APPLY) - */ - Node getOperatorForApplyTerm(TNode node); - /** get the starting index of the arguments for node (node should be either - * APPLY_UF or HO_APPLY) */ - unsigned getArgumentStartIndexForApplyTerm(TNode node); - public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ @@ -211,8 +202,8 @@ private: private: bool areCareDisequal(TNode x, TNode y); - void addCarePairs(TNodeTrie* t1, - TNodeTrie* t2, + void addCarePairs(const TNodeTrie* t1, + const TNodeTrie* t2, unsigned arity, unsigned depth); -- cgit v1.2.3