GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/sep/theory_sep.h Lines: 18 32 56.3 %
Date: 2021-03-22 Branches: 21 102 20.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_sep.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Mathias Preiner
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 sep
13
 **
14
 ** Theory of sep.
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__THEORY__SEP__THEORY_SEP_H
20
#define CVC4__THEORY__SEP__THEORY_SEP_H
21
22
#include "context/cdhashmap.h"
23
#include "context/cdhashset.h"
24
#include "context/cdlist.h"
25
#include "context/cdqueue.h"
26
#include "theory/decision_strategy.h"
27
#include "theory/inference_manager_buffered.h"
28
#include "theory/sep/theory_sep_rewriter.h"
29
#include "theory/theory.h"
30
#include "theory/theory_state.h"
31
#include "theory/uf/equality_engine.h"
32
#include "util/statistics_registry.h"
33
34
namespace CVC4 {
35
namespace theory {
36
37
class TheoryModel;
38
39
namespace sep {
40
41
class TheorySep : public Theory {
42
  typedef context::CDList<Node> NodeList;
43
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
44
  typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
45
46
  /////////////////////////////////////////////////////////////////////////////
47
  // MISC
48
  /////////////////////////////////////////////////////////////////////////////
49
50
 private:
51
  /** all lemmas sent */
52
  NodeSet d_lemmas_produced_c;
53
54
  /** True node for predicates = true */
55
  Node d_true;
56
57
  /** True node for predicates = false */
58
  Node d_false;
59
60
  //whether bounds have been initialized
61
  bool d_bounds_init;
62
63
  TheorySepRewriter d_rewriter;
64
  /** A (default) theory state object */
65
  TheoryState d_state;
66
  /** A buffered inference manager */
67
  InferenceManagerBuffered d_im;
68
69
  Node mkAnd( std::vector< TNode >& assumptions );
70
71
  int processAssertion( Node n, std::map< int, std::map< Node, int > >& visited,
72
                        std::map< int, std::map< Node, std::vector< Node > > >& references, std::map< int, std::map< Node, bool > >& references_strict,
73
                        bool pol, bool hasPol, bool underSpatial );
74
75
 public:
76
  TheorySep(context::Context* c,
77
            context::UserContext* u,
78
            OutputChannel& out,
79
            Valuation valuation,
80
            const LogicInfo& logicInfo,
81
            ProofNodeManager* pnm = nullptr);
82
  ~TheorySep();
83
84
  /**
85
   * Declare heap. For smt2 inputs, this is called when the command
86
   * (declare-heap (locT datat)) is invoked by the user. This sets locT as the
87
   * location type and dataT is the data type for the heap. This command can be
88
   * executed once only, and must be invoked before solving separation logic
89
   * inputs.
90
   */
91
  void declareSepHeap(TypeNode locT, TypeNode dataT) override;
92
93
  //--------------------------------- initialization
94
  /** get the official theory rewriter of this theory */
95
  TheoryRewriter* getTheoryRewriter() override;
96
  /**
97
   * Returns true if we need an equality engine. If so, we initialize the
98
   * information regarding how it should be setup. For details, see the
99
   * documentation in Theory::needsEqualityEngine.
100
   */
101
  bool needsEqualityEngine(EeSetupInfo& esi) override;
102
  /** finish initialization */
103
  void finishInit() override;
104
  //--------------------------------- end initialization
105
  /** preregister term */
106
  void preRegisterTerm(TNode n) override;
107
108
  std::string identify() const override { return std::string("TheorySep"); }
109
110
  /////////////////////////////////////////////////////////////////////////////
111
  // PREPROCESSING
112
  /////////////////////////////////////////////////////////////////////////////
113
114
 public:
115
  void ppNotifyAssertions(const std::vector<Node>& assertions) override;
116
  /////////////////////////////////////////////////////////////////////////////
117
  // T-PROPAGATION / REGISTRATION
118
  /////////////////////////////////////////////////////////////////////////////
119
120
 private:
121
  /** Should be called to propagate the literal.  */
122
  bool propagateLit(TNode literal);
123
  /** Conflict when merging constants */
124
  void conflict(TNode a, TNode b);
125
126
 public:
127
  TrustNode explain(TNode n) override;
128
129
 public:
130
  void computeCareGraph() override;
131
132
  /////////////////////////////////////////////////////////////////////////////
133
  // MODEL GENERATION
134
  /////////////////////////////////////////////////////////////////////////////
135
136
 public:
137
  void postProcessModel(TheoryModel* m) override;
138
139
  /////////////////////////////////////////////////////////////////////////////
140
  // NOTIFICATIONS
141
  /////////////////////////////////////////////////////////////////////////////
142
143
 public:
144
145
  void presolve() override;
146
8986
  void shutdown() override {}
147
148
  /////////////////////////////////////////////////////////////////////////////
149
  // MAIN SOLVER
150
  /////////////////////////////////////////////////////////////////////////////
151
152
  //--------------------------------- standard check
153
  /** Do we need a check call at last call effort? */
154
  bool needsCheckLastEffort() override;
155
  /** Post-check, called after the fact queue of the theory is processed. */
156
  void postCheck(Effort level) override;
157
  /** Pre-notify fact, return true if processed. */
158
  bool preNotifyFact(TNode atom,
159
                     bool pol,
160
                     TNode fact,
161
                     bool isPrereg,
162
                     bool isInternal) override;
163
  /** Notify fact */
164
  void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override;
165
  //--------------------------------- end standard check
166
167
 private:
168
  /** Ensures that the reduction has been added for the given fact */
169
  void reduceFact(TNode atom, bool polarity, TNode fact);
170
  /** Is spatial kind? */
171
  bool isSpatialKind(Kind k) const;
172
  // NotifyClass: template helper class for d_equalityEngine - handles
173
  // call-back from congruence closure module
174
8992
  class NotifyClass : public eq::EqualityEngineNotify
175
  {
176
    TheorySep& d_sep;
177
178
   public:
179
8995
    NotifyClass(TheorySep& sep) : d_sep(sep) {}
180
181
    bool eqNotifyTriggerPredicate(TNode predicate, bool value) override
182
    {
183
      Debug("sep::propagate")
184
          << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", "
185
          << (value ? "true" : "false") << ")" << std::endl;
186
      Assert(predicate.getKind() == kind::EQUAL);
187
      // Just forward to sep
188
      if (value)
189
      {
190
        return d_sep.propagateLit(predicate);
191
      }
192
      return d_sep.propagateLit(predicate.notNode());
193
    }
194
3655
    bool eqNotifyTriggerTermEquality(TheoryId tag,
195
                                     TNode t1,
196
                                     TNode t2,
197
                                     bool value) override
198
    {
199
7310
      Debug("sep::propagate")
200
3655
          << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2
201
3655
          << ", " << (value ? "true" : "false") << ")" << std::endl;
202
3655
      if (value)
203
      {
204
        // Propagate equality between shared terms
205
1186
        return d_sep.propagateLit(t1.eqNode(t2));
206
      }
207
2469
      return d_sep.propagateLit(t1.eqNode(t2).notNode());
208
    }
209
210
    void eqNotifyConstantTermMerge(TNode t1, TNode t2) override
211
    {
212
      Debug("sep::propagate") << "NotifyClass::eqNotifyConstantTermMerge(" << t1
213
                              << ", " << t2 << ")" << std::endl;
214
      d_sep.conflict(t1, t2);
215
    }
216
217
2086
    void eqNotifyNewClass(TNode t) override {}
218
4303
    void eqNotifyMerge(TNode t1, TNode t2) override
219
    {
220
4303
      d_sep.eqNotifyMerge(t1, t2);
221
4303
    }
222
2469
    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) override {}
223
  };
224
225
  /** The notify class for d_equalityEngine */
226
  NotifyClass d_notify;
227
228
  /** list of all refinement lemms */
229
  std::map< Node, std::map< Node, std::vector< Node > > > d_refinement_lem;
230
231
  //cache for positive polarity start reduction
232
  NodeSet d_reduce;
233
  std::map< Node, std::map< Node, Node > > d_red_conc;
234
  std::map< Node, std::map< Node, Node > > d_neg_guard;
235
  std::vector< Node > d_neg_guards;
236
  /** a (singleton) decision strategy for each negative guard. */
237
  std::map<Node, std::unique_ptr<DecisionStrategySingleton> >
238
      d_neg_guard_strategy;
239
  std::map< Node, Node > d_guard_to_assertion;
240
  NodeList d_spatial_assertions;
241
242
  //data,ref type (globally fixed)
243
  TypeNode d_type_ref;
244
  TypeNode d_type_data;
245
  //currently fix one data type for each location type, throw error if using more than one
246
  std::map< TypeNode, TypeNode > d_loc_to_data_type;
247
  //information about types
248
  std::map< TypeNode, Node > d_base_label;
249
  std::map< TypeNode, Node > d_nil_ref;
250
  //reference bound
251
  std::map< TypeNode, Node > d_reference_bound;
252
  std::map< TypeNode, Node > d_reference_bound_max;
253
  std::map< TypeNode, std::vector< Node > > d_type_references;
254
  //kind of bound for reference types
255
  enum {
256
    bound_strict,
257
    bound_default,
258
    bound_invalid,
259
  };
260
  std::map< TypeNode, unsigned > d_bound_kind;
261
262
  std::map< TypeNode, std::vector< Node > > d_type_references_card;
263
  std::map< Node, unsigned > d_type_ref_card_id;
264
  std::map< TypeNode, std::vector< Node > > d_type_references_all;
265
  std::map< TypeNode, unsigned > d_card_max;
266
  //for empty argument
267
  std::map< TypeNode, Node > d_emp_arg;
268
  //map from ( atom, label, child index ) -> label
269
  std::map< Node, std::map< Node, std::map< int, Node > > > d_label_map;
270
  std::map< Node, Node > d_label_map_parent;
271
272
  //term model
273
  std::map< Node, Node > d_tmodel;
274
  std::map< Node, Node > d_pto_model;
275
276
  class HeapAssertInfo {
277
  public:
278
    HeapAssertInfo( context::Context* c );
279
293
    ~HeapAssertInfo(){}
280
    context::CDO< Node > d_pto;
281
    context::CDO< bool > d_has_neg_pto;
282
  };
283
  std::map< Node, HeapAssertInfo * > d_eqc_info;
284
  HeapAssertInfo * getOrMakeEqcInfo( Node n, bool doMake = false );
285
286
  //get global reference/data type
287
  TypeNode getReferenceType( Node n );
288
  TypeNode getDataType( Node n );
289
  /**
290
   * Register reference data types for atom. Calls the method below for
291
   * the appropriate types.
292
   */
293
  void registerRefDataTypesAtom(Node atom);
294
  /**
295
   * This is called either when:
296
   * (A) a declare-heap command is issued with tn1/tn2, and atom is null, or
297
   * (B) an atom specifying the heap type tn1/tn2 is registered to this theory.
298
   * We set the heap type if we are are case (A), and check whether the
299
   * heap type is consistent in the case of (B).
300
   */
301
  void registerRefDataTypes(TypeNode tn1, TypeNode tn2, Node atom);
302
  //get location/data type
303
  //get the base label for the spatial assertion
304
  Node getBaseLabel( TypeNode tn );
305
  Node getNilRef( TypeNode tn );
306
  void setNilRef( TypeNode tn, Node n );
307
  Node getLabel( Node atom, int child, Node lbl );
308
  Node applyLabel( Node n, Node lbl, std::map< Node, Node >& visited );
309
  void getLabelChildren( Node atom, Node lbl, std::vector< Node >& children, std::vector< Node >& labels );
310
311
397
  class HeapInfo {
312
  public:
313
397
    HeapInfo() : d_computed(false) {}
314
    //information about the model
315
    bool d_computed;
316
    std::vector< Node > d_heap_locs;
317
    std::vector< Node > d_heap_locs_model;
318
    //get value
319
    Node getValue( TypeNode tn );
320
  };
321
  //heap info ( label -> HeapInfo )
322
  std::map< Node, HeapInfo > d_label_model;
323
  // loc -> { data_1, ..., data_n } where (not (pto loc data_1))...(not (pto loc data_n))).
324
  std::map< Node, std::vector< Node > > d_heap_locs_nptos;
325
326
  void debugPrintHeap( HeapInfo& heap, const char * c );
327
  void validatePto( HeapAssertInfo * ei, Node ei_n );
328
  void addPto( HeapAssertInfo * ei, Node ei_n, Node p, bool polarity );
329
  void mergePto( Node p1, Node p2 );
330
  void computeLabelModel( Node lbl );
331
  Node instantiateLabel( Node n, Node o_lbl, Node lbl, Node lbl_v, std::map< Node, Node >& visited, std::map< Node, Node >& pto_model,
332
                         TypeNode rtn, std::map< Node, bool >& active_lbl, unsigned ind = 0 );
333
  void setInactiveAssertionRec( Node fact, std::map< Node, std::vector< Node > >& lbl_to_assertions, std::map< Node, bool >& assert_active );
334
335
  Node mkUnion( TypeNode tn, std::vector< Node >& locs );
336
337
 private:
338
  Node getRepresentative( Node t );
339
  bool hasTerm( Node a );
340
  bool areEqual( Node a, Node b );
341
  bool areDisequal( Node a, Node b );
342
  void eqNotifyMerge(TNode t1, TNode t2);
343
344
  void sendLemma( std::vector< Node >& ant, Node conc, InferenceId id, bool infer = false );
345
  void doPending();
346
347
 public:
348
349
  void initializeBounds();
350
};/* class TheorySep */
351
352
}/* CVC4::theory::sep namespace */
353
}/* CVC4::theory namespace */
354
}/* CVC4 namespace */
355
356
#endif /* CVC4__THEORY__SEP__THEORY_SEP_H */