GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/simplex.cpp Lines: 58 162 35.8 %
Date: 2021-03-23 Branches: 82 590 13.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file simplex.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andres Noetzli
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/arith/simplex.h"
19
20
#include "base/output.h"
21
#include "options/arith_options.h"
22
#include "theory/arith/constraint.h"
23
#include "theory/arith/error_set.h"
24
#include "theory/arith/linear_equality.h"
25
#include "theory/arith/tableau.h"
26
27
using namespace std;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace arith {
32
33
34
35988
SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
35
  : d_pivots(0)
36
  , d_conflictVariables()
37
  , d_linEq(linEq)
38
35988
  , d_variables(d_linEq.getVariables())
39
35988
  , d_tableau(d_linEq.getTableau())
40
  , d_errorSet(errors)
41
  , d_numVariables(0)
42
  , d_conflictChannel(conflictChannel)
43
  , d_conflictBuilder(NULL)
44
  , d_arithVarMalloc(tvmalloc)
45
  , d_errorSize(0)
46
  , d_zero(0)
47
  , d_posOne(1)
48
107964
  , d_negOne(-1)
49
{
50
71976
  d_heuristicRule = options::arithErrorSelectionRule();
51
35988
  d_errorSet.setSelectionRule(d_heuristicRule);
52
35988
  d_conflictBuilder = new FarkasConflictBuilder();
53
35988
}
54
55
71952
SimplexDecisionProcedure::~SimplexDecisionProcedure(){
56
35976
  delete d_conflictBuilder;
57
35976
}
58
59
60
989575
bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
61
1979150
  TimerStat::CodeTimer codeTimer(timer);
62
989575
  Assert(d_conflictVariables.empty());
63
64
15955161
  while(d_errorSet.moreSignals()){
65
7482793
    ArithVar curr = d_errorSet.topSignal();
66
7482793
    if(d_tableau.isBasic(curr) && !d_variables.assignmentIsConsistent(curr)){
67
639181
      Assert(d_linEq.basicIsTracked(curr));
68
69
639181
      if(!d_conflictVariables.isMember(curr) && checkBasicForConflict(curr)){
70
71
133360
        Debug("recentlyViolated")
72
66680
          << "It worked? "
73
66680
          << conflicts.get()
74
66680
          << " " << curr
75
66680
          << " "  << checkBasicForConflict(curr) << endl;
76
66680
        reportConflict(curr);
77
66680
        ++conflicts;
78
      }
79
    }
80
    // Pop signal afterwards in case d_linEq.trackVariable(curr);
81
    // is needed for for the ErrorSet
82
7482793
    d_errorSet.popSignal();
83
  }
84
989575
  d_errorSize = d_errorSet.errorSize();
85
86
989575
  Assert(d_errorSet.noSignals());
87
1979150
  return !d_conflictVariables.empty();
88
}
89
90
/** Reports a conflict to on the output channel. */
91
66680
void SimplexDecisionProcedure::reportConflict(ArithVar basic){
92
66680
  Assert(!d_conflictVariables.isMember(basic));
93
66680
  Assert(checkBasicForConflict(basic));
94
95
66680
  ConstraintCP conflicted = generateConflictForBasic(basic);
96
66680
  Assert(conflicted != NullConstraint);
97
66680
  d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
98
99
66680
  d_conflictVariables.add(basic);
100
66680
}
101
102
66680
ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
103
66680
  Assert(d_tableau.isBasic(basic));
104
66680
  Assert(checkBasicForConflict(basic));
105
106
66680
  if(d_variables.cmpAssignmentLowerBound(basic) < 0){
107
37648
    Assert(d_linEq.nonbasicsAtUpperBounds(basic));
108
37648
    return d_linEq.generateConflictBelowLowerBound(basic, *d_conflictBuilder);
109
29032
  }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
110
29032
    Assert(d_linEq.nonbasicsAtLowerBounds(basic));
111
29032
    return d_linEq.generateConflictAboveUpperBound(basic, *d_conflictBuilder);
112
  }else{
113
    Unreachable();
114
    return NullConstraint;
115
  }
116
}
117
bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
118
  if(checkBasicForConflict(basic)){
119
    ConstraintCP conflicted = generateConflictForBasic(basic);
120
    d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
121
    return true;
122
  }else{
123
    return false;
124
  }
125
}
126
127
828675
bool SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic) const {
128
828675
  Assert(d_tableau.isBasic(basic));
129
828675
  Assert(d_linEq.basicIsTracked(basic));
130
131
828675
  if(d_variables.cmpAssignmentLowerBound(basic) < 0){
132
439855
    if(d_linEq.nonbasicsAtUpperBounds(basic)){
133
150592
      return true;
134
    }
135
388820
  }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
136
388820
    if(d_linEq.nonbasicsAtLowerBounds(basic)){
137
116128
      return true;
138
    }
139
  }
140
561955
  return false;
