GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/dio_solver.h Lines: 30 39 76.9 %
Date: 2021-03-23 Branches: 18 112 16.1 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file dio_solver.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief Diophantine equation solver
13
 **
14
 ** A Diophantine equation solver for the theory of arithmetic.
15
 **/
16
17
#include "cvc4_private.h"
18
19
20
#ifndef CVC4__THEORY__ARITH__DIO_SOLVER_H
21
#define CVC4__THEORY__ARITH__DIO_SOLVER_H
22
23
#include <unordered_map>
24
#include <utility>
25
#include <vector>
26
27
#include "context/cdlist.h"
28
#include "context/cdmaybe.h"
29
#include "context/cdo.h"
30
#include "context/cdqueue.h"
31
#include "theory/arith/normal_form.h"
32
#include "util/rational.h"
33
#include "util/statistics_registry.h"
34
#include "util/stats_timer.h"
35
36
namespace CVC4 {
37
namespace context {
38
class Context;
39
}
40
namespace theory {
41
namespace arith {
42
43
8994
class DioSolver {
44
private:
45
  typedef size_t TrailIndex;
46
  typedef size_t InputConstraintIndex;
47
  typedef size_t SubIndex;
48
49
  std::vector<Variable> d_proofVariablePool;
50
  /** Sat context dependent. */
51
  context::CDO<size_t> d_lastUsedProofVariable;
52
53
  /**
54
   * The set of input constraints is stored in a CDList.
55
   * Each constraint point to an element of the trail.
56
   */
57
96522
  struct InputConstraint {
58
    Node d_reason;
59
    TrailIndex d_trailPos;
60
32174
    InputConstraint(Node reason, TrailIndex pos) : d_reason(reason), d_trailPos(pos) {}
61
  };
62
  context::CDList<InputConstraint> d_inputConstraints;
63
64
  /**
65
   * This is the next input constraint to handle.
66
   */
67
  context::CDO<size_t> d_nextInputConstraintToEnqueue;
68
69
70
  /**
71
   * We maintain a map from the variables associated with proofs to an input constraint.
72
   * These variables can then be used in polynomial manipulations.
73
   */
74
  typedef std::unordered_map<Node, InputConstraintIndex, NodeHashFunction> NodeToInputConstraintIndexMap;
75
  NodeToInputConstraintIndexMap d_varToInputConstraintMap;
76
77
455
  Node proofVariableToReason(const Variable& v) const{
78
455
    Assert(d_varToInputConstraintMap.find(v.getNode())
79
           != d_varToInputConstraintMap.end());
80
455
    InputConstraintIndex pos = (*(d_varToInputConstraintMap.find(v.getNode()))).second;
81
455
    Assert(pos < d_inputConstraints.size());
82
455
    return d_inputConstraints[pos].d_reason;
83
  }
84
85
  /**
86
   * The main work horse of the algorithm, the trail of constraints.
87
   * Each constraint is a SumPair that implicitly represents an equality against 0.
88
   *   d_trail[i].d_eq = (+ c (+ [(* coeff var)])) representing (+ [(* coeff var)]) = -c
89
   * Each constraint has a proof in terms of a linear combination of the input constraints.
90
   *   d_trail[i].d_proof
91
   *
92
   * Each Constraint also a monomial in d_eq.getPolynomial()
93
   * of minimal absolute value by the coefficients.
94
   * d_trail[i].d_minimalMonomial
95
   *
96
   * See Alberto's paper for how linear proofs are maintained for the abstract
97
   * state machine in rules (7), (8) and (9).
98
   */
99
256425
  struct Constraint {
100
    SumPair d_eq;
101
    Polynomial d_proof;
102
    Monomial d_minimalMonomial;
103
85475
    Constraint(const SumPair& eq, const Polynomial& p) :
104
85475
      d_eq(eq), d_proof(p), d_minimalMonomial(d_eq.getPolynomial().selectAbsMinimum())
105
85475
    {}
106
  };
107
  context::CDList<Constraint> d_trail;
108
109
  // /** Compare by d_minimal. */
110
  // struct TrailMinimalCoefficientOrder {
111
  //   const context::CDList<Constraint>& d_trail;
112
  //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
113
  //     d_trail(trail)
114
  //   {}
115
116
  //   bool operator()(TrailIndex i, TrailIndex j){
117
  //     return d_trail[i].d_minimalMonomial.absLessThan(d_trail[j].d_minimalMonomial);
118
  //   }
119
  // };
120
121
  /**
122
   * A substitution is stored as a constraint in the trail together with
123
   * the variable to be eliminated, and a fresh variable if one was introduced.
124
   * The variable d_subs[i].d_eliminated is substituted using the implicit equality in
125
   * d_trail[d_subs[i].d_constraint]
126
   *  - d_subs[i].d_eliminated is normalized to have coefficient -1 in
127
   *    d_trail[d_subs[i].d_constraint].
128
   *  - d_subs[i].d_fresh is either Node::null() or it is variable it is normalized
129
   *    to have coefficient 1 in d_trail[d_subs[i].d_constraint].
130
   */
131
58092
  struct Substitution {
132
    Node d_fresh;
133
    Variable d_eliminated;
134
    TrailIndex d_constraint;
135
19364
    Substitution(Node f, const Variable& e, TrailIndex c) :
136
19364
      d_fresh(f), d_eliminated(e), d_constraint(c)
137
19364
    {}
138
  };
139
  context::CDList<Substitution> d_subs;
140
141
  /**
142
   * This is the queue of constraints to be processed in the current context level.
143
   * This is to be empty upon entering solver and cleared upon leaving the solver.
144
   *
145
   * All elements in currentF:
146
   * - are fully substituted according to d_subs.
147
   * - !isConstant().
148
   * - If the element is (+ constant (+ [(* coeff var)] )), then the gcd(coeff) = 1
149
   */
150
  std::deque<TrailIndex> d_currentF;
151
  context::CDList<TrailIndex> d_savedQueue;
152
  context::CDO<size_t> d_savedQueueIndex;
153
  context::CDMaybe<TrailIndex> d_conflictIndex;
154
155
  /**
156
   * Drop derived constraints with a coefficient length larger than
157
   * the maximum input constraints length than 2**MAX_GROWTH_RATE.
158
   */
159
  context::CDO<uint32_t> d_maxInputCoefficientLength;
160
  static const uint32_t MAX_GROWTH_RATE = 3;
161
162
  /** Returns true if the element on the trail should be dropped.*/
163
  bool anyCoefficientExceedsMaximum(TrailIndex j) const;
164
165
  /**
166
   * Is true if decomposeIndex has been used in this context.
167
   */
168
  context::CDO<bool> d_usedDecomposeIndex;
169
170
  context::CDO<SubIndex> d_lastPureSubstitution;
171
  context::CDO<SubIndex> d_pureSubstitionIter;
172
173
  /**
174
   * Decomposition lemma queue.
175
   */
176
  context::CDQueue<TrailIndex> d_decompositionLemmaQueue;
177
178
public:
179
180
  /** Construct a Diophantine equation solver with the given context. */
181
  DioSolver(context::Context* ctxt);
182
183
  /** Returns true if the substitutions use no new variables. */
184
  bool hasMorePureSubstitutions() const{
185
    return d_pureSubstitionIter < d_lastPureSubstitution;
186
  }
187
188
  Node nextPureSubstitution();
189
190
  /**
191
   * Adds an equality to the queue of the DioSolver.
192
   * orig is blamed in a conflict.
193
   * orig can either be of the form (= p c) or (and ub lb).
194
   * where ub is either (leq p c) or (not (> p [- c 1])), and
195
   * where lb is either (geq p c) or (not (< p [+ c 1]))
196
   *
197
   * If eq cannot be used, this constraint is dropped.
198
   */
199
  void pushInputConstraint(const Comparison& eq, Node reason);
200
201
  /**
202
   * Processes the queue looking for any conflict.
203
   * If a conflict is found, this returns conflict.
204
   * Otherwise, it returns null.
205
   * The conflict is guarenteed to be over literals given in addEquality.
206
   */
207
  Node processEquationsForConflict();
208
209
  /**
210
   * Processes the queue looking for an integer unsatisfiable cutting plane.
211
   * If such a plane is found this returns an entailed plane using no
212
   * fresh variables.
213
   */
214
  SumPair processEquationsForCut();
215
216
private:
217
  /** Returns true if the TrailIndex refers to a element in the trail. */
218
19498
  bool inRange(TrailIndex i) const{
219
19498
    return i < d_trail.size();
220
  }
221
222
  Node columnGcdIsOne() const;
223
224
225
  /**
226
   * Returns true if the context dependent flag for conflicts
227
   * has been raised.
228
   */
229
877209
  bool inConflict() const { return d_conflictIndex.isSet(); }
230
231
  /** Raises a conflict at the index ti. */
232
1333
  void raiseConflict(TrailIndex ti){
233
1333
    Assert(!inConflict());
234
1333
    d_conflictIndex.set(ti);
235
1333
  }
236
237
  /** Returns the conflict index. */
238
1333
  TrailIndex getConflictIndex() const{
239
1333
    Assert(inConflict());
240
1333
    return d_conflictIndex.get();
241
  }
242
243
  /**
244
   * Allocates a "unique" proof variable.
245
   * This variable is fresh with respect to the context.
246
   * Returns index of the variable in d_variablePool;
247
   */
248
  size_t allocateProofVariable();
249
250
251
  /** Empties the unproccessed input constraints into the queue. */
252
  void enqueueInputConstraints();
253
254
  /**
255
   * Returns true if an input equality is in the map.
256
   * This is expensive and is only for debug assertions.
257
   */
258
  bool debugEqualityInInputEquations(Node eq);
259
260
  /** Applies the substitution at subIndex to currentF. */
261
  void subAndReduceCurrentFByIndex(SubIndex d_subIndex);
262
263
  /**
264
   * Takes as input a TrailIndex i and an integer that divides d_trail[i].d_eq, and
265
   * returns a TrailIndex j s.t.
266
   *   d_trail[j].d_eq = (1/g) d_trail[i].d_eq
267
   * and
268
   *   d_trail[j].d_proof = (1/g) d_trail[i].d_proof.
269
   *
270
   * g must be non-zero.
271
   *
272
   * This corresponds to an application of Alberto's rule (7).
273
   */
274
  TrailIndex scaleEqAtIndex(TrailIndex i, const Integer& g);
275
276
277
  /**
278
   * Takes as input TrailIndex's i and j and Integer's q and r and a TrailIndex k s.t.
279
   *   d_trail[k].d_eq == d_trail[i].d_eq * q + d_trail[j].d_eq * r
280
   * and
281
   *   d_trail[k].d_proof == d_trail[i].d_proof * q + d_trail[j].d_proof * r
282
   *
283
   * This corresponds to an application of Alberto's rule (8).
284
   */
285
  TrailIndex combineEqAtIndexes(TrailIndex i, const Integer& q, TrailIndex j, const Integer& r);
286
287
  /**
288
   * Decomposes the equation at index ti of trail by the variable
289
   * with the lowest coefficient.
290
   * This corresponds to an application of Alberto's rule (9).
291
   *
292
   * Returns a pair of a SubIndex and a TrailIndex.
293
   * The SubIndex is the index of a newly introduced substition.
294
   */
295
  std::pair<SubIndex, TrailIndex> decomposeIndex(TrailIndex ti);
296
297
  /** Solves the index at ti for the value in minimumMonomial. */
298
  std::pair<SubIndex, TrailIndex> solveIndex(TrailIndex ti);
299
300
  /** Prints the queue for debugging purposes to Debug("arith::dio"). */
301
  void printQueue();
302
303
  /**
304
   * Exhaustively applies all substitutions discovered to an element of the trail.
305
   * Returns a TrailIndex corresponding to the substitutions being applied.
306
   */
307
  TrailIndex applyAllSubstitutionsToIndex(TrailIndex i);
308
309
  /**
310
   * Applies a substitution to an element in the trail.
311
   */
312
  TrailIndex applySubstitution(SubIndex s, TrailIndex i);
313
314
  /**
315
   * Reduces the trail node at i by the gcd of the variables.
316
   * Returns the new trail element.
317
   *
318
   * This raises the conflict flag if unsat is detected.
319
   */
320
  TrailIndex reduceByGCD(TrailIndex i);
321
322
  /**
323
   * Returns true if i'th element in the trail is trivially true.
324
   * (0 = 0)
325
   */
326
  bool triviallySat(TrailIndex t);
327
328
  /**
329
   * Returns true if i'th element in the trail is trivially unsatisfiable.
330
   * (1 = 0)
331
   */
332
  bool triviallyUnsat(TrailIndex t);
333
334
  /** Returns true if the gcd of the i'th element of the trail is 1.*/
335
  bool gcdIsOne(TrailIndex t);
336
337
  bool debugAnySubstitionApplies(TrailIndex t);
338
  bool debugSubstitutionApplies(SubIndex si, TrailIndex ti);
339
340
341
  /** Returns true if the queue of nodes to process is empty. */
342
  bool queueEmpty() const;
343
344
  bool queueConditions(TrailIndex t);
345
346
347
29133
  void pushToQueueBack(TrailIndex t){
348
29133
    Assert(queueConditions(t));
349
29133
    d_currentF.push_back(t);
350
29133
  }
351
352
  void pushToQueueFront(TrailIndex t){
353
    Assert(queueConditions(t));
354
    d_currentF.push_front(t);
355
  }
356
357
  /**
358
   * Moves the minimum Constraint by absolute value of the minimum coefficient to
359
   * the front of the queue.
360
   */
361
  void moveMinimumByAbsToQueueFront();
362
363
  void saveQueue();
364
365
  TrailIndex impliedGcdOfOne();
366
367
368
  /**
369
   * Processing the current set of equations.
370
   *
371
   * decomposeIndex() rule is only applied if allowDecomposition is true.
372
   */
373
  bool processEquations(bool allowDecomposition);
374
375
  /**
376
   * Constructs a proof from any d_trail[i] in terms of input literals.
377
   */
378
  Node proveIndex(TrailIndex i);
379
380
  /**
381
   * Returns the SumPair in d_trail[i].d_eq with all of the fresh variables purified out.
382
   */
383
  SumPair purifyIndex(TrailIndex i);
384
385
386
  void debugPrintTrail(TrailIndex i) const;
387
388
public:
389
  bool hasMoreDecompositionLemmas() const{
390
    return !d_decompositionLemmaQueue.empty();
391
  }
392
  Node nextDecompositionLemma() {
393
    Assert(hasMoreDecompositionLemmas());
394
    TrailIndex front = d_decompositionLemmaQueue.front();
395
    d_decompositionLemmaQueue.pop();
396
    return trailIndexToEquality(front);
397
  }
398
private:
399
  Node trailIndexToEquality(TrailIndex i) const;
400
  void addTrailElementAsLemma(TrailIndex i);
401
402
public:
403
404
  /** These fields are designed to be accessible to TheoryArith methods. */
405
  class Statistics {
406
  public:
407
408
    IntStat d_conflictCalls;
409
    IntStat d_cutCalls;
410
411
    IntStat d_cuts;
412
    IntStat d_conflicts;
413
414
    TimerStat d_conflictTimer;
415
    TimerStat d_cutTimer;
416
417
    Statistics();
418
    ~Statistics();
419
  };
420
421
  Statistics d_statistics;
422
};/* class DioSolver */
423
424
}/* CVC4::theory::arith namespace */
425
}/* CVC4::theory namespace */
426
}/* CVC4 namespace */
427
428
#endif /* CVC4__THEORY__ARITH__DIO_SOLVER_H */