1 /********************* */
2 /*! \file arith_priority_queue.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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"
23 #include "theory/arith/arithvar.h"
24 #include "theory/arith/bound_counts.h"
25 #include "theory/arith/delta_rational.h"
26 #include "theory/arith/partial_model.h"
27 #include "theory/arith/arith_heuristic_pivot_rule.h"
28 #include "theory/arith/tableau_sizes.h"
29 #include "theory/arith/callbacks.h"
31 #include "util/statistics_registry.h"
33 #if CVC4_GCC_HAS_PB_DS_BUG
34 // Unfortunate bug in some older GCCs (e.g., v4.2):
35 // http://gcc.gnu.org/bugzilla/show_bug.cgi?id=36612
36 // Requires some header-hacking to work around
37 # define __throw_container_error inline __throw_container_error
38 # define __throw_insert_error inline __throw_insert_error
39 # define __throw_join_error inline __throw_join_error
40 # define __throw_resize_error inline __throw_resize_error
41 # include <ext/pb_ds/exception.hpp>
42 # undef __throw_container_error
43 # undef __throw_insert_error
44 # undef __throw_join_error
45 # undef __throw_resize_error
46 #endif /* CVC4_GCC_HAS_PB_DS_BUG */
48 #include <ext/pb_ds/priority_queue.hpp>
58 * The priority queue has 3 different modes of operation:
60 * This passively collects arithmetic variables that may be inconsistent.
61 * This does not maintain any heap structure.
62 * dequeueInconsistentBasicVariable() does not work in this mode!
63 * Entering this mode requires the queue to be empty.
66 * This mode uses the difference between a variables and its bound
67 * to determine which to dequeue first.
69 * - Variable Order Queue
70 * This mode uses the variable order to determine which ArithVar is dequeued first.
72 * The transitions between the modes of operation are:
73 * Collection => Difference Queue
74 * Difference Queue => Variable Order Queue
75 * Difference Queue => Collection (queue must be empty!)
76 * Variable Order Queue => Collection (queue must be empty!)
78 * The queue begins in Collection mode.
85 class ComparatorPivotRule
{
87 const ErrorSet
* d_errorSet
;
89 ErrorSelectionRule d_rule
;
91 ComparatorPivotRule();
92 ComparatorPivotRule(const ErrorSet
* es
, ErrorSelectionRule r
);
94 bool operator()(ArithVar v
, ArithVar u
) const;
95 ErrorSelectionRule
getRule() const { return d_rule
; }
98 // typedef boost::heap::d_ary_heap<
100 // boost::heap::arity<2>,
101 // boost::heap::compare<ComparatorPivotRule>,
102 // boost::heap::mutable_<true> > FocusSet;
104 // typedef FocusSet::handle_type FocusSetHandle;
106 typedef CVC4_PB_DS_NAMESPACE::priority_queue
<
109 CVC4_PB_DS_NAMESPACE::pairing_heap_tag
> FocusSet
;
111 typedef FocusSet::point_iterator FocusSetHandle
;
113 class ErrorInformation
{
115 /** The variable that is in error. */
119 * The constraint that was violated.
120 * This needs to be saved in case that the
121 * violated constraint
123 Constraint d_violated
;
126 * This is the sgn of the first derivate the variable must move to satisfy
127 * the bound violated.
128 * If d_sgn > 0, then d_violated was a lowerbound.
129 * If d_sgn < 0, then d_violated was an upperbound.
134 * If this is true, then the bound is no longer set on d_variables.
135 * This MUST be undone before this is deleted.
140 * If this is true, then the variable is in the focus set and the focus heap.
141 * d_handle is then a reasonable thing to interpret.
142 * If this is false, the variable is somewhere in
145 FocusSetHandle d_handle
;
148 * Auxillary information for storing the difference between a variable and its bound.
149 * Only set on signals.
151 DeltaRational
* d_amount
;
158 ErrorInformation(ArithVar var
, Constraint vio
, int sgn
);
160 ErrorInformation(const ErrorInformation
& ei
);
161 ErrorInformation
& operator=(const ErrorInformation
& ei
);
163 void reset(Constraint c
, int sgn
);
165 inline ArithVar
getVariable() const { return d_variable
; }
167 bool isRelaxed() const { return d_relaxed
; }
168 void setRelaxed(){ Assert(!d_relaxed
); d_relaxed
= true; }
169 void setUnrelaxed(){ Assert(d_relaxed
); d_relaxed
= false; }
171 inline int sgn() const { return d_sgn
; }
173 inline bool inFocus() const { return d_inFocus
; }
174 inline int focusSgn() const {
175 return (d_inFocus
) ? sgn() : 0;
178 inline void setInFocus(bool inFocus
) { d_inFocus
= inFocus
; }
180 const DeltaRational
& getAmount() const {
181 Assert(d_amount
!= NULL
);
185 void setAmount(const DeltaRational
& am
);
186 void setMetric(uint32_t m
) { d_metric
= m
; }
187 uint32_t getMetric() const { return d_metric
; }
189 inline void setHandle(FocusSetHandle h
) {
193 inline const FocusSetHandle
& getHandle() const{ return d_handle
; }
195 inline Constraint
getViolated() const { return d_violated
; }
197 bool debugInitialized() const {
199 d_variable
!= ARITHVAR_SENTINEL
&&
200 d_violated
!= NullConstraint
&&
203 void print(std::ostream
& os
) const {
204 os
<< "{ErrorInfo: " << d_variable
205 << ", " << d_violated
208 << ", " << d_inFocus
;
209 if(d_amount
== NULL
){
218 class ErrorInfoMap
: public DenseMap
<ErrorInformation
> {};
223 * Reference to the arithmetic partial model for checking if a variable
224 * is consistent with its upper and lower bounds.
226 ArithVariables
& d_variables
;
229 * The set of all variables that violate exactly one of their bounds.
231 ErrorInfoMap d_errInfo
;
233 ErrorSelectionRule d_selectionRule
;
235 * The ordered heap for the variables that are in ErrorSet.
241 * A strict subset of the error set.
242 * d_outOfFocus \neq d_errInfo.
244 * Its symbolic complement is Focus.
245 * d_outOfFocus \intersect Focus == \emptyset
246 * d_outOfFocus \union Focus == d_errInfo
248 ArithVarVec d_outOfFocus
;
251 * Before a variable is added to the error set, it is added to the signals list.
252 * A variable may appear on the list multiple times.
253 * This introduces a delay.
255 ArithVarVec d_signals
;
257 TableauSizes d_tableauSizes
;
259 BoundCountingLookup d_boundLookup
;
262 * Computes the difference between the assignment and its bound for x.
265 DeltaRational
computeDiff(ArithVar x
) const;
267 void recomputeAmount(ErrorInformation
& ei
, ErrorSelectionRule r
);
269 void update(ErrorInformation
& ei
);
270 void transitionVariableOutOfError(ArithVar v
);
271 void transitionVariableIntoError(ArithVar v
);
272 void addBackIntoFocus(ArithVar v
);
276 /** The new focus set is the entire error set. */
278 void dropFromFocus(ArithVar v
);
280 void dropFromFocusAll(const ArithVarVec
& vec
) {
281 for(ArithVarVec::const_iterator i
= vec
.begin(), i_end
= vec
.end(); i
!= i_end
; ++i
){
287 ErrorSet(ArithVariables
& var
, TableauSizes tabSizes
, BoundCountingLookup boundLookup
);
289 typedef ErrorInfoMap::const_iterator error_iterator
;
290 error_iterator
errorBegin() const { return d_errInfo
.begin(); }
291 error_iterator
errorEnd() const { return d_errInfo
.end(); }
293 bool inError(ArithVar v
) const { return d_errInfo
.isKey(v
); }
294 bool inFocus(ArithVar v
) const { return d_errInfo
[v
].inFocus(); }
296 void pushErrorInto(ArithVarVec
& vec
) const;
297 void pushFocusInto(ArithVarVec
& vec
) const;
299 ErrorSelectionRule
getSelectionRule() const;
300 void setSelectionRule(ErrorSelectionRule rule
);
302 inline ArithVar
topFocusVariable() const{
303 Assert(!focusEmpty());
304 return d_focus
.top();
307 inline void signalVariable(ArithVar var
){
308 d_signals
.push_back(var
);
311 inline void signalUnderCnd(ArithVar var
, bool b
){
312 if(b
){ signalVariable(var
); }
315 inline bool inconsistent(ArithVar var
) const{
316 return !d_variables
.assignmentIsConsistent(var
) ;
318 inline void signalIfInconsistent(ArithVar var
){
319 signalUnderCnd(var
, inconsistent(var
));
322 inline bool errorEmpty() const{
323 return d_errInfo
.empty();
325 inline uint32_t errorSize() const{
326 return d_errInfo
.size();
329 inline bool focusEmpty() const {
330 return d_focus
.empty();
332 inline uint32_t focusSize() const{
333 return d_focus
.size();
336 inline int getSgn(ArithVar x
) const {
338 return d_errInfo
[x
].sgn();
340 inline int focusSgn(ArithVar v
) const {
342 return d_errInfo
[v
].focusSgn();
348 void focusDownToJust(ArithVar v
);
352 /** Clears the set. */
354 void reduceToSignals();
356 bool noSignals() const {
357 return d_signals
.empty();
359 bool moreSignals() const {
362 ArithVar
topSignal() const {
363 Assert(moreSignals());
364 return d_signals
.back();
368 * Moves a variable out of the signals.
369 * This moves it into the error set.
370 * Return the previous focus sign.
374 const DeltaRational
& getAmount(ArithVar v
) const {
375 return d_errInfo
[v
].getAmount();
378 uint32_t sumMetric(ArithVar a
) const{
380 BoundCounts bcs
= d_boundLookup
.atBounds(a
);
381 uint32_t count
= getSgn(a
) > 0 ? bcs
.upperBoundCount() : bcs
.lowerBoundCount();
383 uint32_t length
= d_tableauSizes
.getRowLength(a
);
385 return (length
- count
);
388 uint32_t getMetric(ArithVar a
) const {
389 return d_errInfo
[a
].getMetric();
392 Constraint
getViolated(ArithVar a
) const {
393 return d_errInfo
[a
].getViolated();
397 typedef FocusSet::const_iterator focus_iterator
;
398 focus_iterator
focusBegin() const { return d_focus
.begin(); }
399 focus_iterator
focusEnd() const { return d_focus
.end(); }
401 void debugPrint(std::ostream
& out
) const;
407 IntStat d_enqueuesCollection
;
408 IntStat d_enqueuesDiffMode
;
409 IntStat d_enqueuesVarOrderMode
;
411 IntStat d_enqueuesCollectionDuplicates
;
412 IntStat d_enqueuesVarOrderModeDuplicates
;
418 Statistics d_statistics
;
421 }/* CVC4::theory::arith namespace */
422 }/* CVC4::theory namespace */
423 }/* CVC4 namespace */