141
}
142
143
void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, ArithVar tmp){
144
  TimerStat::CodeTimer codeTimer(timer);
145
  Assert(tmp != ARITHVAR_SENTINEL);
146
  Assert(d_tableau.isBasic(tmp));
147
148
  RowIndex ri = d_tableau.basicToRowIndex(tmp);
149
  d_linEq.stopTrackingRowIndex(ri);
150
  d_tableau.removeBasicRow(tmp);
151
  releaseVariable(tmp);
152
}
153
154
void SimplexDecisionProcedure::shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped){
155
  TimerStat::CodeTimer codeTimer(timer);
156
  for(ArithVarVec::const_iterator i=dropped.begin(), i_end = dropped.end(); i != i_end; ++i){
157
    ArithVar back = *i;
158
159
    int focusSgn = d_errorSet.focusSgn(back);
160
    Rational chg(-focusSgn);
161
162
    d_linEq.substitutePlusTimesConstant(inf, back, chg);
163
  }
164
}
165
166
void SimplexDecisionProcedure::adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges){
167
  TimerStat::CodeTimer codeTimer(timer);
168
  for(AVIntPairVec::const_iterator i=focusChanges.begin(), i_end = focusChanges.end(); i != i_end; ++i){
169
    ArithVar v = (*i).first;
170
    int focusChange = (*i).second;
171
172
    Rational chg(focusChange);
173
    if(d_tableau.isBasic(v)){
174
      d_linEq.substitutePlusTimesConstant(inf, v, chg);
175
    }else{
176
      d_linEq.directlyAddToCoefficient(inf, v, chg);
177
    }
178
  }
179
}
180
181
void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
182
  AVIntPairVec justE;
183
  int sgn  = d_errorSet.getSgn(e);
184
  justE.push_back(make_pair(e, sgn));
185
  adjustInfeasFunc(timer, inf, justE);
186
}
187
188
void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
189
  AVIntPairVec justE;
190
  int opSgn  = -d_errorSet.getSgn(e);
191
  justE.push_back(make_pair(e, opSgn));
192
  adjustInfeasFunc(timer, inf, justE);
193
}
194
195
ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
196
  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;
197
198
  TimerStat::CodeTimer codeTimer(timer);
199
  Assert(!d_errorSet.focusEmpty());
200
  Assert(debugIsASet(set));
201
202
  ArithVar inf = requestVariable();
203
  Assert(inf != ARITHVAR_SENTINEL);
204
205
  std::vector<Rational> coeffs;
206
  std::vector<ArithVar> variables;
207
208
  for(ArithVarVec::const_iterator iter = set.begin(), iend = set.end(); iter != iend; ++iter){
209
    ArithVar e = *iter;
210
211
    Assert(d_tableau.isBasic(e));
212
    Assert(!d_variables.assignmentIsConsistent(e));
213
214
    int sgn = d_errorSet.getSgn(e);
215
    Assert(sgn == -1 || sgn == 1);
216
    const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
217
    coeffs.push_back(violatedCoeff);
218
    variables.push_back(e);
219
220
    Debug("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
221
222
  }
223
  d_tableau.addRow(inf, coeffs, variables);
224
  DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
225
  d_variables.setAssignment(inf, newAssignment);
226
227
  //d_linEq.trackVariable(inf);
228
  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
229
230
  Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
231
  Debug("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
232
  return inf;
233
}
234
235
ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer){
236
  ArithVarVec inError;
237
  d_errorSet.pushFocusInto(inError);
238
  return constructInfeasiblityFunction(timer, inError);
239
}
240
241
ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, ArithVar e){
242
  ArithVarVec justE;
243
  justE.push_back(e);
244
  return constructInfeasiblityFunction(timer, justE);
245
}
246
247
void SimplexDecisionProcedure::addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic){
248
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
249
  sgns[p].push_back(basic);
250
}
251
252
void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns, ArithVar basic, int norm){
253
  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
254
    const Tableau::Entry& entry = *i;
255
    ArithVar v = entry.getColVar();
256
    int sgn = (entry.getCoefficient().sgn());
257
    addSgn(sgns, v, norm * sgn, basic);
258
  }
259
}
260
261
ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside){
262
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
263
  sgn_table::const_iterator i = sgns.find(p);
264
265
  if(i != sgns.end()){
266
    const ArithVarVec& vec = (*i).second;
267
    for(ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end(); viter != vend; ++viter){
268
      ArithVar curr = *viter;
269
      if(inside == m.isMember(curr)){
270
        return curr;
271
      }
272
    }
273
  }
274
  return ARITHVAR_SENTINEL;
275
}
276
277
SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::find_sgns(const sgn_table& sgns, ArithVar col, int sgn){
278
  pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
279
  return sgns.find(p);
280
}
281
}/* CVC4::theory::arith namespace */
282
}/* CVC4::theory namespace */
283
26685
}/* CVC4 namespace */