1 

/********************* */ 
2 

/*! \file term_database.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Mathias Preiner 
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 term database class 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H 
18 

#define CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H 
19 


20 

#include <map> 
21 

#include <unordered_map> 
22 


23 

#include "context/cdhashmap.h" 
24 

#include "context/cdhashset.h" 
25 

#include "expr/attribute.h" 
26 

#include "expr/node_trie.h" 
27 

#include "theory/quantifiers/quant_util.h" 
28 

#include "theory/theory.h" 
29 

#include "theory/type_enumerator.h" 
30 


31 

namespace CVC4 { 
32 

namespace theory { 
33 


34 

class QuantifiersEngine; 
35 


36 

namespace quantifiers { 
37 


38 

class QuantifiersState; 
39 

class QuantifiersInferenceManager; 
40 

class QuantifiersRegistry; 
41 


42 

/** Contextdependent list of nodes */ 
43 
148743 
class DbList 
44 

{ 
45 

public: 
46 
148743 
DbList(context::Context* c) : d_list(c) {} 
47 

/** The list */ 
48 

context::CDList<Node> d_list; 
49 

}; 
50 


51 

/** Term Database 
52 

* 
53 

* This class is a key utility used by 
54 

* a number of approaches for quantifier instantiation, 
55 

* including Ematching, conflictbased instantiation, 
56 

* and modelbased instantiation. 
57 

* 
58 

* The primary responsibilities for this class are to : 
59 

* (1) Maintain a list of all ground terms that exist in the quantifierfree 
60 

* solvers, as notified through the master equality engine. 
61 

* (2) Build TNodeTrie objects that index all ground terms, per operator. 
62 

* 
63 

* Like other utilities, its reset(...) function is called 
64 

* at the beginning of full or last call effort checks. 
65 

* This initializes the database for the round. However, 
66 

* notice that TNodeTrie objects are computed 
67 

* lazily for performance reasons. 
68 

*/ 
69 

class TermDb : public QuantifiersUtil { 
70 

friend class ::CVC4::theory::QuantifiersEngine; 
71 

using NodeBoolMap = context::CDHashMap<Node, bool, NodeHashFunction>; 
72 

using NodeList = context::CDList<Node>; 
73 

using NodeSet = context::CDHashSet<Node, NodeHashFunction>; 
74 

using TypeNodeDbListMap = context:: 
75 

CDHashMap<TypeNode, std::shared_ptr<DbList>, TypeNodeHashFunction>; 
76 

using NodeDbListMap = 
77 

context::CDHashMap<Node, std::shared_ptr<DbList>, NodeHashFunction>; 
78 


79 

public: 
80 

TermDb(QuantifiersState& qs, 
81 

QuantifiersRegistry& qr); 
82 

~TermDb(); 
83 

/** Finish init, which sets the inference manager */ 
84 

void finishInit(QuantifiersInferenceManager* qim); 
85 

/** presolve (called once per user checksat) */ 
86 

void presolve(); 
87 

/** reset (calculate which terms are active) */ 
88 

bool reset(Theory::Effort effort) override; 
89 

/** register quantified formula */ 
90 

void registerQuantifier(Node q) override; 
91 

/** identify */ 
92 
28251 
std::string identify() const override { return "TermDb"; } 
93 

/** get number of operators */ 
94 

size_t getNumOperators() const; 
95 

/** get operator at index i */ 
96 

Node getOperator(size_t i) const; 
97 

/** ground terms for operator 
98 

* Get the number of ground terms with operator f that have been added to the 
99 

* database 
100 

*/ 
101 

size_t getNumGroundTerms(Node f) const; 
102 

/** get ground term for operator 
103 

* Get the i^th ground term with operator f that has been added to the database 
104 

*/ 
105 

Node getGroundTerm(Node f, size_t i) const; 
106 

/** get num type terms 
107 

* Get the number of ground terms of tn that have been added to the database 
108 

*/ 
109 

size_t getNumTypeGroundTerms(TypeNode tn) const; 
110 

/** get type ground term 
111 

* Returns the i^th ground term of type tn 
112 

*/ 
113 

Node getTypeGroundTerm(TypeNode tn, size_t i) const; 
114 

/** get or make ground term 
115 

* 
116 

* Returns the first ground term of type tn, or makes one if none exist. If 
117 

* reqVar is true, then the ground term must be a variable. 
118 

*/ 
119 

Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false); 
120 

/** make fresh variable 
121 

* Returns a fresh variable of type tn. 
122 

* This will return only a single fresh 
123 

* variable per type. 
124 

*/ 
125 

Node getOrMakeTypeFreshVariable(TypeNode tn); 
126 

/** 
127 

* Add a term to the database, which registers it as a term that may be 
128 

* matched with via Ematching, and can be used in entailment tests below. 
129 

*/ 
130 

void addTerm(Node n); 
131 

/** Get the currently added ground terms of the given type */ 
132 

DbList* getOrMkDbListForType(TypeNode tn); 
133 

/** Get the currently added ground terms for the given operator */ 
134 

DbList* getOrMkDbListForOp(TNode op); 
135 

/** get match operator for term n 
136 

* 
137 

* If n has a kind that we index, this function will 
138 

* typically return n.getOperator(). 
139 

* 
140 

* However, for parametric operators f, the match operator is an arbitrary 
141 

* chosen fapplication. For example, consider array select: 
142 

* A : (Array Int Int) 
143 

* B : (Array Bool Int) 
144 

* We require that terms like (select A 1) and (select B 2) are indexed in 
145 

* separate 
146 

* data structures despite the fact that 
147 

* (select A 1).getOperator()==(select B 2).getOperator(). 
148 

* Hence, for the above terms, we may return: 
149 

* getMatchOperator( (select A 1) ) = (select A 1), and 
150 

* getMatchOperator( (select B 2) ) = (select B 2). 
151 

* The match operator is the first instance of an application of the parametric 
152 

* operator of its type. 
153 

* 
154 

* If n has a kind that we do not index (like PLUS), 
155 

* then this function returns Node::null(). 
156 

*/ 
157 

Node getMatchOperator(Node n); 
158 

/** get term arg index for all fapplications in the current context */ 
159 

TNodeTrie* getTermArgTrie(Node f); 
160 

/** get the term arg trie for fapplications in the equivalence class of eqc. 
161 

*/ 
162 

TNodeTrie* getTermArgTrie(Node eqc, Node f); 
163 

/** get congruent term 
164 

* If possible, returns a term t such that: 
165 

* (1) t is a term that is currently indexed by this database, 
166 

* (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ), 
167 

* where ti is in the equivalence class of si for i=1...k. 
168 

*/ 
169 

TNode getCongruentTerm(Node f, Node n); 
170 

/** get congruent term 
171 

* If possible, returns a term t such that: 
172 

* (1) t is a term that is currently indexed by this database, 
173 

* (2) t is of the form f( t1, ..., tk ) where ti is in the 
174 

* equivalence class of args[i] for i=1...k. 
175 

*/ 
176 

TNode getCongruentTerm(Node f, std::vector<TNode>& args); 
177 

/** in relevant domain 
178 

* Returns true if there is at least one term t such that: 
179 

* (1) t is a term that is currently indexed by this database, 
180 

* (2) t is of the form f( t1, ..., tk ) and ti is in the 
181 

* equivalence class of r. 
182 

*/ 
183 

bool inRelevantDomain(TNode f, unsigned i, TNode r); 
184 

