blob: da5cf78b55789b6d95bd4a1e56bce35b81d9cac3 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
|
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
#define __CVC4__THEORY__ARITH__ARITH_PRIORITY_QUEUE_H
#include "theory/arith/arith_utilities.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
#include <queue>
namespace CVC4 {
namespace theory {
namespace arith {
typedef std::pair<ArithVar, DeltaRational> VarDRatPair;
struct VarDRatPairCompare{
inline bool operator()(const VarDRatPair& a, const VarDRatPair& b){
return a.second > b.second;
}
};
typedef std::priority_queue<VarDRatPair, std::vector<VarDRatPair>, VarDRatPairCompare> GriggioPQueue;
typedef std::priority_queue<ArithVar, vector<ArithVar>, std::greater<ArithVar> > PQueue;
class ArithPriorityQueue {
private:
/**
* Priority Queue of the basic variables that may be inconsistent.
* Variables are ordered according to which violates its bound the most.
* This is a hueristic and makes no guarentees to terminate!
* This heuristic comes from Alberto Griggio's thesis.
*/
GriggioPQueue d_griggioRuleQueue;
/**
* Priority Queue of the basic variables that may be inconsistent.
*
* This is required to contain at least 1 instance of every inconsistent
* basic variable. This is only required to be a superset though so its
* contents must be checked to still be basic and inconsistent.
*
* This is also required to agree with the row on variable order for termination.
* Effectively this means that this must be a min-heap.
*/
PQueue d_possiblyInconsistent;
/**
* Reference to the arithmetic partial model for checking if a variable
* is consistent with its upper and lower bounds.
*/
ArithPartialModel& d_partialModel;
/** Reference to the Tableau for checking if a variable is basic. */
const Tableau& d_tableau;
/**
* Controls which priority queue is in use.
* If true, d_griggioRuleQueue is used.
* If false, d_possiblyInconsistent is used.
*/
bool d_usingGriggioRule;
public:
ArithPriorityQueue(ArithPartialModel& pm, const Tableau& tableau);
ArithVar popInconsistentBasicVariable();
void enqueueIfInconsistent(ArithVar basic);
void enqueueTrustedVector(const vector<VarDRatPair>& trusted);
void dumpQueueIntoVector(vector<VarDRatPair>& target);
inline bool basicAndInconsistent(ArithVar var) const{
return d_tableau.isBasic(var)
&& !d_partialModel.assignmentIsConsistent(var) ;
}
void useGriggioQueue();
void useBlandQueue();
inline bool usingGriggioRule() const{
return d_usingGriggioRule;
}
inline bool empty() const{
if(usingGriggioRule()){
return d_griggioRuleQueue.empty();
}else{
return d_possiblyInconsistent.empty();
}
}
inline size_t size() const {
if(usingGriggioRule()){
return d_griggioRuleQueue.size();
}else{
return d_possiblyInconsistent.size();
}
}
void clear();
};
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH_PRIORITY_QUEUE_H */
|
