GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/simplex_update.cpp Lines: 1 116 0.9 %
Date: 2021-03-22 Branches: 2 321 0.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file simplex_update.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King
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 implements UpdateInfo.
13
 **
14
 ** This implements the UpdateInfo.
15
 **/
16
17
#include "theory/arith/simplex_update.h"
18
#include "theory/arith/constraint.h"
19
20
using namespace std;
21
22
namespace CVC4 {
23
namespace theory {
24
namespace arith {
25
26
27
UpdateInfo::UpdateInfo():
28
  d_nonbasic(ARITHVAR_SENTINEL),
29
  d_nonbasicDirection(0),
30
  d_nonbasicDelta(),
31
  d_foundConflict(false),
32
  d_errorsChange(),
33
  d_focusDirection(),
34
  d_tableauCoefficient(),
35
  d_limiting(NullConstraint),
36
  d_witness(AntiProductive)
37
{}
38
39
UpdateInfo::UpdateInfo(ArithVar nb, int dir):
40
  d_nonbasic(nb),
41
  d_nonbasicDirection(dir),
42
  d_nonbasicDelta(),
43
  d_foundConflict(false),
44
  d_errorsChange(),
45
  d_focusDirection(),
46
  d_tableauCoefficient(),
47
  d_limiting(NullConstraint),
48
  d_witness(AntiProductive)
49
{
50
  Assert(dir == 1 || dir == -1);
51
}
52
53
UpdateInfo::UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP c):
54
  d_nonbasic(nb),
55
  d_nonbasicDirection(delta.sgn()),
56
  d_nonbasicDelta(delta),
57
  d_foundConflict(true),
58
  d_errorsChange(),
59
  d_focusDirection(),
60
  d_tableauCoefficient(&r),
61
  d_limiting(c),
62
  d_witness(ConflictFound)
63
{
64
  Assert(conflict);
65
}
66
67
UpdateInfo UpdateInfo::conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim){
68
  return UpdateInfo(true, nb, delta, r, lim);
69
}
70
71
void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
72
  d_limiting = NullConstraint;
73
  d_nonbasicDelta = delta;
74
  d_errorsChange = ec;
75
  d_focusDirection = f;
76
  d_tableauCoefficient.clear();
77
  updateWitness();
78
  Assert(unbounded());
79
  Assert(improvement(d_witness));
80
  Assert(!describesPivot());
81
  Assert(debugSgnAgreement());
82
}
83
void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
84
  d_limiting = c;
85
  d_nonbasicDelta = delta;
86
  d_errorsChange.clear();
87
  d_focusDirection = 1;
88
  d_tableauCoefficient.clear();
89
  updateWitness();
90
  Assert(!describesPivot());
91
  Assert(improvement(d_witness));
92
  Assert(debugSgnAgreement());
93
}
94
95
void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
96
  d_limiting = c;
97
  d_nonbasicDelta = delta;
98
  d_errorsChange.clear();
99
  d_focusDirection.clear();
100
  updateWitness();
101
  Assert(describesPivot());
102
  Assert(debugSgnAgreement());
103
}
104
105
void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec){
106
  d_limiting = c;
107
  d_nonbasicDelta = delta;
108
  d_errorsChange = ec;
109
  d_focusDirection.clear();
110
  d_tableauCoefficient = &r;
111
  updateWitness();
112
  Assert(describesPivot());
113
  Assert(debugSgnAgreement());
114
}
115
116
void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int ec, int fd){
117
  d_limiting = c;
118
  d_nonbasicDelta = delta;
119
  d_errorsChange = ec;
120
  d_focusDirection = fd;
121
  d_tableauCoefficient.clear();
122
  updateWitness();
123
  Assert(describesPivot() || improvement(d_witness));
124
  Assert(debugSgnAgreement());
125
}
126
127
void UpdateInfo::update(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec, int fd){
128
  d_limiting = c;
129
  d_nonbasicDelta = delta;
130
  d_errorsChange = ec;
131
  d_focusDirection = fd;
132
  d_tableauCoefficient = &r;
133
  updateWitness();
134
  Assert(describesPivot() || improvement(d_witness));
135
  Assert(debugSgnAgreement());
136
}
137
138
bool UpdateInfo::describesPivot() const {
139
  return !unbounded() && d_nonbasic != d_limiting->getVariable();
140
}
141
142
void UpdateInfo::output(std::ostream& out) const{
143
  out << "{UpdateInfo"
144
      << ", nb = " << d_nonbasic
145
      << ", dir = " << d_nonbasicDirection
146
      << ", delta = " << d_nonbasicDelta
147
      << ", conflict = " << d_foundConflict
148
      << ", errorChange = " << d_errorsChange
149
      << ", focusDir = " << d_focusDirection
150
      << ", witness = " << d_witness
151
      << ", limiting = " << d_limiting
152
      << "}";
153
}
154
155
ArithVar UpdateInfo::leaving() const{
156
  Assert(describesPivot());
157
158
  return d_limiting->getVariable();
159
}
160
161
std::ostream& operator<<(std::ostream& out, const UpdateInfo& up){
162
  up.output(out);
163
  return out;
164
}
165
166
167
std::ostream& operator<<(std::ostream& out,  WitnessImprovement w){
168
  switch(w){
169
  case ConflictFound:
170
    out << "ConflictFound"; break;
171
  case ErrorDropped:
172
    out << "ErrorDropped"; break;
173
  case FocusImproved:
174
    out << "FocusImproved"; break;
175
  case FocusShrank:
176
    out << "FocusShrank"; break;
177
  case Degenerate:
178
    out << "Degenerate"; break;
179
  case BlandsDegenerate:
180
    out << "BlandsDegenerate"; break;
181
  case HeuristicDegenerate:
182
    out << "HeuristicDegenerate"; break;
183
  case AntiProductive:
184
    out << "AntiProductive"; break;
185
  }
186
  return out;
187
}
188
189
}/* CVC4::theory::arith namespace */
190
}/* CVC4::theory namespace */
191
26676
}/* CVC4 namespace */