GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sets/theory_sets_private.h Lines: 2 3 66.7 %
Date: 2021-03-23 Branches: 0 2 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sets_private.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Kshitij Bansal, 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 theory implementation.
13
 **
14
 ** Sets theory implementation.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
20
#define CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
21
22
#include "context/cdhashset.h"
23
#include "context/cdqueue.h"
24
#include "expr/node_trie.h"
25
#include "theory/sets/cardinality_extension.h"
26
#include "theory/sets/inference_manager.h"
27
#include "theory/sets/solver_state.h"
28
#include "theory/sets/term_registry.h"
29
#include "theory/sets/theory_sets_rels.h"
30
#include "theory/sets/theory_sets_rewriter.h"
31
#include "theory/theory.h"
32
#include "theory/uf/equality_engine.h"
33
34
namespace CVC4 {
35
namespace theory {
36
namespace sets {
37
38
/** Internal classes, forward declared here */
39
class TheorySets;
40
41
class TheorySetsPrivate {
42
  typedef context::CDHashMap< Node, bool, NodeHashFunction> NodeBoolMap;
43
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
44
45
 public:
46
  void eqNotifyNewClass(TNode t);
47
  void eqNotifyMerge(TNode t1, TNode t2);
48
  void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
49
50
 private:
51
  /** Are a and b trigger terms in the equality engine that may be disequal? */
52
  bool areCareDisequal(Node a, Node b);
53
  /**
54
   * Invoke the decision procedure for this theory, which is run at
55
   * full effort. This will either send a lemma or conflict on the output
56
   * channel of this class, or otherwise the current set of constraints is
57
   * satisfiable w.r.t. the theory of sets.
58
   */
59
  void fullEffortCheck();
60
  /**
61
   * Reset the information for a full effort check.
62
   */
63
  void fullEffortReset();
64
  /**
65
   * This implements an inference schema based on the "downwards closure" of
66
   * set membership. This roughly corresponds to the rules UNION DOWN I and II,
67
   * INTER DOWN I and II from Bansal et al IJCAR 2016, as well as rules for set
68
   * difference.
69
   */
70
  void checkDownwardsClosure();
71
  /**
72
   * This implements an inference schema based on the "upwards closure" of
73
   * set membership. This roughly corresponds to the rules UNION UP, INTER
74
   * UP I and II from Bansal et al IJCAR 2016, as well as rules for set
75
   * difference.
76
   */
77
  void checkUpwardsClosure();
78
  /**
79
   * This implements a strategy for splitting for set disequalities which
80
   * roughly corresponds the SET DISEQUALITY rule from Bansal et al IJCAR 2016.
81
   */
82
  void checkDisequalities();
83
  /**
84
   * Check comprehensions. This adds reduction lemmas for all set comprehensions
85
   * in the current context.
86
   */
87
  void checkReduceComprehensions();
88
89
  void addCarePairs(TNodeTrie* t1,
90
                    TNodeTrie* t2,
91
                    unsigned arity,
92
                    unsigned depth,
93
                    unsigned& n_pairs);
94
95
  Node d_true;
96
  Node d_false;
97
  Node d_zero;
98
  NodeBoolMap d_deq;
99
  /**
100
   * The set of terms that we have reduced via a lemma in the current user
101
   * context.
102
   */
103
  NodeSet d_termProcessed;
104
105
  //propagation
106
  class EqcInfo
107
  {
108
  public:
109
    EqcInfo( context::Context* c );
110
4678
    ~EqcInfo(){}
111
    // singleton or emptyset equal to this eqc
112
    context::CDO< Node > d_singleton;
113
  };
114
  /** information necessary for equivalence classes */
115
  std::map< Node, EqcInfo* > d_eqc_info;
116
  /** get or make eqc info */
117
  EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
118
119
  /** full check incomplete
120
   *
121
   * This flag is set to true during a full effort check if this theory
122
   * is incomplete for some reason (for instance, if we combine cardinality
123
   * with a relation or extended function kind).
124
   */
125
  bool d_full_check_incomplete;
126
  std::map< Node, TypeNode > d_most_common_type;
127
  std::map< Node, Node > d_most_common_type_term;
128
129
 public:
130
131
  /**
132
   * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
133
   * contexts.
134
   */
135
  TheorySetsPrivate(TheorySets& external,
136
                    SolverState& state,
137
                    InferenceManager& im,
138
                    SkolemCache& skc);
139
140
  ~TheorySetsPrivate();
141
142
8997
  TheoryRewriter* getTheoryRewriter() { return &d_rewriter; }
143
144
  /** Get the solver state */
145
  SolverState* getSolverState() { return &d_state; }
146
147
  /**
148
   * Finish initialize, called after the equality engine of theory sets has
149
   * been determined.
150
   */
151
  void finishInit();
152
153
  //--------------------------------- standard check
154
  /** Post-check, called after the fact queue of the theory is processed. */
155
  void postCheck(Theory::Effort level);
156
  /** Notify new fact */
157
  void notifyFact(TNode atom, bool polarity, TNode fact);
158
  //--------------------------------- end standard check
159
160
  /** Collect model values in m based on the relevant terms given by termSet */
161
  void addSharedTerm(TNode);
162
  bool collectModelValues(TheoryModel* m, const std::set<Node>& termSet);
163
164
  void computeCareGraph();
165
166
  Node explain(TNode);
167
168
  void preRegisterTerm(TNode node);
169
170
  /** ppRewrite, which expands choose and is_singleton.  */
171
  TrustNode ppRewrite(Node n, std::vector<SkolemLemma>& lems);
172
173
  void presolve();
174
175
  /** get the valuation */
176
  Valuation& getValuation();
177
 private:
178
  TheorySets& d_external;
179
  /** The state of the sets solver at full effort */
180
  SolverState& d_state;
181
  /** The inference manager of the sets solver */
182
  InferenceManager& d_im;
183
  /** Reference to the skolem cache */
184
  SkolemCache& d_skCache;
185
  /** The term registry */
186
  TermRegistry d_treg;
187
188
  /** Pointer to the equality engine of theory of sets */
189
  eq::EqualityEngine* d_equalityEngine;
190
191
  bool isCareArg( Node n, unsigned a );
192
193
 public:
194
  /** Is formula n entailed to have polarity pol in the current context? */
195
  bool isEntailed(Node n, bool pol) { return d_state.isEntailed(n, pol); }
196
197
 private:
198
  /** get choose function
199
   *
200
   * Returns the existing uninterpreted function for the choose operator for the
201
   * given set type, or creates a new one if it does not exist.
202
   */
203
  Node getChooseFunction(const TypeNode& setType);
204
  /** expand the definition of the choose operator */
205
  TrustNode expandChooseOperator(const Node& node,
206
                                 std::vector<SkolemLemma>& lems);
207
  /** expand the definition of is_singleton operator */
208
  TrustNode expandIsSingletonOperator(const Node& node);
209
  /** subtheory solver for the theory of relations */
210
  std::unique_ptr<TheorySetsRels> d_rels;
211
  /** subtheory solver for the theory of sets with cardinality */
212
  std::unique_ptr<CardinalityExtension> d_cardSolver;
213
  /** are relations enabled?
214
   *
215
   * This flag is set to true during a full effort check if any constraint
216
   * involving relational constraints is asserted to this theory.
217
   */
218
  bool d_rels_enabled;
219
  /** is cardinality enabled?
220
   *
221
   * This flag is set to true during a full effort check if any constraint
222
   * involving cardinality constraints is asserted to this theory.
223
   */
224
  bool d_card_enabled;
225
226
  /** The theory rewriter for this theory. */
227
  TheorySetsRewriter d_rewriter;
228
229
  /** a map that stores the choose functions for set types */
230
  std::map<TypeNode, Node> d_chooseFunctions;
231
232
  /** a map that maps each set to an existential quantifier generated for
233
   * operator is_singleton */
234
  std::map<Node, Node> d_isSingletonNodes;
235
};/* class TheorySetsPrivate */
236
237
238
}/* CVC4::theory::sets namespace */
239
}/* CVC4::theory namespace */
240
}/* CVC4 namespace */
241
242
#endif /* CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */