GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/theory_datatypes.h Lines: 15 17 88.2 %
Date: 2021-03-23 Branches: 19 40 47.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_datatypes.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Morgan Deters
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 Theory of datatypes.
13
 **
14
 ** Theory of datatypes.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
20
#define CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H
21
22
#include <iostream>
23
#include <map>
24
25
#include "context/cdlist.h"
26
#include "expr/attribute.h"
27
#include "expr/node_trie.h"
28
#include "theory/datatypes/datatypes_rewriter.h"
29
#include "theory/datatypes/inference_manager.h"
30
#include "theory/datatypes/proof_checker.h"
31
#include "theory/datatypes/sygus_extension.h"
32
#include "theory/theory.h"
33
#include "theory/theory_eq_notify.h"
34
#include "theory/theory_state.h"
35
#include "theory/uf/equality_engine.h"
36
#include "util/hash.h"
37
38
namespace CVC4 {
39
namespace theory {
40
namespace datatypes {
41
42
class TheoryDatatypes : public Theory {
43
 private:
44
  typedef context::CDList<Node> NodeList;
45
  /** maps nodes to an index in a vector */
46
  typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap;
47
  typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap;
48
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap;
49
50
 private:
51
  //notification class for equality engine
52
8994
  class NotifyClass : public TheoryEqNotifyClass
53
  {
54
    TheoryDatatypes& d_dt;
55
  public:
56
8997
   NotifyClass(TheoryInferenceManager& im, TheoryDatatypes& dt)
57
8997
       : TheoryEqNotifyClass(im), d_dt(dt)
58
   {
59
8997
   }
60
322925
   void eqNotifyNewClass(TNode t) override
61
   {
62
322925
     Debug("dt") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
63
322925
     d_dt.eqNotifyNewClass(t);
64
322925
    }
65
3158786
    void eqNotifyMerge(TNode t1, TNode t2) override
66
    {
67
6317572
      Debug("dt") << "NotifyClass::eqNotifyMerge(" << t1 << ", " << t2 << ")"
68
3158786
                  << std::endl;
69
3158786
      d_dt.eqNotifyMerge(t1, t2);
70
3158786
    }
71
  };/* class TheoryDatatypes::NotifyClass */
72
private:
73
  /** equivalence class info
74
   * d_inst is whether the instantiate rule has been applied,
75
   * d_constructor is a node of kind APPLY_CONSTRUCTOR (if any) in this equivalence class,
76
   * d_selectors is whether a selector has been applied to this equivalence class.
77
   */
78
  class EqcInfo
79
  {
80
  public:
81
    EqcInfo( context::Context* c );
82
24253
    ~EqcInfo(){}
83
    //whether we have instantiatied this eqc
84
    context::CDO< bool > d_inst;
85
    //constructor equal to this eqc
86
    context::CDO< Node > d_constructor;
87
    //all selectors whose argument is this eqc
88
    context::CDO< bool > d_selectors;
89
  };
90
  /** does eqc of n have a label (do we know its constructor)? */
91
  bool hasLabel( EqcInfo* eqc, Node n );
92
  /** get the label associated to n */
93
  Node getLabel( Node n );
94
  /** get the index of the label associated to n */
95
  int getLabelIndex( EqcInfo* eqc, Node n );
96
  /** does eqc of n have any testers? */
97
  bool hasTester( Node n );
98
  /** get the possible constructors for n */
99
  void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons );
100
  /** mkExpDefSkolem */
101
  void mkExpDefSkolem( Node sel, TypeNode dt, TypeNode rt );
102
  /** skolems for terms */
103
  NodeMap d_term_sk;
104
  Node getTermSkolemFor( Node n );
105
private:
106
  /** information necessary for equivalence classes */
107
  std::map< Node, EqcInfo* > d_eqc_info;
108
  //---------------------------------labels
109
  /** labels for each equivalence class
110
   *
111
   * For each eqc r, d_labels[r] is testers that hold for this equivalence
112
   * class, either:
113
   * a list of equations of the form
114
   *   NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of
115
   *   which are unique testers, n is less than the number of possible
116
   *   constructors for t minus one,
117
   * or a list of equations of the form
118
   *   NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by
119
   *   is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester.
120
   * In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r.
121
   *
122
   * We store this list in a context-dependent way, using the four data
123
   * structures below. The three vectors d_labels_data, d_labels_args, and
124
   * d_labels_tindex store the tester applications, their arguments and the
125
   * tester index of the application. The map d_labels stores the number of
126
   * values in these vectors that is valid in the current context (this is an
127
   * optimization that ensures we don't need to pop data when changing SAT
128
   * contexts).
129
   */
130
  NodeUIntMap d_labels;
131
  /** the tester applications */
132
  std::map< Node, std::vector< Node > > d_labels_data;
133
  /** the argument of each node in d_labels_data */
134
  std::map<Node, std::vector<Node> > d_labels_args;
135
  /** the tester index of each node in d_labels_data */
136
  std::map<Node, std::vector<unsigned> > d_labels_tindex;
137
  //---------------------------------end labels
138
  /** selector apps for eqch equivalence class */
139
  NodeUIntMap d_selector_apps;
140
  std::map< Node, std::vector< Node > > d_selector_apps_data;
141
  /** The conflict node */
142
  Node d_conflictNode;
143
  /**
144
   * SAT-context dependent cache for which terms we have called
145
   * collectTerms(...) on.
146
   */
147
  BoolMap d_collectTermsCache;
148
  /**
149
   * User-context dependent cache for which terms we have called
150
   * collectTerms(...) on.
151
   */
152
  BoolMap d_collectTermsCacheU;
153
  /** All the function terms that the theory has seen */
154
  context::CDList<TNode> d_functionTerms;
155
  /** counter for forcing assignments (ensures fairness) */
156
  unsigned d_dtfCounter;
157
  /** expand definition skolem functions */
158
  std::map< TypeNode, std::map< Node, Node > > d_exp_def_skolem;
159
  /** uninterpreted constant to variable map */
160
  std::map< Node, Node > d_uc_to_fresh_var;
161
private:
162
  /** singleton lemmas (for degenerate co-datatype case) */
163
  std::map< TypeNode, Node > d_singleton_lemma[2];
164
  /** Cache for singleton equalities processed */
165
  BoolMap d_singleton_eq;
166
  /** list of all lemmas produced */
167
  BoolMap d_lemmas_produced_c;
168
private:
169
  /** assert fact */
170
  void assertFact( Node fact, Node exp );
171
172
  /** get or make eqc info */
173
  EqcInfo* getOrMakeEqcInfo( TNode n, bool doMake = false );
174
175
  /** has eqc info */
176
3345288
  bool hasEqcInfo( TNode n ) { return d_labels.find( n )!=d_labels.end(); }
177
178
  /** get eqc constructor */
179
  TNode getEqcConstructor( TNode r );
180
181
 protected:
182
  void addCarePairs(TNodeTrie* t1,
183
                    TNodeTrie* t2,
184
                    unsigned arity,
185
                    unsigned depth,
186
                    unsigned& n_pairs);
187
  /** compute care graph */
188
  void computeCareGraph() override;
189
190
 public:
191
  TheoryDatatypes(context::Context* c,
192
                  context::UserContext* u,
193
                  OutputChannel& out,
194
                  Valuation valuation,
195
                  const LogicInfo& logicInfo,
196
                  ProofNodeManager* pnm = nullptr);
197
  ~TheoryDatatypes();
198
199
  //--------------------------------- initialization
200
  /** get the official theory rewriter of this theory */
201
  TheoryRewriter* getTheoryRewriter() override;
202
  /**
203
   * Returns true if we need an equality engine. If so, we initialize the
204
   * information regarding how it should be setup. For details, see the
205
   * documentation in Theory::needsEqualityEngine.
206
   */
207
  bool needsEqualityEngine(EeSetupInfo& esi) override;
208
  /** finish initialization */
209
  void finishInit() override;
210
  //--------------------------------- end initialization
211
  /** propagate */
212
  bool propagateLit(TNode literal);
213
  /** Conflict when merging two constants */
214
  void conflict(TNode a, TNode b);
215
  /** explain */
216
  TrustNode explain(TNode literal) override;
217
  /** called when a new equivalance class is created */
218
  void eqNotifyNewClass(TNode t);
219
  /** called when two equivalance classes have merged */
220
  void eqNotifyMerge(TNode t1, TNode t2);
221
222
  //--------------------------------- standard check
223
  /** Do we need a check call at last call effort? */
224
  bool needsCheckLastEffort() override;
225
  /** Pre-check, called before the fact queue of the theory is processed. */
226
  bool preCheck(Effort level) override;
227
  /** Post-check, called after the fact queue of the theory is processed. */
228
  void postCheck(Effort level) override;
229
  /** Notify fact */
230
  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
231
  //--------------------------------- end standard check
232
  void preRegisterTerm(TNode n) override;
233
  TrustNode expandDefinition(Node n) override;
234
  TrustNode ppRewrite(TNode n, std::vector<SkolemLemma>& lems) override;
235
  EqualityStatus getEqualityStatus(TNode a, TNode b) override;
236
  std::string identify() const override
237
  {
238
    return std::string("TheoryDatatypes");
239
  }
240
  /** debug print */
241
  void printModelDebug( const char* c );
242
  /** entailment check */
243
  std::pair<bool, Node> entailmentCheck(TNode lit) override;
244
245
 private:
246
  /** add tester to equivalence class info */
247
  void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg);
248
  /** add selector to equivalence class info */
249
  void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true );
250
  /** add constructor */
251
  void addConstructor( Node c, EqcInfo* eqc, Node n );
252
  /** merge the equivalence class info of t1 and t2 */
253
  void merge( Node t1, Node t2 );
254
  /** collapse selector, s is of the form sel( n ) where n = c */
255
  void collapseSelector( Node s, Node c );
256
  /** for checking if cycles exist */
257
  void checkCycles();
258
  Node searchForCycle(TNode n,
259
                      TNode on,
260
                      std::map<TNode, bool>& visited,
261
                      std::map<TNode, bool>& proc,
262
                      std::vector<Node>& explanation,
263
                      bool firstTime = true);
264
  /** for checking whether two codatatype terms must be equal */
265
  void separateBisimilar(std::vector<Node>& part,
266
                         std::vector<std::vector<Node> >& part_out,
267
                         std::vector<Node>& exp,
268
                         std::map<Node, Node>& cn,
269
                         std::map<Node, std::map<Node, int> >& dni,
270
                         int dniLvl,
271
                         bool mkExp);
272
  /** build model */
273
  Node getCodatatypesValue( Node n, std::map< Node, Node >& eqc_cons, std::map< Node, int >& vmap, int depth );
274
  /** get singleton lemma */
275
  Node getSingletonLemma( TypeNode tn, bool pol );
276
  /** collect terms */
277
  void collectTerms( Node n );
278
  /** get instantiate cons */
279
  Node getInstantiateCons(Node n, const DType& dt, int index);
280
  /** check instantiate */
281
  void instantiate( EqcInfo* eqc, Node n );
282
private:
283
  //equality queries
284
  bool hasTerm( TNode a );
285
  bool areEqual( TNode a, TNode b );
286
  bool areDisequal( TNode a, TNode b );
287
  bool areCareDisequal( TNode x, TNode y );
288
  TNode getRepresentative( TNode a );
289
290
  /** Collect model values in m based on the relevant terms given by termSet */
291
  bool collectModelValues(TheoryModel* m,
292
                          const std::set<Node>& termSet) override;
293
  /**
294
   * Compute relevant terms. This includes datatypes in non-singleton
295
   * equivalence classes.
296
   */
297
  void computeRelevantTerms(std::set<Node>& termSet) override;
298
  /** Commonly used terms */
299
  Node d_true;
300
  Node d_zero;
301
  /** sygus symmetry breaking utility */
302
  std::unique_ptr<SygusExtension> d_sygusExtension;
303
  /** The theory rewriter for this theory. */
304
  DatatypesRewriter d_rewriter;
305
  /** A (default) theory state object */
306
  TheoryState d_state;
307
  /** The inference manager */
308
  InferenceManager d_im;
309
  /** The notify class */
310
  NotifyClass d_notify;
311
  /** Proof checker for datatypes */
312
  DatatypesProofRuleChecker d_pchecker;
313
};/* class TheoryDatatypes */
314
315
}/* CVC4::theory::datatypes namespace */
316
}/* CVC4::theory namespace */
317
}/* CVC4 namespace */
318
319
#endif /* CVC4__THEORY__DATATYPES__THEORY_DATATYPES_H */