/** evaluate term 
185 

* 
186 

* Returns a term n' such that n = n' is entailed based on the equality 
187 

* information ee. This function may generate new terms. In particular, 
188 

* we typically rewrite subterms of n of maximal size to terms that exist in 
189 

* the equality engine specified by ee. 
190 

* 
191 

* useEntailmentTests is whether to call the theory engine's entailmentTest 
192 

* on literals n for which this call fails to find a term n' that is 
193 

* equivalent to n, for increased precision. This is not frequently used. 
194 

* 
195 

* The vector exp stores the explanation for why n evaluates to that term, 
196 

* that is, if this call returns a nonnull node n', then: 
197 

* exp => n = n' 
198 

* 
199 

* If reqHasTerm, then we require that the returned term is a Boolean 
200 

* combination of terms that exist in the equality engine used by this call. 
201 

* If no such term is constructable, this call returns null. The motivation 
202 

* for setting this to true is to "fail fast" if we require the return value 
203 

* of this function to only involve existing terms. This is used e.g. in 
204 

* the "propagating instances" portion of conflictbased instantiation 
205 

* (quant_conflict_find.h). 
206 

*/ 
207 

Node evaluateTerm(TNode n, 
208 

std::vector<Node>& exp, 
209 

bool useEntailmentTests = false, 
210 

bool reqHasTerm = false); 
211 

/** same as above, without exp */ 
212 

Node evaluateTerm(TNode n, 
213 

bool useEntailmentTests = false, 
214 

bool reqHasTerm = false); 
215 

/** get entailed term 
216 

* 
217 

* If possible, returns a term n' such that: 
218 

* (1) n' exists in the current equality engine (as specified by the state), 
219 

* (2) n = n' is entailed in the current context. 
220 

* It returns null if no such term can be found. 
221 

* Wrt evaluateTerm, this version does not construct new terms, and 
222 

* thus is less aggressive. 
223 

*/ 
224 

TNode getEntailedTerm(TNode n); 
225 

/** get entailed term 
226 

* 
227 

* If possible, returns a term n' such that: 
228 

* (1) n' exists in the current equality engine (as specified by the state), 
229 

* (2) n * subs = n' is entailed in the current context, where * denotes 
230 

* substitution application. 
231 

* It returns null if no such term can be found. 
232 

* subsRep is whether the substitution maps to terms that are representatives 
233 

* according to the quantifiers state. 
234 

* Wrt evaluateTerm, this version does not construct new terms, and 
235 

* thus is less aggressive. 
236 

*/ 
237 

TNode getEntailedTerm(TNode n, std::map<TNode, TNode>& subs, bool subsRep); 
238 

/** is entailed 
239 

* Checks whether the current context entails n with polarity pol, based on 
240 

* the equality information in the quantifiers state. Returns true if the 
241 

* entailment can be successfully shown. 
242 

*/ 
243 

bool isEntailed(TNode n, bool pol); 
244 

/** is entailed 
245 

* 
246 

* Checks whether the current context entails ( n * subs ) with polarity pol, 
247 

* based on the equality information in the quantifiers state, 
248 

* where * denotes substitution application. 
249 

* subsRep is whether the substitution maps to terms that are representatives 
250 

* according to in the quantifiers state. 
251 

*/ 
252 

bool isEntailed(TNode n, 
253 

std::map<TNode, TNode>& subs, 
254 

bool subsRep, 
255 

bool pol); 
256 

/** is the term n active in the current context? 
257 

* 
258 

* By default, all terms are active. A term is inactive if: 
259 

* (1) it is congruent to another term 
260 

* (2) it is irrelevant based on the term database mode. This includes terms 
261 

* that only appear in literals that are not relevant. 
262 

* (3) it contains instantiation constants (used for CEGQI and cannot be used 
263 

* in instantiation). 
264 

* (4) it is explicitly set inactive by a call to setTermInactive(...). 
265 

* We store whether a term is inactive in a SATcontextdependent map. 
266 

*/ 
267 

bool isTermActive(Node n); 
268 

/** set that term n is inactive in this context. */ 
269 

void setTermInactive(Node n); 
270 

