1 /********************* */
2 /*! \file soi_simplex.h
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing 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"
57 #include "theory/arith/simplex.h"
58 #include "util/dense_map.h"
59 #include "util/statistics_registry.h"
65 class SumOfInfeasibilitiesSPD
: public SimplexDecisionProcedure
{
67 SumOfInfeasibilitiesSPD(LinearEqualityModule
& linEq
, ErrorSet
& errors
, RaiseConflict conflictChannel
, TempVarMalloc tvmalloc
);
69 Result::Sat
findModel(bool exactResult
);
71 // other error variables are dropping
72 WitnessImprovement
dualLikeImproveError(ArithVar evar
);
73 WitnessImprovement
primalImproveError(ArithVar evar
);
76 /** The current sum of infeasibilities variable. */
81 // - satisfied error set
82 Result::Sat
sumOfInfeasibilities();
84 // static const uint32_t PENALTY = 4;
85 // DenseMultiset d_scores;
86 // void decreasePenalties(){ d_scores.removeOneOfEverything(); }
87 // uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
88 // void setPenalty(ArithVar x, WitnessImprovement w){
89 // if(improvement(w)){
90 // if(d_scores.count(x) > 0){
91 // d_scores.removeAll(x);
94 // d_scores.setCount(x, PENALTY);
98 int32_t d_pivotBudget
;
99 // enum PivotImprovement {
102 // HeuristicDegenerate,
106 WitnessImprovement d_prevWitnessImprovement
;
107 uint32_t d_witnessImprovementInARow
;
109 uint32_t degeneratePivotsInARow() const;
111 static const uint32_t s_focusThreshold
= 6;
112 static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving
= 100;
113 static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering
= 10;
115 DenseMap
<uint32_t> d_leavingCountSinceImprovement
;
116 void increaseLeavingCount(ArithVar x
){
117 if(!d_leavingCountSinceImprovement
.isKey(x
)){
118 d_leavingCountSinceImprovement
.set(x
,1);
120 (d_leavingCountSinceImprovement
.get(x
))++;
123 LinearEqualityModule::UpdatePreferenceFunction
selectLeavingFunction(ArithVar x
){
124 bool useBlands
= d_leavingCountSinceImprovement
.isKey(x
) &&
125 d_leavingCountSinceImprovement
[x
] >= s_maxDegeneratePivotsBeforeBlandsOnEntering
;
127 return &LinearEqualityModule::preferWitness
<false>;
129 return &LinearEqualityModule::preferWitness
<true>;
133 bool debugSOI(WitnessImprovement w
, std::ostream
& out
, int instance
) const;
135 void debugPrintSignal(ArithVar updated
) const;
137 ArithVarVec d_sgnDisagreements
;
139 void logPivot(WitnessImprovement w
);
141 void updateAndSignal(const UpdateInfo
& selected
, WitnessImprovement w
);
143 UpdateInfo
selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf
,
144 LinearEqualityModule::VarPreferenceFunction bpf
);
147 // UpdateInfo selectUpdateForDualLike(ArithVar basic){
148 // TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForDualLike);
150 // LinearEqualityModule::UpdatePreferenceFunction upf =
151 // &LinearEqualityModule::preferWitness<true>;
152 // LinearEqualityModule::VarPreferenceFunction bpf =
153 // &LinearEqualityModule::minVarOrder;
154 // return selectPrimalUpdate(basic, upf, bpf);
157 // UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
158 // TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
160 // LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
161 // &LinearEqualityModule::preferWitness<false>:
162 // &LinearEqualityModule::preferWitness<true>;
164 // LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
165 // &LinearEqualityModule::minVarOrder :
166 // &LinearEqualityModule::minRowLength;
167 // bpf = &LinearEqualityModule::minVarOrder;
169 // return selectPrimalUpdate(basic, upf, bpf);
171 // WitnessImprovement selectFocusImproving() ;
172 WitnessImprovement
soiRound();
173 WitnessImprovement
SOIConflict();
174 std::vector
< ArithVarVec
> greedyConflictSubsets();
175 bool generateSOIConflict(const ArithVarVec
& subset
);
177 // WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
178 // WitnessImprovement focusDownToLastHalf();
179 // WitnessImprovement adjustFocusShrank(const ArithVarVec& drop);
180 // WitnessImprovement focusDownToJust(ArithVar v);
183 void adjustFocusAndError(const UpdateInfo
& up
, const AVIntPairVec
& focusChanges
);
186 * This is the main simplex for DPLL(T) loop.
187 * It runs for at most maxIterations.
189 * Returns true iff it has found a conflict.
190 * d_conflictVariable will be set and the conflict for this row is reported.
192 bool searchForFeasibleSolution(uint32_t maxIterations
);
194 bool initialProcessSignals(){
195 TimerStat
&timer
= d_statistics
.d_initialSignalsTime
;
196 IntStat
& conflictStat
= d_statistics
.d_initialConflicts
;
197 return standardProcessSignals(timer
, conflictStat
);
202 DenseSet d_qeInUAndNotInSoi
;
203 ArithVarVec d_qeConflict
;
204 ArithVarVec d_qeGreedyOrder
;
207 uint32_t quickExplainRec(uint32_t cEnd
, uint32_t uEnd
);
208 void qeAddRange(uint32_t begin
, uint32_t end
);
209 void qeRemoveRange(uint32_t begin
, uint32_t end
);
210 void qeSwapRange(uint32_t N
, uint32_t r
, uint32_t s
);
212 unsigned trySet(const ArithVarVec
& set
);
213 unsigned tryAllSubsets(const ArithVarVec
& set
, unsigned depth
, ArithVarVec
& tmp
);
215 /** These fields are designed to be accessible to TheoryArith methods. */
218 TimerStat d_initialSignalsTime
;
219 IntStat d_initialConflicts
;
221 IntStat d_soiFoundUnsat
;
222 IntStat d_soiFoundSat
;
225 IntStat d_soiConflicts
;
226 IntStat d_hasToBeMinimal
;
227 IntStat d_maybeNotMinimal
;
229 TimerStat d_soiTimer
;
230 TimerStat d_soiFocusConstructionTimer
;
231 TimerStat d_soiConflictMinimization
;
232 TimerStat d_selectUpdateForSOI
;
234 ReferenceStat
<uint32_t> d_finalCheckPivotCounter
;
236 Statistics(uint32_t& pivots
);
239 };/* class FCSimplexDecisionProcedure */
241 }/* CVC4::theory::arith namespace */
242 }/* CVC4::theory namespace */
243 }/* CVC4 namespace */