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