/** has term current 
271 

* 
272 

* This function is used in cases where we restrict which terms appear in the 
273 

* database, such as for heuristics used in local theory extensions 
274 

* and for termdbmode=relevant. 
275 

* It returns whether the term n should be indexed in the current context. 
276 

* 
277 

* If the argument useMode is true, then this method returns a value based on 
278 

* the option options::termDbMode(). 
279 

* Otherwise, it returns the lookup in the map d_has_map. 
280 

*/ 
281 

bool hasTermCurrent(Node n, bool useMode = true); 
282 

/** is term eligble for instantiation? */ 
283 

bool isTermEligibleForInstantiation(TNode n, TNode f); 
284 

/** get eligible term in equivalence class of r */ 
285 

Node getEligibleTermInEqc(TNode r); 
286 

/** get higherorder type match predicate 
287 

* 
288 

* This predicate is used to force certain functions f of type tn to appear as 
289 

* firstclass representatives in the quantifierfree UF solver. For a typical 
290 

* use case, we call getHoTypeMatchPredicate which returns a fresh predicate 
291 

* P of type (tn > Bool). Then, we add P( f ) as a lemma. 
292 

*/ 
293 

Node getHoTypeMatchPredicate(TypeNode tn); 
294 


295 

private: 
296 

/** The quantifiers state object */ 
297 

QuantifiersState& d_qstate; 
298 

/** Pointer to the quantifiers inference manager */ 
299 

QuantifiersInferenceManager* d_qim; 
300 

/** The quantifiers registry */ 
301 

QuantifiersRegistry& d_qreg; 
302 

/** A context for the data structures below, when not contextdependent */ 
303 

context::Context d_termsContext; 
304 

/** The context we are using for the data structures below */ 
305 

context::Context* d_termsContextUse; 
306 

/** terms processed */ 
307 

NodeSet d_processed; 
308 

/** map from types to ground terms for that type */ 
309 

TypeNodeDbListMap d_typeMap; 
310 

/** list of all operators */ 
311 

NodeList d_ops; 
312 

/** map from operators to ground terms for that operator */ 
313 

NodeDbListMap d_opMap; 
314 

/** select op map */ 
315 

std::map< Node, std::map< TypeNode, Node > > d_par_op_map; 
316 

/** whether master equality engine is UFinconsistent */ 
317 

bool d_consistent_ee; 
318 

/** boolean terms */ 
319 

Node d_true; 
320 

Node d_false; 
321 

/** map from type nodes to a fresh variable we introduced */ 
322 

std::unordered_map<TypeNode, Node, TypeNodeHashFunction> d_type_fv; 
323 

/** inactive map */ 
324 

NodeBoolMap d_inactive_map; 
325 

/** count of the number of nonredundant ground terms per operator */ 
326 

std::map< Node, int > d_op_nonred_count; 
327 

/** mapping from terms to representatives of their arguments */ 
328 

std::map< TNode, std::vector< TNode > > d_arg_reps; 
329 

/** map from operators to trie */ 
330 

std::map<Node, TNodeTrie> d_func_map_trie; 
331 

std::map<Node, TNodeTrie> d_func_map_eqc_trie; 
332 

/** mapping from operators to their representative relevant domains */ 
333 

std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; 
334 

/** has map */ 
335 

std::map< Node, bool > d_has_map; 
336 

/** map from reps to a term in eqc in d_has_map */ 
337 

std::map<Node, Node> d_term_elig_eqc; 
338 

/** 
339 

* Dummy predicate that states terms should be considered firstclass members 
340 

* of equality engine (for higherorder). 
341 

*/ 
342 

std::map<TypeNode, Node> d_ho_type_match_pred; 
343 

/** set has term */ 
344 

void setHasTerm( Node n ); 
345 

/** helper for evaluate term */ 
346 

Node evaluateTerm2(TNode n, 
347 

std::map<TNode, Node>& visited, 
348 

std::vector<Node>& exp, 
349 

bool useEntailmentTests, 
350 

bool computeExp, 
351 

bool reqHasTerm); 
352 

/** helper for get entailed term */ 
353 

