From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 12 Apr 2022 22:35:05 +0000 (-0500)
Subject: Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (... 
X-Git-Tag: cvc5-1.0.1~268
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=714393e33a20dbd55f525fdc533968fb6c445cfa;p=cvc5.git

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.
---

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<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 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<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 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]));