From 714393e33a20dbd55f525fdc533968fb6c445cfa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 12 Apr 2022 17:35:05 -0500 Subject: [PATCH] Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (#8608) Also removes an old case for parametric datatypes in getBaseType, which is incorrect since datatypes not longer use subtyping. This avoids more assertion failures in debug mode for LFSC due to subtypes. --- src/expr/type_node.cpp | 6 ------ src/proof/lfsc/lfsc_node_converter.cpp | 5 ++++- src/proof/lfsc/lfsc_post_processor.cpp | 3 +++ 3 files changed, 7 insertions(+), 7 deletions(-) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 71a1563a5..f48f5a320 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -337,12 +337,6 @@ TypeNode TypeNode::getBaseType() const { TypeNode realt = NodeManager::currentNM()->realType(); if (isSubtypeOf(realt)) { return realt; - } else if (isParametricDatatype()) { - std::vector v; - for(size_t i = 1; i < getNumChildren(); ++i) { - v.push_back((*this)[i].getBaseType()); - } - return (*this)[0].getDType().getTypeNode().instantiate(v); } return *this; } diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 7388c46a0..baf3b44ac 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -1132,7 +1132,10 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply) std::vector argTypes; for (const Node& nc : n) { - argTypes.push_back(nc.getType()); + // We take the base type, so that e.g. arithmetic operators are over + // real. This avoids issues with subtyping when currying during proof + // postprocessing + argTypes.push_back(nc.getType().getBaseType()); } // we only use binary operators if (NodeManager::isNAryKind(k)) diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index 34190ab7e..727ee1b7c 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -251,6 +251,7 @@ bool LfscProofPostprocessCallback::update(Node res, for (size_t i = 0; i < nchildren; i++) { size_t ii = (nchildren - 1) - i; + Trace("lfsc-pp-cong") << "Process child " << ii << std::endl; Node uop = op; // special case: each bv concat in the chain has a different type, // so remake the operator here. @@ -262,6 +263,8 @@ bool LfscProofPostprocessCallback::update(Node res, nm->mkNode(kind::BITVECTOR_CONCAT, children[ii][0], currEq[0]); uop = d_tproc.getOperatorOfTerm(currApp); } + Trace("lfsc-pp-cong") << "Apply " << uop << " to " << children[ii][0] + << " and " << children[ii][1] << std::endl; Node argAppEq = nm->mkNode(HO_APPLY, uop, children[ii][0]) .eqNode(nm->mkNode(HO_APPLY, uop, children[ii][1])); -- 2.30.2