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