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 : : * Sets state object.
11 : : */
12 : :
13 : : #include "cvc5_private.h"
14 : :
15 : : #ifndef CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H
16 : : #define CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H
17 : :
18 : : #include <map>
19 : : #include <vector>
20 : :
21 : : #include "context/cdhashset.h"
22 : : #include "theory/sets/skolem_cache.h"
23 : : #include "theory/theory_state.h"
24 : : #include "theory/uf/equality_engine.h"
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace sets {
29 : :
30 : : class TheorySetsPrivate;
31 : :
32 : : /** Sets state
33 : : *
34 : : * The purpose of this class is to maintain information concerning the current
35 : : * set of assertions during a full effort check.
36 : : *
37 : : * During a full effort check, the solver for theory of sets should call:
38 : : * reset; ( registerEqc | registerTerm )*
39 : : * to initialize the information in this class regarding full effort checks.
40 : : * Other query calls are then valid for the remainder of the full effort check.
41 : : */
42 : : class SolverState : public TheoryState
43 : : {
44 : : typedef context::CDHashMap<Node, size_t> NodeIntMap;
45 : :
46 : : public:
47 : : SolverState(Env& env, Valuation val, SkolemCache& skc);
48 : : //-------------------------------- initialize per check
49 : : /** reset, clears the data structures maintained by this class. */
50 : : void reset();
51 : : /** register equivalence class whose type is tn */
52 : : void registerEqc(TypeNode tn, Node r);
53 : : /** register term n of type tnn in the equivalence class of r */
54 : : void registerTerm(Node r, TypeNode tnn, Node n);
55 : : //-------------------------------- end initialize per check
56 : : /** add equality to explanation
57 : : *
58 : : * This adds a = b to exp if a and b are syntactically disequal. The equality
59 : : * a = b should hold in the current context.
60 : : */
61 : : void addEqualityToExp(Node a, Node b, std::vector<Node>& exp) const;
62 : : /** Is formula n entailed to have polarity pol in the current context? */
63 : : bool isEntailed(Node n, bool pol) const;
64 : : /**
65 : : * Is the disequality between sets s and t entailed in the current context?
66 : : */
67 : : bool isSetDisequalityEntailed(Node s, Node t) const;
68 : : /**
69 : : * Get the equivalence class of the empty set of type tn, or null if it does
70 : : * not exist as a term in the current context.
71 : : */
72 : : Node getEmptySetEqClass(TypeNode tn) const;
73 : : /**
74 : : * Get the equivalence class of the universe set of type tn, or null if it
75 : : * does not exist as a term in the current context.
76 : : */
77 : : Node getUnivSetEqClass(TypeNode tn) const;
78 : : /**
79 : : * Get the singleton set in the equivalence class of representative r if it
80 : : * exists, or null if none exists.
81 : : */
82 : : Node getSingletonEqClass(Node r) const;
83 : : /** get binary operator term (modulo equality)
84 : : *
85 : : * This method returns a non-null node n if and only if a term n that is
86 : : * congruent to <k>(r1,r2) exists in the current context.
87 : : */
88 : : Node getBinaryOpTerm(Kind k, Node r1, Node r2) const;
89 : : /**
90 : : * Returns a term that is congruent to n in the current context.
91 : : *
92 : : * To ensure that inferences and processing is not redundant,
93 : : * this class computes congruence over all terms that exist in the current
94 : : * context. If a set of terms f( t1 ), ... f( tn ) are pairwise congruent
95 : : * (call this a "congruence class"), it selects one of these terms as a
96 : : * representative. All other terms return the representative term from
97 : : * its congruence class.
98 : : */
99 : : Node getCongruent(Node n) const;
100 : : /**
101 : : * This method returns true if n is not the representative of its congruence
102 : : * class.
103 : : */
104 : : bool isCongruent(Node n) const;
105 : :
106 : : /** Get the list of all equivalence classes of set terms */
107 : 87027 : const std::vector<Node>& getSetsEqClasses() const { return d_set_eqc; }
108 : : /** Get the list of all equivalence classes of set terms that have element
109 : : * type t */
110 : : const std::vector<Node> getSetsEqClasses(const TypeNode& t) const;
111 : :
112 : : /**
113 : : * Get the list of non-variable sets that exists in the equivalence class
114 : : * whose representative is r.
115 : : */
116 : : const std::vector<Node>& getNonVariableSets(Node r) const;
117 : : /**
118 : : * Get a variable set in the equivalence class with representative r, or null
119 : : * if none exist.
120 : : */
121 : : Node getVariableSet(Node r) const;
122 : : /** Get comprehension sets in equivalence class with representative r */
123 : : const std::vector<Node>& getComprehensionSets(Node r) const;
124 : : /** Get (positive) members of the set equivalence class r
125 : : *
126 : : * The members are return as a map, which maps members to their explanation.
127 : : * For example, if x = y, (member 5 y), (member 6 x), then getMembers(x)
128 : : * returns the map [ 5 -> (member 5 y), 6 -> (member 6 x)].
129 : : */
130 : : const std::map<Node, Node>& getMembers(Node r) const;
131 : : /** Get negative members of the set equivalence class r, similar to above */
132 : : const std::map<Node, Node>& getNegativeMembers(Node r) const;
133 : : /** Is the (positive) members list of set equivalence class r non-empty? */
134 : : bool hasMembers(Node r) const;
135 : : /** Get binary operator index
136 : : *
137 : : * This returns a mapping from binary operator kinds (INTERSECT, SET_MINUS,
138 : : * SET_UNION) to index of terms of that kind. Each kind k maps to a map whose
139 : : * entries are of the form [r1 -> r2 -> t], where t is a term in the current
140 : : * context, and t is of the form <k>(t1,t2) where t1=r1 and t2=r2 hold in the
141 : : * current context. The term t is the representative of its congruence class.
142 : : */
143 : : const std::map<Kind, std::map<Node, std::map<Node, Node>>>& getBinaryOpIndex()
144 : : const;
145 : :
146 : : /** Get binary operator index
147 : : *
148 : : * This returns the binary operator index of the given kind.
149 : : * See getBinaryOpIndex() above.
150 : : */
151 : : const std::map<Node, std::map<Node, Node>>& getBinaryOpIndex(Kind k);
152 : : /** get operator list
153 : : *
154 : : * This returns a mapping from set kinds to a list of terms of that kind
155 : : * that exist in the current context. Each of the terms in the range of this
156 : : * map is a representative of its congruence class.
157 : : */
158 : : const std::map<Kind, std::vector<Node>>& getOperatorList() const;
159 : : /** Get the list of all set.filter terms */
160 : : const std::vector<Node>& getFilterTerms() const;
161 : : /** Get the list of all set.map terms in the current user context */
162 : : const context::CDHashSet<Node>& getMapTerms() const;
163 : : /** Get the list of all rel.group terms in the current user context */
164 : : const context::CDHashSet<Node>& getGroupTerms() const;
165 : : /** Get the list of all skolem elements generated for map terms down rules in
166 : : * the current user context */
167 : : std::shared_ptr<context::CDHashSet<Node>> getMapSkolemElements(Node n);
168 : : /** Get the list of all comprehension sets in the current context */
169 : : const std::vector<Node>& getComprehensionSets() const;
170 : :
171 : : /**
172 : : * Is x entailed to be a member of set s in the current context?
173 : : */
174 : : bool isMember(TNode x, TNode s) const;
175 : : /**
176 : : * Add member, called when atom is of the form (member x s) where s is in the
177 : : * equivalence class of r.
178 : : */
179 : : void addMember(TNode r, TNode atom);
180 : : /**
181 : : * Called when equivalence classes t1 and t2 merge. This updates the
182 : : * membership lists, adding members of t2 into t1.
183 : : *
184 : : * If cset is non-null, then this is a singleton or empty set in the
185 : : * equivalence class of t1 where moreover t2 has no singleton or empty sets.
186 : : * When this is the case, notice that all members of t2 should be made equal
187 : : * to the element that cset contains, or we are in conflict if cset is the
188 : : * empty set. These conclusions are added to facts.
189 : : *
190 : : * This method returns false if a (single) conflict was added to facts, and
191 : : * true otherwise.
192 : : */
193 : : bool merge(TNode t1, TNode t2, std::vector<Node>& facts, TNode cset);
194 : :
195 : : /** register the skolem element for the set.map term n */
196 : : void registerMapSkolemElement(const Node& n, const Node& element);
197 : : /** register skolem element generated by grup count rule */
198 : : void registerPartElementSkolem(Node group, Node skolemElement);
199 : : /** return skolem elements generated by group part count rule. */
200 : : std::shared_ptr<context::CDHashSet<Node>> getPartElementSkolems(Node n);
201 : :
202 : : private:
203 : : /** constants */
204 : : Node d_true;
205 : : Node d_false;
206 : : /** the empty vector and map */
207 : : const std::vector<Node> d_emptyVec;
208 : : /** a convenient constant empty map */
209 : : const std::map<Node, Node> d_emptyMap;
210 : : /** Reference to skolem cache */
211 : : SkolemCache& d_skCache;
212 : : /** The list of all equivalence classes of type set in the current context */
213 : : std::vector<Node> d_set_eqc;
214 : : /** Maps types to the equivalence class containing empty set of that type */
215 : : std::map<TypeNode, Node> d_eqc_emptyset;
216 : : /** Maps types to the equivalence class containing univ set of that type */
217 : : std::map<TypeNode, Node> d_eqc_univset;
218 : : /** Maps equivalence classes to a singleton set that exists in it. */
219 : : std::map<Node, Node> d_eqc_singleton;
220 : : /** Map from terms to the representative of their congruence class */
221 : : std::map<Node, Node> d_congruent;
222 : : /** Map from equivalence classes to the list of non-variable sets in it */
223 : : std::map<Node, std::vector<Node>> d_nvar_sets;
224 : : /** A list of filter terms. It is initialized during full effort check */
225 : : std::vector<Node> d_filterTerms;
226 : : /** User context collection of set.map terms */
227 : : context::CDHashSet<Node> d_mapTerms;
228 : : /** User context collection of rel.group terms */
229 : : context::CDHashSet<Node> d_groupTerms;
230 : : /** User context collection of skolem elements generated for set.map terms */
231 : : context::CDHashMap<Node, std::shared_ptr<context::CDHashSet<Node>>>
232 : : d_mapSkolemElements;
233 : : /** Map from equivalence classes to the list of comprehension sets in it */
234 : : std::map<Node, std::vector<Node>> d_compSets;
235 : : /** Map from equivalence classes to a variable sets in it */
236 : : std::map<Node, Node> d_var_set;
237 : : /** polarity memberships
238 : : *
239 : : * d_pol_mems[0] maps equivalence class to their positive membership list
240 : : * with explanations (see getMembers), d_pol_mems[1] maps equivalence classes
241 : : * to their negative memberships.
242 : : */
243 : : std::map<Node, std::map<Node, Node>> d_pol_mems[2];
244 : : // -------------------------------- term indices
245 : : /** Term index for SET_MEMBER
246 : : *
247 : : * A term index maps equivalence class representatives to the representative
248 : : * of their congruence class.
249 : : *
250 : : * For example, the term index for member may contain an entry
251 : : * [ r1 -> r2 -> (member t1 t2) ] where r1 and r2 are representatives of their
252 : : * equivalence classes, (member t1 t2) is the representative of its congruence
253 : : * class, and r1=t1 and r2=t2 hold in the current context.
254 : : */
255 : : std::map<Node, std::map<Node, Node>> d_members_index;
256 : : /** Term index for SET_SINGLETON */
257 : : std::map<Node, Node> d_singleton_index;
258 : : /** Indices for the binary kinds INTERSECT, SET_MINUS and SET_UNION. */
259 : : std::map<Kind, std::map<Node, std::map<Node, Node>>> d_bop_index;
260 : : /** A list of comprehension sets */
261 : : std::vector<Node> d_allCompSets;
262 : : // -------------------------------- end term indices
263 : : /** List of operators per kind */
264 : : std::map<Kind, std::vector<Node>> d_op_list;
265 : : //--------------------------------- SAT-context-dependent member list
266 : : /**
267 : : * Map from representatives r of set equivalence classes to atoms of the form
268 : : * (member x s) where s is in the equivalence class of r.
269 : : */
270 : : std::map<Node, std::vector<Node>> d_members_data;
271 : : /** A (SAT-context-dependent) number of members in the above map */
272 : : NodeIntMap d_members;
273 : : //--------------------------------- end
274 : : /** is set disequality entailed internal
275 : : *
276 : : * This returns true if disequality between sets a and b is entailed in the
277 : : * current context. We use an incomplete test based on equality and membership
278 : : * information.
279 : : *
280 : : * re is the representative of the equivalence class of the empty set
281 : : * whose type is the same as a and b.
282 : : */
283 : : bool isSetDisequalityEntailedInternal(Node a, Node b, Node re) const;
284 : : /**
285 : : * Get members internal, returns the positive members if i=0, or negative
286 : : * members if i=1.
287 : : */
288 : : const std::map<Node, Node>& getMembersInternal(Node r, unsigned i) const;
289 : :
290 : : /**
291 : : * A cache that stores skolem elements generated by inference rule
292 : : * InferenceId::RELATIONS_GROUP_PART_MEMBER.
293 : : * It maps rel.group nodes to generated skolem elements.
294 : : * The skolem elements need to persist during checking, and should only change
295 : : * when the user context changes.
296 : : */
297 : : context::CDHashMap<Node, std::shared_ptr<context::CDHashSet<Node>>>
298 : : d_partElementSkolems;
299 : : }; /* class TheorySetsPrivate */
300 : :
301 : : } // namespace sets
302 : : } // namespace theory
303 : : } // namespace cvc5::internal
304 : :
305 : : #endif /* CVC5__THEORY__SETS__THEORY_SOLVER_STATE_H */
|
