From: Andrew Reynolds Date: Wed, 8 Sep 2021 13:39:31 +0000 (-0500) Subject: Add LFSC side condition conversion utility for list variables (#7131) X-Git-Tag: cvc5-1.0.0~1260 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=46c7d9d919c40962ec0c538754dac5a975eedb25;p=cvc5.git Add LFSC side condition conversion utility for list variables (#7131) Required for automatic generation of side conditions from DSL rewrite rules. --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a25d287a9..ba88080b8 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -178,6 +178,8 @@ libcvc5_add_sources( proof/lazy_proof_chain.h proof/lazy_tree_proof_generator.cpp proof/lazy_tree_proof_generator.h + proof/lfsc/lfsc_list_sc_node_converter.cpp + proof/lfsc/lfsc_list_sc_node_converter.h proof/lfsc/lfsc_node_converter.cpp proof/lfsc/lfsc_node_converter.h proof/lfsc/lfsc_util.cpp diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.cpp b/src/proof/lfsc/lfsc_list_sc_node_converter.cpp new file mode 100644 index 000000000..bf72fb85a --- /dev/null +++ b/src/proof/lfsc/lfsc_list_sc_node_converter.cpp @@ -0,0 +1,128 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of LFSC node conversion for list variables in side conditions + */ + +#include "proof/lfsc/lfsc_list_sc_node_converter.h" + +namespace cvc5 { +namespace proof { + +LfscListScNodeConverter::LfscListScNodeConverter( + LfscNodeConverter& conv, + const std::unordered_set& listVars, + bool isPre) + : d_conv(conv), d_listVars(listVars), d_isPre(isPre) +{ +} + +Node LfscListScNodeConverter::postConvert(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + Kind k = n.getKind(); + if (d_isPre) + { + // is this an application that may require nary elimination? + if (NodeManager::isNAryKind(k)) + { + size_t minLength = 0; + for (const Node& nc : n) + { + if (d_listVars.find(nc) == d_listVars.end()) + { + minLength++; + if (minLength >= 2) + { + // no need to convert + return n; + } + } + } + TypeNode tn = n.getType(); + // if so, (or a b c) becomes (nary_elim f_or (or a b c) false), + // where the children of this are converted + std::vector children; + Node f = d_conv.getOperatorOfTerm(n); + children.push_back(f); + // convert n, since this node will not be converted further + children.push_back(d_conv.convert(n)); + Node null = d_conv.getNullTerminator(k, tn); + Assert(!null.isNull()); + // likewise, convert null + children.push_back(d_conv.convert(null)); + Node sop = mkOperatorFor("nary_elim", children, tn); + children.insert(children.begin(), sop); + return nm->mkNode(kind::APPLY_UF, children); + } + return n; + } + Assert(k == kind::APPLY_UF || k == kind::APPLY_CONSTRUCTOR + || !NodeManager::isNAryKind(k) || n.getNumChildren() == 2) + << "Cannot convert LFSC side condition for " << n; + // note that after converting to binary form, variables should only appear + // as the first child of binary applications of n-ary operators + if (n.getNumChildren() == 2 && d_listVars.find(n[0]) != d_listVars.end()) + { + // this will fail if e.g. a list variable is a child of a non-n-ary kind + Assert(NodeManager::isNAryKind(k)); + TypeNode tn = n.getType(); + // We are in converted form, but need to get the null terminator for the + // original term. Hence, we convert the application back to original form + // if we replaced with an APPLY_UF. + if (k == kind::APPLY_UF) + { + k = d_conv.getBuiltinKindForInternalSymbol(n.getOperator()); + Assert(k != kind::UNDEFINED_KIND); + // for uniformity, reconstruct in original form + std::vector nchildren(n.begin(), n.end()); + n = nm->mkNode(k, nchildren); + } + Node null = d_conv.getNullTerminator(k, tn); + AlwaysAssert(!null.isNull()) + << "No null terminator for " << k << ", " << tn; + null = d_conv.convert(null); + // if a list variable occurs as a rightmost child, then we return just + // the variable + if (n[1] == null) + { + return n[0]; + } + // E.g. (or x t) becomes (nary_concat f_or x t false) + std::vector children; + Node f = d_conv.getOperatorOfTerm(n); + children.push_back(f); + children.insert(children.end(), n.begin(), n.end()); + children.push_back(null); + Node sop = mkOperatorFor("nary_concat", children, tn); + children.insert(children.begin(), sop); + return nm->mkNode(kind::APPLY_UF, children); + } + return n; +} + +Node LfscListScNodeConverter::mkOperatorFor(const std::string& name, + const std::vector& children, + TypeNode retType) +{ + NodeManager* nm = NodeManager::currentNM(); + std::vector childTypes; + for (const Node& c : children) + { + childTypes.push_back(c.getType()); + } + TypeNode ftype = nm->mkFunctionType(childTypes, retType); + return d_conv.mkInternalSymbol(name, ftype); +} + +} // namespace proof +} // namespace cvc5 diff --git a/src/proof/lfsc/lfsc_list_sc_node_converter.h b/src/proof/lfsc/lfsc_list_sc_node_converter.h new file mode 100644 index 000000000..fe0f18878 --- /dev/null +++ b/src/proof/lfsc/lfsc_list_sc_node_converter.h @@ -0,0 +1,86 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of LFSC node conversion for list variables in side conditions + */ +#include "cvc5_private.h" + +#ifndef CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H +#define CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H + +#include "expr/node_converter.h" +#include "proof/lfsc/lfsc_node_converter.h" + +namespace cvc5 { +namespace proof { + +/** + * Convert list variables in side conditions. This class converts nodes + * representing LFSC side condition programs to a form that prints properly + * in LFSC. In particular, this node converter gives consideration to + * input variables that are "list" variables in the rewrite DSL. + * + * For example, for DSL rule: + * (define-rule bool-and-flatten + * ((xs Bool :list) (b Bool) (ys Bool :list) (zs Bool :list)) + * (and xs (and b ys) zs) (and xs zs b ys)) + * This is a helper class used to compute the conclusion of this rule. This + * class is used to turn + * (= (and xs (and b ys) zs) (and xs zs b ys)) + * into: + * (= + * (nary_concat + * f_and + * xs + * (and (and b ys) zs) + * true) + * (nary_elim + * f_and + * (nary_concat f_and xs (nary_concat f_and zs (and b ys) true) true) + * true))) + * Where notice that the list variables xs, ys, zs are treated as lists to + * concatenate instead of being subterms, according to the semantics of list + * variables in the rewrite DSL. For exact definitions of nary_elim, + * nary_concat, see the LFSC signature nary_programs.plf. + * + * This runs in two modes. + * - If isPre is true, then the input is in its original form, and we add + * applications of nary_elim. + * - If isPre is false, then the input is in converted form, and we add + * applications of nary_concat. + */ +class LfscListScNodeConverter : public NodeConverter +{ + public: + LfscListScNodeConverter(LfscNodeConverter& conv, + const std::unordered_set& listVars, + bool isPre = false); + /** convert to internal */ + Node postConvert(Node n) override; + + private: + /** Make application for */ + Node mkOperatorFor(const std::string& name, + const std::vector& children, + TypeNode retType); + /** The parent converter, used for getting internal symbols and utilities */ + LfscNodeConverter& d_conv; + /** Variables we are treating as list variables */ + std::unordered_set d_listVars; + /** In pre or post */ + bool d_isPre; +}; + +} // namespace proof +} // namespace cvc5 + +#endif