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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
|
#include "cvc4_private.h"
#ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
#define __CVC4__THEORY__ARITH__SIMPLEX_H
#include "theory/arith/arith_utilities.h"
#include "theory/arith/arith_priority_queue.h"
#include "theory/arith/arithvar_set.h"
#include "theory/arith/delta_rational.h"
#include "theory/arith/tableau.h"
#include "theory/arith/partial_model.h"
#include "theory/output_channel.h"
#include "util/stats.h"
#include <queue>
namespace CVC4 {
namespace theory {
namespace arith {
class SimplexDecisionProcedure {
private:
/** Stores system wide constants to avoid unnessecary reconstruction. */
const ArithConstants& d_constants;
/**
* Manages information about the assignment and upper and lower bounds on
* variables.
*/
ArithPartialModel& d_partialModel;
OutputChannel* d_out;
Tableau& d_tableau;
ArithPriorityQueue d_queue;
ArithVar d_numVariables;
public:
SimplexDecisionProcedure(const ArithConstants& constants,
ArithPartialModel& pm,
OutputChannel* out,
Tableau& tableau) :
d_constants(constants),
d_partialModel(pm),
d_out(out),
d_tableau(tableau),
d_queue(pm, tableau),
d_numVariables(0)
{}
void increaseMax() {d_numVariables++;}
/**
* Assert*(n, orig) takes an bound n that is implied by orig.
* and asserts that as a new bound if it is tighter than the current bound
* and updates the value of a basic variable if needed.
* If this new bound is in conflict with the other bound,
* a conflict is created and asserted to the output channel.
*
* orig must be an atom in the SAT solver so that it can be used for
* conflict analysis.
*
* n is of the form (x =?= c) where x is a variable,
* c is a constant and =?= is either LT, LEQ, EQ, GEQ, or GT.
*
* returns true if a conflict was asserted.
*/
bool AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode orig);
bool AssertUpper(ArithVar x_i, const DeltaRational& c_i, TNode orig);
bool AssertEquality(ArithVar x_i, const DeltaRational& c_i, TNode orig);
private:
/**
* Updates the assignment of a nonbasic variable x_i to v.
* Also updates the assignment of basic variables accordingly.
*/
void update(ArithVar x_i, const DeltaRational& v);
/**
* Updates the value of a basic variable x_i to v,
* and then pivots x_i with the nonbasic variable in its row x_j.
* Updates the assignment of the other basic variables accordingly.
*/
void pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v);
public:
/**
* Tries to update the assignments of variables such that all of the
* assignments are consistent with their bounds.
*
* This is done by searching through the tableau.
* If all of the variables can be made consistent with their bounds
* Node::null() is returned. Otherwise a minimized conflict is returned.
*
* If a conflict is found, changes to the assignments need to be reverted.
*
* Tableau pivoting is performed so variables may switch from being basic to
* nonbasic and vice versa.
*
* Corresponds to the "check()" procedure in [Cav06].
*/
Node updateInconsistentVars();
private:
template <bool limitIterations> Node searchForFeasibleSolution(uint32_t maxIterations);
enum SearchPeriod {BeforeDiffSearch, AfterDiffSearch, DuringVarOrderSearch};
Node findConflictOnTheQueue(SearchPeriod period);
private:
/**
* Given the basic variable x_i,
* this function finds the smallest nonbasic variable x_j in the row of x_i
* in the tableau that can "take up the slack" to let x_i satisfy its bounds.
* This returns TNode::null() if none exists.
*
* If first is true, return the first ArithVar in the row to satisfy these conditions.
* If first is false, return the ArithVar with the smallest row count.
*
* More formally one of the following conditions must be satisfied:
* - above && a_ij < 0 && assignment(x_j) < upperbound(x_j)
* - above && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
* - !above && a_ij > 0 && assignment(x_j) < upperbound(x_j)
* - !above && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
*/
template <bool above> ArithVar selectSlack(ArithVar x_i, bool first);
ArithVar selectSlackBelow(ArithVar x_i, bool first) {
return selectSlack<false>(x_i, first);
}
ArithVar selectSlackAbove(ArithVar x_i, bool first) {
return selectSlack<true>(x_i, first);
}
/**
* Returns the smallest basic variable whose assignment is not consistent
* with its upper and lower bounds.
*/
ArithVar selectSmallestInconsistentVar();
/**
* Given a non-basic variable that is know to not be updatable
* to a consistent value, construct and return a conflict.
* Follows section 4.2 in the CAV06 paper.
*/
Node generateConflictAbove(ArithVar conflictVar);
Node generateConflictBelow(ArithVar conflictVar);
public:
/**
* Checks to make sure the assignment is consistent with the tableau.
* This code is for debugging.
*/
void checkTableau();
/**
* Computes the value of a basic variable using the assignments
* of the values of the variables in the basic variable's row tableau.
* This can compute the value using either:
* - the the current assignment (useSafe=false) or
* - the safe assignment (useSafe = true).
*/
DeltaRational computeRowValue(ArithVar x, bool useSafe);
private:
/**
* Checks a basic variable, b, to see if it is in conflict.
* If a conflict is discovered a node summarizing the conflict is returned.
* Otherwise, Node::null() is returned.
*/
Node checkBasicForConflict(ArithVar b);
/** These fields are designed to be accessable to TheoryArith methods. */
class Statistics {
public:
IntStat d_statPivots, d_statUpdates;
IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
IntStat d_statUpdateConflicts;
TimerStat d_findConflictOnTheQueueTime;
IntStat d_attemptBeforeDiffSearch, d_successBeforeDiffSearch;
IntStat d_attemptAfterDiffSearch, d_successAfterDiffSearch;
IntStat d_attemptDuringVarOrderSearch, d_successDuringVarOrderSearch;
TimerStat d_pivotTime;
AverageStat d_avgNumRowsNotContainingOnUpdate;
AverageStat d_avgNumRowsNotContainingOnPivot;
Statistics();
~Statistics();
};
Statistics d_statistics;
};/* class SimplexDecisionProcedure */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */
|
