Improvements for LFSC proof conversion (#7524)

Includes miscellaneous improvements and fixes to the LFSC proof conversion from proof-new in preparation for CI on master.

diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp
index 92b4591054d0fc30f7e9e48b49592fcff808e054..eabe1d4f1346e9fa1cbf56ca37d1301d3907294e 100644 (file)
--- a/src/expr/node_converter.cpp
+++ b/src/expr/node_converter.cpp
@@ -25,6 +25,10 @@ NodeConverter::NodeConverter(bool forceIdem) : d_forceIdem(forceIdem) {}
 
 Node NodeConverter::convert(Node n)
 {
+  if (n.isNull())
+  {
+    return n;
+  }
   Trace("nconv-debug") << "NodeConverter::convert: " << n << std::endl;
   NodeManager* nm = NodeManager::currentNM();
   std::unordered_map<Node, Node>::iterator it;

diff --git a/src/expr/node_converter.h b/src/expr/node_converter.h
index 6edb2522c5a3d20f71005ae3e3e342f6c7b3d095..a2aaeca6ff0fd964361ed0765b516a8269ab4dbe 100644 (file)
--- a/src/expr/node_converter.h
+++ b/src/expr/node_converter.h
@@ -46,6 +46,8 @@ class NodeConverter
   /**
    * This converts node n based on the preConvert/postConvert methods that can
    * be overriden by instances of this class.
+   *
+   * If n is null, this always returns the null node.
    */
   Node convert(Node n);
 

diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp
index 12326b2129bd5b8597a53933167cbd2ac12003bd..b64506af5d94eef206a62a1cc162fef26ff9e5da 100644 (file)
--- a/src/proof/lfsc/lfsc_node_converter.cpp
+++ b/src/proof/lfsc/lfsc_node_converter.cpp
@@ -226,7 +226,7 @@ Node LfscNodeConverter::postConvert(Node n)
   {
     TypeNode btn = nm->booleanType();
     TypeNode tnv = nm->mkFunctionType(btn, tn);
-    TypeNode btnv = nm->mkFunctionType(btn, btn);
+    TypeNode btnv = nm->mkFunctionType({btn, btn}, btn);
     BitVector bv = n.getConst<BitVector>();
     size_t w = bv.getSize();
     Node ret = getSymbolInternal(k, btn, "bvn");
@@ -352,6 +352,21 @@ Node LfscNodeConverter::postConvert(Node n)
     // currently unsupported
     return n;
   }
+  else if (k == BITVECTOR_BB_TERM)
+  {
+    TypeNode btn = nm->booleanType();
+    // (bbT t1 ... tn) is (bbT t1 (bbT t2 ... (bbT tn emptybv)))
+    // where notice that each bbT has a different type
+    Node curr = getNullTerminator(BITVECTOR_CONCAT, tn);
+    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; ++i)
+    {
+      TypeNode bvt = nm->mkBitVectorType(i + 1);
+      TypeNode ftype = nm->mkFunctionType({btn, curr.getType()}, bvt);
+      Node bbt = getSymbolInternal(k, ftype, "bbT");
+      curr = nm->mkNode(APPLY_UF, bbt, n[nchild - (i + 1)], curr);
+    }
+    return curr;
+  }
   else if (k == SEP_NIL)
   {
     Node tnn = typeAsNode(convertType(tn));
@@ -591,8 +606,8 @@ std::string LfscNodeConverter::getNameForUserName(const std::string& name)
 bool LfscNodeConverter::shouldTraverse(Node n)
 {
   Kind k = n.getKind();
-  // don't convert bound variable list directly
-  if (k == BOUND_VAR_LIST)
+  // don't convert bound variable or instantiation pattern list directly
+  if (k == BOUND_VAR_LIST || k == INST_PATTERN_LIST)
   {
     return false;
   }

diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp
index 72db06060201f783a784701b9477493c22af0c00..33004e81f8121858f4a7ea6362fe77566b9edc2b 100644 (file)
--- a/src/proof/lfsc/lfsc_post_processor.cpp
+++ b/src/proof/lfsc/lfsc_post_processor.cpp
@@ -16,6 +16,7 @@
 
 #include "options/proof_options.h"
 #include "proof/lazy_proof.h"
+#include "proof/lfsc/lfsc_printer.h"
 #include "proof/proof_checker.h"
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
@@ -158,6 +159,8 @@ bool LfscProofPostprocessCallback::update(Node res,
     {
       Assert(res.getKind() == EQUAL);
       Assert(res[0].getOperator() == res[1].getOperator());
+      Trace("lfsc-pp-cong") << "Processing congruence for " << res << " "
+                            << res[0].getKind() << std::endl;
       // different for closures
       if (res[0].isClosure())
       {
@@ -210,6 +213,8 @@ bool LfscProofPostprocessCallback::update(Node res,
       // REFL step. Notice this may be for interpreted or uninterpreted
       // function symbols.
       Node op = d_tproc.getOperatorOfTerm(res[0]);
+      Trace("lfsc-pp-cong") << "Processing cong for op " << op << " "
+                            << op.getType() << std::endl;
       Assert(!op.isNull());
       // initial base step is REFL
       Node opEq = op.eqNode(op);
@@ -245,9 +250,20 @@ bool LfscProofPostprocessCallback::update(Node res,
         for (size_t i = 0; i < nchildren; i++)
         {
           size_t ii = (nchildren - 1) - i;
+          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)
+          {
+            // 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]);
+            uop = d_tproc.getOperatorOfTerm(currApp);
+          }
           Node argAppEq =
-              nm->mkNode(HO_APPLY, op, children[ii][0])
-                  .eqNode(nm->mkNode(HO_APPLY, op, children[ii][1]));
+              nm->mkNode(HO_APPLY, uop, children[ii][0])
+                  .eqNode(nm->mkNode(HO_APPLY, uop, children[ii][1]));
           addLfscRule(cdp, argAppEq, {opEq, children[ii]}, LfscRule::CONG, {});
           // now, congruence to the current equality
           Node nextEq;