TNode getEntailedTerm2(TNode n, 
354 

std::map<TNode, TNode>& subs, 
355 

bool subsRep, 
356 

bool hasSubs); 
357 

/** helper for is entailed */ 
358 

bool isEntailed2(TNode n, 
359 

std::map<TNode, TNode>& subs, 
360 

bool subsRep, 
361 

bool hasSubs, 
362 

bool pol); 
363 

/** compute uf eqc terms : 
364 

* Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes 
365 

*/ 
366 

void computeUfEqcTerms( TNode f ); 
367 

/** compute uf terms 
368 

* Ensure that an entry for f is in d_func_map_trie 
369 

*/ 
370 

void computeUfTerms( TNode f ); 
371 

/** compute arg reps 
372 

* Ensure that an entry for n is in d_arg_reps 
373 

*/ 
374 

void computeArgReps(TNode n); 
375 

//higherorder term indexing 
376 

/** 
377 

* Map from nonvariable function terms to the operator used to purify it in 
378 

* this database. For details, see addTermHo. 
379 

*/ 
380 

std::map<Node, Node> d_ho_fun_op_purify; 
381 

/** 
382 

* Map from terms to the term that they purified. For details, see addTermHo. 
383 

*/ 
384 

std::map<Node, Node> d_ho_purify_to_term; 
385 

/** 
386 

* Map from terms in the domain of the above map to an equality between that 
387 

* term and its range in the above map. 
388 

*/ 
389 

std::map<Node, Node> d_ho_purify_to_eq; 
390 

/** a map from matchable operators to their representative */ 
391 

std::map< TNode, TNode > d_ho_op_rep; 
392 

/** for each representative matchable operator, the list of other matchable operators in their equivalence class */ 
393 

std::map<TNode, std::vector<TNode> > d_ho_op_slaves; 
394 

/** add term higherorder 
395 

* 
396 

* This registers additional terms corresponding to (possibly multiple) 
397 

* purifications of a higherorder term n. 
398 

* 
399 

* Consider the example: 
400 

* g : Int > Int, f : Int x Int > Int 
401 

* constraints: (@ f 0) = g, (f 0 1) = (@ (@ f 0) 1) = 3 
402 

* pattern: (g x) 
403 

* where @ is HO_APPLY. 
404 

* We have that (g x){ x > 1 } is an Ematch for (@ (@ f 0) 1). 
405 

* With the standard registration in addTerm, we construct term indices for 
406 

* f, g, @ : Int x Int > Int, @ : Int > Int. 
407 

* However, to match (g x) with (@ (@ f 0) 1), we require that 
408 

* [1] > (@ (@ f 0) 1) 
409 

* is an entry in the term index of g. To do this, we maintain a term 
410 

* index for a fresh variable pfun, the purification variable for 
411 

* (@ f 0). Thus, we register the term (pfun 1) in the call to this function 
412 

* for (@ (@ f 0) 1). This ensures that, when processing the equality 
413 

* (@ f 0) = g, we merge the term indices of g and pfun. Hence, the entry 
414 

* [1] > (@ (@ f 0) 1) 
415 

* is added to the term index of g, assuming g is the representative of 
416 

* the equivalence class of g and pfun. 
417 

* 
418 

* Above, we set d_ho_fun_op_purify[(@ f 0)] = pfun, and 
419 

* d_ho_purify_to_term[(pfun 1)] = (@ (@ f 0) 1). 
420 

*/ 
421 

void addTermHo(Node n); 
422 

/** get operator representative */ 
423 

Node getOperatorRepresentative( TNode op ) const; 
424 

//end higherorder term indexing 
425 

};/* class TermDb */ 
426 


427 

}/* CVC4::theory::quantifiers namespace */ 
428 

}/* CVC4::theory namespace */ 
429 

}/* CVC4 namespace */ 
430 


431 

#endif /* CVC4__THEORY__QUANTIFIERS__TERM_DATABASE_H */ 