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