From c1e90ce118705dc3d572300fd8c922973864df91 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 29 Oct 2021 08:32:06 -0500 Subject: [PATCH] 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. --- src/expr/node_converter.cpp | 4 ++++ src/expr/node_converter.h | 2 ++ src/proof/lfsc/lfsc_node_converter.cpp | 21 ++++++++++++++++++--- src/proof/lfsc/lfsc_post_processor.cpp | 20 ++++++++++++++++++-- 4 files changed, 42 insertions(+), 5 deletions(-) diff --git a/src/expr/node_converter.cpp b/src/expr/node_converter.cpp index 92b459105..eabe1d4f1 100644 --- 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::iterator it; diff --git a/src/expr/node_converter.h b/src/expr/node_converter.h index 6edb2522c..a2aaeca6f 100644 --- 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 12326b212..b64506af5 100644 --- 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(); 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 72db06060..33004e81f 100644 --- 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; -- 2.30.2