GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/partial_model.h Lines: 34 34 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file partial_model.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, 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 Datastructures that track variable by variable information.
13
 **
14
 ** This is a datastructure that tracks variable specific information.
15
 ** This is partially context dependent to back track upper/lower bounds
16
 ** and information derived from these.
17
 **/
18
19
#include "cvc4_private.h"
20
21
#ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
22
#define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
23
24
#include <vector>
25
26
#include "context/cdlist.h"
27
#include "expr/node.h"
28
#include "theory/arith/arith_utilities.h"
29
#include "theory/arith/arithvar.h"
30
#include "theory/arith/bound_counts.h"
31
#include "theory/arith/callbacks.h"
32
#include "theory/arith/constraint_forward.h"
33
#include "theory/arith/delta_rational.h"
34
35
namespace CVC4 {
36
namespace context {
37
class Context;
38
}
39
namespace theory {
40
namespace arith {
41
42
/**
43
 * (For the moment) the type hierarchy goes as:
44
 * Integer <: Real
45
 * The type number of a variable is an integer representing the most specific
46
 * type of the variable. The possible values of type number are:
47
 */
48
enum class ArithType {
49
  Unset,
50
  Real,
51
  Integer,
52
};
53
54
8992
class ArithVariables {
55
private:
56
57
845728
  class VarInfo {
58
    friend class ArithVariables;
59
    ArithVar d_var;
60
61
    DeltaRational d_assignment;
62
    ConstraintP d_lb;
63
    ConstraintP d_ub;
64
    int d_cmpAssignmentLB;
65
    int d_cmpAssignmentUB;
66
67
    unsigned d_pushCount;
68
    ArithType d_type;
69
    Node d_node;
70
    bool d_auxiliary;
71
72
  public:
73
    VarInfo();
74
75
    bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
76
    bool setLowerBound(ConstraintP c, BoundsInfo& prev);
77
    bool setUpperBound(ConstraintP c, BoundsInfo& prev);
78
79
    /** Returns true if this VarInfo has been initialized. */
80
    bool initialized() const;
81
82
    /**
83
     * Initializes the VarInfo with the ArithVar index it is associated with,
84
     * the node that the variable represents, and whether it is an auxillary
85
     * variable.
86
     */
87
    void initialize(ArithVar v, Node n, bool aux);
88
89
    /** Uninitializes the VarInfo. */
90
    void uninitialize();
91
92
    bool canBeReclaimed() const;
93
94
    /** Indicator variables for if the assignment is equal to the upper
95
     * and lower bounds. */
96
    BoundCounts atBoundCounts() const;
97
98
    /** Combination of indicator variables for whether it has upper and
99
     * lower bounds.  */
100
    BoundCounts hasBoundCounts() const;
101
102
    /** Stores both atBoundCounts() and hasBoundCounts().  */
103
    BoundsInfo boundsInfo() const;
104
  };
105
106
  /**Maps from ArithVar -> VarInfo */
107
  typedef DenseMap<VarInfo> VarInfoVec;
108
109
  /** This maps an ArithVar to its Variable information.*/
110
  VarInfoVec d_vars;
111
112
  /** Partial Map from Arithvar -> PreviousAssignment */
113
  DenseMap<DeltaRational> d_safeAssignment;
114
115
  /** if d_vars.isKey(x), then x < d_numberOfVariables */
116
  ArithVar d_numberOfVariables;
117
118
  /** [0, d_numberOfVariables) \intersect d_vars.keys == d_pool */
119
  // Everything in the pool is fair game.
120
  // There must be NO outstanding assertions
121
  std::vector<ArithVar> d_pool;
122
  std::vector<ArithVar> d_released;
123
  //std::list<ArithVar>::iterator d_releasedIterator;
124
125
  // Reverse Map from Node to ArithVar
126
  // Inverse of d_vars[x].d_node
127
  NodeToArithVarMap d_nodeToArithVarMap;
128
129
130
  /** The queue of constraints where the assignment is at the bound.*/
131
  DenseMap<BoundsInfo> d_boundsQueue;
132
133
  /**
134
   * If this is true, record the incoming changes to the bound information.
135
   * If this is false, the responsibility of recording the changes is
136
   * LinearEqualities's.
137
   */
138
  bool d_enqueueingBoundCounts;
139
140
 public:
141
142
  /** Returns the number of variables. */
143
  ArithVar getNumberOfVariables() const;
144
145
  /** Returns true if the node has an associated variables. */
146
  bool hasArithVar(TNode x) const;
147
148
  /** Returns true if the variable has a defining node. */
149
  bool hasNode(ArithVar a) const;
150
151
  /** Returns the ArithVar associated with a node. */
152
  ArithVar asArithVar(TNode x) const;
153
154
  /** Returns the node associated with an ArithVar. */
155
  Node asNode(ArithVar a) const;
156
157
  /** Allocates a freshly allocated variables. */
158
  ArithVar allocateVariable();
159
160
  class var_iterator {
161
  private:
162
    const VarInfoVec* d_vars;
163
    VarInfoVec::const_iterator d_wrapped;
164
  public:
165
    var_iterator();
166
    var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci);
167
    var_iterator& operator++();
168
169
    bool operator==(const var_iterator& other) const;
170
    bool operator!=(const var_iterator& other) const;
171
    ArithVar operator*() const;
172
173
  private:
174
    void nextInitialized();
175
  };
176
177
  var_iterator var_begin() const;
178
  var_iterator var_end() const;
179
180
181
  bool canBeReleased(ArithVar v) const;
182
  void releaseArithVar(ArithVar v);
183
  void attemptToReclaimReleased();
184
185
  /** Is this variable guaranteed to have an integer assignment?
186
   * (Should agree with the type system.) */
187
  bool isInteger(ArithVar x) const;
188
189
  /** Is the assignment to x integral? */
190
  bool integralAssignment(ArithVar x) const;
191
192
  /* Is this variable defined as a linear sum of other variables? */
193
  bool isAuxiliary(ArithVar x) const;
194
195
  /* Is the variable both input and not auxiliary? */
196
  bool isIntegerInput(ArithVar x) const;
197
198
 private:
199
200
  typedef std::pair<ArithVar, ConstraintP> AVCPair;
201
  class LowerBoundCleanUp {
202
  private:
203
    ArithVariables* d_pm;
204
  public:
205
    LowerBoundCleanUp(ArithVariables* pm);
206
    void operator()(AVCPair* restore);
207
  };
208
209
  class UpperBoundCleanUp {
210
  private:
211
    ArithVariables* d_pm;
212
  public:
213
    UpperBoundCleanUp(ArithVariables* pm);
214
    void operator()(AVCPair* restore);
215
  };
216
217
  typedef context::CDList<AVCPair, LowerBoundCleanUp> LBReverts;
218
  LBReverts d_lbRevertHistory;
219
220
  typedef context::CDList<AVCPair, UpperBoundCleanUp> UBReverts;
221
  UBReverts d_ubRevertHistory;
222
223
  void pushUpperBound(VarInfo&);
224
  void popUpperBound(AVCPair*);
225
  void pushLowerBound(VarInfo&);
226
  void popLowerBound(AVCPair*);
227
228
  // This is true when setDelta() is called, until invalidateDelta is called
229
  bool d_deltaIsSafe;
230
  // Cache of a value of delta to ensure a total order.
231
  Rational d_delta;
232
  // Function to call if the value of delta needs to be recomputed.
233
  DeltaComputeCallback d_deltaComputingFunc;
234
235
236
public:
237
238
  ArithVariables(context::Context* c, DeltaComputeCallback deltaComputation);
239
240
  /**
241
   * This sets the lower bound for a variable in the current context.
242
   * This must be stronger the previous constraint.
243
   */
244
  void setLowerBoundConstraint(ConstraintP lb);
245
246
  /**
247
   * This sets the upper bound for a variable in the current context.
248
   * This must be stronger the previous constraint.
249
   */
250
  void setUpperBoundConstraint(ConstraintP ub);
251
252
  /** Returns the constraint for the upper bound of a variable. */
253
8262480
  inline ConstraintP getUpperBoundConstraint(ArithVar x) const{
254
8262480
    return d_vars[x].d_ub;
255
  }
256
  /** Returns the constraint for the lower bound of a variable. */
257
9008153
  inline ConstraintP getLowerBoundConstraint(ArithVar x) const{
258
9008153
    return d_vars[x].d_lb;
259
  }
260
261
  /* Initializes a variable to a safe value.*/
262
  void initialize(ArithVar x, Node n, bool aux);
263
264
  ArithVar allocate(Node n, bool aux = false);
265
266
  /* Gets the last assignment to a variable that is known to be consistent. */
267
  const DeltaRational& getSafeAssignment(ArithVar x) const;
268
  const DeltaRational& getAssignment(ArithVar x, bool safe) const;
269
270
  /* Reverts all variable assignments to their safe values. */
271
  void revertAssignmentChanges();
272
273
  /* Commits all variables assignments as safe.*/
274
  void commitAssignmentChanges();
275
276
277
  bool lowerBoundIsZero(ArithVar x);
278
  bool upperBoundIsZero(ArithVar x);
279
280
  bool boundsAreEqual(ArithVar x) const;
281
282
  /* Sets an unsafe variable assignment */
283
  void setAssignment(ArithVar x, const DeltaRational& r);
284
  void setAssignment(ArithVar x, const DeltaRational& safe, const DeltaRational& r);
285
286
287
  /** Must know that the bound exists before calling this! */
288
  const DeltaRational& getUpperBound(ArithVar x) const;
289
  const DeltaRational& getLowerBound(ArithVar x) const;
290
  const DeltaRational& getAssignment(ArithVar x) const;
291
292
293
  bool equalsLowerBound(ArithVar x, const DeltaRational& c);
294
  bool equalsUpperBound(ArithVar x, const DeltaRational& c);
295
296
  /**
297
   * If lowerbound > - \infty:
298
   *   return getAssignment(x).cmp(getLowerBound(x))
299
   * If lowerbound = - \infty:
300
   *   return 1
301
   */
302
  int cmpToLowerBound(ArithVar x, const DeltaRational& c) const;
303
304
1011238
  inline bool strictlyLessThanLowerBound(ArithVar x, const DeltaRational& c) const{
305
1011238
    return cmpToLowerBound(x, c) < 0;
306
  }
307
1977807
  inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c) const{
308
1977807
    return cmpToLowerBound(x, c) <= 0;
309
  }
310
311
294342
  inline bool strictlyGreaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
312
294342
    return cmpToLowerBound(x, c) > 0;
313
  }
314
315
2031374
  inline bool greaterThanLowerBound(ArithVar x, const DeltaRational& c) const{
316
2031374
    return cmpToLowerBound(x, c) >= 0;
317
  }
318
  /**
319
   * If upperbound < \infty:
320
   *   return getAssignment(x).cmp(getUpperBound(x))
321
   * If upperbound = \infty:
322
   *   return -1
323
   */
324
  int cmpToUpperBound(ArithVar x, const DeltaRational& c) const;
325
326
118154
  inline bool strictlyLessThanUpperBound(ArithVar x, const DeltaRational& c) const{
327
118154
    return cmpToUpperBound(x, c) < 0;
328
  }
329
330
1994767
  inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c) const{
331
1994767
    return cmpToUpperBound(x, c) <= 0;
332
  }
