1 /********************* */
4 ** Top contributors (to current version):
5 ** Tim King, Mathias Preiner, Morgan Deters
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 [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
19 #include "cvc4_private.h"
25 #include "options/arith_options.h"
26 #include "theory/arith/arithvar.h"
27 #include "theory/arith/bound_counts.h"
28 #include "theory/arith/callbacks.h"
29 #include "theory/arith/delta_rational.h"
30 #include "theory/arith/partial_model.h"
31 #include "theory/arith/tableau_sizes.h"
32 #include "util/bin_heap.h"
33 #include "util/statistics_registry.h"
41 * The priority queue has 3 different modes of operation:
43 * This passively collects arithmetic variables that may be inconsistent.
44 * This does not maintain any heap structure.
45 * dequeueInconsistentBasicVariable() does not work in this mode!
46 * Entering this mode requires the queue to be empty.
49 * This mode uses the difference between a variables and its bound
50 * to determine which to dequeue first.
52 * - Variable Order Queue
53 * This mode uses the variable order to determine which ArithVar is dequeued first.
55 * The transitions between the modes of operation are:
56 * Collection => Difference Queue
57 * Difference Queue => Variable Order Queue
58 * Difference Queue => Collection (queue must be empty!)
59 * Variable Order Queue => Collection (queue must be empty!)
61 * The queue begins in Collection mode.
68 class ComparatorPivotRule
{
70 const ErrorSet
* d_errorSet
;
72 options::ErrorSelectionRule d_rule
;
75 ComparatorPivotRule();
76 ComparatorPivotRule(const ErrorSet
* es
, options::ErrorSelectionRule r
);
78 bool operator()(ArithVar v
, ArithVar u
) const;
79 options::ErrorSelectionRule
getRule() const { return d_rule
; }
82 // typedef boost::heap::d_ary_heap<
84 // boost::heap::arity<2>,
85 // boost::heap::compare<ComparatorPivotRule>,
86 // boost::heap::mutable_<true> > FocusSet;
88 // typedef FocusSet::handle_type FocusSetHandle;
90 // typedef CVC4_PB_DS_NAMESPACE::priority_queue<
92 // ComparatorPivotRule,
93 // CVC4_PB_DS_NAMESPACE::pairing_heap_tag> FocusSet;
95 // typedef FocusSet::point_iterator FocusSetHandle;
97 typedef BinaryHeap
<ArithVar
, ComparatorPivotRule
> FocusSet
;
98 typedef FocusSet::handle FocusSetHandle
;
101 class ErrorInformation
{
103 /** The variable that is in error. */
107 * The constraint that was violated.
108 * This needs to be saved in case that the
109 * violated constraint
111 ConstraintP d_violated
;
114 * This is the sgn of the first derivate the variable must move to satisfy
115 * the bound violated.
116 * If d_sgn > 0, then d_violated was a lowerbound.
117 * If d_sgn < 0, then d_violated was an upperbound.
122 * If this is true, then the bound is no longer set on d_variables.
123 * This MUST be undone before this is deleted.
128 * If this is true, then the variable is in the focus set and the focus heap.
129 * d_handle is then a reasonable thing to interpret.
130 * If this is false, the variable is somewhere in
133 FocusSetHandle d_handle
;
136 * Auxillary information for storing the difference between a variable and its bound.
137 * Only set on signals.
139 DeltaRational
* d_amount
;
146 ErrorInformation(ArithVar var
, ConstraintP vio
, int sgn
);
148 ErrorInformation(const ErrorInformation
& ei
);
149 ErrorInformation
& operator=(const ErrorInformation
& ei
);
151 void reset(ConstraintP c
, int sgn
);
153 inline ArithVar
getVariable() const { return d_variable
; }
155 bool isRelaxed() const { return d_relaxed
; }
167 inline int sgn() const { return d_sgn
; }
169 inline bool inFocus() const { return d_inFocus
; }
170 inline int focusSgn() const {
171 return (d_inFocus
) ? sgn() : 0;
174 inline void setInFocus(bool inFocus
) { d_inFocus
= inFocus
; }
176 const DeltaRational
& getAmount() const {
177 Assert(d_amount
!= NULL
);
181 void setAmount(const DeltaRational
& am
);
182 void setMetric(uint32_t m
) { d_metric
= m
; }
183 uint32_t getMetric() const { return d_metric
; }
185 inline void setHandle(FocusSetHandle h
) {
189 inline const FocusSetHandle
& getHandle() const{ return d_handle
; }
191 inline ConstraintP
getViolated() const { return d_violated
; }
193 bool debugInitialized() const {
195 d_variable
!= ARITHVAR_SENTINEL
&&
196 d_violated
!= NullConstraint
&&
199 void print(std::ostream
& os
) const {
200 os
<< "{ErrorInfo: " << d_variable
201 << ", " << d_violated
204 << ", " << d_inFocus
;
205 if(d_amount
== NULL
){
214 class ErrorInfoMap
: public DenseMap
<ErrorInformation
> {};
219 * Reference to the arithmetic partial model for checking if a variable
220 * is consistent with its upper and lower bounds.
222 ArithVariables
& d_variables
;
225 * The set of all variables that violate exactly one of their bounds.
227 ErrorInfoMap d_errInfo
;
229 options::ErrorSelectionRule d_selectionRule
;
231 * The ordered heap for the variables that are in ErrorSet.
237 * A strict subset of the error set.
238 * d_outOfFocus \neq d_errInfo.
240 * Its symbolic complement is Focus.
241 * d_outOfFocus \intersect Focus == \emptyset
242 * d_outOfFocus \union Focus == d_errInfo
244 ArithVarVec d_outOfFocus
;
247 * Before a variable is added to the error set, it is added to the signals list.
248 * A variable may appear on the list multiple times.
249 * This introduces a delay.
251 ArithVarVec d_signals
;
253 TableauSizes d_tableauSizes
;
255 BoundCountingLookup d_boundLookup
;
258 * Computes the difference between the assignment and its bound for x.
261 DeltaRational
computeDiff(ArithVar x
) const;
263 void recomputeAmount(ErrorInformation
& ei
, options::ErrorSelectionRule r
);
265 void update(ErrorInformation
& ei
);
266 void transitionVariableOutOfError(ArithVar v
);
267 void transitionVariableIntoError(ArithVar v
);
268 void addBackIntoFocus(ArithVar v
);
272 /** The new focus set is the entire error set. */
274 void dropFromFocus(ArithVar v
);
276 void dropFromFocusAll(const ArithVarVec
& vec
) {
277 for(ArithVarVec::const_iterator i
= vec
.begin(), i_end
= vec
.end(); i
!= i_end
; ++i
){
283 ErrorSet(ArithVariables
& var
, TableauSizes tabSizes
, BoundCountingLookup boundLookup
);
285 typedef ErrorInfoMap::const_iterator error_iterator
;
286 error_iterator
errorBegin() const { return d_errInfo
.begin(); }
287 error_iterator
errorEnd() const { return d_errInfo
.end(); }
289 bool inError(ArithVar v
) const { return d_errInfo
.isKey(v
); }
290 bool inFocus(ArithVar v
) const { return d_errInfo
[v
].inFocus(); }
292 void pushErrorInto(ArithVarVec
& vec
) const;
293 void pushFocusInto(ArithVarVec
& vec
) const;
295 options::ErrorSelectionRule
getSelectionRule() const;
296 void setSelectionRule(options::ErrorSelectionRule rule
);
298 inline ArithVar
topFocusVariable() const{
299 Assert(!focusEmpty());
300 return d_focus
.top();
303 inline void signalVariable(ArithVar var
){
304 d_signals
.push_back(var
);
307 inline void signalUnderCnd(ArithVar var
, bool b
){
308 if(b
){ signalVariable(var
); }
311 inline bool inconsistent(ArithVar var
) const{
312 return !d_variables
.assignmentIsConsistent(var
) ;
314 inline void signalIfInconsistent(ArithVar var
){
315 signalUnderCnd(var
, inconsistent(var
));
318 inline bool errorEmpty() const{
319 return d_errInfo
.empty();
321 inline uint32_t errorSize() const{
322 return d_errInfo
.size();
325 inline bool focusEmpty() const {
326 return d_focus
.empty();
328 inline uint32_t focusSize() const{
329 return d_focus
.size();
332 inline int getSgn(ArithVar x
) const {
334 return d_errInfo
[x
].sgn();
336 inline int focusSgn(ArithVar v
) const {
338 return d_errInfo
[v
].focusSgn();
344 void focusDownToJust(ArithVar v
);
348 /** Clears the set. */
350 void reduceToSignals();
352 bool noSignals() const {
353 return d_signals
.empty();
355 bool moreSignals() const {
358 ArithVar
topSignal() const {
359 Assert(moreSignals());
360 return d_signals
.back();
364 * Moves a variable out of the signals.
365 * This moves it into the error set.
366 * Return the previous focus sign.
370 const DeltaRational
& getAmount(ArithVar v
) const {
371 return d_errInfo
[v
].getAmount();
374 uint32_t sumMetric(ArithVar a
) const{
376 BoundCounts bcs
= d_boundLookup
.atBounds(a
);
377 uint32_t count
= getSgn(a
) > 0 ? bcs
.upperBoundCount() : bcs
.lowerBoundCount();
379 uint32_t length
= d_tableauSizes
.getRowLength(a
);
381 return (length
- count
);
384 uint32_t getMetric(ArithVar a
) const {
385 return d_errInfo
[a
].getMetric();
388 ConstraintP
getViolated(ArithVar a
) const {
389 return d_errInfo
[a
].getViolated();
393 typedef FocusSet::const_iterator focus_iterator
;
394 focus_iterator
focusBegin() const { return d_focus
.begin(); }
395 focus_iterator
focusEnd() const { return d_focus
.end(); }
397 void debugPrint(std::ostream
& out
) const;
403 IntStat d_enqueuesCollection
;
404 IntStat d_enqueuesDiffMode
;
405 IntStat d_enqueuesVarOrderMode
;
407 IntStat d_enqueuesCollectionDuplicates
;
408 IntStat d_enqueuesVarOrderModeDuplicates
;
414 Statistics d_statistics
;
417 }/* CVC4::theory::arith namespace */
418 }/* CVC4::theory namespace */
419 }/* CVC4 namespace */