Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Gereon Kremer, Daniel Larraz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 is an implementation of the Simplex Module for the Simplex for
14 : : * DPLL(T) decision procedure.
15 : : */
16 : :
17 : : #include "theory/arith/linear/simplex.h"
18 : :
19 : : #include "base/output.h"
20 : : #include "options/arith_options.h"
21 : : #include "options/smt_options.h"
22 : : #include "smt/env.h"
23 : : #include "theory/arith/linear/constraint.h"
24 : : #include "theory/arith/linear/error_set.h"
25 : : #include "theory/arith/linear/linear_equality.h"
26 : : #include "theory/arith/linear/tableau.h"
27 : : #include "util/statistics_value.h"
28 : :
29 : : using namespace std;
30 : :
31 : : namespace cvc5::internal {
32 : : namespace theory {
33 : : namespace arith::linear {
34 : :
35 : 199628 : SimplexDecisionProcedure::SimplexDecisionProcedure(
36 : : Env& env,
37 : : LinearEqualityModule& linEq,
38 : : ErrorSet& errors,
39 : : RaiseConflict conflictChannel,
40 : 199628 : TempVarMalloc tvmalloc)
41 : : : EnvObj(env),
42 : 199628 : d_pivots(0),
43 : 199628 : d_conflictVariables(),
44 : 199628 : d_linEq(linEq),
45 : 199628 : d_variables(d_linEq.getVariables()),
46 : 199628 : d_tableau(d_linEq.getTableau()),
47 : 199628 : d_errorSet(errors),
48 : 199628 : d_numVariables(0),
49 : 199628 : d_conflictChannel(conflictChannel),
50 : 199628 : d_conflictBuilder(NULL),
51 : 199628 : d_arithVarMalloc(tvmalloc),
52 : 199628 : d_errorSize(0),
53 : 199628 : d_zero(0),
54 : 199628 : d_posOne(1),
55 : 399256 : d_negOne(-1)
56 : : {
57 : 199628 : d_heuristicRule = options().arith.arithErrorSelectionRule;
58 : 199628 : d_errorSet.setSelectionRule(d_heuristicRule);
59 : 199628 : d_conflictBuilder = new FarkasConflictBuilder(options().smt.produceProofs);
60 : 199628 : }
61 : :
62 : 792992 : SimplexDecisionProcedure::~SimplexDecisionProcedure(){
63 [ + - ]: 198248 : delete d_conflictBuilder;
64 : 198248 : }
65 : :
66 : :
67 : 1784793 : bool SimplexDecisionProcedure::standardProcessSignals(TimerStat &timer, IntStat& conflicts) {
68 : 1784793 : TimerStat::CodeTimer codeTimer(timer);
69 [ - + ][ - + ]: 1784793 : Assert(d_conflictVariables.empty());
[ - - ]
70 : :
71 [ + + ]: 15545312 : while(d_errorSet.moreSignals()){
72 : 13760519 : ArithVar curr = d_errorSet.topSignal();
73 [ + + ][ + + ]: 13760519 : if(d_tableau.isBasic(curr) && !d_variables.assignmentIsConsistent(curr)){
[ + + ]
74 [ - + ][ - + ]: 1120951 : Assert(d_linEq.basicIsTracked(curr));
[ - - ]
75 : :
76 [ + + ][ + + ]: 1120951 : if(!d_conflictVariables.isMember(curr) && checkBasicForConflict(curr)){
[ + + ]
77 : :
78 [ + - ]: 200186 : Trace("recentlyViolated")
79 : 0 : << "It worked? "
80 : 0 : << conflicts.get()
81 : 0 : << " " << curr
82 : 100093 : << " " << checkBasicForConflict(curr) << endl;
83 : 100093 : reportConflict(curr);
84 : 100093 : ++conflicts;
85 : : }
86 : : }
87 : : // Pop signal afterwards in case d_linEq.trackVariable(curr);
88 : : // is needed for for the ErrorSet
89 : 13760519 : d_errorSet.popSignal();
90 : : }
91 : 1784793 : d_errorSize = d_errorSet.errorSize();
92 : :
93 [ - + ][ - + ]: 1784793 : Assert(d_errorSet.noSignals());
[ - - ]
94 : 3569586 : return !d_conflictVariables.empty();
95 : 1784793 : }
96 : :
97 : : /** Reports a conflict to on the output channel. */
98 : 101283 : void SimplexDecisionProcedure::reportConflict(ArithVar basic){
99 [ - + ][ - + ]: 101283 : Assert(!d_conflictVariables.isMember(basic));
[ - - ]
100 [ - + ][ - + ]: 101283 : Assert(checkBasicForConflict(basic));
[ - - ]
101 : :
102 : 101283 : ConstraintCP conflicted = generateConflictForBasic(basic);
103 [ - + ][ - + ]: 101283 : Assert(conflicted != NullConstraint);
[ - - ]
104 : 101283 : d_conflictChannel.raiseConflict(conflicted, InferenceId::ARITH_CONF_SIMPLEX);
105 : :
106 : 101283 : d_conflictVariables.add(basic);
107 : 101283 : }
108 : :
109 : 101283 : ConstraintCP SimplexDecisionProcedure::generateConflictForBasic(ArithVar basic) const {
110 [ - + ][ - + ]: 101283 : Assert(d_tableau.isBasic(basic));
[ - - ]
111 [ - + ][ - + ]: 101283 : Assert(checkBasicForConflict(basic));
[ - - ]
112 : :
113 [ + + ]: 101283 : if(d_variables.cmpAssignmentLowerBound(basic) < 0){
114 [ - + ][ - + ]: 52301 : Assert(d_linEq.nonbasicsAtUpperBounds(basic));
[ - - ]
115 : 52301 : return d_linEq.generateConflictBelowLowerBound(
116 : 104602 : nodeManager(), basic, *d_conflictBuilder);
117 [ + - ]: 48982 : }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
118 [ - + ][ - + ]: 48982 : Assert(d_linEq.nonbasicsAtLowerBounds(basic));
[ - - ]
119 : 48982 : return d_linEq.generateConflictAboveUpperBound(
120 : 97964 : nodeManager(), basic, *d_conflictBuilder);
121 : : }else{
122 : 0 : Unreachable();
123 : : return NullConstraint;
124 : : }
125 : : }
126 : 0 : bool SimplexDecisionProcedure::maybeGenerateConflictForBasic(ArithVar basic) const {
127 [ - - ]: 0 : if(checkBasicForConflict(basic)){
128 : 0 : ConstraintCP conflicted = generateConflictForBasic(basic);
129 : 0 : d_conflictChannel.raiseConflict(conflicted, InferenceId::UNKNOWN);
130 : 0 : return true;
131 : : }else{
132 : 0 : return false;
133 : : }
134 : : }
135 : :
136 : 1311375 : bool SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic) const {
137 [ - + ][ - + ]: 1311375 : Assert(d_tableau.isBasic(basic));
[ - - ]
138 [ - + ][ - + ]: 1311375 : Assert(d_linEq.basicIsTracked(basic));
[ - - ]
139 : :
140 [ + + ]: 1311375 : if(d_variables.cmpAssignmentLowerBound(basic) < 0){
141 [ + + ]: 665085 : if(d_linEq.nonbasicsAtUpperBounds(basic)){
142 : 156903 : return true;
143 : : }
144 [ + - ]: 646290 : }else if(d_variables.cmpAssignmentUpperBound(basic) > 0){
145 [ + + ]: 646290 : if(d_linEq.nonbasicsAtLowerBounds(basic)){
146 : 146946 : return true;
147 : : }
148 : : }
149 : 1007526 : return false;
150 : : }
151 : :
152 : 3943 : void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, ArithVar tmp){
153 : 3943 : TimerStat::CodeTimer codeTimer(timer);
154 [ - + ][ - + ]: 3943 : Assert(tmp != ARITHVAR_SENTINEL);
[ - - ]
155 [ - + ][ - + ]: 3943 : Assert(d_tableau.isBasic(tmp));
[ - - ]
156 : :
157 : 3943 : RowIndex ri = d_tableau.basicToRowIndex(tmp);
158 : 3943 : d_linEq.stopTrackingRowIndex(ri);
159 : 3943 : d_tableau.removeBasicRow(tmp);
160 : 3943 : releaseVariable(tmp);
161 : 3943 : }
162 : :
163 : 0 : void SimplexDecisionProcedure::shrinkInfeasFunc(TimerStat& timer, ArithVar inf, const ArithVarVec& dropped){
164 : 0 : TimerStat::CodeTimer codeTimer(timer);
165 [ - - ]: 0 : for(ArithVarVec::const_iterator i=dropped.begin(), i_end = dropped.end(); i != i_end; ++i){
166 : 0 : ArithVar back = *i;
167 : :
168 : 0 : int focusSgn = d_errorSet.focusSgn(back);
169 : 0 : Rational chg(-focusSgn);
170 : :
171 : 0 : d_linEq.substitutePlusTimesConstant(inf, back, chg);
172 : 0 : }
173 : 0 : }
174 : :
175 : 7410 : void SimplexDecisionProcedure::adjustInfeasFunc(TimerStat& timer, ArithVar inf, const AVIntPairVec& focusChanges){
176 : 7410 : TimerStat::CodeTimer codeTimer(timer);
177 [ + + ]: 16667 : for(AVIntPairVec::const_iterator i=focusChanges.begin(), i_end = focusChanges.end(); i != i_end; ++i){
178 : 9257 : ArithVar v = (*i).first;
179 : 9257 : int focusChange = (*i).second;
180 : :
181 : 9257 : Rational chg(focusChange);
182 [ + + ]: 9257 : if(d_tableau.isBasic(v)){
183 : 4914 : d_linEq.substitutePlusTimesConstant(inf, v, chg);
184 : : }else{
185 : 4343 : d_linEq.directlyAddToCoefficient(inf, v, chg);
186 : : }
187 : 9257 : }
188 : 7410 : }
189 : :
190 : 0 : void SimplexDecisionProcedure::addToInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
191 : 0 : AVIntPairVec justE;
192 : 0 : int sgn = d_errorSet.getSgn(e);
193 : 0 : justE.push_back(make_pair(e, sgn));
194 : 0 : adjustInfeasFunc(timer, inf, justE);
195 : 0 : }
196 : :
197 : 0 : void SimplexDecisionProcedure::removeFromInfeasFunc(TimerStat& timer, ArithVar inf, ArithVar e){
198 : 0 : AVIntPairVec justE;
199 : 0 : int opSgn = -d_errorSet.getSgn(e);
200 : 0 : justE.push_back(make_pair(e, opSgn));
201 : 0 : adjustInfeasFunc(timer, inf, justE);
202 : 0 : }
203 : :
204 : 3943 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, const ArithVarVec& set){
205 [ + - ]: 3943 : Trace("constructInfeasiblityFunction") << "constructInfeasiblityFunction start" << endl;
206 : :
207 : 3943 : TimerStat::CodeTimer codeTimer(timer);
208 [ - + ][ - + ]: 3943 : Assert(!d_errorSet.focusEmpty());
[ - - ]
209 [ - + ][ - + ]: 3943 : Assert(debugIsASet(set));
[ - - ]
210 : :
211 : 3943 : ArithVar inf = requestVariable();
212 [ - + ][ - + ]: 3943 : Assert(inf != ARITHVAR_SENTINEL);
[ - - ]
213 : :
214 : 3943 : std::vector<Rational> coeffs;
215 : 3943 : std::vector<ArithVar> variables;
216 : :
217 [ + + ]: 12918 : for(ArithVarVec::const_iterator iter = set.begin(), iend = set.end(); iter != iend; ++iter){
218 : 8975 : ArithVar e = *iter;
219 : :
220 [ - + ][ - + ]: 8975 : Assert(d_tableau.isBasic(e));
[ - - ]
221 [ - + ][ - + ]: 8975 : Assert(!d_variables.assignmentIsConsistent(e));
[ - - ]
222 : :
223 : 8975 : int sgn = d_errorSet.getSgn(e);
224 [ + + ][ + - ]: 8975 : Assert(sgn == -1 || sgn == 1);
[ - + ][ - + ]
[ - - ]
225 [ + + ]: 8975 : const Rational& violatedCoeff = sgn < 0 ? d_negOne : d_posOne;
226 : 8975 : coeffs.push_back(violatedCoeff);
227 : 8975 : variables.push_back(e);
228 : :
229 [ + - ]: 8975 : Trace("constructInfeasiblityFunction") << violatedCoeff << " " << e << endl;
230 : :
231 : : }
232 : 3943 : d_tableau.addRow(inf, coeffs, variables);
233 : 3943 : DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
234 : 3943 : d_variables.setAssignment(inf, newAssignment);
235 : :
236 : : //d_linEq.trackVariable(inf);
237 : 3943 : d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
238 : :
239 [ + - ]: 3943 : Trace("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
240 [ + - ]: 3943 : Trace("constructInfeasiblityFunction") << "constructInfeasiblityFunction done" << endl;
241 : 3943 : return inf;
242 : 3943 : }
243 : :
244 : 3905 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer){
245 : 3905 : ArithVarVec inError;
246 : 3905 : d_errorSet.pushFocusInto(inError);
247 : 7810 : return constructInfeasiblityFunction(timer, inError);
248 : 3905 : }
249 : :
250 : 0 : ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& timer, ArithVar e){
251 : 0 : ArithVarVec justE;
252 : 0 : justE.push_back(e);
253 : 0 : return constructInfeasiblityFunction(timer, justE);
254 : 0 : }
255 : :
256 : 0 : void SimplexDecisionProcedure::addSgn(sgn_table& sgns, ArithVar col, int sgn, ArithVar basic){
257 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
258 : 0 : sgns[p].push_back(basic);
259 : 0 : }
260 : :
261 : 0 : void SimplexDecisionProcedure::addRowSgns(sgn_table& sgns, ArithVar basic, int norm){
262 [ - - ]: 0 : for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
263 : 0 : const Tableau::Entry& entry = *i;
264 : 0 : ArithVar v = entry.getColVar();
265 : 0 : int sgn = (entry.getCoefficient().sgn());
266 : 0 : addSgn(sgns, v, norm * sgn, basic);
267 : : }
268 : 0 : }
269 : :
270 : 0 : ArithVar SimplexDecisionProcedure::find_basic_in_sgns(const sgn_table& sgns, ArithVar col, int sgn, const DenseSet& m, bool inside){
271 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
272 : 0 : sgn_table::const_iterator i = sgns.find(p);
273 : :
274 [ - - ]: 0 : if(i != sgns.end()){
275 : 0 : const ArithVarVec& vec = (*i).second;
276 [ - - ]: 0 : for(ArithVarVec::const_iterator viter = vec.begin(), vend = vec.end(); viter != vend; ++viter){
277 : 0 : ArithVar curr = *viter;
278 [ - - ]: 0 : if(inside == m.isMember(curr)){
279 : 0 : return curr;
280 : : }
281 : : }
282 : : }
283 : 0 : return ARITHVAR_SENTINEL;
284 : : }
285 : :
286 : 0 : SimplexDecisionProcedure::sgn_table::const_iterator SimplexDecisionProcedure::find_sgns(const sgn_table& sgns, ArithVar col, int sgn){
287 : 0 : pair<ArithVar, int> p = make_pair(col, determinizeSgn(sgn));
288 : 0 : return sgns.find(p);
289 : : }
290 : : } // namespace arith
291 : : } // namespace theory
292 : : } // namespace cvc5::internal
|