333
334
766621
  inline bool strictlyGreaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
335
766621
    return cmpToUpperBound(x, c) > 0;
336
  }
337
338
2048589
  inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c) const{
339
2048589
    return cmpToUpperBound(x, c) >= 0;
340
  }
341
342
10368894
  inline int cmpAssignmentLowerBound(ArithVar x) const{
343
10368894
    return d_vars[x].d_cmpAssignmentLB;
344
  }
345
8792208
  inline int cmpAssignmentUpperBound(ArithVar x) const{
346
8792208
    return d_vars[x].d_cmpAssignmentUB;
347
  }
348
349
7941754
  inline BoundCounts atBoundCounts(ArithVar x) const {
350
7941754
    return d_vars[x].atBoundCounts();
351
  }
352
  inline BoundCounts hasBoundCounts(ArithVar x) const {
353
    return d_vars[x].hasBoundCounts();
354
  }
355
63483057
  inline BoundsInfo boundsInfo(ArithVar x) const{
356
63483057
    return d_vars[x].boundsInfo();
357
  }
358
359
  bool strictlyBelowUpperBound(ArithVar x) const;
360
  bool strictlyAboveLowerBound(ArithVar x) const;
361
  bool assignmentIsConsistent(ArithVar x) const;
362
363
  void printModel(ArithVar x, std::ostream& out) const;
