GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/dual_simplex.cpp Lines: 112 123 91.1 %
Date: 2021-03-23 Branches: 224 586 38.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dual_simplex.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Aina Niemetz, Morgan Deters
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
#include "theory/arith/dual_simplex.h"
18
19
#include "base/output.h"
20
#include "options/arith_options.h"
21
#include "smt/smt_statistics_registry.h"
22
#include "theory/arith/constraint.h"
23
#include "theory/arith/error_set.h"
24
#include "theory/arith/linear_equality.h"
25
26
27
using namespace std;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace arith {
32
33
8997
DualSimplexDecisionProcedure::DualSimplexDecisionProcedure(LinearEqualityModule& linEq, ErrorSet& errors, RaiseConflict conflictChannel, TempVarMalloc tvmalloc)
34
  : SimplexDecisionProcedure(linEq, errors, conflictChannel, tvmalloc)
35
  , d_pivotsInRound()
36
8997
  , d_statistics(d_pivots)
37
8997
{ }
38
39
8997
DualSimplexDecisionProcedure::Statistics::Statistics(uint32_t& pivots):
40
  d_statUpdateConflicts("theory::arith::dual::UpdateConflicts", 0),
41
  d_processSignalsTime("theory::arith::dual::findConflictOnTheQueueTime"),
42
  d_simplexConflicts("theory::arith::dual::simplexConflicts",0),
43
  d_recentViolationCatches("theory::arith::dual::recentViolationCatches",0),
44
  d_searchTime("theory::arith::dual::searchTime"),
45
8997
  d_finalCheckPivotCounter("theory::arith::dual::lastPivots", pivots)
46
{
47
8997
  smtStatisticsRegistry()->registerStat(&d_statUpdateConflicts);
48
8997
  smtStatisticsRegistry()->registerStat(&d_processSignalsTime);
49
8997
  smtStatisticsRegistry()->registerStat(&d_simplexConflicts);
50
8997
  smtStatisticsRegistry()->registerStat(&d_recentViolationCatches);
51
8997
  smtStatisticsRegistry()->registerStat(&d_searchTime);
52
8997
  smtStatisticsRegistry()->registerStat(&d_finalCheckPivotCounter);
53
8997
}
54
55
17988
DualSimplexDecisionProcedure::Statistics::~Statistics(){
56
8994
  smtStatisticsRegistry()->unregisterStat(&d_statUpdateConflicts);
57
8994
  smtStatisticsRegistry()->unregisterStat(&d_processSignalsTime);
58
8994
  smtStatisticsRegistry()->unregisterStat(&d_simplexConflicts);
59
8994
  smtStatisticsRegistry()->unregisterStat(&d_recentViolationCatches);
60
8994
  smtStatisticsRegistry()->unregisterStat(&d_searchTime);
61
8994
  smtStatisticsRegistry()->unregisterStat(&d_finalCheckPivotCounter);
62
8994
}
63
64
1769430
Result::Sat DualSimplexDecisionProcedure::dualFindModel(bool exactResult){
65
1769430
  Assert(d_conflictVariables.empty());
66
67
  static thread_local unsigned int instance = 0;
68
1769430
  instance = instance + 1;
69
1769430
  d_pivots = 0;
70
71
1769430
  if(d_errorSet.errorEmpty() && !d_errorSet.moreSignals()){
72
974782
    Debug("arith::findModel") << "dualFindModel("<< instance <<") trivial" << endl;
73
974782
    return Result::SAT;
74
  }
75
76
  // We need to reduce this because of
77
794648
  d_errorSet.reduceToSignals();
78
794648
  d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
79
80
794648
  if(processSignals()){
81
31352
    d_conflictVariables.purge();
82
83
31352
    Debug("arith::findModel") << "dualFindModel("<< instance <<") early conflict" << endl;
84
31352
    return Result::UNSAT;
85
763296
  }else if(d_errorSet.errorEmpty()){
86
675959
    Debug("arith::findModel") << "dualFindModel("<< instance <<") fixed itself" << endl;
87
675959
    Assert(!d_errorSet.moreSignals());
88
675959
    return Result::SAT;
89
  }
90
91
87337
  Debug("arith::findModel") << "dualFindModel(" << instance <<") start non-trivial" << endl;
92
93
87337
  Result::Sat result = Result::SAT_UNKNOWN;
94
95
  static const bool verbose = false;
96
87337
  exactResult |= options::arithStandardCheckVarOrderPivots() < 0;
97
98
99
174674
  uint32_t checkPeriod = options::arithSimplexCheckPeriod();
100
87337
  if(result == Result::SAT_UNKNOWN){
101
174674
    uint32_t numDifferencePivots = options::arithHeuristicPivots() < 0 ?
102
174674
      d_numVariables + 1 : options::arithHeuristicPivots();
103
    // The signed to unsigned conversion is safe.
104
87337
    if(numDifferencePivots > 0){
105
106
75608
      d_errorSet.setSelectionRule(d_heuristicRule);
107
75608
      if(searchForFeasibleSolution(numDifferencePivots)){
108
10697
        result = Result::UNSAT;
109
      }
110
    }
111
112
    if (verbose && numDifferencePivots > 0)
113
    {
114
      if (result == Result::UNSAT)
115
      {
116
        CVC4Message() << "diff order found unsat" << endl;
117
      }
118
      else if (d_errorSet.errorEmpty())
119
      {
120
        CVC4Message() << "diff order found model" << endl;
121
      }
122
      else
123
      {
124
        CVC4Message() << "diff order missed" << endl;
125
      }
126
    }
127
  }
128
87337
  Assert(!d_errorSet.moreSignals());
129
130
87337
  if(!d_errorSet.errorEmpty() && result != Result::UNSAT){
131
13157
    if(exactResult){
132
1205
      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
133
3623
      while(!d_errorSet.errorEmpty() && result != Result::UNSAT){
134
1209
        Assert(checkPeriod > 0);
135
1209
        if(searchForFeasibleSolution(checkPeriod)){
136
109
          result = Result::UNSAT;
137
        }
138
      }
139
11952
    }else if( options::arithStandardCheckVarOrderPivots() > 0){
140
11952
      d_errorSet.setSelectionRule(options::ErrorSelectionRule::VAR_ORDER);
141
11952
      if(searchForFeasibleSolution(options::arithStandardCheckVarOrderPivots())){
142
3300
        result = Result::UNSAT;
143
      }
144
      if (verbose)
145
      {
146
        if (result == Result::UNSAT)
147
        {
148
          CVC4Message() << "restricted var order found unsat" << endl;
149
        }
150
        else if (d_errorSet.errorEmpty())
151
        {
152
          CVC4Message() << "restricted var order found model" << endl;
153
        }
154
        else
155
        {
156
          CVC4Message() << "restricted var order missed" << endl;
157
        }
158
      }
159
    }
160
  }
161
162
87337
  Assert(!d_errorSet.moreSignals());
163
87337
  if(result == Result::SAT_UNKNOWN && d_errorSet.errorEmpty()){
164
73231
    result = Result::SAT;
165
  }
166
167
87337
  d_pivotsInRound.purge();
168
  // ensure that the conflict variable is still in the queue.
169
87337
  d_conflictVariables.purge();
170
171
87337
  Debug("arith::findModel") << "end findModel() " << instance << " " << result <<  endl;
172
173
87337
  return result;
174
}
175
176
//corresponds to Check() in dM06
177
//template <SimplexDecisionProcedure::PreferenceFunction pf>
178
88769
bool DualSimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
179
177538
  TimerStat::CodeTimer codeTimer(d_statistics.d_searchTime);
180
181
88769
  Debug("arith") << "searchForFeasibleSolution" << endl;
182
88769
  Assert(remainingIterations > 0);
183
184
450411
  while(remainingIterations > 0 && !d_errorSet.focusEmpty()){
185
194927
    if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
186
194927
    Assert(d_conflictVariables.empty());
187
194927
    ArithVar x_i = d_errorSet.topFocusVariable();
188
189
194927
    Debug("arith::update::select") << "selectSmallestInconsistentVar()=" << x_i << endl;
190
194927
    if(x_i == ARITHVAR_SENTINEL){
191
      Debug("arith::update") << "No inconsistent variables" << endl;
192
14106
      return false; //sat
193
    }
194
195
194927
    --remainingIterations;
196
197
194927
    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  options::arithPivotThreshold();
198
194927
    if(!useVarOrderPivot){
199
194809
      d_pivotsInRound.add(x_i);
200
    }
201
202
203
389854
    Debug("arith::update")
204
389854
      << "pivots in rounds: " <<  d_pivotsInRound.count(x_i)
205
194927
      << " use " << useVarOrderPivot
206
389854
      << " threshold " << options::arithPivotThreshold()
207
194927
      << endl;
208
209
194927
    LinearEqualityModule::VarPreferenceFunction pf = useVarOrderPivot ?
210
      &LinearEqualityModule::minVarOrder : &LinearEqualityModule::minBoundAndColLength;
211
212
    //DeltaRational beta_i = d_variables.getAssignment(x_i);
213
194927
    ArithVar x_j = ARITHVAR_SENTINEL;
214
215
194927
    int32_t prevErrorSize CVC4_UNUSED = d_errorSet.errorSize();
216
217
194927
    if(d_variables.cmpAssignmentLowerBound(x_i) < 0 ){
218
106378
      x_j = d_linEq.selectSlackUpperBound(x_i, pf);
219
106378
      if(x_j == ARITHVAR_SENTINEL ){
220
        Unreachable();
221
        // ++(d_statistics.d_statUpdateConflicts);
222
        // reportConflict(x_i);
223
        // ++(d_statistics.d_simplexConflicts);
224
        // Node conflict = d_linEq.generateConflictBelowLowerBound(x_i); //unsat
225
        // d_conflictVariable = x_i;
226
        // reportConflict(conflict);
227
        // return true;
228
      }else{
229
106378
        const DeltaRational& l_i = d_variables.getLowerBound(x_i);
230
106378
        d_linEq.pivotAndUpdate(x_i, x_j, l_i);
231
      }
232
88549
    }else if(d_variables.cmpAssignmentUpperBound(x_i) > 0){
233
88549
      x_j = d_linEq.selectSlackLowerBound(x_i, pf);
234
88549
      if(x_j == ARITHVAR_SENTINEL ){
235
        Unreachable();
236
        // ++(d_statistics.d_statUpdateConflicts);
237
        // reportConflict(x_i);
238
        // ++(d_statistics.d_simplexConflicts);
239
        // Node conflict = d_linEq.generateConflictAboveUpperBound(x_i); //unsat
240
        // d_conflictVariable = x_i;
241
        // reportConflict(conflict);
242
        // return true;
243
      }else{
244
88549
        const DeltaRational& u_i = d_variables.getUpperBound(x_i);
245
88549
        d_linEq.pivotAndUpdate(x_i, x_j, u_i);
246
      }
247
    }
248
194927
    Assert(x_j != ARITHVAR_SENTINEL);
249
250
194927
    bool conflict = processSignals();
251
194927
    int32_t currErrorSize CVC4_UNUSED = d_errorSet.errorSize();
252
194927
    d_pivots++;
253
254
194927
    if(Debug.isOn("arith::dual")){
255
      Debug("arith::dual")
256
        << "#" << d_pivots
257
        << " c" << conflict
258
        << " d" << (prevErrorSize - currErrorSize)
259
        << " f"  << d_errorSet.inError(x_j)
260
        << " h" << d_conflictVariables.isMember(x_j)
261
        << " " << x_i << "->" << x_j
262
        << endl;
263
    }
264
265
194927
    if(conflict){
266
14106
      return true;
267
    }
268
  }
269
74663
  Assert(!d_errorSet.focusEmpty() || d_errorSet.errorEmpty());
270
74663
  Assert(remainingIterations == 0 || d_errorSet.focusEmpty());
271
74663
  Assert(d_errorSet.noSignals());
272
273
74663
  return false;
274
}
275
276
}/* CVC4::theory::arith namespace */
277
}/* CVC4::theory namespace */
278
26685
}/* CVC4 namespace */