1 /********************* */
2 /*! \file partial_model.h
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-2020 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
12 ** \brief Datastructures that track variable by variable information.
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.
19 #include "cvc4_private.h"
21 #ifndef CVC4__THEORY__ARITH__PARTIAL_MODEL_H
22 #define CVC4__THEORY__ARITH__PARTIAL_MODEL_H
27 #include "context/cdlist.h"
28 #include "context/context.h"
29 #include "expr/node.h"
30 #include "theory/arith/arith_utilities.h"
31 #include "theory/arith/arithvar.h"
32 #include "theory/arith/bound_counts.h"
33 #include "theory/arith/callbacks.h"
34 #include "theory/arith/constraint_forward.h"
35 #include "theory/arith/delta_rational.h"
42 * (For the moment) the type hierarchy goes as:
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:
47 enum class ArithType
{
53 class ArithVariables
{
57 friend class ArithVariables
;
60 DeltaRational d_assignment
;
63 int d_cmpAssignmentLB
;
64 int d_cmpAssignmentUB
;
74 bool setAssignment(const DeltaRational
& r
, BoundsInfo
& prev
);
75 bool setLowerBound(ConstraintP c
, BoundsInfo
& prev
);
76 bool setUpperBound(ConstraintP c
, BoundsInfo
& prev
);
78 /** Returns true if this VarInfo has been initialized. */
79 bool initialized() const;
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
86 void initialize(ArithVar v
, Node n
, bool aux
);
88 /** Uninitializes the VarInfo. */
91 bool canBeReclaimed() const;
93 /** Indicator variables for if the assignment is equal to the upper
94 * and lower bounds. */
95 BoundCounts
atBoundCounts() const;
97 /** Combination of indicator variables for whether it has upper and
99 BoundCounts
hasBoundCounts() const;
101 /** Stores both atBoundCounts() and hasBoundCounts(). */
102 BoundsInfo
boundsInfo() const;
105 /**Maps from ArithVar -> VarInfo */
106 typedef DenseMap
<VarInfo
> VarInfoVec
;
108 /** This maps an ArithVar to its Variable information.*/
111 /** Partial Map from Arithvar -> PreviousAssignment */
112 DenseMap
<DeltaRational
> d_safeAssignment
;
114 /** if d_vars.isKey(x), then x < d_numberOfVariables */
115 ArithVar d_numberOfVariables
;
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;
124 // Reverse Map from Node to ArithVar
125 // Inverse of d_vars[x].d_node
126 NodeToArithVarMap d_nodeToArithVarMap
;
129 /** The queue of constraints where the assignment is at the bound.*/
130 DenseMap
<BoundsInfo
> d_boundsQueue
;
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.
137 bool d_enqueueingBoundCounts
;
141 /** Returns the number of variables. */
142 ArithVar
getNumberOfVariables() const;
144 /** Returns true if the node has an associated variables. */
145 bool hasArithVar(TNode x
) const;
147 /** Returns true if the variable has a defining node. */
148 bool hasNode(ArithVar a
) const;
150 /** Returns the ArithVar associated with a node. */
151 ArithVar
asArithVar(TNode x
) const;
153 /** Returns the node associated with an ArithVar. */
154 Node
asNode(ArithVar a
) const;
156 /** Allocates a freshly allocated variables. */
157 ArithVar
allocateVariable();
161 const VarInfoVec
* d_vars
;
162 VarInfoVec::const_iterator d_wrapped
;
165 var_iterator(const VarInfoVec
* vars
, VarInfoVec::const_iterator ci
);
166 var_iterator
& operator++();
168 bool operator==(const var_iterator
& other
) const;
169 bool operator!=(const var_iterator
& other
) const;
170 ArithVar
operator*() const;
173 void nextInitialized();
176 var_iterator
var_begin() const;
177 var_iterator
var_end() const;
180 bool canBeReleased(ArithVar v
) const;
181 void releaseArithVar(ArithVar v
);
182 void attemptToReclaimReleased();
184 /** Is this variable guaranteed to have an integer assignment?
185 * (Should agree with the type system.) */
186 bool isInteger(ArithVar x
) const;
188 /** Is the assignment to x integral? */
189 bool integralAssignment(ArithVar x
) const;
191 /* Is this variable defined as a linear sum of other variables? */
192 bool isAuxiliary(ArithVar x
) const;
194 /* Is the variable both input and not auxiliary? */
195 bool isIntegerInput(ArithVar x
) const;
199 typedef std::pair
<ArithVar
, ConstraintP
> AVCPair
;
200 class LowerBoundCleanUp
{
202 ArithVariables
* d_pm
;
204 LowerBoundCleanUp(ArithVariables
* pm
);
205 void operator()(AVCPair
* restore
);
208 class UpperBoundCleanUp
{
210 ArithVariables
* d_pm
;
212 UpperBoundCleanUp(ArithVariables
* pm
);
213 void operator()(AVCPair
* restore
);
216 typedef context::CDList
<AVCPair
, LowerBoundCleanUp
> LBReverts
;
217 LBReverts d_lbRevertHistory
;
219 typedef context::CDList
<AVCPair
, UpperBoundCleanUp
> UBReverts
;
220 UBReverts d_ubRevertHistory
;
222 void pushUpperBound(VarInfo
&);
223 void popUpperBound(AVCPair
*);
224 void pushLowerBound(VarInfo
&);
225 void popLowerBound(AVCPair
*);
227 // This is true when setDelta() is called, until invalidateDelta is called
229 // Cache of a value of delta to ensure a total order.
231 // Function to call if the value of delta needs to be recomputed.
232 DeltaComputeCallback d_deltaComputingFunc
;
237 ArithVariables(context::Context
* c
, DeltaComputeCallback deltaComputation
);
240 * This sets the lower bound for a variable in the current context.
241 * This must be stronger the previous constraint.
243 void setLowerBoundConstraint(ConstraintP lb
);
246 * This sets the upper bound for a variable in the current context.
247 * This must be stronger the previous constraint.
249 void setUpperBoundConstraint(ConstraintP ub
);
251 /** Returns the constraint for the upper bound of a variable. */
252 inline ConstraintP
getUpperBoundConstraint(ArithVar x
) const{
253 return d_vars
[x
].d_ub
;
255 /** Returns the constraint for the lower bound of a variable. */
256 inline ConstraintP
getLowerBoundConstraint(ArithVar x
) const{
257 return d_vars
[x
].d_lb
;
260 /* Initializes a variable to a safe value.*/
261 void initialize(ArithVar x
, Node n
, bool aux
);
263 ArithVar
allocate(Node n
, bool aux
= false);
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;
269 /* Reverts all variable assignments to their safe values. */
270 void revertAssignmentChanges();
272 /* Commits all variables assignments as safe.*/
273 void commitAssignmentChanges();
276 bool lowerBoundIsZero(ArithVar x
);
277 bool upperBoundIsZero(ArithVar x
);
279 bool boundsAreEqual(ArithVar x
) const;
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
);
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;
292 bool equalsLowerBound(ArithVar x
, const DeltaRational
& c
);
293 bool equalsUpperBound(ArithVar x
, const DeltaRational
& c
);
296 * If lowerbound > - \infty:
297 * return getAssignment(x).cmp(getLowerBound(x))
298 * If lowerbound = - \infty:
301 int cmpToLowerBound(ArithVar x
, const DeltaRational
& c
) const;
303 inline bool strictlyLessThanLowerBound(ArithVar x
, const DeltaRational
& c
) const{
304 return cmpToLowerBound(x
, c
) < 0;
306 inline bool lessThanLowerBound(ArithVar x
, const DeltaRational
& c
) const{
307 return cmpToLowerBound(x
, c
) <= 0;
310 inline bool strictlyGreaterThanLowerBound(ArithVar x
, const DeltaRational
& c
) const{
311 return cmpToLowerBound(x
, c
) > 0;
314 inline bool greaterThanLowerBound(ArithVar x
, const DeltaRational
& c
) const{
315 return cmpToLowerBound(x
, c
) >= 0;
318 * If upperbound < \infty:
319 * return getAssignment(x).cmp(getUpperBound(x))
320 * If upperbound = \infty:
323 int cmpToUpperBound(ArithVar x
, const DeltaRational
& c
) const;
325 inline bool strictlyLessThanUpperBound(ArithVar x
, const DeltaRational
& c
) const{
326 return cmpToUpperBound(x
, c
) < 0;
329 inline bool lessThanUpperBound(ArithVar x
, const DeltaRational
& c
) const{
330 return cmpToUpperBound(x
, c
) <= 0;
333 inline bool strictlyGreaterThanUpperBound(ArithVar x
, const DeltaRational
& c
) const{
334 return cmpToUpperBound(x
, c
) > 0;
337 inline bool greaterThanUpperBound(ArithVar x
, const DeltaRational
& c
) const{
338 return cmpToUpperBound(x
, c
) >= 0;
341 inline int cmpAssignmentLowerBound(ArithVar x
) const{
342 return d_vars
[x
].d_cmpAssignmentLB
;
344 inline int cmpAssignmentUpperBound(ArithVar x
) const{
345 return d_vars
[x
].d_cmpAssignmentUB
;
348 inline BoundCounts
atBoundCounts(ArithVar x
) const {
349 return d_vars
[x
].atBoundCounts();
351 inline BoundCounts
hasBoundCounts(ArithVar x
) const {
352 return d_vars
[x
].hasBoundCounts();
354 inline BoundsInfo
boundsInfo(ArithVar x
) const{
355 return d_vars
[x
].boundsInfo();
358 bool strictlyBelowUpperBound(ArithVar x
) const;
359 bool strictlyAboveLowerBound(ArithVar x
) const;
360 bool assignmentIsConsistent(ArithVar x
) const;
362 void printModel(ArithVar x
, std::ostream
& out
) const;
363 void printModel(ArithVar x
) const;
365 /** returns true iff x has both a lower and upper bound. */
366 bool hasEitherBound(ArithVar x
) const;
367 inline bool hasLowerBound(ArithVar x
) const{
368 return d_vars
[x
].d_lb
!= NullConstraint
;
370 inline bool hasUpperBound(ArithVar x
) const{
371 return d_vars
[x
].d_ub
!= NullConstraint
;
374 const Rational
& getDelta();
376 void invalidateDelta();
378 void setDelta(const Rational
& d
);
380 void startQueueingBoundCounts();
381 void stopQueueingBoundCounts();
382 void addToBoundQueue(ArithVar v
, const BoundsInfo
& prev
);
384 BoundsInfo
selectBoundsInfo(ArithVar v
, bool old
) const;
386 bool boundsQueueEmpty() const;
387 void processBoundsQueue(BoundUpdateCallback
& changed
);
389 void printEntireModel(std::ostream
& out
) const;
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).
398 std::pair
<ConstraintP
, ConstraintP
> explainEqualBounds(ArithVar x
) const;
403 * This function implements the mostly identical:
404 * revertAssignmentChanges() and commitAssignmentChanges().
406 void clearSafeAssignments(bool revert
);
408 bool debugEqualSizes();
410 bool inMaps(ArithVar x
) const;
412 };/* class ArithVariables */
415 }/* CVC4::theory::arith namespace */
416 }/* CVC4::theory namespace */
417 }/* CVC4 namespace */
419 #endif /* CVC4__THEORY__ARITH__PARTIAL_MODEL_H */