GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/solver_state.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 3 4 75.0 %

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