Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Datastructures that track variable by variable information.
11 : : *
12 : : * This is a datastructure that tracks variable specific information.
13 : : * This is partially context dependent to back track upper/lower bounds
14 : : * and information derived from these.
15 : : */
16 : :
17 : : #include "cvc5_private.h"
18 : :
19 : : #ifndef CVC5__THEORY__ARITH__PARTIAL_MODEL_H
20 : : #define CVC5__THEORY__ARITH__PARTIAL_MODEL_H
21 : :
22 : : #include <vector>
23 : :
24 : : #include "context/cdlist.h"
25 : : #include "expr/node.h"
26 : : #include "theory/arith/arith_utilities.h"
27 : : #include "theory/arith/delta_rational.h"
28 : : #include "theory/arith/linear/arithvar.h"
29 : : #include "theory/arith/linear/arithvar_node_map.h"
30 : : #include "theory/arith/linear/bound_counts.h"
31 : : #include "theory/arith/linear/callbacks.h"
32 : : #include "theory/arith/linear/constraint_forward.h"
33 : :
34 : : namespace cvc5::context {
35 : : class Context;
36 : : }
37 : : namespace cvc5::internal {
38 : : namespace theory {
39 : : namespace arith::linear {
40 : :
41 : : /**
42 : : * (For the moment) the type hierarchy goes as:
43 : : * Integer <: Real
44 : : * The type number of a variable is an integer representing the most specific
45 : : * type of the variable. The possible values of type number are:
46 : : */
47 : : enum class ArithType
48 : : {
49 : : Unset,
50 : : Real,
51 : : Integer,
52 : : };
53 : :
54 : : class ArithVariables
55 : : {
56 : : private:
57 : : class VarInfo
58 : : {
59 : : friend class ArithVariables;
60 : : ArithVar d_var;
61 : :
62 : : DeltaRational d_assignment;
63 : : ConstraintP d_lb;
64 : : ConstraintP d_ub;
65 : : int d_cmpAssignmentLB;
66 : : int d_cmpAssignmentUB;
67 : :
68 : : unsigned d_pushCount;
69 : : ArithType d_type;
70 : : Node d_node;
71 : : bool d_auxiliary;
72 : :
73 : : public:
74 : : VarInfo();
75 : :
76 : : bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
77 : : bool setLowerBound(ConstraintP c, BoundsInfo& prev);
78 : : bool setUpperBound(ConstraintP c, BoundsInfo& prev);
79 : :
80 : : /** Returns true if this VarInfo has been initialized. */
81 : : bool initialized() const;
82 : :
83 : : /**
84 : : * Initializes the VarInfo with the ArithVar index it is associated with,
85 : : * the node that the variable represents, and whether it is an auxillary
86 : : * variable.
87 : : */
88 : : void initialize(ArithVar v, Node n, bool aux);
89 : :
90 : : /** Uninitializes the VarInfo. */
91 : : void uninitialize();
92 : :
93 : : bool canBeReclaimed() const;
94 : :
95 : : /** Indicator variables for if the assignment is equal to the upper
96 : : * and lower bounds. */
97 : : BoundCounts atBoundCounts() const;
98 : :
99 : : /** Combination of indicator variables for whether it has upper and
100 : : * lower bounds. */
101 : : BoundCounts hasBoundCounts() const;
102 : :
103 : : /** Stores both atBoundCounts() and hasBoundCounts(). */
104 : : BoundsInfo boundsInfo() const;
105 : : };
106 : :
107 : : /**Maps from ArithVar -> VarInfo */
108 : : typedef DenseMap<VarInfo> VarInfoVec;
109 : :
110 : : /** This maps an ArithVar to its Variable information.*/
111 : : VarInfoVec d_vars;
112 : :
113 : : /** Partial Map from Arithvar -> PreviousAssignment */
114 : : DenseMap<DeltaRational> d_safeAssignment;
115 : :
116 : : /** if d_vars.isKey(x), then x < d_numberOfVariables */
117 : : ArithVar d_numberOfVariables;
118 : :
119 : : /** [0, d_numberOfVariables) \intersect d_vars.keys == d_pool */
120 : : // Everything in the pool is fair game.
121 : : // There must be NO outstanding assertions
122 : : std::vector<ArithVar> d_pool;
123 : : std::vector<ArithVar> d_released;
124 : : // std::list<ArithVar>::iterator d_releasedIterator;
125 : :
126 : : // Reverse Map from Node to ArithVar
127 : : // Inverse of d_vars[x].d_node
128 : : NodeToArithVarMap d_nodeToArithVarMap;
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 : : /** Returns the number of variables. */
142 : : ArithVar getNumberOfVariables() const;
143 : :
144 : : /** Returns true if the node has an associated variables. */
145 : : bool hasArithVar(TNode x) const;
146 : :
147 : : /** Returns true if the variable has a defining node. */
148 : : bool hasNode(ArithVar a) const;
149 : :
150 : : /** Returns the ArithVar associated with a node. */
151 : : ArithVar asArithVar(TNode x) const;
152 : :
153 : : /** Returns the node associated with an ArithVar. */
154 : : Node asNode(ArithVar a) const;
155 : :
156 : : /** Allocates a freshly allocated variables. */
157 : : ArithVar allocateVariable();
158 : :
159 : : class var_iterator
160 : : {
161 : : private:
162 : : const VarInfoVec* d_vars;
163 : : VarInfoVec::const_iterator d_wrapped;
164 : :
165 : : public:
166 : : var_iterator();
167 : : var_iterator(const VarInfoVec* vars, VarInfoVec::const_iterator ci);
168 : : var_iterator& operator++();
169 : :
170 : : bool operator==(const var_iterator& other) const;
171 : : bool operator!=(const var_iterator& other) const;
172 : : ArithVar operator*() const;
173 : :
174 : : private:
175 : : void nextInitialized();
176 : : };
177 : :
178 : : var_iterator var_begin() const;
179 : : var_iterator var_end() const;
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 : : typedef std::pair<ArithVar, ConstraintP> AVCPair;
200 : : class LowerBoundCleanUp
201 : : {
202 : : private:
203 : : ArithVariables* d_pm;
204 : :
205 : : public:
206 : : LowerBoundCleanUp(ArithVariables* pm);
207 : : void operator()(AVCPair& restore);
208 : : };
209 : :
210 : : class UpperBoundCleanUp
211 : : {
212 : : private:
213 : : ArithVariables* d_pm;
214 : :
215 : : public:
216 : : UpperBoundCleanUp(ArithVariables* pm);
217 : : void operator()(AVCPair& restore);
218 : : };
219 : :
220 : : typedef context::CDList<AVCPair, LowerBoundCleanUp> LBReverts;
221 : : LBReverts d_lbRevertHistory;
222 : :
223 : : typedef context::CDList<AVCPair, UpperBoundCleanUp> UBReverts;
224 : : UBReverts d_ubRevertHistory;
225 : :
226 : : void pushUpperBound(VarInfo&);
227 : : void popUpperBound(AVCPair*);
228 : : void pushLowerBound(VarInfo&);
229 : : void popLowerBound(AVCPair*);
230 : :
231 : : // This is true when setDelta() is called, until invalidateDelta is called
232 : : bool d_deltaIsSafe;
233 : : // Cache of a value of delta to ensure a total order.
234 : : Rational d_delta;
235 : : // Function to call if the value of delta needs to be recomputed.
236 : : DeltaComputeCallback d_deltaComputingFunc;
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 : 20978389 : inline ConstraintP getUpperBoundConstraint(ArithVar x) const
255 : : {
256 : 20978389 : return d_vars[x].d_ub;
257 : : }
258 : : /** Returns the constraint for the lower bound of a variable. */
259 : 22158785 : inline ConstraintP getLowerBoundConstraint(ArithVar x) const
260 : : {
261 : 22158785 : return d_vars[x].d_lb;
262 : : }
263 : :
264 : : /* Initializes a variable to a safe value.*/
265 : : void initialize(ArithVar x, Node n, bool aux);
266 : :
267 : : ArithVar allocate(Node n, bool aux = false);
268 : :
269 : : /* Gets the last assignment to a variable that is known to be consistent. */
270 : : const DeltaRational& getSafeAssignment(ArithVar x) const;
271 : : const DeltaRational& getAssignment(ArithVar x, bool safe) const;
272 : :
273 : : /* Reverts all variable assignments to their safe values. */
274 : : void revertAssignmentChanges();
275 : :
276 : : /* Commits all variables assignments as safe.*/
277 : : void commitAssignmentChanges();
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,
287 : : const DeltaRational& safe,
288 : : const DeltaRational& r);
289 : :
290 : : /** Must know that the bound exists before calling this! */
291 : : const DeltaRational& getUpperBound(ArithVar x) const;
292 : : const DeltaRational& getLowerBound(ArithVar x) const;
293 : : const DeltaRational& getAssignment(ArithVar x) const;
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 : 1870681 : inline bool strictlyLessThanLowerBound(ArithVar x,
307 : : const DeltaRational& c) const
308 : : {
309 : 1870681 : return cmpToLowerBound(x, c) < 0;
310 : : }
311 : 3991366 : inline bool lessThanLowerBound(ArithVar x, const DeltaRational& c) const
312 : : {
313 : 3991366 : return cmpToLowerBound(x, c) <= 0;
314 : : }
315 : :
316 : 629949 : inline bool strictlyGreaterThanLowerBound(ArithVar x,
317 : : const DeltaRational& c) const
318 : : {
319 : 629949 : return cmpToLowerBound(x, c) > 0;
320 : : }
321 : :
322 : 4218624 : inline bool greaterThanLowerBound(ArithVar x, const DeltaRational& c) const
323 : : {
324 : 4218624 : return cmpToLowerBound(x, c) >= 0;
325 : : }
326 : : /**
327 : : * If upperbound < \infty:
328 : : * return getAssignment(x).cmp(getUpperBound(x))
329 : : * If upperbound = \infty:
330 : : * return -1
331 : : */
332 : : int cmpToUpperBound(ArithVar x, const DeltaRational& c) const;
333 : :
334 : 224151 : inline bool strictlyLessThanUpperBound(ArithVar x,
335 : : const DeltaRational& c) const
336 : : {
337 : 224151 : return cmpToUpperBound(x, c) < 0;
338 : : }
339 : :
340 : 4004571 : inline bool lessThanUpperBound(ArithVar x, const DeltaRational& c) const
341 : : {
342 : 4004571 : return cmpToUpperBound(x, c) <= 0;
343 : : }
344 : :
345 : 1349404 : inline bool strictlyGreaterThanUpperBound(ArithVar x,
346 : : const DeltaRational& c) const
347 : : {
348 : 1349404 : return cmpToUpperBound(x, c) > 0;
349 : : }
350 : :
351 : 3747573 : inline bool greaterThanUpperBound(ArithVar x, const DeltaRational& c) const
352 : : {
353 : 3747573 : return cmpToUpperBound(x, c) >= 0;
354 : : }
355 : :
356 : 16016182 : inline int cmpAssignmentLowerBound(ArithVar x) const
357 : : {
358 : 16016182 : return d_vars[x].d_cmpAssignmentLB;
359 : : }
360 : 13368317 : inline int cmpAssignmentUpperBound(ArithVar x) const
361 : : {
362 : 13368317 : return d_vars[x].d_cmpAssignmentUB;
363 : : }
364 : :
365 : 14134334 : inline BoundCounts atBoundCounts(ArithVar x) const
366 : : {
367 : 14134334 : return d_vars[x].atBoundCounts();
368 : : }
369 : : inline BoundCounts hasBoundCounts(ArithVar x) const
370 : : {
371 : : return d_vars[x].hasBoundCounts();
372 : : }
373 : 90951293 : inline BoundsInfo boundsInfo(ArithVar x) const
374 : : {
375 : 90951293 : return d_vars[x].boundsInfo();
376 : : }
377 : :
378 : : bool strictlyBelowUpperBound(ArithVar x) const;
379 : : bool strictlyAboveLowerBound(ArithVar x) const;
380 : : bool assignmentIsConsistent(ArithVar x) const;
381 : :
382 : : void printModel(ArithVar x, std::ostream& out) const;
383 : : void printModel(ArithVar x) const;
384 : :
385 : : /** returns true iff x has both a lower and upper bound. */
386 : : bool hasEitherBound(ArithVar x) const;
387 : 62520709 : inline bool hasLowerBound(ArithVar x) const
388 : : {
389 : 62520709 : return d_vars[x].d_lb != NullConstraint;
390 : : }
391 : 58937853 : inline bool hasUpperBound(ArithVar x) const
392 : : {
393 : 58937853 : return d_vars[x].d_ub != NullConstraint;
394 : : }
395 : :
396 : : const Rational& getDelta();
397 : :
398 : : void invalidateDelta();
399 : :
400 : : void setDelta(const Rational& d);
401 : :
402 : : void startQueueingBoundCounts();
403 : : void stopQueueingBoundCounts();
404 : : void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
405 : :
406 : : BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
407 : :
408 : : bool boundsQueueEmpty() const;
409 : : void processBoundsQueue(BoundUpdateCallback& changed);
410 : :
411 : : void printEntireModel(std::ostream& out) const;
412 : :
413 : : /**
414 : : * Precondition: assumes boundsAreEqual(x).
415 : : * If the either the lower/ upper bound is an equality, eq,
416 : : * this returns make_pair(eq, NullConstraint).
417 : : * Otherwise, this returns make_pair(lb, ub).
418 : : */
419 : : std::pair<ConstraintP, ConstraintP> explainEqualBounds(ArithVar x) const;
420 : :
421 : : private:
422 : : /**
423 : : * This function implements the mostly identical:
424 : : * revertAssignmentChanges() and commitAssignmentChanges().
425 : : */
426 : : void clearSafeAssignments(bool revert);
427 : :
428 : : bool debugEqualSizes();
429 : :
430 : : bool inMaps(ArithVar x) const;
431 : :
432 : : }; /* class ArithVariables */
433 : :
434 : : } // namespace arith::linear
435 : : } // namespace theory
436 : : } // namespace cvc5::internal
437 : :
438 : : #endif /* CVC5__THEORY__ARITH__PARTIAL_MODEL_H */
|
