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 : : * Diophantine equation solver
11 : : *
12 : : * A Diophantine equation solver for the theory of arithmetic.
13 : : */
14 : : #include "theory/arith/linear/dio_solver.h"
15 : :
16 : : #include <iostream>
17 : :
18 : : #include "base/output.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "options/arith_options.h"
21 : : #include "smt/env.h"
22 : : #include "theory/arith/linear/partial_model.h"
23 : :
24 : : using namespace std;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace arith::linear {
29 : :
30 : 13086 : inline Node makeIntegerVariable(NodeManager* nm)
31 : : {
32 : 13086 : return NodeManager::mkDummySkolem("intvar", nm->integerType());
33 : : }
34 : :
35 : 50907 : DioSolver::DioSolver(Env& env)
36 : : : EnvObj(env),
37 : 50907 : d_lastUsedProofVariable(context(), 0),
38 : 50907 : d_inputConstraints(context()),
39 : 50907 : d_nextInputConstraintToEnqueue(context(), 0),
40 : 50907 : d_trail(context()),
41 : 50907 : d_subs(context()),
42 : 50907 : d_currentF(),
43 : 50907 : d_savedQueue(context()),
44 : 50907 : d_savedQueueIndex(context(), 0),
45 : 50907 : d_conflictIndex(context()),
46 : 50907 : d_maxInputCoefficientLength(context(), 0),
47 : 50907 : d_usedDecomposeIndex(context(), false),
48 : 50907 : d_lastPureSubstitution(context(), 0),
49 : 50907 : d_pureSubstitionIter(context(), 0),
50 : 50907 : d_decompositionLemmaQueue(context()),
51 : 152721 : d_statistics(statisticsRegistry())
52 : : {
53 : 50907 : }
54 : :
55 : 50907 : DioSolver::Statistics::Statistics(StatisticsRegistry& sr)
56 : 50907 : : d_conflictCalls(sr.registerInt("theory::arith::dio::conflictCalls")),
57 : 50907 : d_cutCalls(sr.registerInt("theory::arith::dio::cutCalls")),
58 : 50907 : d_cuts(sr.registerInt("theory::arith::dio::cuts")),
59 : 50907 : d_conflicts(sr.registerInt("theory::arith::dio::conflicts")),
60 : 50907 : d_conflictTimer(sr.registerTimer("theory::arith::dio::conflictTimer")),
61 : 50907 : d_cutTimer(sr.registerTimer("theory::arith::dio::cutTimer"))
62 : : {
63 : 50907 : }
64 : :
65 : 91325 : bool DioSolver::queueConditions(TrailIndex t){
66 [ + - ]: 91325 : Trace("queueConditions") << !inConflict() << std::endl;
67 [ + - ]: 91325 : Trace("queueConditions") << gcdIsOne(t) << std::endl;
68 [ + - ]: 91325 : Trace("queueConditions") << !debugAnySubstitionApplies(t) << std::endl;
69 [ + - ]: 91325 : Trace("queueConditions") << !triviallySat(t) << std::endl;
70 [ + - ]: 91325 : Trace("queueConditions") << !triviallyUnsat(t) << std::endl;
71 : :
72 : : return
73 : 91325 : !inConflict() &&
74 [ + - ]: 91325 : gcdIsOne(t) &&
75 [ + - ]: 91325 : !debugAnySubstitionApplies(t) &&
76 [ + - ][ + - ]: 273975 : !triviallySat(t) &&
77 [ + - ]: 182650 : !triviallyUnsat(t);
78 : : }
79 : :
80 : 43062 : size_t DioSolver::allocateProofVariable() {
81 [ - + ][ - + ]: 43062 : Assert(d_lastUsedProofVariable <= d_proofVariablePool.size());
[ - - ]
82 [ + + ]: 43062 : if(d_lastUsedProofVariable == d_proofVariablePool.size()){
83 [ - + ][ - + ]: 11612 : Assert(d_lastUsedProofVariable == d_proofVariablePool.size());
[ - - ]
84 : 11612 : Node intVar = makeIntegerVariable(nodeManager());
85 : 11612 : d_proofVariablePool.push_back(Variable(intVar));
86 : 11612 : }
87 : 43062 : size_t res = d_lastUsedProofVariable;
88 : 43062 : d_lastUsedProofVariable = d_lastUsedProofVariable + 1;
89 : 43062 : return res;
90 : : }
91 : :
92 : :
93 : 0 : Node DioSolver::nextPureSubstitution(){
94 : 0 : Assert(hasMorePureSubstitutions());
95 : 0 : SubIndex curr = d_pureSubstitionIter;
96 : 0 : d_pureSubstitionIter = d_pureSubstitionIter + 1;
97 : :
98 : 0 : Assert(d_subs[curr].d_fresh.isNull());
99 : 0 : Variable v = d_subs[curr].d_eliminated;
100 : :
101 : 0 : SumPair sp = d_trail[d_subs[curr].d_constraint].d_eq;
102 : 0 : Polynomial p = sp.getPolynomial();
103 : 0 : Constant c = -sp.getConstant();
104 : 0 : Polynomial cancelV = p + Polynomial::mkPolynomial(v);
105 : 0 : Node eq = nodeManager()->mkNode(Kind::EQUAL, v.getNode(), cancelV.getNode());
106 : 0 : return eq;
107 : 0 : }
108 : :
109 : :
110 : 43062 : bool DioSolver::debugEqualityInInputEquations(Node eq){
111 : : typedef context::CDList<InputConstraint>::const_iterator const_iterator;
112 : 43062 : const_iterator i=d_inputConstraints.begin(), end = d_inputConstraints.end();
113 [ + + ]: 1230371 : for(; i != end; ++i){
114 : 1187309 : Node reason_i = (*i).d_reason;
115 [ - + ]: 1187309 : if(eq == reason_i){
116 : 0 : return true;
117 : : }
118 [ + - ]: 1187309 : }
119 : 43062 : return false;
120 : : }
121 : :
122 : :
123 : 43062 : void DioSolver::pushInputConstraint(const Comparison& eq, Node reason){
124 [ - + ][ - + ]: 43062 : Assert(!debugEqualityInInputEquations(reason));
[ - - ]
125 [ - + ][ - + ]: 43062 : Assert(eq.debugIsIntegral());
[ - - ]
126 [ - + ][ - + ]: 43062 : Assert(eq.getNode().getKind() == Kind::EQUAL);
[ - - ]
127 : :
128 : 43062 : SumPair sp = eq.toSumPair();
129 [ - + ][ - + ]: 43062 : Assert(!sp.isNonlinear());
[ - - ]
130 : :
131 : :
132 : :
133 : 43062 : uint32_t length = sp.maxLength();
134 [ + + ]: 43062 : if(length > d_maxInputCoefficientLength){
135 : 4874 : d_maxInputCoefficientLength = length;
136 : : }
137 : :
138 : 43062 : size_t varIndex = allocateProofVariable();
139 : 43062 : Variable proofVariable(d_proofVariablePool[varIndex]);
140 : : // Variable proofVariable(makeIntegerVariable(nodeManager()));
141 : :
142 : 43062 : TrailIndex posInTrail = d_trail.size();
143 [ + - ]: 86124 : Trace("dio::pushInputConstraint") << "pushInputConstraint @ " << posInTrail
144 : 0 : << " " << eq.getNode()
145 : 43062 : << " " << reason << endl;
146 : 43062 : d_trail.push_back(Constraint(sp,Polynomial::mkPolynomial(proofVariable)));
147 : :
148 : 43062 : size_t posInConstraintList = d_inputConstraints.size();
149 : 43062 : d_inputConstraints.push_back(InputConstraint(reason, posInTrail));
150 : :
151 : 43062 : d_varToInputConstraintMap[proofVariable.getNode()] = posInConstraintList;
152 : 43062 : }
153 : :
154 : :
155 : 26735 : DioSolver::TrailIndex DioSolver::scaleEqAtIndex(DioSolver::TrailIndex i, const Integer& g){
156 [ - + ][ - + ]: 26735 : Assert(g != 0);
[ - - ]
157 : 53470 : Constant invg = Constant::mkConstant(nodeManager(), Rational(Integer(1), g));
158 : 26735 : const SumPair& sp = d_trail[i].d_eq;
159 : 26735 : const Polynomial& proof = d_trail[i].d_proof;
160 : :
161 : 26735 : SumPair newSP = sp * invg;
162 : 26735 : Polynomial newProof = proof * invg;
163 : :
164 [ - + ][ - + ]: 26735 : Assert(newSP.isIntegral());
[ - - ]
165 [ - + ][ - + ]: 26735 : Assert(newSP.gcd() == 1);
[ - - ]
166 : :
167 : 26735 : TrailIndex j = d_trail.size();
168 : :
169 : 26735 : d_trail.push_back(Constraint(newSP, newProof));
170 : :
171 [ + - ]: 26735 : Trace("arith::dio") << "scaleEqAtIndex(" << i <<","<<g<<")"<<endl;
172 [ + - ]: 53470 : Trace("arith::dio") << "derived "<< newSP.getNode()
173 : 26735 : <<" with proof " << newProof.getNode() << endl;
174 : 26735 : return j;
175 : 26735 : }
176 : :
177 : 244 : Node DioSolver::proveIndex(TrailIndex i){
178 [ - + ][ - + ]: 244 : Assert(inRange(i));
[ - - ]
179 : 244 : const Polynomial& proof = d_trail[i].d_proof;
180 [ - + ][ - + ]: 244 : Assert(!proof.isConstant());
[ - - ]
181 : :
182 : 244 : NodeBuilder nb(nodeManager(), Kind::AND);
183 [ + + ]: 975 : for(Polynomial::iterator iter = proof.begin(), end = proof.end(); iter!= end; ++iter){
184 : 731 : Monomial m = (*iter);
185 [ - + ][ - + ]: 731 : Assert(!m.isConstant());
[ - - ]
186 : 731 : VarList vl = m.getVarList();
187 [ - + ][ - + ]: 731 : Assert(vl.singleton());
[ - - ]
188 : 731 : Variable v = vl.getHead();
189 : :
190 : 731 : Node input = proofVariableToReason(v);
191 [ + + ]: 731 : if (input.getKind() == Kind::AND)
192 : : {
193 [ + + ]: 233 : for(Node::iterator input_iter = input.begin(), input_end = input.end(); input_iter != input_end; ++input_iter){
194 : 158 : Node inputChild = *input_iter;
195 : 158 : nb << inputChild;
196 : 158 : }
197 : : }
198 : : else
199 : : {
200 : 656 : nb << input;
201 : : }
202 : 975 : }
203 : :
204 [ - + ]: 244 : Node result = (nb.getNumChildren() == 1) ? nb[0] : (Node)nb;
205 [ + - ]: 488 : Trace("arith::dio") << "Proof at " << i << " is "
206 : 0 : << d_trail[i].d_eq.getNode() << endl
207 : 0 : << d_trail[i].d_proof.getNode() << endl
208 : 244 : << " which becomes " << result << endl;
209 : 488 : return result;
210 : 244 : }
211 : :
212 : 61158 : bool DioSolver::anyCoefficientExceedsMaximum(TrailIndex j) const{
213 : 61158 : uint32_t length = d_trail[j].d_eq.maxLength();
214 : 61158 : uint32_t nmonos = d_trail[j].d_eq.getPolynomial().numMonomials();
215 : :
216 : : bool result =
217 [ + + ]: 99164 : nmonos >= 2 &&
218 [ + + ]: 38006 : length > d_maxInputCoefficientLength + MAX_GROWTH_RATE;
219 : 61158 : if(TraceIsOn("arith::dio::max") && result){
220 : :
221 : 0 : const SumPair& eq = d_trail[j].d_eq;
222 : 0 : const Polynomial& proof = d_trail[j].d_proof;
223 : :
224 [ - - ]: 0 : Trace("arith::dio::max") << "about to drop:" << std::endl;
225 [ - - ]: 0 : Trace("arith::dio::max") << "d_trail[" << j << "].d_eq = " << eq.getNode() << std::endl;
226 [ - - ]: 0 : Trace("arith::dio::max") << "d_trail[" << j << "].d_proof = " << proof.getNode() << std::endl;
227 : : }
228 : 61158 : return result;
229 : : }
230 : :
231 : 6891 : void DioSolver::enqueueInputConstraints(){
232 [ - + ][ - + ]: 6891 : Assert(d_currentF.empty());
[ - - ]
233 [ - + ]: 6891 : while(d_savedQueueIndex < d_savedQueue.size()){
234 : 0 : d_currentF.push_back(d_savedQueue[d_savedQueueIndex]);
235 : 0 : d_savedQueueIndex = d_savedQueueIndex + 1;
236 : : }
237 : :
238 [ + + ][ + + ]: 48546 : while(d_nextInputConstraintToEnqueue < d_inputConstraints.size() && !inConflict()){
[ + + ]
239 : 41655 : size_t curr = d_nextInputConstraintToEnqueue;
240 : 41655 : d_nextInputConstraintToEnqueue = d_nextInputConstraintToEnqueue + 1;
241 : :
242 : 41655 : TrailIndex i = d_inputConstraints[curr].d_trailPos;
243 : 41655 : TrailIndex j = applyAllSubstitutionsToIndex(i);
244 : :
245 [ + + ]: 41655 : if(!triviallySat(j)){
246 [ - + ]: 40728 : if(triviallyUnsat(j)){
247 : 0 : raiseConflict(j);
248 : : }else{
249 : 40728 : TrailIndex k = reduceByGCD(j);
250 : :
251 [ + + ]: 40728 : if(!inConflict()){
252 [ - + ]: 39848 : if(triviallyUnsat(k)){
253 : 0 : raiseConflict(k);
254 [ + - ][ + + ]: 39848 : }else if(!(triviallySat(k) || anyCoefficientExceedsMaximum(k))){
[ + + ]
255 : 39820 : pushToQueueBack(k);
256 : : }
257 : : }
258 : : }
259 : : }
260 : : }
261 : 6891 : }
262 : :
263 : :
264 : : /*TODO Currently linear in the size of the Queue
265 : : *It is not clear if am O(log n) strategy would be better.
266 : : *Right before this in the algorithm is a substitution which could potentially
267 : : *effect the key values of everything in the queue.
268 : : */
269 : 29029 : void DioSolver::moveMinimumByAbsToQueueFront(){
270 [ - + ][ - + ]: 29029 : Assert(!queueEmpty());
[ - - ]
271 : :
272 : : //Select the minimum element.
273 : 29029 : size_t indexInQueue = 0;
274 : 29029 : Monomial minMonomial = d_trail[d_currentF[indexInQueue]].d_minimalMonomial;
275 : :
276 : 29029 : size_t N = d_currentF.size();
277 [ + + ]: 547485 : for(size_t i=1; i < N; ++i){
278 : 518456 : Monomial curr = d_trail[d_currentF[i]].d_minimalMonomial;
279 [ + + ]: 518456 : if(curr.absCmp(minMonomial) < 0){
280 : 1563 : indexInQueue = i;
281 : 1563 : minMonomial = curr;
282 : : }
283 : 518456 : }
284 : :
285 : 29029 : TrailIndex tmp = d_currentF[indexInQueue];
286 : 29029 : d_currentF[indexInQueue] = d_currentF.front();
287 : 29029 : d_currentF.front() = tmp;
288 : 29029 : }
289 : :
290 : 64949 : bool DioSolver::queueEmpty() const{
291 : 64949 : return d_currentF.empty();
292 : : }
293 : :
294 : 1754 : Node DioSolver::columnGcdIsOne() const{
295 : 1754 : std::unordered_map<Node, Integer> gcdMap;
296 : :
297 : 1754 : std::deque<TrailIndex>::const_iterator iter, end;
298 [ + + ]: 5181 : for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
299 : 3707 : TrailIndex curr = *iter;
300 : 3707 : Polynomial p = d_trail[curr].d_eq.getPolynomial();
301 : 3707 : Polynomial::iterator monoIter = p.begin(), monoEnd = p.end();
302 [ + + ]: 10882 : for(; monoIter != monoEnd; ++monoIter){
303 : 7455 : Monomial m = *monoIter;
304 : 7455 : VarList vl = m.getVarList();
305 : 7455 : Node vlNode = vl.getNode();
306 : :
307 : 7455 : Constant c = m.getConstant();
308 : 7455 : Integer zc = c.getValue().getNumerator();
309 [ + + ]: 7455 : if(gcdMap.find(vlNode) == gcdMap.end()){
310 : : // have not seen vl yet.
311 : : // gcd is c
312 [ - + ][ - + ]: 5392 : Assert(c.isIntegral());
[ - - ]
313 [ - + ][ - + ]: 5392 : Assert(!m.absCoefficientIsOne());
[ - - ]
314 : 5392 : gcdMap.insert(make_pair(vlNode, zc.abs()));
315 : : }else{
316 : 2063 : const Integer& currentGcd = gcdMap[vlNode];
317 : 2063 : Integer newGcd = currentGcd.gcd(zc);
318 [ + + ]: 2063 : if(newGcd == 1){
319 : 280 : return vlNode;
320 : : }else{
321 : 1783 : gcdMap[vlNode] = newGcd;
322 : : }
323 [ + + ]: 2063 : }
324 [ + + ][ + + ]: 8575 : }
[ + + ][ + + ]
[ + + ]
325 [ + + ][ + + ]: 4267 : }
[ + + ]
326 : 1474 : return Node::null();
327 : 1754 : }
328 : :
329 : 0 : void DioSolver::saveQueue(){
330 : 0 : std::deque<TrailIndex>::const_iterator iter, end;
331 [ - - ]: 0 : for(iter = d_currentF.begin(), end = d_currentF.end(); iter != end; ++iter){
332 : 0 : d_savedQueue.push_back(*iter);
333 : : }
334 : 0 : }
335 : :
336 : 1754 : DioSolver::TrailIndex DioSolver::impliedGcdOfOne(){
337 : 1754 : Node canReduce = columnGcdIsOne();
338 [ + + ]: 1754 : if(canReduce.isNull()){
339 : 1474 : return 0;
340 : : }else{
341 : 280 : VarList vl = VarList::parseVarList(canReduce);
342 : :
343 : : TrailIndex current;
344 : 280 : Integer currentCoeff, currentGcd;
345 : :
346 : : //step 1 find the first equation containing vl
347 : : //Set current and currentCoefficient
348 : 280 : std::deque<TrailIndex>::const_iterator iter, end;
349 : 588 : for(iter = d_currentF.begin(), end = d_currentF.end(); true; ++iter){
350 [ - + ][ - + ]: 588 : Assert(iter != end);
[ - - ]
351 : 588 : current = *iter;
352 : 588 : Constant coeff = d_trail[current].d_eq.getPolynomial().getCoefficient(vl);
353 [ + + ]: 588 : if(!coeff.isZero()){
354 : 280 : currentCoeff = coeff.getValue().getNumerator();
355 : 280 : currentGcd = currentCoeff.abs();
356 : :
357 : 280 : ++iter;
358 : 280 : break;
359 : : }
360 [ + + ]: 896 : }
361 : :
362 : : //For the rest of the equations keep reducing until the coefficient is one
363 [ + - ]: 282 : for(; iter != end; ++iter){
364 [ + - ]: 282 : Trace("arith::dio") << "next round : " << currentCoeff << " " << currentGcd << endl;
365 : 282 : TrailIndex inQueue = *iter;
366 : 282 : Constant iqc = d_trail[inQueue].d_eq.getPolynomial().getCoefficient(vl);
367 [ + - ]: 282 : if(!iqc.isZero()){
368 : 282 : Integer inQueueCoeff = iqc.getValue().getNumerator();
369 : :
370 : : //mpz_gcdext (mpz_t g, mpz_t s, mpz_t t, mpz_t a, mpz_t b);
371 : 282 : Integer g, s, t;
372 : : // g = a*s + b*t
373 : 282 : Integer::extendedGcd(g, s, t, currentCoeff, inQueueCoeff);
374 : :
375 [ + - ]: 282 : Trace("arith::dio") << "extendedReduction : " << endl;
376 [ + - ]: 282 : Trace("arith::dio") << g << " = " << s <<"*"<< currentCoeff << " + " << t <<"*"<< inQueueCoeff << endl;
377 : :
378 [ - + ][ - + ]: 282 : Assert(g <= currentGcd);
[ - - ]
379 [ + + ]: 282 : if(g < currentGcd){
380 [ - + ]: 280 : if(s.sgn() == 0){
381 [ - - ]: 0 : Trace("arith::dio") << "extendedReduction drop" << endl;
382 : 0 : Assert(inQueueCoeff.divides(currentGcd));
383 : 0 : current = *iter;
384 : 0 : currentCoeff = inQueueCoeff;
385 : 0 : currentGcd = inQueueCoeff.abs();
386 : : }else{
387 : :
388 [ + - ]: 280 : Trace("arith::dio") << "extendedReduction combine" << endl;
389 : 280 : TrailIndex next = combineEqAtIndexes(current, s, inQueue, t);
390 : :
391 [ - + ][ - + ]: 280 : Assert(d_trail[next]
[ - - ]
392 : : .d_eq.getPolynomial()
393 : : .getCoefficient(vl)
394 : : .getValue()
395 : : .getNumerator()
396 : : == g);
397 : :
398 : 280 : current = next;
399 : 280 : currentCoeff = g;
400 : 280 : currentGcd = g;
401 [ + - ]: 280 : if(currentGcd == 1){
402 : 280 : return current;
403 : : }
404 : : }
405 : : }
406 [ + + ][ + + ]: 1122 : }
[ + + ][ + + ]
407 [ + + ]: 282 : }
408 : : //This is not reachble as it is assured that the gcd of the column is 1
409 : 0 : Unreachable();
410 : 280 : }
411 : 1754 : }
412 : :
413 : 6891 : bool DioSolver::processEquations(bool allowDecomposition){
414 [ - + ][ - + ]: 6891 : Assert(!inConflict());
[ - - ]
415 : :
416 : 6891 : enqueueInputConstraints();
417 [ + + ][ + + ]: 35920 : while(! queueEmpty() && !inConflict()){
[ + + ]
418 : 29029 : moveMinimumByAbsToQueueFront();
419 : :
420 : 29029 : TrailIndex minimum = d_currentF.front();
421 : : TrailIndex reduceIndex;
422 : :
423 [ - + ][ - + ]: 29029 : Assert(inRange(minimum));
[ - - ]
424 [ - + ][ - + ]: 29029 : Assert(!inConflict());
[ - - ]
425 : :
426 [ + - ]: 29029 : Trace("arith::dio") << "processEquations " << minimum << " : " << d_trail[minimum].d_eq.getNode() << endl;
427 : :
428 [ - + ][ - + ]: 29029 : Assert(queueConditions(minimum));
[ - - ]
429 : :
430 : 29029 : bool canDirectlySolve = d_trail[minimum].d_minimalMonomial.absCoefficientIsOne();
431 : :
432 : 29029 : std::pair<SubIndex, TrailIndex> p;
433 [ + + ]: 29029 : if(canDirectlySolve){
434 : 27275 : d_currentF.pop_front();
435 : 27275 : p = solveIndex(minimum);
436 : 27275 : reduceIndex = minimum;
437 : : }else{
438 : 1754 : TrailIndex implied = impliedGcdOfOne();
439 : :
440 [ + + ]: 1754 : if(implied != 0){
441 : 280 : p = solveIndex(implied);
442 : 280 : reduceIndex = implied;
443 [ + - ]: 1474 : }else if(allowDecomposition){
444 : 1474 : d_currentF.pop_front();
445 : 1474 : p = decomposeIndex(minimum);
446 : 1474 : reduceIndex = minimum;
447 : : }else {
448 : : // Cannot make progress without decomposeIndex
449 : 0 : saveQueue();
450 : 0 : break;
451 : : }
452 : : }
453 : :
454 : 29029 : SubIndex subIndex = p.first;
455 : 29029 : TrailIndex next = p.second;
456 : 29029 : subAndReduceCurrentFByIndex(subIndex);
457 : :
458 [ + + ]: 29029 : if(next != reduceIndex){
459 [ - + ]: 1474 : if(triviallyUnsat(next)){
460 : 0 : raiseConflict(next);
461 [ + - ]: 1474 : }else if(! triviallySat(next) ){
462 : 1474 : pushToQueueBack(next);
463 : : }
464 : : }
465 : : }
466 : :
467 : 6891 : d_currentF.clear();
468 : 6891 : return inConflict();
469 : : }
470 : :
471 : 4073 : Node DioSolver::processEquationsForConflict(){
472 : 4073 : TimerStat::CodeTimer codeTimer(d_statistics.d_conflictTimer);
473 : 4073 : ++(d_statistics.d_conflictCalls);
474 : :
475 [ - + ][ - + ]: 4073 : Assert(!inConflict());
[ - - ]
476 [ + + ]: 4073 : if(processEquations(true)){
477 : 244 : ++(d_statistics.d_conflicts);
478 : 244 : return proveIndex(getConflictIndex());
479 : : }else{
480 : 3829 : return Node::null();
481 : : }
482 : 4073 : }
483 : :
484 : 2818 : SumPair DioSolver::processEquationsForCut(){
485 : 2818 : TimerStat::CodeTimer codeTimer(d_statistics.d_cutTimer);
486 : 2818 : ++(d_statistics.d_cutCalls);
487 : :
488 [ - + ][ - + ]: 2818 : Assert(!inConflict());
[ - - ]
489 [ + + ]: 2818 : if(processEquations(true)){
490 : 1864 : ++(d_statistics.d_cuts);
491 : 1864 : return purifyIndex(getConflictIndex());
492 : : }else{
493 : 954 : return SumPair::mkZero(nodeManager());
494 : : }
495 : 2818 : }
496 : :
497 : :
498 : 1864 : SumPair DioSolver::purifyIndex(TrailIndex i){
499 : : // TODO: "This uses the substitution trail to reverse the substitutions from the sum term. Using the proof term should be more efficient."
500 : :
501 : 1864 : SumPair curr = d_trail[i].d_eq;
502 : :
503 : 1864 : Constant negOne = Constant::mkConstant(nodeManager(), -1);
504 : :
505 [ + + ]: 27196 : for(uint32_t revIter = d_subs.size(); revIter > 0; --revIter){
506 : 25332 : uint32_t i2 = revIter - 1;
507 : 25332 : Node freshNode = d_subs[i2].d_fresh;
508 [ + + ]: 25332 : if(freshNode.isNull()){
509 : 23816 : continue;
510 : : }else{
511 : 1516 : Variable var(freshNode);
512 : 1516 : Polynomial vsum = curr.getPolynomial();
513 : :
514 : 3032 : Constant a = vsum.getCoefficient(VarList(var));
515 [ + + ]: 1516 : if(!a.isZero()){
516 : 696 : const SumPair& sj = d_trail[d_subs[i2].d_constraint].d_eq;
517 [ - + ][ - + ]: 696 : Assert(sj.getPolynomial().getCoefficient(VarList(var)).isOne());
[ - - ]
518 : 1392 : SumPair newSi = (curr * negOne) + (sj * a);
519 [ - + ][ - + ]: 696 : Assert(newSi.getPolynomial().getCoefficient(VarList(var)).isZero());
[ - - ]
520 : 696 : curr = newSi;
521 : 696 : }
522 : 1516 : }
523 [ + + ]: 25332 : }
524 : 3728 : return curr;
525 : 1864 : }
526 : :
527 : 45000 : DioSolver::TrailIndex DioSolver::combineEqAtIndexes(DioSolver::TrailIndex i, const Integer& q, DioSolver::TrailIndex j, const Integer& r){
528 : 45000 : Constant cq = Constant::mkConstant(nodeManager(), q);
529 : 45000 : Constant cr = Constant::mkConstant(nodeManager(), r);
530 : :
531 : 45000 : const SumPair& si = d_trail[i].d_eq;
532 : 45000 : const SumPair& sj = d_trail[j].d_eq;
533 : :
534 [ + - ]: 45000 : Trace("arith::dio") << "combineEqAtIndexes(" << i <<","<<q<<","<<j<<","<<r<<")"<<endl;
535 [ + - ]: 90000 : Trace("arith::dio") << "d_facts[i] = " << si.getNode() << endl
536 : 45000 : << "d_facts[j] = " << sj.getNode() << endl;
537 : :
538 : :
539 : 90000 : SumPair newSi = (si * cq) + (sj * cr);
540 : :
541 : :
542 : 45000 : const Polynomial& pi = d_trail[i].d_proof;
543 : 45000 : const Polynomial& pj = d_trail[j].d_proof;
544 : 90000 : Polynomial newPi = (pi * cq) + (pj * cr);
545 : :
546 : 45000 : TrailIndex k = d_trail.size();
547 : 45000 : d_trail.push_back(Constraint(newSi, newPi));
548 : :
549 : :
550 [ + - ]: 90000 : Trace("arith::dio") << "derived "<< newSi.getNode()
551 : 45000 : <<" with proof " << newPi.getNode() << endl;
552 : :
553 : 45000 : return k;
554 : :
555 : 45000 : }
556 : :
557 : 0 : void DioSolver::printQueue(){
558 [ - - ]: 0 : Trace("arith::dio") << "DioSolver::printQueue()" << endl;
559 [ - - ]: 0 : for(TrailIndex i = 0, last = d_trail.size(); i < last; ++i){
560 [ - - ]: 0 : Trace("arith::dio") << "d_trail[i].d_eq = " << d_trail[i].d_eq.getNode() << endl;
561 [ - - ]: 0 : Trace("arith::dio") << "d_trail[i].d_proof = " << d_trail[i].d_proof.getNode() << endl;
562 : : }
563 : :
564 [ - - ]: 0 : Trace("arith::dio") << "DioSolver::printSubs()" << endl;
565 [ - - ]: 0 : for(SubIndex si=0, sN=d_subs.size(); si < sN; ++si){
566 [ - - ]: 0 : Trace("arith::dio") << "d_subs[i] = {"
567 : 0 : << "d_fresh="<< d_subs[si].d_fresh <<","
568 : 0 : << "d_eliminated="<< d_subs[si].d_eliminated.getNode() <<","
569 : 0 : << "d_constraint="<< d_subs[si].d_constraint <<"}" << endl;
570 [ - - ]: 0 : Trace("arith::dio") << "d_trail[d_subs[i].d_constraint].d_eq="
571 : 0 : << d_trail[d_subs[si].d_constraint].d_eq.getNode() << endl;
572 : : }
573 : 0 : }
574 : :
575 : 41655 : DioSolver::TrailIndex DioSolver::applyAllSubstitutionsToIndex(DioSolver::TrailIndex trailIndex){
576 : 41655 : TrailIndex currentIndex = trailIndex;
577 [ + + ]: 403968 : for(SubIndex subIter = 0, siEnd = d_subs.size(); subIter < siEnd; ++subIter){
578 : 362313 : currentIndex = applySubstitution(subIter, currentIndex);
579 : : }
580 : 41655 : return currentIndex;
581 : : }
582 : :
583 : 1302881 : bool DioSolver::debugSubstitutionApplies(DioSolver::SubIndex si, DioSolver::TrailIndex ti){
584 : 1302881 : Variable var = d_subs[si].d_eliminated;
585 : :
586 : 1302881 : const SumPair& curr = d_trail[ti].d_eq;
587 : 1302881 : Polynomial vsum = curr.getPolynomial();
588 : :
589 : 2605762 : Constant a = vsum.getCoefficient(VarList(var));
590 : 2605762 : return !a.isZero();
591 : 1302881 : }
592 : :
593 : 91325 : bool DioSolver::debugAnySubstitionApplies(DioSolver::TrailIndex i){
594 [ + + ]: 1394206 : for(SubIndex subIter = 0, siEnd = d_subs.size(); subIter < siEnd; ++subIter){
595 [ - + ]: 1302881 : if(debugSubstitutionApplies(subIter, i)){
596 : 0 : return true;
597 : : }
598 : : }
599 : 91325 : return false;
600 : : }
601 : :
602 : 27555 : std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::solveIndex(DioSolver::TrailIndex i){
603 : 27555 : const SumPair& si = d_trail[i].d_eq;
604 : :
605 [ + - ]: 27555 : Trace("arith::dio") << "before solveIndex("<<i<<":"<<si.getNode()<< ")" << endl;
606 : :
607 : : #ifdef CVC5_ASSERTIONS
608 : 27555 : const Polynomial& p = si.getPolynomial();
609 : : #endif
610 : :
611 [ - + ][ - + ]: 27555 : Assert(p.isIntegral());
[ - - ]
612 : :
613 [ - + ][ - + ]: 27555 : Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
[ - - ]
614 : 27555 : const Monomial av = d_trail[i].d_minimalMonomial;
615 : :
616 : 27555 : VarList vl = av.getVarList();
617 [ - + ][ - + ]: 27555 : Assert(vl.singleton());
[ - - ]
618 : 27555 : Variable var = vl.getHead();
619 : 27555 : Constant a = av.getConstant();
620 : 27555 : Integer a_abs = a.getValue().getNumerator().abs();
621 : :
622 [ - + ][ - + ]: 27555 : Assert(a_abs == 1);
[ - - ]
623 : :
624 [ + + ][ + + ]: 27555 : TrailIndex ci = !a.isNegative() ? scaleEqAtIndex(i, Integer(-1)) : i;
[ - - ]
625 : :
626 : 27555 : SubIndex subBy = d_subs.size();
627 : 27555 : d_subs.push_back(Substitution(Node::null(), var, ci));
628 : :
629 [ + - ]: 27555 : Trace("arith::dio") << "after solveIndex " << d_trail[ci].d_eq.getNode() << " for " << av.getNode() << endl;
630 [ - + ][ - + ]: 137775 : AssertEqual(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl),
[ - - ]
631 : : Constant::mkConstant(nodeManager(), -1));
632 : :
633 : 55110 : return make_pair(subBy, i);
634 : 27555 : }
635 : :
636 : 1474 : std::pair<DioSolver::SubIndex, DioSolver::TrailIndex> DioSolver::decomposeIndex(DioSolver::TrailIndex i){
637 : 1474 : const SumPair& si = d_trail[i].d_eq;
638 : :
639 : 1474 : d_usedDecomposeIndex = true;
640 : :
641 [ + - ]: 1474 : Trace("arith::dio") << "before decomposeIndex("<<i<<":"<<si.getNode()<< ")" << endl;
642 : :
643 : : #ifdef CVC5_ASSERTIONS
644 : 1474 : const Polynomial& p = si.getPolynomial();
645 : : #endif
646 : :
647 [ - + ][ - + ]: 1474 : Assert(p.isIntegral());
[ - - ]
648 : :
649 [ - + ][ - + ]: 1474 : Assert(p.selectAbsMinimum() == d_trail[i].d_minimalMonomial);
[ - - ]
650 : 1474 : const Monomial& av = d_trail[i].d_minimalMonomial;
651 : :
652 : 1474 : VarList vl = av.getVarList();
653 [ - + ][ - + ]: 1474 : Assert(vl.singleton());
[ - - ]
654 : 1474 : Variable var = vl.getHead();
655 : 1474 : Constant a = av.getConstant();
656 : 1474 : Integer a_abs = a.getValue().getNumerator().abs();
657 : :
658 [ - + ][ - + ]: 1474 : Assert(a_abs > 1);
[ - - ]
659 : :
660 : : //It is not sufficient to reduce the case where abs(a) == 1 to abs(a) > 1.
661 : : //We need to handle both cases seperately to ensure termination.
662 : 1474 : Node qr = SumPair::computeQR(si, a.getValue().getNumerator());
663 : :
664 [ - + ][ - + ]: 1474 : Assert(qr.getKind() == Kind::ADD);
[ - - ]
665 [ - + ][ - + ]: 1474 : Assert(qr.getNumChildren() == 2);
[ - - ]
666 : 2948 : SumPair q = SumPair::parseSumPair(qr[0]);
667 : 2948 : SumPair r = SumPair::parseSumPair(qr[1]);
668 : :
669 : 1474 : NodeManager* nm = nodeManager();
670 [ - + ][ - + ]: 7370 : AssertEqual(q.getPolynomial().getCoefficient(vl),
[ - - ]
671 : : Constant::mkConstant(nm, 1));
672 : :
673 [ - + ][ - + ]: 1474 : Assert(!r.isZero());
[ - - ]
674 : 1474 : Node freshNode = makeIntegerVariable(nodeManager());
675 : 1474 : Variable fresh(freshNode);
676 : 1474 : SumPair fresh_one=SumPair::mkSumPair(fresh);
677 : 1474 : SumPair fresh_a = fresh_one * a;
678 : :
679 : 1474 : SumPair newSI = SumPair(fresh_one) - q;
680 : : // this normalizes the coefficient of var to -1
681 : :
682 : :
683 : 1474 : TrailIndex ci = d_trail.size();
684 : 1474 : d_trail.push_back(Constraint(newSI, Polynomial::mkZero(nm)));
685 : : // no longer reference av safely!
686 : 1474 : addTrailElementAsLemma(ci);
687 : :
688 [ + - ]: 2948 : Trace("arith::dio") << "Decompose ci(" << ci <<":" << d_trail[ci].d_eq.getNode()
689 : 1474 : << ") for " << d_trail[i].d_minimalMonomial.getNode() << endl;
690 [ - + ][ - + ]: 7370 : AssertEqual(d_trail[ci].d_eq.getPolynomial().getCoefficient(vl),
[ - - ]
691 : : Constant::mkConstant(nm, -1));
692 : :
693 : 1474 : SumPair newFact = r + fresh_a;
694 : :
695 : 1474 : TrailIndex nextIndex = d_trail.size();
696 : 1474 : d_trail.push_back(Constraint(newFact, d_trail[i].d_proof));
697 : :
698 : 1474 : SubIndex subBy = d_subs.size();
699 : 1474 : d_subs.push_back(Substitution(freshNode, var, ci));
700 : :
701 [ + - ]: 1474 : Trace("arith::dio") << "Decompose nextIndex " << d_trail[nextIndex].d_eq.getNode() << endl;
702 : 2948 : return make_pair(subBy, nextIndex);
703 : 1474 : }
704 : :
705 : :
706 : 877836 : DioSolver::TrailIndex DioSolver::applySubstitution(DioSolver::SubIndex si, DioSolver::TrailIndex ti){
707 : 877836 : Variable var = d_subs[si].d_eliminated;
708 : 877836 : TrailIndex subIndex = d_subs[si].d_constraint;
709 : :
710 : 877836 : const SumPair& curr = d_trail[ti].d_eq;
711 : 877836 : Polynomial vsum = curr.getPolynomial();
712 : :
713 : 1755672 : Constant a = vsum.getCoefficient(VarList(var));
714 [ - + ][ - + ]: 877836 : Assert(a.isIntegral());
[ - - ]
715 [ + + ]: 877836 : if(!a.isZero()){
716 : 44720 : Integer one(1);
717 : 44720 : TrailIndex afterSub = combineEqAtIndexes(ti, one, subIndex, a.getValue().getNumerator());
718 [ - + ][ - + ]: 44720 : Assert(d_trail[afterSub]
[ - - ]
719 : : .d_eq.getPolynomial()
720 : : .getCoefficient(VarList(var))
721 : : .isZero());
722 : 44720 : return afterSub;
723 : 44720 : }else{
724 : 833116 : return ti;
725 : : }
726 : 877836 : }
727 : :
728 : :
729 : 63266 : DioSolver::TrailIndex DioSolver::reduceByGCD(DioSolver::TrailIndex ti){
730 : 63266 : const SumPair& sp = d_trail[ti].d_eq;
731 : 63266 : Polynomial vsum = sp.getPolynomial();
732 : 63266 : Constant c = sp.getConstant();
733 : :
734 [ + - ]: 63266 : Trace("arith::dio") << "reduceByGCD " << vsum.getNode() << endl;
735 [ - + ][ - + ]: 63266 : Assert(!vsum.isConstant());
[ - - ]
736 : 63266 : Integer g = vsum.gcd();
737 [ - + ][ - + ]: 63266 : Assert(g >= 1);
[ - - ]
738 [ + - ]: 63266 : Trace("arith::dio") << "gcd("<< vsum.getNode() <<")=" << g << " " << c.getValue() << endl;
739 [ + + ]: 63266 : if(g.divides(c.getValue().getNumerator())){
740 [ + + ]: 61158 : if(g > 1){
741 : 2303 : return scaleEqAtIndex(ti, g);
742 : : }else{
743 : 58855 : return ti;
744 : : }
745 : : }else{
746 : 2108 : raiseConflict(ti);
747 : 2108 : return ti;
748 : : }
749 : 63266 : }
750 : :
751 : 200750 : bool DioSolver::triviallySat(TrailIndex i){
752 : 200750 : const SumPair& eq = d_trail[i].d_eq;
753 [ + + ]: 200750 : if(eq.isConstant()){
754 : 4837 : return eq.getConstant().isZero();
755 : : }else{
756 : 195913 : return false;
757 : : }
758 : : }
759 : :
760 : 199823 : bool DioSolver::triviallyUnsat(DioSolver::TrailIndex i){
761 : 199823 : const SumPair& eq = d_trail[i].d_eq;
762 [ + + ]: 199823 : if(eq.isConstant()){
763 : 3910 : return !eq.getConstant().isZero();
764 : : }else{
765 : 195913 : return false;
766 : : }
767 : : }
768 : :
769 : :
770 : 91325 : bool DioSolver::gcdIsOne(DioSolver::TrailIndex i){
771 : 91325 : const SumPair& eq = d_trail[i].d_eq;
772 : 91325 : return eq.gcd() == Integer(1);
773 : : }
774 : :
775 : 29029 : void DioSolver::subAndReduceCurrentFByIndex(DioSolver::SubIndex subIndex){
776 : 29029 : size_t N = d_currentF.size();
777 : :
778 : 29029 : size_t readIter = 0, writeIter = 0;
779 [ + + ][ + + ]: 544552 : for(; readIter < N && !inConflict(); ++readIter){
[ + + ]
780 : 515523 : TrailIndex curr = d_currentF[readIter];
781 : 515523 : TrailIndex nextTI = applySubstitution(subIndex, curr);
782 [ + + ]: 515523 : if(nextTI == curr){
783 : 489075 : d_currentF[writeIter] = curr;
784 : 489075 : ++writeIter;
785 : : }else{
786 [ - + ][ - + ]: 26448 : Assert(nextTI != curr);
[ - - ]
787 : :
788 [ - + ]: 26448 : if(triviallyUnsat(nextTI)){
789 : 0 : raiseConflict(nextTI);
790 [ + + ]: 26448 : }else if(!triviallySat(nextTI)){
791 : 22538 : TrailIndex nextNextTI = reduceByGCD(nextTI);
792 : :
793 [ + + ][ + + ]: 22538 : if(!(inConflict() || anyCoefficientExceedsMaximum(nextNextTI))){
[ + + ]
794 [ - + ][ - + ]: 21002 : Assert(queueConditions(nextNextTI));
[ - - ]
795 : 21002 : d_currentF[writeIter] = nextNextTI;
796 : 21002 : ++writeIter;
797 : : }
798 : : }
799 : : }
800 : : }
801 [ + + ][ + + ]: 29029 : if(!inConflict() && writeIter < N){
[ + + ]
802 : 2821 : d_currentF.resize(writeIter);
803 : : }
804 : 29029 : }
805 : :
806 : 1474 : void DioSolver::addTrailElementAsLemma(TrailIndex i) {
807 [ - + ]: 1474 : if (options().arith.exportDioDecompositions)
808 : : {
809 : 0 : d_decompositionLemmaQueue.push(i);
810 : : }
811 : 1474 : }
812 : :
813 : 0 : Node DioSolver::trailIndexToEquality(TrailIndex i) const {
814 : 0 : const SumPair& sp = d_trail[i].d_eq;
815 : 0 : Node n = sp.getNode();
816 : 0 : Node zero = nodeManager()->mkConstRealOrInt(n.getType(), Rational(0));
817 : 0 : Node eq = n.eqNode(zero);
818 : 0 : return eq;
819 : 0 : }
820 : :
821 : : } // namespace arith
822 : : } // namespace theory
823 : : } // namespace cvc5::internal
|
