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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 termtoletify 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 