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 : 238140 : 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 : : using NodeBoolMap = context::CDHashMap<Node, bool>;
67 : : using NodeList = context::CDList<Node>;
68 : : using NodeSet = context::CDHashSet<Node>;
69 : : using TypeNodeDbListMap =
70 : : context::CDHashMap<TypeNode, std::shared_ptr<DbList>>;
71 : : using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
72 : :
73 : : public:
74 : : TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
75 : : virtual ~TermDb();
76 : : /** Finish init, which sets the inference manager */
77 : : void finishInit(QuantifiersInferenceManager* qim);
78 : : /** presolve (called once per user check-sat) */
79 : : void presolve() override;
80 : : /** reset (calculate which terms are active) */
81 : : bool reset(Theory::Effort effort) override;
82 : : /** register quantified formula */
83 : : void registerQuantifier(Node q) override;
84 : : /** identify */
85 : 0 : std::string identify() const override { return "TermDb"; }
86 : : /** get number of operators */
87 : : size_t getNumOperators() const;
88 : : /** get operator at index i */
89 : : Node getOperator(size_t i) const;
90 : : /** ground terms for operator
91 : : * Get the number of ground terms with operator f that have been added to the
92 : : * database
93 : : */
94 : : size_t getNumGroundTerms(TNode f) const;
95 : : /** get ground term for operator
96 : : * Get the i^th ground term with operator f that has been added to the database
97 : : */
98 : : Node getGroundTerm(TNode f, size_t i) const;
99 : : /** Get ground term list */
100 : : DbList* getGroundTermList(TNode f) const;
101 : : /** get num type terms
102 : : * Get the number of ground terms of tn that have been added to the database
103 : : */
104 : : size_t getNumTypeGroundTerms(TypeNode tn) const;
105 : : /** get type ground term
106 : : * Returns the i^th ground term of type tn
107 : : */
108 : : Node getTypeGroundTerm(TypeNode tn, size_t i) const;
109 : : /** get or make ground term
110 : : *
111 : : * Returns the first ground term of type tn, or makes one if none exist. If
112 : : * reqVar is true, then the ground term must be a variable.
113 : : */
114 : : Node getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar = false);
115 : : /** make fresh variable
116 : : * Returns a fresh variable of type tn.
117 : : * This will return only a single fresh
118 : : * variable per type.
119 : : */
120 : : Node getOrMakeTypeFreshVariable(TypeNode tn);
121 : : /**
122 : : * Add a term to the database, which registers it as a term that may be
123 : : * matched with via E-matching, and can be used in entailment tests below.
124 : : */
125 : : void addTerm(Node n);
126 : : /** notification when master equality engine merges two classes*/
127 : : void eqNotifyMerge(TNode t1, TNode t2);
128 : : /** Get the currently added ground terms of the given type */
129 : : DbList* getOrMkDbListForType(TypeNode tn);
130 : : /** Get the currently added ground terms for the given operator */
131 : : DbList* getOrMkDbListForOp(TNode op);
132 : : /** get match operator for term n
133 : : *
134 : : * If n has a kind that we index, this function will
135 : : * typically return n.getOperator().
136 : : *
137 : : * However, for parametric operators f, the match operator is an arbitrary
138 : : * chosen f-application. For example, consider array select:
139 : : * A : (Array Int Int)
140 : : * B : (Array Bool Int)
141 : : * We require that terms like (select A 1) and (select B 2) are indexed in
142 : : * separate
143 : : * data structures despite the fact that
144 : : * (select A 1).getOperator()==(select B 2).getOperator().
145 : : * Hence, for the above terms, we may return:
146 : : * getMatchOperator( (select A 1) ) = (select A 1), and
147 : : * getMatchOperator( (select B 2) ) = (select B 2).
148 : : * The match operator is the first instance of an application of the
149 : : * parametric operator of its type.
150 : : *
151 : : * If n has a kind that we do not index (like ADD),
152 : : * then this function returns Node::null().
153 : : */
154 : : Node getMatchOperator(TNode n);
155 : : /** Is matchable? true if the above method is non-null */
156 : : bool isMatchable(TNode n);
157 : : /** get term arg index for all f-applications in the current context */
158 : : TNodeTrie* getTermArgTrie(Node f);
159 : : /** get the term arg trie for f-applications in the equivalence class of eqc.
160 : : */
161 : : TNodeTrie* getTermArgTrie(Node eqc, Node f);
162 : : /** get congruent term
163 : : * If possible, returns a term t such that:
164 : : * (1) t is a term that is currently indexed by this database,
165 : : * (2) t is of the form f( t1, ..., tk ) and n is of the form f( s1, ..., sk ),
166 : : * where ti is in the equivalence class of si for i=1...k.
167 : : */
168 : : TNode getCongruentTerm(Node f, Node n);
169 : : /** get congruent term
170 : : * If possible, returns a term t such that:
171 : : * (1) t is a term that is currently indexed by this database,
172 : : * (2) t is of the form f( t1, ..., tk ) where ti is in the
173 : : * equivalence class of args[i] for i=1...k.
174 : : * If not possible, return the null node.
175 : : */
176 : : TNode getCongruentTerm(Node f, const 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, size_t i, TNode r);
184 : : /** is the term n active in the current context?
185 : : *
186 : : * By default, all terms are active. A term is inactive if:
187 : : * (1) it is congruent to another term
188 : : * (2) it is irrelevant based on the term database mode. This includes terms
189 : : * that only appear in literals that are not relevant.
190 : : * (3) it contains instantiation constants (used for CEGQI and cannot be used
191 : : * in instantiation).
192 : : * (4) it is explicitly set inactive by a call to setTermInactive(...).
193 : : * We store whether a term is inactive in a SAT-context-dependent map.
194 : : */
195 : : bool isTermActive(Node n);
196 : : /** set that term n is inactive in this context. */
197 : : void setTermInactive(Node n);
198 : : /** has term current
199 : : *
200 : : * This function is used in cases where we restrict which terms appear in the
201 : : * database, such as for heuristics used in local theory extensions
202 : : * and for --term-db-mode=relevant.
203 : : * It returns whether the term n should be indexed in the current context.
204 : : *
205 : : * If the argument useMode is true, then this method returns a value based on
206 : : * the option termDbMode.
207 : : * Otherwise, it returns the lookup in the map d_has_map.
208 : : */
209 : : bool hasTermCurrent(const Node& n, bool useMode = true) const;
210 : : /** is term eligble for instantiation? */
211 : : bool isTermEligibleForInstantiation(TNode n, TNode f);
212 : : /** get eligible term in equivalence class of r */
213 : : Node getEligibleTermInEqc(TNode r);
214 : :
215 : : protected:
216 : : /** The quantifiers state object */
217 : : QuantifiersState& d_qstate;
218 : : /** Pointer to the quantifiers inference manager */
219 : : QuantifiersInferenceManager* d_qim;
220 : : /** The quantifiers registry */
221 : : QuantifiersRegistry& d_qreg;
222 : : /** A context for the data structures below, when not context-dependent */
223 : : context::Context d_termsContext;
224 : : /** The context we are using for the data structures below */
225 : : context::Context* d_termsContextUse;
226 : : /** terms processed */
227 : : NodeSet d_processed;
228 : : /** map from types to ground terms for that type */
229 : : TypeNodeDbListMap d_typeMap;
230 : : /** list of all operators */
231 : : NodeList d_ops;
232 : : /** map from operators to ground terms for that operator */
233 : : NodeDbListMap d_opMap;
234 : : /** select op map */
235 : : std::map< Node, std::map< TypeNode, Node > > d_par_op_map;
236 : : /** boolean terms */
237 : : Node d_true;
238 : : Node d_false;
239 : : /** map from type nodes to a fresh variable we introduced */
240 : : std::unordered_map<TypeNode, Node> d_type_fv;
241 : : /** inactive map */
242 : : NodeBoolMap d_inactive_map;
243 : : /** count of the number of non-redundant ground terms per operator */
244 : : std::map< Node, int > d_op_nonred_count;
245 : : /** mapping from terms to representatives of their arguments */
246 : : std::map< TNode, std::vector< TNode > > d_arg_reps;
247 : : /** map from operators to trie */
248 : : std::map<Node, TNodeTrie> d_func_map_trie;
249 : : std::map<Node, TNodeTrie> d_func_map_eqc_trie;
250 : : /**
251 : : * Mapping from operators to their representative relevant domains. The
252 : : * size of the range is equal to the arity of the domain symbol. The
253 : : * terms in each vector are the representatives that occur in a term for
254 : : * that argument position (see inRelevantDomain).
255 : : */
256 : : std::map<Node, std::vector<std::vector<TNode>>> d_fmapRelDom;
257 : : /** has map */
258 : : context::CDHashSet<Node> d_has_map;
259 : : /** map from reps to a term in eqc in d_has_map */
260 : : std::map<Node, Node> d_term_elig_eqc;
261 : : /**
262 : : * Dummy predicate that states terms should be considered first-class members
263 : : * of equality engine (for higher-order).
264 : : */
265 : : std::map<TypeNode, Node> d_ho_type_match_pred;
266 : : /** A proof generator for disequal congruent terms */
267 : : std::shared_ptr<DeqCongProofGenerator> d_dcproof;
268 : : //----------------------------- implementation-specific
269 : : /**
270 : : * Finish reset internal, called at the end of reset(e). Returning false will
271 : : * cause the overall reset to return false.
272 : : */
273 : : virtual bool finishResetInternal(Theory::Effort e);
274 : : /** Add term internal, called when addTerm(n) is called */
275 : : virtual void addTermInternal(Node n);
276 : : /** Get operators that we know are equivalent to f, typically only f itself */
277 : : virtual void getOperatorsFor(TNode f, std::vector<TNode>& ops);
278 : : /** get the chosen representative for operator op */
279 : : virtual Node getOperatorRepresentative(TNode op) const;
280 : : /**
281 : : * This method is called when terms a and b are indexed by the same operator,
282 : : * and have equivalent arguments. This method checks if we are in conflict,
283 : : * which is the case if a and b are disequal in the equality engine.
284 : : * If so, it adds any additional arguments that explain why a = b, e.g. the
285 : : * equivalence of their operators if their operators are different.
286 : : */
287 : : virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp);
288 : : //----------------------------- end implementation-specific
289 : : /** set has term */
290 : : void setHasTerm( Node n );
291 : : /** compute uf eqc terms :
292 : : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
293 : : */
294 : : void computeUfEqcTerms( TNode f );
295 : : /** compute uf terms
296 : : * Ensure that an entry for f is in d_func_map_trie
297 : : */
298 : : void computeUfTerms( TNode f );
299 : : /** compute arg reps
300 : : * Ensure that an entry for n is in d_arg_reps
301 : : */
302 : : void computeArgReps(TNode n);
303 : : };/* class TermDb */
304 : :
305 : : } // namespace quantifiers
306 : : } // namespace theory
307 : : } // namespace cvc5::internal
308 : :
309 : : #endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
|
