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-2024 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 : :
40 : : /** Context-dependent list of nodes */
41 : : class DbList
42 : : {
43 : : public:
44 : 239070 : DbList(context::Context* c) : d_list(c) {}
45 : : /** The list */
46 : : context::CDList<Node> d_list;
47 : : };
48 : :
49 : : /** Term Database
50 : : *
51 : : * This class is a key utility used by
52 : : * a number of approaches for quantifier instantiation,
53 : : * including E-matching, conflict-based instantiation,
54 : : * and model-based instantiation.
55 : : *
56 : : * The primary responsibilities for this class are to :
57 : : * (1) Maintain a list of all ground terms that exist in the quantifier-free
58 : : * solvers, as notified through the master equality engine.
59 : : * (2) Build TNodeTrie objects that index all ground terms, per operator.
60 : : *
61 : : * Like other utilities, its reset(...) function is called
62 : : * at the beginning of full or last call effort checks.
63 : : * This initializes the database for the round. However,
64 : : * notice that TNodeTrie objects are computed
65 : : * lazily for performance reasons.
66 : : */
67 : : class TermDb : public QuantifiersUtil {
68 : : using NodeBoolMap = context::CDHashMap<Node, bool>;
69 : : using NodeList = context::CDList<Node>;
70 : : using NodeSet = context::CDHashSet<Node>;
71 : : using TypeNodeDbListMap =
72 : : context::CDHashMap<TypeNode, std::shared_ptr<DbList>>;
73 : : using NodeDbListMap = context::CDHashMap<Node, std::shared_ptr<DbList>>;
74 : :
75 : : public:
76 : : TermDb(Env& env, QuantifiersState& qs, QuantifiersRegistry& qr);
77 : : virtual ~TermDb();
78 : : /** Finish init, which sets the inference manager */
79 : : void finishInit(QuantifiersInferenceManager* qim);
80 : : /** presolve (called once per user check-sat) */
81 : : void presolve() override;
82 : : /** reset (calculate which terms are active) */
83 : : bool reset(Theory::Effort effort) override;
84 : : /** register quantified formula */
85 : : void registerQuantifier(Node q) override;
86 : : /** identify */
87 : 0 : std::string identify() const override { return "TermDb"; }
88 : : /** get number of operators */
89 : : size_t getNumOperators() const;
90 : : /** get operator at index i */
91 : : Node getOperator(size_t i) const;
92 : : /** ground terms for operator
93 : : * Get the number of ground terms with operator f that have been added to the
94 : : * database
95 : : */
96 : : size_t getNumGroundTerms(TNode f) const;
97 : : /** get ground term for operator
98 : : * Get the i^th ground term with operator f that has been added to the 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 : : /** 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 : : std::map< Node, bool > 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 : : //----------------------------- implementation-specific
267 : : /**
268 : : * Finish reset internal, called at the end of reset(e). Returning false will
269 : : * cause the overall reset to return false.
270 : : */
271 : : virtual bool finishResetInternal(Theory::Effort e);
272 : : /** Add term internal, called when addTerm(n) is called */
273 : : virtual void addTermInternal(Node n);
274 : : /** Get operators that we know are equivalent to f, typically only f itself */
275 : : virtual void getOperatorsFor(TNode f, std::vector<TNode>& ops);
276 : : /** get the chosen representative for operator op */
277 : : virtual Node getOperatorRepresentative(TNode op) const;
278 : : /**
279 : : * This method is called when terms a and b are indexed by the same operator,
280 : : * and have equivalent arguments. This method checks if we are in conflict,
281 : : * which is the case if a and b are disequal in the equality engine.
282 : : * If so, it adds the set of literals that are implied but do not hold, e.g.
283 : : * the equality (= a b).
284 : : */
285 : : virtual bool checkCongruentDisequal(TNode a, TNode b, std::vector<Node>& exp);
286 : : //----------------------------- end implementation-specific
287 : : /** set has term */
288 : : void setHasTerm( Node n );
289 : : /** compute uf eqc terms :
290 : : * Ensure entries for f are in d_func_map_eqc_trie for all equivalence classes
291 : : */
292 : : void computeUfEqcTerms( TNode f );
293 : : /** compute uf terms
294 : : * Ensure that an entry for f is in d_func_map_trie
295 : : */
296 : : void computeUfTerms( TNode f );
297 : : /** compute arg reps
298 : : * Ensure that an entry for n is in d_arg_reps
299 : : */
300 : : void computeArgReps(TNode n);
301 : : };/* class TermDb */
302 : :
303 : : } // namespace quantifiers
304 : : } // namespace theory
305 : : } // namespace cvc5::internal
306 : :
307 : : #endif /* CVC5__THEORY__QUANTIFIERS__TERM_DATABASE_H */
|
