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