Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Term database class.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
16 : : #define CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H
17 : :
18 : : #include <map>
19 : : #include <unordered_map>
20 : :
21 : : #include "context/cdhashmap.h"
22 : : #include "context/cdhashset.h"
23 : : #include "expr/attribute.h"
24 : : #include "expr/node_trie.h"
25 : : #include "theory/quantifiers/quant_util.h"
26 : : #include "theory/theory.h"
27 : : #include "theory/type_enumerator.h"
28 : :
29 : : namespace cvc5::internal {
30 : : namespace theory {
31 : : namespace quantifiers {
32 : :
33 : : class QuantifiersState;
34 : : class QuantifiersInferenceManager;
35 : : class QuantifiersRegistry;
36 : : class DeqCongProofGenerator;
37 : :
38 : : /** Context-dependent list of nodes */
39 : : class DbList
40 : : {
41 : : public:
42 : 238197 : DbList(context::Context* c) : d_list(c) {}
43 : : /** The list */
44 : : context::CDList<Node> d_list;
45 : : };
46 : :
47 : : /** Term Database
48 : : *
49 : : * This class is a key utility used by
50 : : * a number of approaches for quantifier instantiation,
51 : : * including E-matching, conflict-based instantiation,
52 : : * and model-based instantiation.
53 : : *
54 : : * The primary responsibilities for this class are to :
55 : : * (1) Maintain a list of all ground terms that exist in the quantifier-free
56 : : * solvers, as notified through the master equality engine.
57 : : * (2) Build TNodeTrie objects that index all ground terms, per operator.
58 : : *
59 : : * Like other utilities, its reset(...) function is called
60 : : * at the beginning of full or last call effort checks.
61 : : * This initializes the database for the round. However,
62 : : * notice that TNodeTrie objects are computed
63 : : * lazily for performance reasons.
64 : : */
65 : : class TermDb : public QuantifiersUtil
66 : : {
67 : : using NodeBoolMap = context::CDHashMap<Node, bool>;
68 : : using NodeList = context::CDList<Node>;
69 : : using NodeSet = context::CDHashSet<Node>;
70 : : using TypeNodeDbListMap =
71 : : context::CDHashMap<TypeNode, std::shared_ptr<DbList>>;
72 : : using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
73 : :
74 : : public:
75 : : TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
76 : : virtual ~TermDb();
77 : : /** Finish init, which sets the inference manager */
78 : : void finishInit(QuantifiersInferenceManager* qim);
79 : : /** presolve (called once per user check-sat) */
80 : : void presolve() override;
81 : : /** reset (calculate which terms are active) */
82 : : bool reset(Theory::Effort effort) override;
83 : : /** register quantified formula */
84 : : void registerQuantifier(Node q) override;
85 : : /** identify */
86 : 0 : std::string identify() const override { return "TermDb"; }
87 : : /** get number of operators */
88 : : size_t getNumOperators() const;
89 : : /** get operator at index i */
90 : : Node getOperator(size_t i) const;
91 : : /** ground terms for operator
92 : : * Get the number of ground terms with operator f that have been added to the
93 : : * database
94 : : */
95 : : size_t getNumGroundTerms(TNode f) const;
96 : : /** get ground term for operator
97 : : * Get the i^th ground term with operator f that has been added to the
98 : : * database
99 : : */
100 : : Node getGroundTerm(TNode f, size_t i) const;
101 : : /** Get ground term list */
102 : : DbList* getGroundTermList(TNode f) const;
103 : : /** get num type terms
104 : : * Get the number of ground terms of tn that have been added to the database
105 : : */
106 : : size_t getNumTypeGroundTerms(TypeNode tn) const;
107 : : /** get type ground term
108 : : * Returns the i^th ground term of type tn
109 : : */
110 : : Node getTypeGroundTerm(TypeNode tn, size_t i) const;
111 : : /** get or make ground term
112 : : *
113 : : * Returns the first ground term of type tn, or makes one if none exist. If
114 : : * reqVar is true, then the ground term must be a variable.
115 : : */
116 : : Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false);
117 : : /** make fresh variable
118 : : * Returns a fresh variable of type tn.
119 : : * This will return only a single fresh
120 : : * variable per type.
121 : : */
122 : : Node getOrMakeTypeFreshVariable(TypeNode tn);
123 : : /**
124 : : * Add a term to the database, which registers it as a term that may be
125 : : * matched with via E-matching, and can be used in entailment tests below.
126 : : */
127 : : void addTerm(Node n);
128 : : /** notification when master equality engine merges two classes*/
129 : : void eqNotifyMerge(TNode t1, TNode t2);
130 : : /** Get the currently added ground terms of the given type */
131 : : DbList* getOrMkDbListForType(TypeNode tn);
132 : : /** Get the currently added ground terms for the given operator */
133 : : DbList* getOrMkDbListForOp(TNode op);
134 : : /** get match operator for term n
135 : : *
136 : : * If n has a kind that we index, this function will
137 : : * typically return n.getOperator().
138 : : *
139 : : * However, for parametric operators f, the match operator is an arbitrary
140 : : * chosen f-application. For example, consider array select:
141 : : * A : (Array Int Int)
142 : : * B : (Array Bool Int)
143 : : * We require that terms like (select A 1) and (select B 2) are indexed in
144 : : * separate
145 : : * data structures despite the fact that
146 : : * (select A 1).getOperator()==(select B 2).getOperator().
147 : : * Hence, for the above terms, we may return:
148 : : * getMatchOperator( (select A 1) ) = (select A 1), and
149 : : * getMatchOperator( (select B 2) ) = (select B 2).
150 : : * The match operator is the first instance of an application of the
151 : : * parametric operator of its type.
152 : : *
153 : : * If n has a kind that we do not index (like ADD),
154 : : * then this function returns Node::null().
155 : : */
156 : : Node getMatchOperator(TNode n);
157 : : /** Is matchable? true if the above method is non-null */
158 : : bool isMatchable(TNode n);
159 : : /** get term arg index for all f-applications in the current context */
160 : : TNodeTrie* getTermArgTrie(Node f);
161 : : /** get the term arg trie for f-applications in the equivalence class of eqc.
162 : : */
163 : : TNodeTrie* getTermArgTrie(Node eqc, Node f);
164 : : /** get congruent term
165 : : * If possible, returns a term t such that:
166 : : * (1) t is a term that is currently indexed by this database,
167 : : * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk
168 : : * ), where ti is in the equivalence class of si for i=1...k.
169 : : */
170 : : TNode getCongruentTerm(Node f, Node n);
171 : : /** get congruent term
172 : : * If possible, returns a term t such that:
173 : : * (1) t is a term that is currently indexed by this database,
174 : : * (2) t is of the form f( t1, ..., tk ) where ti is in the
175 : : * equivalence class of args[i] for i=1...k.
176 : : * If not possible, return the null node.
177 : : */
178 : : TNode getCongruentTerm(Node f, const std::vector<TNode>& args);
179 : : /** in relevant domain
180 : : * Returns true if there is at least one term t such that:
181 : : * (1) t is a term that is currently indexed by this database,
182 : : * (2) t is of the form f( t1, ..., tk ) and ti is in the
183 : : * equivalence class of r.
184 : : */
185 : : bool inRelevantDomain(TNode f, size_t i, TNode r);
186 : : /** is the term n active in the current context?
187 : : *
188 : : * By default, all terms are active. A term is inactive if:
189 : : * (1) it is congruent to another term
190 : : * (2) it is irrelevant based on the term database mode. This includes terms
191 : : * that only appear in literals that are not relevant.
192 : : * (3) it contains instantiation constants (used for CEGQI and cannot be used
193 : : * in instantiation).
194 : : * (4) it is explicitly set inactive by a call to setTermInactive(...).
195 : : * We store whether a term is inactive in a SAT-context-dependent map.
196 : : */
197 : : bool isTermActive(Node n);
198 : : /** set that term n is inactive in this context. */
199 : : void setTermInactive(Node n);
200 : : /** has term current
201 : : *
202 : : * This function is used in cases where we restrict which terms appear in the
203 : : * database, such as for heuristics used in local theory extensions
204 : : * and for --term-db-mode=relevant.
205 : : * It returns whether the term n should be indexed in the current context.
206 : : *
207 : : * If the argument useMode is true, then this method returns a value based on
208 : : * the option termDbMode.
209 : : * Otherwise, it returns the lookup in the map d_has_map.
210 : : */
211 : : bool hasTermCurrent(const Node& n, bool useMode = true) const;
212 : : /** is term eligble for instantiation? */
213 : : bool isTermEligibleForInstantiation(TNode n, TNode f);
214 : : /** get eligible term in equivalence class of r */
215 : : Node getEligibleTermInEqc(TNode r);
216 : : /**
217 : : * Set has term. This marks that n should be added to the term indicies
218 : : * used for E-matching when term-db is RELEVANT or RELEVANT_ALL_DELAY. This
219 : : * method is called on all terms that appear in assertions, and on all terms
220 : : * that appear in the master equality engine at last call effort if term-db is
221 : : * RELEVANT_ALL_DELAY.
222 : : * @param n the term to add.
223 : : */
224 : : void setHasTerm(Node n);
225 : :
226 : : protected:
227 : : /** The quantifiers state object */
228 : : QuantifiersState& d_qstate;
229 : : /** Pointer to the quantifiers inference manager */
230 : : QuantifiersInferenceManager* d_qim;
231 : : /** The quantifiers registry */
232 : : QuantifiersRegistry& d_qreg;
233 : : /** Whether we are tracking relevant terms */
234 : : bool d_trackRlv;
235 : : /** A context for the data structures below, when not context-dependent */
236 : : context::Context d_termsContext;
237 : : /** The context we are using for the data structures below */
238 : : context::Context* d_termsContextUse;
239 : : /** terms processed */
240 : : NodeSet d_processed;
241 : : /** map from types to ground terms for that type */
242 : : TypeNodeDbListMap d_typeMap;
243 : : /** list of all operators */
244 : : NodeList d_ops;
245 : : /** map from operators to ground terms for that operator */
246 : : NodeDbListMap d_opMap;
247 : : /** select op map */
248 : : std::map<Node, std::map<TypeNode, Node>> d_par_op_map;
249 : : /** boolean terms */
250 : : Node d_true;
251 : : Node d_false;
252 : : /** map from type nodes to a fresh variable we introduced */
253 : : std::unordered_map<TypeNode, Node> d_type_fv;
254 : : /** inactive map */
255 : : NodeBoolMap d_inactive_map;
256 : : /** count of the number of non-redundant ground terms per operator */
257 : : std::map<Node, int> d_op_nonred_count;
258 : : /** mapping from terms to representatives of their arguments */
259 : : std::map<TNode, std::vector<TNode>> d_arg_reps;
260 : : /** map from operators to trie */
261 : : std::map<Node, TNodeTrie> d_func_map_trie;
262 : : std::map<Node, TNodeTrie> d_func_map_eqc_trie;
263 : : /**
264 : : * Mapping from operators to their representative relevant domains. The
265 : : * size of the range is equal to the arity of the domain symbol. The
266 : : * terms in each vector are the representatives that occur in a term for
267 : : * that argument position (see inRelevantDomain).
268 : : */
269 : : std::map<Node, std::vector<std::vector<TNode>>> d_fmapRelDom;
270 : : /** has map */
271 : : context::CDHashSet<Node> d_has_map;
272 : : /** map from reps to a term in eqc in d_has_map */
273 : : std::map<Node, Node> d_term_elig_eqc;
274 : : /**
275 : : * Dummy predicate that states terms should be considered first-class members
276 : : * of equality engine (for higher-order).
277 : : */
278 : : std::map<TypeNode, Node> d_ho_type_match_pred;
279 : : /** A proof generator for disequal congruent terms */
280 : : std::shared_ptr<DeqCongProofGenerator> d_dcproof;
281 : : //----------------------------- implementation-specific
282 : : /**
283 : : * Finish reset internal, called at the end of reset(e). Returning false will
284 : : * cause the overall reset to return false.
285 : : */
286 : : virtual bool finishResetInternal(Theory::Effort e);
287 : : /** Add term internal, called when addTerm(n) is called */
288 : : virtual void addTermInternal(Node n);
289 : : /** Get operators that we know are equivalent to f, typically only f itself */
290 : : virtual void getOperatorsFor(TNode f, std::vector<TNode>& ops);
291 : : /** get the chosen representative for operator op */
292 : : virtual Node getOperatorRepresentative(TNode op) const;
293 : : /**
294 : : * This method is called when terms a and b are indexed by the same operator,
295 : : * and have equivalent arguments. This method checks if we are in conflict,
296 : : * which is the case if a and b are disequal in the equality engine.
297 : : * If so, it adds any additional arguments that explain why a = b, e.g. the
298 : : * equivalence of their operators if their operators are different.
299 : : */
300 : : virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp);
301 : : //----------------------------- end implementation-specific
302 : : /** compute uf eqc terms :
303 : : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
304 : : */
305 : : void computeUfEqcTerms(TNode f);
306 : : /** compute uf terms
307 : : * Ensure that an entry for f is in d_func_map_trie
308 : : */
309 : : void computeUfTerms(TNode f);
310 : : /** compute arg reps
311 : : * Ensure that an entry for n is in d_arg_reps
312 : : */
313 : : void computeArgReps(TNode n);
314 : : }; /* class TermDb */
315 : :
316 : : } // namespace quantifiers
317 : : } // namespace theory
318 : : } // namespace cvc5::internal
319 : :
320 : : #endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
|
