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