Fix debug failures in LFSC proofs due to curried arithmetic operators (#8763)

This ensures we use different variants of PLUS, MULT, NONLINEAR_MULT internally to avoid type checking failures in debug mode during LFSC printing.

Fixes regression failures in debug mode for LFSC.

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 5eab07dd6063b229695ad73e42c40f6599845400..2ed7c3f89c530e92694e831f90670ab47511d260 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -461,31 +461,33 @@ Node LfscNodeConverter::postConvert(Node n)
       // must convert recursively, since nullTerm may have subterms.
       ret = convert(nullTerm);
     }
-    // the kind to chain
-    Kind ck = k;
     // check whether we are also changing the operator name, in which case
     // we build a binary uninterpreted function opc
-    Node opc;
-    if (k == ADD || k == MULT || k == NONLINEAR_MULT)
+    bool isArithOp = (k == ADD || k == MULT || k == NONLINEAR_MULT);
+    std::stringstream arithOpName;
+    if (isArithOp)
     {
-      std::stringstream opName;
       // currently allow subtyping
-      opName << "a.";
-      opName << printer::smt2::Smt2Printer::smtKindString(k);
-      TypeNode ftype = nm->mkFunctionType({tn, tn}, tn);
-      opc = getSymbolInternal(k, ftype, opName.str());
-      ck = APPLY_UF;
+      arithOpName << "a.";
+      arithOpName << printer::smt2::Smt2Printer::smtKindString(k);
     }
     // now, iterate over children and make binary conversion
     for (size_t i = istart, npchild = children.size(); i < npchild; i++)
     {
-      if (!opc.isNull())
+      if (isArithOp)
       {
-        ret = nm->mkNode(ck, opc, children[i], ret);
+        // Arithmetic operators must deal with permissive type rules for
+        // ADD, MULT, NONLINEAR_MULT. We use the properly typed operator to
+        // avoid debug failures.
+        TypeNode tn1 = children[i].getType();
+        TypeNode tn2 = ret.getType();
+        TypeNode ftype = nm->mkFunctionType({tn1, tn2}, tn);
+        Node opc = getSymbolInternal(k, ftype, arithOpName.str());
+        ret = nm->mkNode(APPLY_UF, opc, children[i], ret);
       }
       else
       {
-        ret = nm->mkNode(ck, children[i], ret);
+        ret = nm->mkNode(k, children[i], ret);
       }
     }
     Trace("lfsc-term-process-debug")
@@ -1202,10 +1204,7 @@ Node LfscNodeConverter::getOperatorOfTerm(Node n, bool macroApply)
   std::vector<TypeNode> argTypes;
   for (const Node& nc : n)
   {
-    // 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());
+    argTypes.push_back(nc.getType());
   }
   // 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 37f97b905853c52d44776f19b3983e4bda42dbe4..f849047ff60ca2bf7d47b832ff770808c22d0995 100644 (file)
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -258,14 +258,14 @@ bool LfscProofPostprocessCallback::update(Node res,
           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.
-          if (k == kind::BITVECTOR_CONCAT)
+          // special case: applications of the following kinds in the chain may
+          // have a different type, so remake the operator here.
+          if (k == kind::BITVECTOR_CONCAT || k == ADD || k == MULT
+              || k == NONLINEAR_MULT)
           {
             // we get the operator of the next argument concatenated with the
             // current accumulated remainder.
-            Node currApp =
-                nm->mkNode(kind::BITVECTOR_CONCAT, children[ii][0], currEq[0]);
+            Node currApp = nm->mkNode(k, children[ii][0], currEq[0]);
             uop = d_tproc.getOperatorOfTerm(currApp);
           }
           Trace("lfsc-pp-cong") << "Apply " << uop << " to " << children[ii][0]

diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp
index ad5cd5347f162b3afa9518655434eb714a4ab9ab..b56ab47f61e47d3fab74647d0209111e880746ba 100644 (file)
--- a/src/proof/lfsc/lfsc_printer.cpp
+++ b/src/proof/lfsc/lfsc_printer.cpp
@@ -617,7 +617,7 @@ bool LfscPrinter::computeProofArgs(const ProofNode* pn,
     {
       Node res = pn->getResult();
       Assert(res.getNumChildren() == 2);
-      Assert(res[1].getKind() == CONST_RATIONAL);
+      Assert(res[1].isConst());
       pf << h << h << d_tproc.convert(res[1]) << cs[0];
     }
     break;