GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/printer/let_binding.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file let_binding.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
6
 ** This file is part of the CVC4 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.\endverbatim
11
 **
12
 ** \brief A let binding
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__PRINTER__LET_BINDING_H
18
#define CVC4__PRINTER__LET_BINDING_H
19
20
#include <vector>
21
22
#include "context/cdhashmap.h"
23
#include "context/cdlist.h"
24
#include "expr/node.h"
25
26
namespace CVC4 {
27
28
/**
29
 * A flexible let binding class. This class provides functionalities for
30
 * printing letified terms. A simple use case is the following for Node n
31
 * and LetBinding lbind:
32
 * ```
33
 *   std::vector<Node> letList;
34
 *   lbind.letify(n, letList);
35
 * ```
36
 * Now, letList contains a list of subterms of n that should be letified based
37
 * on the threshold value passed to this class where a value n>0 indicates that
38
 * terms with n or more occurrences should be letified.
39
 *
40
 * The above is equivalent to:
41
 * ```
42
 *   std::vector<Node> letList;
43
 *   lbind.pushScope();
44
 *   lbind.process(n);
45
 *   lbind.letify(letList);
46
 * ```
47
 * In fact, multiple terms can be passed to calls to process, in which case the
48
 * counting is cumulative.
49
 *
50
 * All quantified formulas are treated as black boxes. This class can be used
51
 * to letify terms with quantifiers, where multiple calls to pushScope /
52
 * popScope can be used. In particular, consider:
53
 * ```
54
 *   std::vector<Node> letList1;
55
 *   lbind.letify(n1, letList1);
56
 *   std::vector<Node> letList2;
57
 *   lbind.letify(n2, letList2);
58
 *   ...
59
 *   lbind.popScope();
60
 *   lbind.popScope();
61
 * ```
62
 * In a typical use case, n2 is the body of a quantified formula that is a
63
 * subterm of n1. We have that letList2 is the list of subterms of n2 that
64
 * should be letified, assuming that we have already have let definitions
65
 * given by letList1.
66
 *
67
 * Internally, a let binding is a list and a map that can be printed as a let
68
 * expression. In particular, the list d_letList is ordered such that
69
 * d_letList[i] does not contain subterm d_letList[j] for j>i.
70
 * It is intended that d_letList contains only unique nodes. Each node
71
 * in d_letList is mapped to a unique identifier in d_letMap.
72
 *
73
 * Notice that this class will *not* use introduced let symbols when converting
74
 * the bodies of quantified formulas. Consider the formula:
75
 * (let ((Q (forall ((x Int)) (= x (+ a a))))) (and (= (+ a a) (+ a a)) Q Q))
76
 * where "let" above is from the user. When this is letified by this class,
77
 * note that (+ a a) occurs as a subterm of Q, however it is not seen until
78
 * after we have seen Q twice, since we traverse in reverse topological order.
79
 * Since we do not traverse underneath quantified formulas, this means that Q
80
 * may be marked as a term-to-letify before (+ a a), which leads to violation
81
 * of the above invariant concerning containment. Thus, when converting, if
82
 * a let symbol is introduced for (+ a a), we will not replace the occurence
83
 * of (+ a a) within Q. Instead, the user of this class is responsible for
84
 * letifying the bodies of quantified formulas independently.
85
 */
86
58683
class LetBinding
87
{
88
  using NodeList = context::CDList<Node>;
89
  using NodeIdMap = context::CDHashMap<Node, uint32_t, NodeHashFunction>;
90
91
 public:
92
  LetBinding(uint32_t thresh = 2);
93
  /** Get threshold */
94
  uint32_t getThreshold() const;
95
  /**
96
   * This updates this let binding to consider the counts for node n.
97
   */
98
  void process(Node n);
99
  /**
100
   * This pushes a scope, computes the letification for n, adds the (new) terms
101
   * that must be letified in this context to letList.
102
   *
103
   * Notice that this method does not traverse inside of closures.
104
   *
105
   * @param n The node to letify
106
   * @param letList The list of terms that should be letified within n. This
107
   * list is ordered in such a way that letList[i] does not contain subterm
108
   * letList[j] for j>i.
109
   */
110
  void letify(Node n, std::vector<Node>& letList);
111
  /**
112
   * Same as above, without a node to letify.
113
   */
114
  void letify(std::vector<Node>& letList);
115
  /** Push scope */
116
  void pushScope();
117
  /** Pop scope for n, reverts the state change of the above method */
118
  void popScope();
119
  /**
120
   * @return the identifier for node n, or 0 if it does not have one.
121
   */
122
  uint32_t getId(Node n) const;
123
  /**
124
   * Convert n based on the state of the let binding. This replaces all
125
   * letified subterms of n with a fresh variable whose name prefix is the
126
   * given one.
127
   *
128
   * @param n The node to convert
129
   * @param prefix The prefix of variables to convert
130
   * @param letTop Whether we letify n itself
131
   * @return the converted node.
132
   */
133
  Node convert(Node n, const std::string& prefix, bool letTop = true) const;
134
135
 private:
136
  /**
137
   * Compute the count of sub nodes in n, store in d_count. Additionally,
138
   * store each node in the domain of d_count in an order in d_visitList
139
   * such that d_visitList[i] does not contain sub d_visitList[j] for j>i.
140
   */
141
  void updateCounts(Node n);
142
  /**
143
   * Convert a count to a let binding.
144
   */
145
  void convertCountToLet();
146
  /** The dag threshold */
147
  uint32_t d_thresh;
148
  /** An internal context */
149
  context::Context d_context;
150
  /** Visit list */
151
  NodeList d_visitList;
152
  /** Count */
153
  NodeIdMap d_count;
154
  /** The let list */
155
  NodeList d_letList;
156
  /** The let map */
157
  NodeIdMap d_letMap;
158
};
159
160
}  // namespace CVC4
161
162
#endif