From 910887748fef32cf57c0bad3b5eac2c44d6f48f8 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 14 Apr 2022 18:25:09 -0500 Subject: [PATCH] Fix internal type issue for congruence over quantifiers in LFSC post-processor (#8619) Avoids debug assertions in LFSC proof conversion when doing congruence over closures. --- src/proof/lfsc/lfsc_node_converter.cpp | 3 ++- src/proof/lfsc/lfsc_post_processor.cpp | 8 ++++++-- 2 files changed, 8 insertions(+), 3 deletions(-) diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 12302bd7a..def75fe46 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -372,7 +372,8 @@ Node LfscNodeConverter::postConvert(Node n) { size_t ii = (nchild - 1) - i; Node v = n[0][ii]; - // use the partial operator for variables beyond the first + // use the partial operator for variables except the last one. This + // avoids type errors in internal representation of LFSC terms. Node vop = getOperatorOfBoundVar(ii == 0 ? cop : pcop, v); ret = nm->mkNode(APPLY_UF, vop, ret); } diff --git a/src/proof/lfsc/lfsc_post_processor.cpp b/src/proof/lfsc/lfsc_post_processor.cpp index 727ee1b7c..df902e6d6 100644 --- a/src/proof/lfsc/lfsc_post_processor.cpp +++ b/src/proof/lfsc/lfsc_post_processor.cpp @@ -171,6 +171,7 @@ bool LfscProofPostprocessCallback::update(Node res, return false; } Node cop = d_tproc.getOperatorOfClosure(res[0]); + Node pcop = d_tproc.getOperatorOfClosure(res[0], false, true); Trace("lfsc-pp-qcong") << "Operator for closure " << cop << std::endl; // start with base case body = body' Node curL = children[1][0]; @@ -179,10 +180,13 @@ bool LfscProofPostprocessCallback::update(Node res, Trace("lfsc-pp-qcong") << "Base congruence " << currEq << std::endl; for (size_t i = 0, nvars = res[0][0].getNumChildren(); i < nvars; i++) { + size_t ii = (nvars - 1) - i; Trace("lfsc-pp-qcong") << "Process child " << i << std::endl; // CONG rules for each variable - Node v = res[0][0][nvars - 1 - i]; - Node vop = d_tproc.getOperatorOfBoundVar(cop, v); + Node v = res[0][0][ii]; + // Use partial version for each argument except the last one. This + // avoids type errors in internal representation of LFSC terms. + Node vop = d_tproc.getOperatorOfBoundVar(ii == 0 ? cop : pcop, v); Node vopEq = vop.eqNode(vop); cdp->addStep(vopEq, PfRule::REFL, {}, {vop}); Node nextEq; -- 2.30.2