364
  void printModel(ArithVar x) const;
365
366
  /** returns true iff x has both a lower and upper bound. */
367
  bool hasEitherBound(ArithVar x) const;
368
25948373
  inline bool hasLowerBound(ArithVar x) const{
369
25948373
    return d_vars[x].d_lb != NullConstraint;
370
  }
371
23520874
  inline bool hasUpperBound(ArithVar x) const{
372
23520874
    return d_vars[x].d_ub != NullConstraint;
373
  }
374
375
  const Rational& getDelta();
376
377
  void invalidateDelta();
378
379
  void setDelta(const Rational& d);
380
381
  void startQueueingBoundCounts();
382
  void stopQueueingBoundCounts();
383
  void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
384
385
  BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
386
387
  bool boundsQueueEmpty() const;
388
  void processBoundsQueue(BoundUpdateCallback& changed);
389
390
  void printEntireModel(std::ostream& out) const;
391
392
393
  /**
394
   * Precondition: assumes boundsAreEqual(x).
395
   * If the either the lower/ upper bound is an equality, eq,
396
   * this returns make_pair(eq, NullConstraint).
397
   * Otherwise, this returns make_pair(lb, ub).
398
   */
399
  std::pair<ConstraintP, ConstraintP> explainEqualBounds(ArithVar x) const;
400
401
private:
402
403
  /**
404
   * This function implements the mostly identical:
405
   * revertAssignmentChanges() and commitAssignmentChanges().
406
   */
407
  void clearSafeAssignments(bool revert);
408
409
  bool debugEqualSizes();
410
411
  bool inMaps(ArithVar x) const;
412
413
};/* class ArithVariables */
414
415
416
}/* CVC4::theory::arith namespace */
417
}/* CVC4::theory namespace */
418
}/* CVC4 namespace */
419
420
#endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */