GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/soi_simplex.h Lines: 1 16 6.3 %
Date: 2021-03-23 Branches: 0 10 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file soi_simplex.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
11
 **
12
 ** \brief This is an implementation of the Simplex Module for the Simplex for
13
 ** DPLL(T) decision procedure.
14
 **
15
 ** This implements the Simplex module for the Simpelx for DPLL(T) decision
16
 ** procedure.
17
 ** See the Simplex for DPLL(T) technical report for more background.(citation?)
18
 ** This shares with the theory a Tableau, and a PartialModel that:
19
 **  - satisfies the equalities in the Tableau, and
20
 **  - the assignment for the non-basic variables satisfies their bounds.
21
 ** This is required to either produce a conflict or satisifying PartialModel.
22
 ** Further, we require being told when a basic variable updates its value.
23
 **
24
 ** During the Simplex search we maintain a queue of variables.
25
 ** The queue is required to contain all of the basic variables that voilate
26
 ** their bounds.
27
 ** As elimination from the queue is more efficient to be done lazily,
28
 ** we do not maintain that the queue of variables needs to be only basic
29
 ** variables or only variables that satisfy their bounds.
30
 **
31
 ** The simplex procedure roughly follows Alberto's thesis. (citation?)
32
 ** There is one round of selecting using a heuristic pivoting rule.
33
 ** (See PreferenceFunction Documentation for the available options.)
34
 ** The non-basic variable is the one that appears in the fewest pivots.
35
 ** (Bruno says that Leonardo invented this first.)
36
 ** After this, Bland's pivot rule is invoked.
37
 **
38
 ** During this proccess, we periodically inspect the queue of variables to
39
 ** 1) remove now extraneous extries,
40
 ** 2) detect conflicts that are "waiting" on the queue but may not be detected
41
 **    by the current queue heuristics, and
42
 ** 3) detect multiple conflicts.
43
 **
44
 ** Conflicts are greedily slackened to use the weakest bounds that still
45
 ** produce the conflict.
46
 **
47
 ** Extra things tracked atm: (Subject to change at Tim's whims)
48
 ** - A superset of all of the newly pivoted variables.
49
 ** - A queue of additional conflicts that were discovered by Simplex.
50
 **   These are theory valid and are currently turned into lemmas
51
 **/
52
53
#include "cvc4_private.h"
54
55
#pragma once
56
57
#include "theory/arith/linear_equality.h"
58
#include "theory/arith/simplex.h"
59
#include "theory/arith/simplex_update.h"
60
#include "util/dense_map.h"
61
#include "util/statistics_registry.h"
62
63
namespace CVC4 {
64
namespace theory {
65
namespace arith {
66
67
8994
class SumOfInfeasibilitiesSPD : public SimplexDecisionProcedure {
68
public:
69
  SumOfInfeasibilitiesSPD(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc);
70
71
  Result::Sat findModel(bool exactResult) override;
72
73
  // other error variables are dropping
74
  WitnessImprovement dualLikeImproveError(ArithVar evar);
75
  WitnessImprovement primalImproveError(ArithVar evar);
76
77
private:
78
  /** The current sum of infeasibilities variable. */
79
  ArithVar d_soiVar;
80
81
  // dual like
82
  // - found conflict
83
  // - satisfied error set
84
  Result::Sat sumOfInfeasibilities();
85
86
  // static const uint32_t PENALTY = 4;
87
  // DenseMultiset d_scores;
88
  // void decreasePenalties(){ d_scores.removeOneOfEverything(); }
89
  // uint32_t penalty(ArithVar x) const { return d_scores.count(x); }
90
  // void setPenalty(ArithVar x, WitnessImprovement w){
91
  //   if(improvement(w)){
92
  //     if(d_scores.count(x) > 0){
93
  //       d_scores.removeAll(x);
94
  //     }
95
  //   }else{
96
  //     d_scores.setCount(x, PENALTY);
97
  //   }
98
  // }
99
100
  int32_t d_pivotBudget;
101
  // enum PivotImprovement {
102
  //   ErrorDropped,
103
  //   NonDegenerate,
104
  //   HeuristicDegenerate,
105
  //   BlandsDegenerate
106
  // };
107
108
  WitnessImprovement d_prevWitnessImprovement;
109
  uint32_t d_witnessImprovementInARow;
110
111
  uint32_t degeneratePivotsInARow() const;
112
113
  static const uint32_t s_focusThreshold = 6;
114
  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnLeaving = 100;
115
  static const uint32_t s_maxDegeneratePivotsBeforeBlandsOnEntering = 10;
116
117
  DenseMap<uint32_t> d_leavingCountSinceImprovement;
118
  void increaseLeavingCount(ArithVar x){
119
    if(!d_leavingCountSinceImprovement.isKey(x)){
120
      d_leavingCountSinceImprovement.set(x,1);
121
    }else{
122
      (d_leavingCountSinceImprovement.get(x))++;
123
    }
124
  }
125
  LinearEqualityModule::UpdatePreferenceFunction selectLeavingFunction(ArithVar x){
126
    bool useBlands = d_leavingCountSinceImprovement.isKey(x) &&
127
      d_leavingCountSinceImprovement[x] >= s_maxDegeneratePivotsBeforeBlandsOnEntering;
128
    if(useBlands) {
129
      return &LinearEqualityModule::preferWitness<false>;
130
    } else {
131
      return &LinearEqualityModule::preferWitness<true>;
132
    }
133
  }
134
135
  bool debugSOI(WitnessImprovement w, std::ostream& out, int instance) const;
136
137
  void debugPrintSignal(ArithVar updated) const;
138
139
  ArithVarVec d_sgnDisagreements;
140
141
  void logPivot(WitnessImprovement w);
142
143
  void updateAndSignal(const UpdateInfo& selected, WitnessImprovement w);
144
145
  UpdateInfo selectUpdate(LinearEqualityModule::UpdatePreferenceFunction upf,
146
                          LinearEqualityModule::VarPreferenceFunction bpf);
147
148
149
  // UpdateInfo selectUpdateForDualLike(ArithVar basic){
150
  //   TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForDualLike);
151
152
  //   LinearEqualityModule::UpdatePreferenceFunction upf =
153
  //     &LinearEqualityModule::preferWitness<true>;
154
  //   LinearEqualityModule::VarPreferenceFunction bpf =
155
  //     &LinearEqualityModule::minVarOrder;
156
  //   return selectPrimalUpdate(basic, upf, bpf);
157
  // }
158
159
  // UpdateInfo selectUpdateForPrimal(ArithVar basic, bool useBlands){
160
  //   TimerStat::CodeTimer codeTimer(d_statistics.d_selectUpdateForPrimal);
161
162
  //   LinearEqualityModule::UpdatePreferenceFunction upf = useBlands ?
163
  //     &LinearEqualityModule::preferWitness<false>:
164
  //     &LinearEqualityModule::preferWitness<true>;
165
166
  //   LinearEqualityModule::VarPreferenceFunction bpf = useBlands ?
167
  //     &LinearEqualityModule::minVarOrder :
168
  //     &LinearEqualityModule::minRowLength;
169
  //   bpf = &LinearEqualityModule::minVarOrder;
170
171
  //   return selectPrimalUpdate(basic, upf, bpf);
172
  // }
173
  // WitnessImprovement selectFocusImproving() ;
174
  WitnessImprovement soiRound();
175
  WitnessImprovement SOIConflict();
176
  std::vector< ArithVarVec > greedyConflictSubsets();
177
  bool generateSOIConflict(const ArithVarVec& subset);
178
179
  // WitnessImprovement focusUsingSignDisagreements(ArithVar basic);
180
  // WitnessImprovement focusDownToLastHalf();
181
  // WitnessImprovement adjustFocusShrank(const ArithVarVec& drop);
182
  // WitnessImprovement focusDownToJust(ArithVar v);
183
184
185
  void adjustFocusAndError(const UpdateInfo& up, const AVIntPairVec& focusChanges);
186
187
  /**
188
   * This is the main simplex for DPLL(T) loop.
189
   * It runs for at most maxIterations.
190
   *
191
   * Returns true iff it has found a conflict.
192
   * d_conflictVariable will be set and the conflict for this row is reported.
193
   */
194
  bool searchForFeasibleSolution(uint32_t maxIterations);
195
196
  bool initialProcessSignals(){
197
    TimerStat &timer = d_statistics.d_initialSignalsTime;
198
    IntStat& conflictStat  = d_statistics.d_initialConflicts;
199
    return standardProcessSignals(timer, conflictStat);
200
  }
201
202
  void quickExplain();
203
  DenseSet d_qeInSoi;
204
  DenseSet d_qeInUAndNotInSoi;
205
  ArithVarVec d_qeConflict;
206
  ArithVarVec d_qeGreedyOrder;
207
  sgn_table d_qeSgns;
208
209
  uint32_t quickExplainRec(uint32_t cEnd, uint32_t uEnd);
210
  void qeAddRange(uint32_t begin, uint32_t end);
211
  void qeRemoveRange(uint32_t begin, uint32_t end);
212
  void qeSwapRange(uint32_t N, uint32_t r, uint32_t s);
213
214
  unsigned trySet(const ArithVarVec& set);
215
  unsigned tryAllSubsets(const ArithVarVec& set, unsigned depth, ArithVarVec& tmp);
216
217
  /** These fields are designed to be accessible to TheoryArith methods. */
218
  class Statistics {
219
  public:
220
    TimerStat d_initialSignalsTime;
221
    IntStat d_initialConflicts;
222
223
    IntStat d_soiFoundUnsat;
224
    IntStat d_soiFoundSat;
225
    IntStat d_soiMissed;
226
227
    IntStat d_soiConflicts;
228
    IntStat d_hasToBeMinimal;
229
    IntStat d_maybeNotMinimal;
230
231
    TimerStat d_soiTimer;
232
    TimerStat d_soiFocusConstructionTimer;
233
    TimerStat d_soiConflictMinimization;
234
    TimerStat d_selectUpdateForSOI;
235
236
    ReferenceStat<uint32_t> d_finalCheckPivotCounter;
237
238
    Statistics(uint32_t& pivots);
239
    ~Statistics();
240
  } d_statistics;
241
};/* class FCSimplexDecisionProcedure */
242
243
}/* CVC4::theory::arith namespace */
244
}/* CVC4::theory namespace */
245
}/* CVC4 namespace */