1 /********************* */
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): kshitij, 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 This is an implementation of the Simplex Module for the Simplex for DPLL(T)
13 ** decision procedure.
15 ** This implements the Simplex module for the Simpelx for DPLL(T) decision procedure.
16 ** See the Simplex for DPLL(T) technical report for more background.(citation?)
17 ** This shares with the theory a Tableau, and a PartialModel that:
18 ** - satisfies the equalities in the Tableau, and
19 ** - the assignment for the non-basic variables satisfies their bounds.
20 ** This is required to either produce a conflict or satisifying PartialModel.
21 ** Further, we require being told when a basic variable updates its value.
23 ** During the Simplex search we maintain a queue of variables.
24 ** The queue is required to contain all of the basic variables that voilate their bounds.
25 ** As elimination from the queue is more efficient to be done lazily,
26 ** we do not maintain that the queue of variables needs to be only basic variables or only
27 ** variables that satisfy their bounds.
29 ** The simplex procedure roughly follows Alberto's thesis. (citation?)
30 ** There is one round of selecting using a heuristic pivoting rule. (See PreferenceFunction
31 ** Documentation for the available options.)
32 ** The non-basic variable is the one that appears in the fewest pivots. (Bruno says that
33 ** Leonardo invented this first.)
34 ** After this, Bland's pivot rule is invoked.
36 ** During this proccess, we periodically inspect the queue of variables to
37 ** 1) remove now extraneous extries,
38 ** 2) detect conflicts that are "waiting" on the queue but may not be detected by the
39 ** current queue heuristics, and
40 ** 3) detect multiple conflicts.
42 ** Conflicts are greedily slackened to use the weakest bounds that still produce the
45 ** Extra things tracked atm: (Subject to change at Tim's whims)
46 ** - A superset of all of the newly pivoted variables.
47 ** - A queue of additional conflicts that were discovered by Simplex.
48 ** These are theory valid and are currently turned into lemmas
51 #include "cvc4_private.h"
55 #include "theory/arith/simplex.h"
56 #include "util/dense_map.h"
57 #include "util/statistics_registry.h"
64 class FCSimplexDecisionProcedure
: public SimplexDecisionProcedure
{
66 FCSimplexDecisionProcedure(LinearEqualityModule
& linEq
, ErrorSet
& errors
, RaiseConflict conflictChannel
, TempVarMalloc tvmalloc
);
68 Result::Sat
findModel(bool exactResult
);
70 // other error variables are dropping
71 WitnessImprovement
dualLikeImproveError(ArithVar evar
);
72 WitnessImprovement
primalImproveError(ArithVar evar
);
76 // - satisfied error set
77 Result::Sat
dualLike();
80 static const uint32_t PENALTY
= 4;
81 DenseMultiset d_scores
;
82 void decreasePenalties(){ d_scores
.removeOneOfEverything(); }
83 uint32_t penalty(ArithVar x
) const { return d_scores
.count(x
); }
84 void setPenalty(ArithVar x
, WitnessImprovement w
){
86 if(d_scores
.count(x
) > 0){
87 d_scores
.removeAll(x
);
90 d_scores
.setCount(x
, PENALTY
);
94 /** The size of the focus set. */
97 /** The current error focus variable. */
98 ArithVar d_focusErrorVar
;
101 * The signs of the coefficients in the focus set.
102 * This is empty until this has been loaded.
104 DenseMap
<const Rational
*> d_focusCoefficients
;
107 * Loads the signs of the coefficients of the variables on the row d_focusErrorVar
110 void loadFocusSigns();
112 /** Unloads the information from d_focusSgns. */
113 void unloadFocusSigns();
116 * The signs of a variable in the row of d_focusErrorVar.
117 * d_focusSgns must be loaded.
119 const Rational
& focusCoefficient(ArithVar nb
) const;
121 int32_t d_pivotBudget
;
122 // enum PivotImprovement {
125 // HeuristicDegenerate,
129 WitnessImprovement d_prevWitnessImprovement
;
130 uint32_t d_witnessImprovementInARow
;
132 uint32_t degeneratePivotsInARow() const;
134 static const uint32_t s_focusThreshold
= 6;
135 static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving
= 100;
136 static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering
= 10;
138 DenseMap
<uint32_t> d_leavingCountSinceImprovement
;
139 void increaseLeavingCount(ArithVar x
){
140 if(!d_leavingCountSinceImprovement
.isKey(x
)){
141 d_leavingCountSinceImprovement
.set(x
,1);
143 (d_leavingCountSinceImprovement
.get(x
))++;
146 LinearEqualityModule::UpdatePreferenceFunction
selectLeavingFunction(ArithVar x
){
147 bool useBlands
= d_leavingCountSinceImprovement
.isKey(x
) &&
148 d_leavingCountSinceImprovement
[x
] >= s_maxDegeneratePivotsBeforeBlandsOnEntering
;
150 return &LinearEqualityModule::preferWitness
<false>;
152 return &LinearEqualityModule::preferWitness
<true>;
156 bool debugDualLike(WitnessImprovement w
, std::ostream
& out
,
158 uint32_t prevFocusSize
, uint32_t prevErrorSize
) const;
160 void debugPrintSignal(ArithVar updated
) const;
162 ArithVarVec d_sgnDisagreements
;
164 //static PivotImprovement pivotImprovement(const UpdateInfo& selected, bool useBlands = false);
166 void logPivot(WitnessImprovement w
);
168 void updateAndSignal(const UpdateInfo
& selected
, WitnessImprovement w
);
170 UpdateInfo
selectPrimalUpdate(ArithVar error
,
171 LinearEqualityModule::UpdatePreferenceFunction upf
,
172 LinearEqualityModule::VarPreferenceFunction bpf
);
175 UpdateInfo
selectUpdateForDualLike(ArithVar basic
){
176 TimerStat::CodeTimer
codeTimer(d_statistics
.d_selectUpdateForDualLike
);
178 LinearEqualityModule::UpdatePreferenceFunction upf
=
179 &LinearEqualityModule::preferWitness
<true>;
180 LinearEqualityModule::VarPreferenceFunction bpf
=
181 &LinearEqualityModule::minVarOrder
;
182 return selectPrimalUpdate(basic
, upf
, bpf
);
185 UpdateInfo
selectUpdateForPrimal(ArithVar basic
, bool useBlands
){
186 TimerStat::CodeTimer
codeTimer(d_statistics
.d_selectUpdateForPrimal
);
188 LinearEqualityModule::UpdatePreferenceFunction upf
;
190 upf
= &LinearEqualityModule::preferWitness
<false>;
192 upf
= &LinearEqualityModule::preferWitness
<true>;
195 LinearEqualityModule::VarPreferenceFunction bpf
= useBlands
?
196 &LinearEqualityModule::minVarOrder
:
197 &LinearEqualityModule::minRowLength
;
198 bpf
= &LinearEqualityModule::minVarOrder
;
200 return selectPrimalUpdate(basic
, upf
, bpf
);
202 WitnessImprovement
selectFocusImproving() ;
204 WitnessImprovement
focusUsingSignDisagreements(ArithVar basic
);
205 WitnessImprovement
focusDownToLastHalf();
206 WitnessImprovement
adjustFocusShrank(const ArithVarVec
& drop
);
207 WitnessImprovement
focusDownToJust(ArithVar v
);
210 void adjustFocusAndError(const UpdateInfo
& up
, const AVIntPairVec
& focusChanges
);
213 * This is the main simplex for DPLL(T) loop.
214 * It runs for at most maxIterations.
216 * Returns true iff it has found a conflict.
217 * d_conflictVariable will be set and the conflict for this row is reported.
219 bool searchForFeasibleSolution(uint32_t maxIterations
);
221 bool initialProcessSignals(){
222 TimerStat
&timer
= d_statistics
.d_initialSignalsTime
;
223 IntStat
& conflictStat
= d_statistics
.d_initialConflicts
;
224 bool res
= standardProcessSignals(timer
, conflictStat
);
225 d_focusSize
= d_errorSet
.focusSize();
229 static bool debugCheckWitness(const UpdateInfo
& inf
, WitnessImprovement w
, bool useBlands
);
231 /** These fields are designed to be accessible to TheoryArith methods. */
234 TimerStat d_initialSignalsTime
;
235 IntStat d_initialConflicts
;
237 IntStat d_fcFoundUnsat
;
238 IntStat d_fcFoundSat
;
242 TimerStat d_fcFocusConstructionTimer
;
244 TimerStat d_selectUpdateForDualLike
;
245 TimerStat d_selectUpdateForPrimal
;
247 ReferenceStat
<uint32_t> d_finalCheckPivotCounter
;
249 Statistics(uint32_t& pivots
);
252 };/* class FCSimplexDecisionProcedure */
254 }/* CVC4::theory::arith namespace */
255 }/* CVC4::theory namespace */
256 }/* CVC4 namespace */