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 is an implementation of the Simplex Module for the Simplex for
11 : : * DPLL(T) decision procedure.
12 : : */
13 : :
14 : : #include "theory/arith/linear/simplex.h"
15 : :
16 : : #include "base/output.h"
17 : : #include "options/arith_options.h"
18 : : #include "options/smt_options.h"
19 : : #include "smt/env.h"
20 : : #include "theory/arith/linear/constraint.h"
21 : : #include "theory/arith/linear/error_set.h"
22 : : #include "theory/arith/linear/linear_equality.h"
23 : : #include "theory/arith/linear/tableau.h"
24 : : #include "util/statistics_value.h"
25 : :
26 : : using namespace std;
27 : :
28 : : namespace cvc5::internal {
29 : : namespace theory {
30 : : namespace arith::linear {
31 : :
32 : 205084 : SimplexDecisionProcedure::SimplexDecisionProcedure(
33 : : Env& env,
34 : : LinearEqualityModule& linEq,
35 : : ErrorSet& errors,
36 : : RaiseConflict conflictChannel,
37 : 205084 : TempVarMalloc tvmalloc)
38 : : : EnvObj(env),
39 : 205084 : d_pivots(0),
40 : 205084 : d_conflictVariables(),
41 : 205084 : d_linEq(linEq),
42 : 205084 : d_variables(d_linEq.getVariables()),
43 : 205084 : d_tableau(d_linEq.getTableau()),
44 : 205084 : d_errorSet(errors),
45 : 205084 : d_numVariables(0),
46 : 205084 : d_conflictChannel(conflictChannel),
47 : 205084 : d_conflictBuilder(nullptr),
48 : 205084 : d_arithVarMalloc(tvmalloc),
49 : 205084 : d_errorSize(0),
50 : 205084 : d_zero(0),
51 : 205084 : d_posOne(1),
52 : 410168 : d_negOne(-1)
53 : : {
54 : 205084 : d_heuristicRule = options().arith.arithErrorSelectionRule;
55 : 205084 : d_errorSet.setSelectionRule(d_heuristicRule);
56 : 205084 : d_conflictBuilder = new FarkasConflictBuilder(options().smt.produceProofs);
57 : 205084 : }
58 : :
59 : 814768 : SimplexDecisionProcedure::~SimplexDecisionProcedure()
60 : : {
61 [ + - ]: 203692 : delete d_conflictBuilder;
62 : 203692 : }
63 : :
64 : 1770592 : bool SimplexDecisionProcedure::standardProcessSignals(TimerStat& timer,
65 : : IntStat& conflicts)
66 : : {
67 : 1770592 : TimerStat::CodeTimer codeTimer(timer);
68 [ - + ][ - + ]: 1770592 : Assert(d_conflictVariables.empty());
[ - - ]
69 : :
70 [ + + ]: 15156848 : while (d_errorSet.moreSignals())
71 : : {
72 : 13386256 : ArithVar curr = d_errorSet.topSignal();
73 [ + + ][ + + ]: 13386256 : if (d_tableau.isBasic(curr) && !d_variables.assignmentIsConsistent(curr))
[ + + ]
74 : : {
75 [ - + ][ - + ]: 1074072 : Assert(d_linEq.basicIsTracked(curr));
[ - - ]
76 : :
77 [ + + ][ + + ]: 1074072 : if (!d_conflictVariables.isMember(curr) && checkBasicForConflict(curr))
[ + + ]
78 : : {
79 [ + - ]: 204404 : Trace("recentlyViolated")
80 : 0 : << "It worked? " << conflicts.get() << " " << curr << " "
81 : 102202 : << checkBasicForConflict(curr) << endl;
82 : 102202 : reportConflict(curr);
83 : 102202 : ++conflicts;
84 : : }
85 : : }
86 : : // Pop signal afterwards in case d_linEq.trackVariable(curr);
87 : : // is needed for for the ErrorSet
88 : 13386256 : d_errorSet.popSignal();
89 : : }
90 : 1770592 : d_errorSize = d_errorSet.errorSize();
91 : :
92 [ - + ][ - + ]: 1770592 : Assert(d_errorSet.noSignals());
[ - - ]
93 : 3541184 : return !d_conflictVariables.empty();
94 : 1770592 : }
95 : :
96 : : /** Reports a conflict to on the output channel. */
97 : 103262 : void SimplexDecisionProcedure::reportConflict(ArithVar basic)
98 : : {
99 [ - + ][ - + ]: 103262 : Assert(!d_conflictVariables.isMember(basic));
[ - - ]
100 [ - + ][ - + ]: 103262 : Assert(checkBasicForConflict(basic));
[ - - ]
101 : :
102 : 103262 : ConstraintCP conflicted = generateConflictForBasic(basic);
103 [ - + ][ - + ]: 103262 : Assert(conflicted != NullConstraint);
[ - - ]
104 : 103262 : d_conflictChannel.raiseConflict(conflicted, InferenceId::ARITH_CONF_SIMPLEX);
105 : :
106 : 103262 : d_conflictVariables.add(basic);
107 : 103262 : }
108 : :
109 : 103262 : ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(
110 : : ArithVar basic) const
111 : : {
112 [ - + ][ - + ]: 103262 : Assert(d_tableau.isBasic(basic));
[ - - ]
113 [ - + ][ - + ]: 103262 : Assert(checkBasicForConflict(basic));
[ - - ]
114 : :
115 [ + + ]: 103262 : if (d_variables.cmpAssignmentLowerBound(basic) < 0)
116 : : {
117 [ - + ][ - + ]: 52615 : Assert(d_linEq.nonbasicsAtUpperBounds(basic));
[ - - ]
118 : 52615 : return d_linEq.generateConflictBelowLowerBound(
119 : 105230 : nodeManager(), basic, *d_conflictBuilder);
120 : : }
121 [ + - ]: 50647 : else if (d_variables.cmpAssignmentUpperBound(basic) > 0)
122 : : {
123 [ - + ][ - + ]: 50647 : Assert(d_linEq.nonbasicsAtLowerBounds(basic));
[ - - ]
124 : 50647 : return d_linEq.generateConflictAboveUpperBound(
125 : 101294 : nodeManager(), basic, *d_conflictBuilder);
126 : : }
127 : : else
128 : : {
129 : 0 : Unreachable();
130 : : return NullConstraint;
131 : : }
132 : : }
133 : 0 : bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(
134 : : ArithVar basic) const
135 : : {
136 [ - - ]: 0 : if (checkBasicForConflict(basic))
137 : : {
138 : 0 : ConstraintCP conflicted = generateConflictForBasic(basic);
139 : 0 : d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
140 : 0 : return true;
141 : : }
142 : : else
143 : : {
144 : 0 : return false;
145 : : }
146 : : }
147 : :
148 : 1268440 : bool SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic) const
149 : : {
150 [ - + ][ - + ]: 1268440 : Assert(d_tableau.isBasic(basic));
[ - - ]
151 [ - + ][ - + ]: 1268440 : Assert(d_linEq.basicIsTracked(basic));
[ - - ]
152 : :
153 [ + + ]: 1268440 : if (d_variables.cmpAssignmentLowerBound(basic) < 0)
154 : : {
155 [ + + ]: 637771 : if (d_linEq.nonbasicsAtUpperBounds(basic))
156 : : {
157 : 157845 : return true;
158 : : }
159 : : }
160 [ + - ]: 630669 : else if (d_variables.cmpAssignmentUpperBound(basic) > 0)
161 : : {
162 [ + + ]: 630669 : if (d_linEq.nonbasicsAtLowerBounds(basic))
163 : : {
164 : 151941 : return true;
165 : : }
166 : : }
167 : 958654 : return false;
168 : : }
169 : :
170 : 4096 : void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer,
171 : : ArithVar tmp)
172 : : {
173 : 4096 : TimerStat::CodeTimer codeTimer(timer);
174 [ - + ][ - + ]: 4096 : Assert(tmp != ARITHVAR_SENTINEL);
[ - - ]
175 [ - + ][ - + ]: 4096 : Assert(d_tableau.isBasic(tmp));
[ - - ]
176 : :
177 : 4096 : RowIndex ri = d_tableau.basicToRowIndex(tmp);
178 : 4096 : d_linEq.stopTrackingRowIndex(ri);
179 : 4096 : d_tableau.removeBasicRow(tmp);
180 : 4096 : releaseVariable(tmp);
181 : 4096 : }
182 : :
183 : 0 : void SimplexDecisionProcedure::shrinkInfeasFunc(TimerStat& timer,
184 : : ArithVar inf,
185 : : const ArithVarVec& dropped)
186 : : {
187 : 0 : TimerStat::CodeTimer codeTimer(timer);
188 : 0 : for (ArithVarVec::const_iterator i = dropped.begin(), i_end = dropped.end();
189 [ - - ]: 0 : i != i_end;
190 : 0 : ++i)
191 : : {
192 : 0 : ArithVar back = *i;
193 : :
194 : 0 : int focusSgn = d_errorSet.focusSgn(back);
195 : 0 : Rational chg(-focusSgn);
196 : :
197 : 0 : d_linEq.substitutePlusTimesConstant(inf, back, chg);
198 : 0 : }
199 : 0 : }
200 : :
201 : 7918 : void SimplexDecisionProcedure::adjustInfeasFunc(
202 : : TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges)
203 : : {
204 : 7918 : TimerStat::CodeTimer codeTimer(timer);
205 : 15836 : for (AVIntPairVec::const_iterator i = focusChanges.begin(),
206 : 7918 : i_end = focusChanges.end();
207 [ + + ]: 17498 : i != i_end;
208 : 9580 : ++i)
209 : : {
210 : 9580 : ArithVar v = (*i).first;
211 : 9580 : int focusChange = (*i).second;
212 : :
213 : 9580 : Rational chg(focusChange);
214 [ + + ]: 9580 : if (d_tableau.isBasic(v))
215 : : {
216 : 5039 : d_linEq.substitutePlusTimesConstant(inf, v, chg);
217 : : }
218 : : else
219 : : {
220 : 4541 : d_linEq.directlyAddToCoefficient(inf, v, chg);
221 : : }
222 : 9580 : }
223 : 7918 : }
224 : :
225 : 0 : void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer,
226 : : ArithVar inf,
227 : : ArithVar e)
228 : : {
229 : 0 : AVIntPairVec justE;
230 : 0 : int sgn = d_errorSet.getSgn(e);
231 : 0 : justE.push_back(make_pair(e, sgn));
232 : 0 : adjustInfeasFunc(timer, inf, justE);
233 : 0 : }
234 : :
235 : 0 : void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer,
236 : : ArithVar inf,
237 : : ArithVar e)
238 : : {
239 : 0 : AVIntPairVec justE;
240 : 0 : int opSgn = -d_errorSet.getSgn(e);
241 : 0 : justE.push_back(make_pair(e, opSgn));
242 : 0 : adjustInfeasFunc(timer, inf, justE);
243 : 0 : }
244 : :
245 : 4096 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(
246 : : TimerStat& timer, const ArithVarVec& set)
247 : : {
248 [ + - ]: 8192 : Trace("constructInfeasiblityFunction")
249 : 4096 : << "constructInfeasiblityFunction start" << endl;
250 : :
251 : 4096 : TimerStat::CodeTimer codeTimer(timer);
252 [ - + ][ - + ]: 4096 : Assert(!d_errorSet.focusEmpty());
[ - - ]
253 [ - + ][ - + ]: 4096 : Assert(debugIsASet(set));
[ - - ]
254 : :
255 : 4096 : ArithVar inf = requestVariable();
256 [ - + ][ - + ]: 4096 : Assert(inf != ARITHVAR_SENTINEL);
[ - - ]
257 : :
258 : 4096 : std::vector<Rational> coeffs;
259 : 4096 : std::vector<ArithVar> variables;
260 : :
261 : 4096 : for (ArithVarVec::const_iterator iter = set.begin(), iend = set.end();
262 [ + + ]: 13509 : iter != iend;
263 : 9413 : ++iter)
264 : : {
265 : 9413 : ArithVar e = *iter;
266 : :
267 [ - + ][ - + ]: 9413 : Assert(d_tableau.isBasic(e));
[ - - ]
268 [ - + ][ - + ]: 9413 : Assert(!d_variables.assignmentIsConsistent(e));
[ - - ]
269 : :
270 : 9413 : int sgn = d_errorSet.getSgn(e);
271 [ + + ][ + - ]: 9413 : Assert(sgn == -1 || sgn == 1);
[ - + ][ - + ]
[ - - ]
272 [ + + ]: 9413 : const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
273 : 9413 : coeffs.push_back(violatedCoeff);
274 : 9413 : variables.push_back(e);
275 : :
276 [ + - ]: 9413 : Trace("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
277 : : }
278 : 4096 : d_tableau.addRow(inf, coeffs, variables);
279 : 4096 : DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
280 : 4096 : d_variables.setAssignment(inf, newAssignment);
281 : :
282 : : // d_linEq.trackVariable(inf);
283 : 4096 : d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
284 : :
285 [ + - ]: 4096 : Trace("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
286 [ + - ]: 8192 : Trace("constructInfeasiblityFunction")
287 : 4096 : << "constructInfeasiblityFunction done" << endl;
288 : 4096 : return inf;
289 : 4096 : }
290 : :
291 : 4043 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(
292 : : TimerStat& timer)
293 : : {
294 : 4043 : ArithVarVec inError;
295 : 4043 : d_errorSet.pushFocusInto(inError);
296 : 8086 : return constructInfeasiblityFunction(timer, inError);
297 : 4043 : }
298 : :
299 : 0 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(
300 : : TimerStat& timer, ArithVar e)
301 : : {
302 : 0 : ArithVarVec justE;
303 : 0 : justE.push_back(e);
304 : 0 : return constructInfeasiblityFunction(timer, justE);
305 : 0 : }
306 : :
307 : 0 : void SimplexDecisionProcedure::addSgn(sgn_table& sgns,
308 : : ArithVar col,
309 : : int sgn,
310 : : ArithVar basic)
311 : : {
312 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
313 : 0 : sgns[p].push_back(basic);
314 : 0 : }
315 : :
316 : 0 : void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns,
317 : : ArithVar basic,
318 : : int norm)
319 : : {
320 [ - - ]: 0 : for (Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd();
321 : 0 : ++i)
322 : : {
323 : 0 : const Tableau::Entry& entry = *i;
324 : 0 : ArithVar v = entry.getColVar();
325 : 0 : int sgn = (entry.getCoefficient().sgn());
326 : 0 : addSgn(sgns, v, norm * sgn, basic);
327 : : }
328 : 0 : }
329 : :
330 : 0 : ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns,
331 : : ArithVar col,
332 : : int sgn,
333 : : const DenseSet& m,
334 : : bool inside)
335 : : {
336 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
337 : 0 : sgn_table::const_iterator i = sgns.find(p);
338 : :
339 [ - - ]: 0 : if (i != sgns.end())
340 : : {
341 : 0 : const ArithVarVec& vec = (*i).second;
342 : 0 : for (ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end();
343 [ - - ]: 0 : viter != vend;
344 : 0 : ++viter)
345 : : {
346 : 0 : ArithVar curr = *viter;
347 [ - - ]: 0 : if (inside == m.isMember(curr))
348 : : {
349 : 0 : return curr;
350 : : }
351 : : }
352 : : }
353 : 0 : return ARITHVAR_SENTINEL;
354 : : }
355 : :
356 : : SimplexDecisionProcedure::sgn_table::const_iterator
357 : 0 : SimplexDecisionProcedure::find_sgns(const sgn_table& sgns,
358 : : ArithVar col,
359 : : int sgn)
360 : : {
361 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
362 : 0 : return sgns.find(p);
363 : : }
364 : : } // namespace arith::linear
365 : : } // namespace theory
366 : : } // namespace cvc5::internal
|
