Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Andres Noetzli, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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.
11 : : * ****************************************************************************
12 : : *
13 : : * This implements the UpdateInfo.
14 : : */
15 : :
16 : : #include "theory/arith/linear/simplex_update.h"
17 : :
18 : : #include "theory/arith/linear/constraint.h"
19 : :
20 : : using namespace std;
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace arith::linear {
25 : :
26 : : /*
27 : : * Generates a string representation of std::optional and inserts it into a
28 : : * stream.
29 : : *
30 : : * Note: We define this function here in the cvc5::internal::theory::arith namespace,
31 : : * because it would otherwise not be found for std::optional<int>. This is due
32 : : * to the argument-dependent lookup rules.
33 : : *
34 : : * @param out The stream
35 : : * @param m The value
36 : : * @return The stream
37 : : */
38 : 0 : std::ostream& operator<<(std::ostream& out, const std::optional<int>& m)
39 : : {
40 : 0 : return cvc5::internal::operator<<(out, m);
41 : : }
42 : :
43 : 33296 : UpdateInfo::UpdateInfo():
44 : : d_nonbasic(ARITHVAR_SENTINEL),
45 : : d_nonbasicDirection(0),
46 : : d_nonbasicDelta(),
47 : : d_foundConflict(false),
48 : : d_errorsChange(),
49 : : d_focusDirection(),
50 : : d_tableauCoefficient(),
51 : : d_limiting(NullConstraint),
52 : 33296 : d_witness(AntiProductive)
53 : 33296 : {}
54 : :
55 : 77345 : UpdateInfo::UpdateInfo(ArithVar nb, int dir):
56 : : d_nonbasic(nb),
57 : : d_nonbasicDirection(dir),
58 : : d_nonbasicDelta(),
59 : : d_foundConflict(false),
60 : : d_errorsChange(),
61 : : d_focusDirection(),
62 : : d_tableauCoefficient(),
63 : : d_limiting(NullConstraint),
64 : 77345 : d_witness(AntiProductive)
65 : : {
66 [ + + ][ - + ]: 77345 : Assert(dir == 1 || dir == -1);
[ - + ][ - - ]
67 : 77345 : }
68 : :
69 : 37 : UpdateInfo::UpdateInfo(bool conflict, ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP c):
70 : : d_nonbasic(nb),
71 : 74 : d_nonbasicDirection(delta.sgn()),
72 : : d_nonbasicDelta(delta),
73 : : d_foundConflict(true),
74 : : d_errorsChange(),
75 : : d_focusDirection(),
76 : 0 : d_tableauCoefficient(&r),
77 : : d_limiting(c),
78 : 37 : d_witness(ConflictFound)
79 : : {
80 [ - + ][ - + ]: 37 : Assert(conflict);
[ - - ]
81 : 37 : }
82 : :
83 : 37 : UpdateInfo UpdateInfo::conflict(ArithVar nb, const DeltaRational& delta, const Rational& r, ConstraintP lim){
84 : 37 : return UpdateInfo(true, nb, delta, r, lim);
85 : : }
86 : :
87 : 0 : void UpdateInfo::updateUnbounded(const DeltaRational& delta, int ec, int f){
88 : 0 : d_limiting = NullConstraint;
89 : 0 : d_nonbasicDelta = delta;
90 : 0 : d_errorsChange = ec;
91 : 0 : d_focusDirection = f;
92 : 0 : d_tableauCoefficient.reset();
93 : 0 : updateWitness();
94 : 0 : Assert(unbounded());
95 : 0 : Assert(improvement(d_witness));
96 : 0 : Assert(!describesPivot());
97 : 0 : Assert(debugSgnAgreement());
98 : 0 : }
99 : 0 : void UpdateInfo::updatePureFocus(const DeltaRational& delta, ConstraintP c){
100 : 0 : d_limiting = c;
101 : 0 : d_nonbasicDelta = delta;
102 : 0 : d_errorsChange.reset();
103 : 0 : d_focusDirection = 1;
104 : 0 : d_tableauCoefficient.reset();
105 : 0 : updateWitness();
106 : 0 : Assert(!describesPivot());
107 : 0 : Assert(improvement(d_witness));
108 : 0 : Assert(debugSgnAgreement());
109 : 0 : }
110 : :
111 : 0 : void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c){
112 : 0 : d_limiting = c;
113 : 0 : d_nonbasicDelta = delta;
114 : 0 : d_errorsChange.reset();
115 : 0 : d_focusDirection.reset();
116 : 0 : updateWitness();
117 : 0 : Assert(describesPivot());
118 : 0 : Assert(debugSgnAgreement());
119 : 0 : }
120 : :
121 : 0 : void UpdateInfo::updatePivot(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec){
122 : 0 : d_limiting = c;
123 : 0 : d_nonbasicDelta = delta;
124 : 0 : d_errorsChange = ec;
125 : 0 : d_focusDirection.reset();
126 : 0 : d_tableauCoefficient = &r;
127 : 0 : updateWitness();
128 : 0 : Assert(describesPivot());
129 : 0 : Assert(debugSgnAgreement());
130 : 0 : }
131 : :
132 : 974 : void UpdateInfo::witnessedUpdate(const DeltaRational& delta, ConstraintP c, int ec, int fd){
133 : 974 : d_limiting = c;
134 : 974 : d_nonbasicDelta = delta;
135 : 974 : d_errorsChange = ec;
136 : 974 : d_focusDirection = fd;
137 : 974 : d_tableauCoefficient.reset();
138 : 974 : updateWitness();
139 [ + - ][ - + ]: 974 : Assert(describesPivot() || improvement(d_witness));
[ - + ][ - - ]
140 [ - + ][ - + ]: 974 : Assert(debugSgnAgreement());
[ - - ]
141 : 974 : }
142 : :
143 : 76371 : void UpdateInfo::update(const DeltaRational& delta, const Rational& r, ConstraintP c, int ec, int fd){
144 : 76371 : d_limiting = c;
145 : 76371 : d_nonbasicDelta = delta;
146 : 76371 : d_errorsChange = ec;
147 : 76371 : d_focusDirection = fd;
148 : 76371 : d_tableauCoefficient = &r;
149 : 76371 : updateWitness();
150 [ - + ][ - - ]: 76371 : Assert(describesPivot() || improvement(d_witness));
[ - + ][ - - ]
151 [ - + ][ - + ]: 76371 : Assert(debugSgnAgreement());
[ - - ]
152 : 76371 : }
153 : :
154 : 978905 : bool UpdateInfo::describesPivot() const {
155 [ + - ][ + + ]: 978905 : return !unbounded() && d_nonbasic != d_limiting->getVariable();
156 : : }
157 : :
158 : 0 : void UpdateInfo::output(std::ostream& out) const{
159 : : out << "{UpdateInfo"
160 : 0 : << ", nb = " << d_nonbasic
161 : 0 : << ", dir = " << d_nonbasicDirection
162 : 0 : << ", delta = " << d_nonbasicDelta
163 : 0 : << ", conflict = " << d_foundConflict
164 : 0 : << ", errorChange = " << d_errorsChange
165 : 0 : << ", focusDir = " << d_focusDirection
166 : 0 : << ", witness = " << d_witness
167 : 0 : << ", limiting = " << d_limiting
168 : 0 : << "}";
169 : 0 : }
170 : :
171 : 344758 : ArithVar UpdateInfo::leaving() const{
172 [ - + ][ - + ]: 344758 : Assert(describesPivot());
[ - - ]
173 : :
174 : 344758 : return d_limiting->getVariable();
175 : : }
176 : :
177 : 0 : std::ostream& operator<<(std::ostream& out, const UpdateInfo& up){
178 : 0 : up.output(out);
179 : 0 : return out;
180 : : }
181 : :
182 : :
183 : 0 : std::ostream& operator<<(std::ostream& out, WitnessImprovement w){
184 [ - - ][ - - ]: 0 : switch(w){
[ - - ][ - - ]
[ - ]
185 : 0 : case ConflictFound:
186 : 0 : out << "ConflictFound"; break;
187 : 0 : case ErrorDropped:
188 : 0 : out << "ErrorDropped"; break;
189 : 0 : case FocusImproved:
190 : 0 : out << "FocusImproved"; break;
191 : 0 : case FocusShrank:
192 : 0 : out << "FocusShrank"; break;
193 : 0 : case Degenerate:
194 : 0 : out << "Degenerate"; break;
195 : 0 : case BlandsDegenerate:
196 : 0 : out << "BlandsDegenerate"; break;
197 : 0 : case HeuristicDegenerate:
198 : 0 : out << "HeuristicDegenerate"; break;
199 : 0 : case AntiProductive:
200 : 0 : out << "AntiProductive"; break;
201 : : }
202 : 0 : return out;
203 : : }
204 : :
205 : : } // namespace arith
206 : : } // namespace theory
207 : : } // namespace cvc5::internal
|
