2 #include "cvc4_private.h"
4 #ifndef __CVC4__THEORY__ARITH__SIMPLEX_H
5 #define __CVC4__THEORY__ARITH__SIMPLEX_H
7 #include "theory/arith/arith_utilities.h"
8 #include "theory/arith/arith_priority_queue.h"
9 #include "theory/arith/arithvar_set.h"
10 #include "theory/arith/delta_rational.h"
11 #include "theory/arith/tableau.h"
12 #include "theory/arith/partial_model.h"
13 #include "theory/arith/arith_prop_manager.h"
15 #include "util/options.h"
17 #include "util/stats.h"
25 class SimplexDecisionProcedure
{
29 * Manages information about the assignment and upper and lower bounds on
32 ArithPartialModel
& d_partialModel
;
35 ArithPriorityQueue d_queue
;
37 ArithPropManager
& d_propManager
;
39 ArithVar d_numVariables
;
41 std::queue
<Node
> d_delayedLemmas
;
43 PermissiveBackArithVarSet d_updatedBounds
;
44 PermissiveBackArithVarSet d_candidateBasics
;
47 DeltaRational d_DELTA_ZERO
;
50 SimplexDecisionProcedure(ArithPropManager
& propManager
,
51 ArithPartialModel
& pm
,
56 * Assert*(n, orig) takes an bound n that is implied by orig.
57 * and asserts that as a new bound if it is tighter than the current bound
58 * and updates the value of a basic variable if needed.
60 * orig must be a literal in the SAT solver so that it can be used for
63 * x is the variable getting the new bound,
64 * c is the value of the new bound.
66 * If this new bound is in conflict with the other bound,
67 * a node describing this conflict is returned.
68 * If this new bound is not in conflict, Node::null() is returned.
70 Node
AssertLower(ArithVar x
, const DeltaRational
& c
, TNode orig
);
71 Node
AssertUpper(ArithVar x
, const DeltaRational
& c
, TNode orig
);
72 Node
AssertEquality(ArithVar x
, const DeltaRational
& c
, TNode orig
);
76 * Updates the assignment of a nonbasic variable x_i to v.
77 * Also updates the assignment of basic variables accordingly.
79 void update(ArithVar x_i
, const DeltaRational
& v
);
82 * Updates the value of a basic variable x_i to v,
83 * and then pivots x_i with the nonbasic variable in its row x_j.
84 * Updates the assignment of the other basic variables accordingly.
86 void pivotAndUpdate(ArithVar x_i
, ArithVar x_j
, DeltaRational
& v
);
90 * A PreferenceFunction takes a const ref to the SimplexDecisionProcedure,
91 * and 2 ArithVar variables and returns one of the ArithVar variables potentially
92 * using the internals of the SimplexDecisionProcedure.
94 * Both ArithVar must be non-basic in d_tableau.
96 typedef ArithVar (*PreferenceFunction
)(const SimplexDecisionProcedure
&, ArithVar
, ArithVar
);
99 * minVarOrder is a PreferenceFunction for selecting the smaller of the 2 ArithVars.
100 * This PreferenceFunction is used during the VarOrder stage of
101 * updateInconsistentVars.
103 static ArithVar
minVarOrder(const SimplexDecisionProcedure
& simp
, ArithVar x
, ArithVar y
);
106 * minRowCount is a PreferenceFunction for selecting the variable with the smaller
107 * row count in the tableau.
109 * This is a hueristic rule and should not be used
110 * during the VarOrder stage of updateInconsistentVars.
112 static ArithVar
minColLength(const SimplexDecisionProcedure
& simp
, ArithVar x
, ArithVar y
);
114 * minBoundAndRowCount is a PreferenceFunction for preferring a variable
115 * without an asserted bound over variables with an asserted bound.
116 * If both have bounds or both do not have bounds,
117 * the rule falls back to minRowCount(...).
119 * This is a hueristic rule and should not be used
120 * during the VarOrder stage of updateInconsistentVars.
122 static ArithVar
minBoundAndRowCount(const SimplexDecisionProcedure
& simp
, ArithVar x
, ArithVar y
);
126 * Tries to update the assignments of variables such that all of the
127 * assignments are consistent with their bounds.
129 * This is done by searching through the tableau.
130 * If all of the variables can be made consistent with their bounds
131 * Node::null() is returned. Otherwise a minimized conflict is returned.
133 * If a conflict is found, changes to the assignments need to be reverted.
135 * Tableau pivoting is performed so variables may switch from being basic to
136 * nonbasic and vice versa.
138 * Corresponds to the "check()" procedure in [Cav06].
140 Node
updateInconsistentVars();
142 template <PreferenceFunction
> Node
searchForFeasibleSolution(uint32_t maxIterations
);
144 enum SearchPeriod
{BeforeDiffSearch
, DuringDiffSearch
, AfterDiffSearch
, DuringVarOrderSearch
, AfterVarOrderSearch
};
146 Node
findConflictOnTheQueue(SearchPeriod period
, bool returnFirst
= true);
150 * Given the basic variable x_i,
151 * this function finds the smallest nonbasic variable x_j in the row of x_i
152 * in the tableau that can "take up the slack" to let x_i satisfy its bounds.
153 * This returns ARITHVAR_SENTINEL if none exists.
155 * More formally one of the following conditions must be satisfied:
156 * - lowerBound && a_ij < 0 && assignment(x_j) < upperbound(x_j)
157 * - lowerBound && a_ij > 0 && assignment(x_j) > lowerbound(x_j)
158 * - !lowerBound && a_ij > 0 && assignment(x_j) < upperbound(x_j)
159 * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
162 template <bool lowerBound
, PreferenceFunction
> ArithVar
selectSlack(ArithVar x_i
);
163 template <PreferenceFunction pf
> ArithVar
selectSlackLowerBound(ArithVar x_i
) {
164 return selectSlack
<true, pf
>(x_i
);
166 template <PreferenceFunction pf
> ArithVar
selectSlackUpperBound(ArithVar x_i
) {
167 return selectSlack
<false, pf
>(x_i
);
170 * Returns the smallest basic variable whose assignment is not consistent
171 * with its upper and lower bounds.
173 ArithVar
selectSmallestInconsistentVar();
177 * Exports either the explanation of an upperbound or a lower bound
178 * of the basic variable basic, using the non-basic variables in the row.
180 template <bool upperBound
>
181 void explainNonbasics(ArithVar basic
, NodeBuilder
<>& output
);
182 void explainNonbasicsLowerBound(ArithVar basic
, NodeBuilder
<>& output
){
183 explainNonbasics
<false>(basic
, output
);
185 void explainNonbasicsUpperBound(ArithVar basic
, NodeBuilder
<>& output
){
186 explainNonbasics
<true>(basic
, output
);
189 Node
deduceUpperBound(ArithVar basicVar
);
190 Node
deduceLowerBound(ArithVar basicVar
);
193 * Given a non-basic variable that is know to not be updatable
194 * to a consistent value, construct and return a conflict.
195 * Follows section 4.2 in the CAV06 paper.
197 Node
generateConflictAboveUpperBound(ArithVar conflictVar
);
198 Node
generateConflictBelowLowerBound(ArithVar conflictVar
);
202 * Checks to make sure the assignment is consistent with the tableau.
203 * This code is for debugging.
205 void debugCheckTableau();
206 void debugPivotSimplex(ArithVar x_i
, ArithVar x_j
);
210 * Computes the value of a basic variable using the assignments
211 * of the values of the variables in the basic variable's row tableau.
212 * This can compute the value using either:
213 * - the the current assignment (useSafe=false) or
214 * - the safe assignment (useSafe = true).
216 DeltaRational
computeRowValue(ArithVar x
, bool useSafe
);
218 bool hasAnyUpdates() { return !d_updatedBounds
.empty(); }
220 d_updatedBounds
.purge();
222 void propagateCandidates();
224 void increaseMax() {d_numVariables
++;}
226 /** Returns true if the simplex procedure has more delayed lemmas in its queue.*/
227 bool hasMoreLemmas() const {
228 return !d_delayedLemmas
.empty();
230 /** Returns the next delayed lemmas on the queue.*/
232 Assert(hasMoreLemmas());
233 Node lemma
= d_delayedLemmas
.front();
234 d_delayedLemmas
.pop();
239 /** Adds a lemma to the queue. */
240 void pushLemma(Node lemma
){
241 d_delayedLemmas
.push(lemma
);
242 ++(d_statistics
.d_delayedConflicts
);
245 /** Adds a conflict as a lemma to the queue. */
246 void delayConflictAsLemma(Node conflict
){
247 Node negatedConflict
= negateConjunctionAsClause(conflict
);
248 pushLemma(negatedConflict
);
251 template <bool above
>
252 inline bool isAcceptableSlack(int sgn
, ArithVar nonbasic
){
254 ( above
&& sgn
< 0 && d_partialModel
.strictlyBelowUpperBound(nonbasic
)) ||
255 ( above
&& sgn
> 0 && d_partialModel
.strictlyAboveLowerBound(nonbasic
)) ||
256 (!above
&& sgn
> 0 && d_partialModel
.strictlyBelowUpperBound(nonbasic
)) ||
257 (!above
&& sgn
< 0 && d_partialModel
.strictlyAboveLowerBound(nonbasic
));
261 * Checks a basic variable, b, to see if it is in conflict.
262 * If a conflict is discovered a node summarizing the conflict is returned.
263 * Otherwise, Node::null() is returned.
265 Node
checkBasicForConflict(ArithVar b
);
267 Node
weakenConflict(bool aboveUpper
, ArithVar basicVar
);
268 TNode
weakestExplanation(bool aboveUpper
, DeltaRational
& surplus
, ArithVar v
, const Rational
& coeff
, bool& anyWeakening
, ArithVar basic
);
270 void propagateCandidate(ArithVar basic
);
271 bool propagateCandidateBound(ArithVar basic
, bool upperBound
);
273 inline bool propagateCandidateLowerBound(ArithVar basic
){
274 return propagateCandidateBound(basic
, false);
276 inline bool propagateCandidateUpperBound(ArithVar basic
){
277 return propagateCandidateBound(basic
, true);
280 bool hasBounds(ArithVar basic
, bool upperBound
);
281 bool hasLowerBounds(ArithVar basic
){
282 return hasBounds(basic
, false);
284 bool hasUpperBounds(ArithVar basic
){
285 return hasBounds(basic
, true);
287 DeltaRational
computeBound(ArithVar basic
, bool upperBound
);
289 inline DeltaRational
computeLowerBound(ArithVar basic
){
290 return computeBound(basic
, false);
292 inline DeltaRational
computeUpperBound(ArithVar basic
){
293 return computeBound(basic
, true);
297 /** These fields are designed to be accessable to TheoryArith methods. */
300 IntStat d_statPivots
, d_statUpdates
;
302 IntStat d_statAssertUpperConflicts
, d_statAssertLowerConflicts
;
303 IntStat d_statUpdateConflicts
;
305 TimerStat d_findConflictOnTheQueueTime
;
307 IntStat d_attemptBeforeDiffSearch
, d_successBeforeDiffSearch
;
308 IntStat d_attemptAfterDiffSearch
, d_successAfterDiffSearch
;
309 IntStat d_attemptDuringDiffSearch
, d_successDuringDiffSearch
;
310 IntStat d_attemptDuringVarOrderSearch
, d_successDuringVarOrderSearch
;
311 IntStat d_attemptAfterVarOrderSearch
, d_successAfterVarOrderSearch
;
313 IntStat d_weakeningAttempts
, d_weakeningSuccesses
, d_weakenings
;
314 TimerStat d_weakenTime
;
316 TimerStat d_boundComputationTime
;
317 IntStat d_boundComputations
, d_boundPropagations
;
319 IntStat d_delayedConflicts
;
321 TimerStat d_pivotTime
;
323 AverageStat d_avgNumRowsNotContainingOnUpdate
;
324 AverageStat d_avgNumRowsNotContainingOnPivot
;
330 Statistics d_statistics
;
332 };/* class SimplexDecisionProcedure */
334 }/* CVC4::theory::arith namespace */
335 }/* CVC4::theory namespace */
336 }/* CVC4 namespace */
338 #endif /* __CVC4__THEORY__ARITH__SIMPLEX_H */