Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (...

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.

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 71a1563a51dc685414f6f0f3e13549e1e0ef0fb8..f48f5a320131f72f665f36433433ade8ea2f4aeb 100644 (file)
--- 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<TypeNode> 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 7388c46a029efcdeaa78c982aaa8a785152182c1..baf3b44aca7e54b6733d9b95756eef9894e30dcf 100644 (file)
--- 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<TypeNode> 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 34190ab7ed0a6a83b7d30a867df889c6f21acb88..727ee1b7c35bccdd024daa13adab744ea2a74931 100644 (file)
--- 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]));