From 35f58d81fb57608d52884f560ff281fe52c7b18f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 15 Dec 2020 14:49:33 -0600 Subject: [PATCH] Fix datatypes compute ground value (#5671) We were using the wrong cache on one call, leading to non-constant values being enumerated. Fixes #5659, for that benchmark, CVC4 now answers "unknown". --- src/expr/dtype.cpp | 21 +++++++++++++-------- src/expr/dtype_cons.cpp | 21 ++++++++++++++++----- src/theory/type_enumerator.h | 3 ++- 3 files changed, 31 insertions(+), 14 deletions(-) diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index 4c93e5727..5cb76858a 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -598,6 +598,7 @@ bool DType::computeWellFounded(std::vector& processing) const Node DType::mkGroundTerm(TypeNode t) const { + Trace("datatypes-init") << "DType::mkGroundTerm of type " << t << std::endl; Assert(isResolved()); return mkGroundTermInternal(t, false); } @@ -605,7 +606,9 @@ Node DType::mkGroundTerm(TypeNode t) const Node DType::mkGroundValue(TypeNode t) const { Assert(isResolved()); - return mkGroundTermInternal(t, true); + Trace("datatypes-init") << "DType::mkGroundValue of type " << t << std::endl; + Node v = mkGroundTermInternal(t, true); + return v; } Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const @@ -631,7 +634,8 @@ Node DType::mkGroundTermInternal(TypeNode t, bool isValue) const << "constructed: " << getName() << " => " << groundTerm << std::endl; } // if ground term is null, we are not well-founded - Trace("datatypes-init") << "DType::mkGroundTerm for " << t << " returns " + Trace("datatypes-init") << "DType::mkGroundTerm for " << t + << ", isValue=" << isValue << " returns " << groundTerm << std::endl; return groundTerm; } @@ -790,11 +794,12 @@ Node DType::computeGroundTerm(TypeNode t, { if (std::find(processing.begin(), processing.end(), t) != processing.end()) { - Debug("datatypes-gt") << "...already processing " << t << " " << d_self - << std::endl; + Trace("datatypes-init") + << "...already processing " << t << " " << d_self << std::endl; return Node(); } processing.push_back(t); + std::map& gtCache = isValue ? d_groundValue : d_groundTerm; for (unsigned r = 0; r < 2; r++) { for (std::shared_ptr ctor : d_constructors) @@ -804,10 +809,10 @@ Node DType::computeGroundTerm(TypeNode t, { continue; } - Trace("datatypes-init") - << "Try constructing for " << ctor->getName() - << ", processing = " << processing.size() << std::endl; - Node e = ctor->computeGroundTerm(t, processing, d_groundTerm, isValue); + Trace("datatypes-init") << "Try constructing for " << ctor->getName() + << ", processing = " << processing.size() + << ", isValue=" << isValue << std::endl; + Node e = ctor->computeGroundTerm(t, processing, gtCache, isValue); if (!e.isNull()) { // must check subterms for the same type to avoid infinite loops in diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index d63db28d5..b378985be 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -377,6 +377,9 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t, NodeManager* nm = NodeManager::currentNM(); std::vector groundTerms; groundTerms.push_back(getConstructor()); + Trace("datatypes-init") << "cons " << d_constructor + << " computeGroundTerm, isValue = " << isValue + << std::endl; // for each selector, get a ground term std::vector instTypes; @@ -418,13 +421,18 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t, } if (arg.isNull()) { - Trace("datatypes") << "...unable to construct arg of " - << d_args[i]->getName() << std::endl; + Trace("datatypes-init") << "...unable to construct arg of " + << d_args[i]->getName() << std::endl; return Node(); } else { - Trace("datatypes") << "...constructed arg " << arg.getType() << std::endl; + Trace("datatypes-init") + << "...constructed arg " << arg << " of type " << arg.getType() + << ", isConst = " << arg.isConst() << std::endl; + Assert(!isValue || arg.isConst()) + << "Expected non-constant constructor argument : " << arg + << " of type " << arg.getType(); groundTerms.push_back(arg); } } @@ -434,14 +442,17 @@ Node DTypeConstructor::computeGroundTerm(TypeNode t, { Assert(DType::datatypeOf(d_constructor).isParametric()); // type is parametric, must apply type ascription - Debug("datatypes-gt") << "ambiguous type for " << groundTerm - << ", ascribe to " << t << std::endl; + Trace("datatypes-init") << "ambiguous type for " << groundTerm + << ", ascribe to " << t << std::endl; groundTerms[0] = nm->mkNode( APPLY_TYPE_ASCRIPTION, nm->mkConst(AscriptionType(getSpecializedConstructorType(t))), groundTerms[0]); groundTerm = nm->mkNode(APPLY_CONSTRUCTOR, groundTerms); } + Trace("datatypes-init") << "...return " << groundTerm << std::endl; + Assert(!isValue || groundTerm.isConst()) << "Non-constant term " << groundTerm + << " returned for computeGroundTerm"; return groundTerm; } diff --git a/src/theory/type_enumerator.h b/src/theory/type_enumerator.h index b77fdcd9f..3aeb55897 100644 --- a/src/theory/type_enumerator.h +++ b/src/theory/type_enumerator.h @@ -156,7 +156,8 @@ class TypeEnumerator { #if defined(CVC4_ASSERTIONS) && !(defined(__APPLE__) && defined(__clang__)) try { Node n = **d_te; - Assert(n.isConst()); + Assert(n.isConst()) << "Term " << n + << " from type enumerator is not constant"; Assert(!isFinished()); return n; } catch(NoMoreValuesException&) { -- 2.30.2