From: Andrew Reynolds Date: Wed, 23 Feb 2022 03:12:06 +0000 (-0600) Subject: Fix issue in datatypes care graph computation involving subtyping (#8125) X-Git-Tag: cvc5-1.0.0~404 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f039c2a0eaf7ce44af9e8b8df64960cf0c409478;p=cvc5.git Fix issue in datatypes care graph computation involving subtyping (#8125) The datatypes care graph was incorrectly computed for constructors taking `Real` arguments, due to subtyping. This fixes the term index to cache on the *return* type for constructors, not the argument types. Caching based on argument types was incorrect even for non-parametric datatypes with arguments that have subtyping. Fixes https://github.com/cvc5/cvc5/issues/8124. This also does minor cleanup and additions done while debugging the issue. --- diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp index 9a55d8377..542dfc906 100644 --- a/src/printer/ast/ast_printer.cpp +++ b/src/printer/ast/ast_printer.cpp @@ -136,23 +136,37 @@ void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const void AstPrinter::toStream(std::ostream& out, const smt::Model& m) const { - out << "Model()"; + out << "Model(" << std::endl; + this->Printer::toStream(out, m); + out << ")" << std::endl; } void AstPrinter::toStreamModelSort(std::ostream& out, TypeNode tn, const std::vector& elements) const { - // shouldn't be called; only the non-Command* version above should be - Unreachable(); + out << "(" << tn << "("; + bool firstTime = true; + for (const Node& elem : elements) + { + if (firstTime) + { + firstTime = false; + } + else + { + out << " "; + } + out << elem; + } + out << "))" << std::endl; } void AstPrinter::toStreamModelTerm(std::ostream& out, const Node& n, const Node& value) const { - // shouldn't be called; only the non-Command* version above should be - Unreachable(); + out << "(" << n << " " << value << ")" << std::endl; } void AstPrinter::toStreamCmdEmpty(std::ostream& out, diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a689be7c5..8854db877 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1057,79 +1057,93 @@ void TheoryDatatypes::addCarePairs(TNodeTrie* t1, unsigned depth, unsigned& n_pairs) { + Trace("dt-cg") << "Process at depth " << depth << "/" << arity << std::endl; if( depth==arity ){ - if( t2!=NULL ){ - Node f1 = t1->getData(); - Node f2 = t2->getData(); - if( !areEqual( f1, f2 ) ){ - Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; - vector< pair > 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(!areDisequal(x, y)); - Assert(!areCareDisequal(x, y)); - if (!d_equalityEngine->areEqual(x, y)) + Assert(t2 != nullptr); + Node f1 = t1->getData(); + Node f2 = t2->getData(); + if (!areEqual(f1, f2)) + { + Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; + std::vector > currentPairs; + for (size_t k = 0, nchild = f1.getNumChildren(); k < nchild; ++k) + { + TNode x = f1[k]; + TNode y = f2[k]; + 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)) { - 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); - currentPairs.push_back(make_pair(x_shared, y_shared)); - } + TNode x_shared = d_equalityEngine->getTriggerTermRepresentative( + x, THEORY_DATATYPES); + TNode y_shared = d_equalityEngine->getTriggerTermRepresentative( + y, THEORY_DATATYPES); + currentPairs.push_back(make_pair(x_shared, y_shared)); } } - for (unsigned c = 0; c < currentPairs.size(); ++ c) { - Trace("dt-cg-pair") << "Pair : " << currentPairs[c].first << " " << currentPairs[c].second << std::endl; - addCarePair(currentPairs[c].first, currentPairs[c].second); - n_pairs++; - } + } + for (std::pair& p : currentPairs) + { + Trace("dt-cg-pair") + << "Pair : " << p.first << " " << p.second << std::endl; + addCarePair(p.first, p.second); + n_pairs++; } } - }else{ - if( t2==NULL ){ - if( depth<(arity-1) ){ - //add care pairs internal to each child - for (std::pair& tt : t1->d_data) - { - addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs); - } + return; + } + if (t2 == nullptr) + { + if (depth + 1 < arity) + { + // add care pairs internal to each child + for (std::pair& tt : t1->d_data) + { + Trace("dt-cg-debug") << "Traverse into arg " << tt.first << " at depth " + << depth << std::endl; + addCarePairs(&tt.second, nullptr, arity, depth + 1, n_pairs); } - //add care pairs based on each pair of non-disequal arguments - for (std::map::iterator it = t1->d_data.begin(); - it != t1->d_data.end(); - ++it) + } + // add care pairs based on each pair of non-disequal arguments + for (std::map::iterator it = t1->d_data.begin(); + it != t1->d_data.end(); + ++it) + { + std::map::iterator it2 = it; + ++it2; + for (; it2 != t1->d_data.end(); ++it2) { - std::map::iterator it2 = it; - ++it2; - for( ; it2 != t1->d_data.end(); ++it2 ){ - if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) + if (!d_equalityEngine->areDisequal(it->first, it2->first, false)) + { + if (!areCareDisequal(it->first, it2->first)) { - if( !areCareDisequal(it->first, it2->first) ){ - addCarePairs( &it->second, &it2->second, arity, depth+1, n_pairs ); - } + addCarePairs(&it->second, &it2->second, arity, depth + 1, n_pairs); } } } - }else{ - //add care pairs based on product of indices, non-disequal arguments - for (std::pair& tt1 : t1->d_data) + } + return; + } + // add care pairs based on product of indices, non-disequal arguments + for (std::pair& tt1 : t1->d_data) + { + for (std::pair& tt2 : t2->d_data) + { + if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) { - for (std::pair& tt2 : t2->d_data) + if (!areCareDisequal(tt1.first, tt2.first)) { - if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false)) - { - if (!areCareDisequal(tt1.first, tt2.first)) - { - addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); - } - } + Trace("dt-cg-debug") + << "Traverse into " << tt1.first << " " << tt2.first + << " at depth " << depth << std::endl; + addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs); } } } @@ -1148,9 +1162,13 @@ void TheoryDatatypes::computeCareGraph(){ TNode f1 = d_functionTerms[i]; Assert(d_equalityEngine->hasTerm(f1)); Trace("dt-cg-debug") << "...build for " << f1 << std::endl; - //break into index based on operator, and type of first argument (since some operators are parametric) + // Break into index based on operator. + // To handle parameteric datatypes, we also indexed based on the overall + // type if a constructor, or the type of the argument (e.g. if a selector) + // otherwise Node op = f1.getOperator(); - TypeNode tn = f1[0].getType(); + TypeNode tn = + f1.getKind() == APPLY_CONSTRUCTOR ? f1.getType() : f1[0].getType(); std::vector< TNode > reps; bool has_trigger_arg = false; for( unsigned j=0; j