1 /******************************************************************************
2 * Top contributors (to current version):
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
13 * Implementation of LFSC node conversion for list variables in side conditions
15 #include "cvc5_private.h"
17 #ifndef CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
18 #define CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
20 #include "expr/node_converter.h"
21 #include "proof/lfsc/lfsc_node_converter.h"
27 * Convert list variables in side conditions. This class converts nodes
28 * representing LFSC side condition programs to a form that prints properly
29 * in LFSC. In particular, this node converter gives consideration to
30 * input variables that are "list" variables in the rewrite DSL.
32 * For example, for DSL rule:
33 * (define-rule bool-and-flatten
34 * ((xs Bool :list) (b Bool) (ys Bool :list) (zs Bool :list))
35 * (and xs (and b ys) zs) (and xs zs b ys))
36 * This is a helper class used to compute the conclusion of this rule. This
37 * class is used to turn
38 * (= (and xs (and b ys) zs) (and xs zs b ys))
48 * (nary_concat f_and xs (nary_concat f_and zs (and b ys) true) true)
50 * Where notice that the list variables xs, ys, zs are treated as lists to
51 * concatenate instead of being subterms, according to the semantics of list
52 * variables in the rewrite DSL. For exact definitions of nary_elim,
53 * nary_concat, see the LFSC signature nary_programs.plf.
55 * This runs in two modes.
56 * - If isPre is true, then the input is in its original form, and we add
57 * applications of nary_elim.
58 * - If isPre is false, then the input is in converted form, and we add
59 * applications of nary_concat.
61 class LfscListScNodeConverter
: public NodeConverter
64 LfscListScNodeConverter(LfscNodeConverter
& conv
,
65 const std::unordered_set
<Node
>& listVars
,
67 /** convert to internal */
68 Node
postConvert(Node n
) override
;
71 /** Make application for */
72 Node
mkOperatorFor(const std::string
& name
,
73 const std::vector
<Node
>& children
,
75 /** The parent converter, used for getting internal symbols and utilities */
76 LfscNodeConverter
& d_conv
;
77 /** Variables we are treating as list variables */
78 std::unordered_set
<Node
> d_listVars
;