src/proof/lfsc/lfsc_list_sc_node_converter.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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  * ****************************************************************************
  12  *
  13  * Implementation of LFSC node conversion for list variables in side conditions
  14  */
  15 #include "cvc5_private.h"
  16
  17 #ifndef CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
  18 #define CVC4__PROOF__LFSC__LFSC_LIST_SC_NODE_CONVERTER_H
  19
  20 #include "expr/node_converter.h"
  21 #include "proof/lfsc/lfsc_node_converter.h"
  22
  23 namespace cvc5 {
  24 namespace proof {
  25
  26 /**
  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.
  31  *
  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))
  39  * into:
  40  *   (=
  41  *      (nary_concat
  42  *        f_and
  43  *        xs
  44  *        (and (and b ys) zs)
  45  *        true)
  46  *      (nary_elim
  47  *        f_and
  48  *        (nary_concat f_and xs (nary_concat f_and zs (and b ys) true) true)
  49  *        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.
  54  *
  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.
  60  */
  61 class LfscListScNodeConverter : public NodeConverter
  62 {
  63  public:
  64   LfscListScNodeConverter(LfscNodeConverter& conv,
  65                           const std::unordered_set<Node>& listVars,
  66                           bool isPre = false);
  67   /** convert to internal */
  68   Node postConvert(Node n) override;
  69
  70  private:
  71   /** Make application for */
  72   Node mkOperatorFor(const std::string& name,
  73                      const std::vector<Node>& children,
  74                      TypeNode retType);
  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;
  79   /** In pre or post */
  80   bool d_isPre;
  81 };
  82
  83 }  // namespace proof
  84 }  // namespace cvc5
  85
  86 #endif