From 68b6948dcf2bc1b0d4f08f038aa18a31c3857b57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Sun, 1 May 2022 19:32:32 -0500 Subject: [PATCH] Fix tuple printing in LFSC (#8696) We weren't collecting them as user-defined types after the recent refactor to Tuples. --- src/proof/lfsc/lfsc_node_converter.cpp | 12 ++++++++++++ src/proof/lfsc/lfsc_node_converter.h | 2 ++ 2 files changed, 14 insertions(+) diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index f8e79e014..6cd2d56eb 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -495,6 +495,18 @@ Node LfscNodeConverter::postConvert(Node n) return n; } +TypeNode LfscNodeConverter::preConvertType(TypeNode tn) +{ + if (tn.getKind() == TUPLE_TYPE) + { + // Must collect the tuple type here, since at post-order traversal, the + // type has been modified and no longer maintains the mapping to its + // datatype encoding. + d_declTypes.insert(tn); + } + return tn; +} + TypeNode LfscNodeConverter::postConvertType(TypeNode tn) { NodeManager* nm = NodeManager::currentNM(); diff --git a/src/proof/lfsc/lfsc_node_converter.h b/src/proof/lfsc/lfsc_node_converter.h index 497c94fd5..38754961f 100644 --- a/src/proof/lfsc/lfsc_node_converter.h +++ b/src/proof/lfsc/lfsc_node_converter.h @@ -40,6 +40,8 @@ class LfscNodeConverter : public NodeConverter Node preConvert(Node n) override; /** convert at post-order traversal */ Node postConvert(Node n) override; + /** convert type at pre-order traversal */ + TypeNode preConvertType(TypeNode tn) override; /** convert type at post-order traversal */ TypeNode postConvertType(TypeNode tn) override; /** -- 2.30.2