GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/theory_arith_private.h Lines: 28 33 84.8 %
Date: 2021-03-22 Branches: 6 28 21.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_arith_private.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andrew Reynolds, Alex Ozdemir
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#pragma once
19
20
#include <map>
21
#include <vector>
22
23
#include "context/cdhashset.h"
24
#include "context/cdinsert_hashmap.h"
25
#include "context/cdlist.h"
26
#include "context/cdqueue.h"
27
#include "expr/kind.h"
28
#include "expr/node.h"
29
#include "expr/node_builder.h"
30
#include "theory/arith/arith_static_learner.h"
31
#include "theory/arith/arith_utilities.h"
32
#include "theory/arith/arithvar.h"
33
#include "theory/arith/attempt_solution_simplex.h"
34
#include "theory/arith/congruence_manager.h"
35
#include "theory/arith/constraint.h"
36
#include "theory/arith/delta_rational.h"
37
#include "theory/arith/dio_solver.h"
38
#include "theory/arith/dual_simplex.h"
39
#include "theory/arith/error_set.h"
40
#include "theory/arith/fc_simplex.h"
41
#include "theory/arith/infer_bounds.h"
42
#include "theory/arith/linear_equality.h"
43
#include "theory/arith/matrix.h"
44
#include "theory/arith/normal_form.h"
45
#include "theory/arith/partial_model.h"
46
#include "theory/arith/proof_checker.h"
47
#include "theory/arith/soi_simplex.h"
48
#include "theory/arith/theory_arith.h"
49
#include "theory/trust_node.h"
50
#include "theory/valuation.h"
51
#include "util/dense_map.h"
52
#include "util/integer.h"
53
#include "util/rational.h"
54
#include "util/result.h"
55
#include "util/statistics_registry.h"
56
57
namespace CVC4 {
58
namespace theory {
59
60
class EagerProofGenerator;
61
class TheoryModel;
62
63
namespace arith {
64
65
class BranchCutInfo;
66
class TreeLog;
67
class ApproximateStatistics;
68
69
class ArithEntailmentCheckParameters;
70
class ArithEntailmentCheckSideEffects;
71
namespace inferbounds {
72
  class InferBoundAlgorithm;
73
}
74
class InferBoundsResult;
75
76
/**
77
 * Implementation of QF_LRA.
78
 * Based upon:
79
 * http://research.microsoft.com/en-us/um/people/leonardo/cav06.pdf
80
 */
81
class TheoryArithPrivate {
82
private:
83
84
  static const uint32_t RESET_START = 2;
85
86
  TheoryArith& d_containing;
87
88
  /**
89
   * Whether we encountered non-linear arithmetic at any time during solving.
90
   */
91
  bool d_foundNl;
92
93
  BoundInfoMap d_rowTracking;
94
95
  // For proofs
96
  /** Manages the proof nodes of this theory. */
97
  ProofNodeManager* d_pnm;
98
  /** Checks the proof rules of this theory. */
99
  ArithProofRuleChecker d_checker;
100
  /** Stores proposition(node)/proof pairs. */
101
  std::unique_ptr<EagerProofGenerator> d_pfGen;
102
103
  /**
104
   * The constraint database associated with the theory.
105
   * This must be declared before ArithPartialModel.
106
   */
107
  ConstraintDatabase d_constraintDatabase;
108
109
  enum Result::Sat d_qflraStatus;
110
  // check()
111
  //   !done() -> d_qflraStatus = Unknown
112
  //   fullEffort(e) -> simplex returns either sat or unsat
113
  //   !fullEffort(e) -> simplex returns either sat, unsat or unknown
114
  //                     if unknown, save the assignment
115
  //                     if unknown, the simplex priority queue cannot be emptied
116
  int d_unknownsInARow;
117
118
  bool d_replayedLemmas;
119
120
  /**
121
   * This counter is false if nothing has been done since the last cut.
122
   * This is used to break an infinite loop.
123
   */
124
  bool d_hasDoneWorkSinceCut;
125
126
  /** Static learner. */
127
  ArithStaticLearner d_learner;
128
129
  //std::vector<ArithVar> d_pool;
130
public:
131
  void releaseArithVar(ArithVar v);
132
5608372
  void signal(ArithVar v){ d_errorSet.signalVariable(v); }
133
134
135
private:
136
  // t does not contain constants
137
  void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
138
  void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
139
140
  std::pair<Node, DeltaRational> entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out);
141
142
  //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p);
143
  //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p);
144
  //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p);
145
146
  /**
147
   * Infers either a new upper/lower bound on term in the real relaxation.
148
   * Either:
149
   * - term is malformed (see below)
150
   * - a maximum/minimum is found with the result being a pair
151
   * -- <dr, exp> where
152
   * -- term <?> dr is implies by exp
153
   * -- <?> is <= if inferring an upper bound, >= otherwise
154
   * -- exp is in terms of the assertions to the theory.
155
   * - No upper or lower bound is inferrable in the real relaxation.
156
   * -- Returns <0, Null()>
157
   * - the maximum number of rounds was exhausted:
158
   * -- Returns <v, term> where v is the current feasible value of term
159
   * - Threshold reached:
160
   * -- If theshold != NULL, and a feasible value is found to exceed threshold
161
   * -- Simplex stops and returns <threshold, term>
162
   */
163
  //std::pair<DeltaRational, Node> inferBound(TNode term, bool lb, int maxRounds = -1, const DeltaRational* threshold = NULL);
164
165
private:
166
  static bool decomposeTerm(Node term, Rational& m, Node& p, Rational& c);
167
  static bool decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm,  Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep);
168
  static void setToMin(int sgn, std::pair<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e);
169
170
  /**
171
   * The map between arith variables to nodes.
172
   */
173
  //ArithVarNodeMap d_arithvarNodeMap;
174
175
  typedef ArithVariables::var_iterator var_iterator;
176
1803654
  var_iterator var_begin() const { return d_partialModel.var_begin(); }
177
1803654
  var_iterator var_end() const { return d_partialModel.var_end(); }
178
179
  NodeSet d_setupNodes;
180
public:
181
5421897
  bool isSetup(Node n) const {
182
5421897
    return d_setupNodes.find(n) != d_setupNodes.end();
183
  }
184
390651
  void markSetup(Node n){
185
390651
    Assert(!isSetup(n));
186
390651
    d_setupNodes.insert(n);
187
390651
  }
188
private:
189
  void setupVariable(const Variable& x);
190
  void setupVariableList(const VarList& vl);
191
  void setupPolynomial(const Polynomial& poly);
192
public:
193
  void setupAtom(TNode atom);
194
private:
195
  void cautiousSetupPolynomial(const Polynomial& p);
196
197
  /**
198
   * A superset of all of the assertions that currently are not the literal for
199
   * their constraint do not match constraint literals. Not just the witnesses.
200
   */
201
  context::CDInsertHashMap<Node, ConstraintP, NodeHashFunction> d_assertionsThatDoNotMatchTheirLiterals;
202
203
204
  /** Returns true if x is of type Integer. */
205
18748123
  inline bool isInteger(ArithVar x) const {
206
18748123
    return d_partialModel.isInteger(x);
207
  }
208
209
210
  /** Returns true if the variable was initially introduced as an auxiliary variable. */
211
680781
  inline bool isAuxiliaryVariable(ArithVar x) const{
212
680781
    return d_partialModel.isAuxiliary(x);
213
  }
214
215
680263101
  inline bool isIntegerInput(ArithVar x) const {
216
680263101
    return d_partialModel.isIntegerInput(x);
217
  }
218
219
  /**
220
   * On full effort checks (after determining LA(Q) satisfiability), we
221
   * consider integer vars, but we make sure to do so fairly to avoid
222
   * nontermination (although this isn't a guarantee).  To do it fairly,
223
   * we consider variables in round-robin fashion.  This is the
224
   * round-robin index.
225
   */
226
  ArithVar d_nextIntegerCheckVar;
227
228
  /**
229
   * Queue of Integer variables that are known to be equal to a constant.
230
   */
231
  context::CDQueue<ArithVar> d_constantIntegerVariables;
232
233
  Node callDioSolver();
234
  /**
235
   * Produces lemmas of the form (or (>= f 0) (<= f 0)),
236
   * where f is a plane that the diophantine solver is interested in.
237
   *
238
   * More precisely, produces lemmas of the form (or (>= lc -c) (<= lc -c))
239
   * where lc is a linear combination of variables, c is a constant, and lc + c
240
   * is the plane.
241
   */
242
  TrustNode dioCutting();
243
244
  Comparison mkIntegerEqualityFromAssignment(ArithVar v);
245
246
  /**
247
   * List of all of the disequalities asserted in the current context that are not known
248
   * to be satisfied.
249
   */
250
  context::CDQueue<ConstraintP> d_diseqQueue;
251
252
  /**
253
   * Constraints that have yet to be processed by proagation work list.
254
   * All of the elements have type of LowerBound, UpperBound, or
255
   * Equality.
256
   *
257
   * This is empty at the beginning of every check call.
258
   *
259
   * If head()->getType() == LowerBound or UpperBound,
260
   * then d_cPL[1] is the previous constraint in d_partialModel for the
261
   * corresponding bound.
262
   * If head()->getType() == Equality,
263
   * then d_cPL[1] is the previous lowerBound in d_partialModel,
264
   * and d_cPL[2] is the previous upperBound in d_partialModel.
265
   */
266
  std::deque<ConstraintP> d_currentPropagationList;
267
268
  context::CDQueue<ConstraintP> d_learnedBounds;
269
270
271
  /**
272
   * Manages information about the assignment and upper and lower bounds on
273
   * variables.
274
   */
275
  ArithVariables d_partialModel;
276
277
  /** The set of variables in error in the partial model. */
278
  ErrorSet d_errorSet;
279
280
  /**
281
   * The tableau for all of the constraints seen thus far in the system.
282
   */
283
  Tableau d_tableau;
284
285
  /**
286
   * Maintains the relationship between the PartialModel and the Tableau.
287
   */
288
  LinearEqualityModule d_linEq;
289
290
  /**
291
   * A Diophantine equation solver.  Accesses the tableau and partial
292
   * model (each in a read-only fashion).
293
   */
294
  DioSolver d_diosolver;
295
296
  /** Counts the number of notifyRestart() calls to the theory. */
297
  uint32_t d_restartsCounter;
298
299
  /**
300
   * Every number of restarts equal to s_TABLEAU_RESET_PERIOD,
301
   * the density of the tableau, d, is computed.
302
   * If d >= s_TABLEAU_RESET_DENSITY * d_initialDensity, the tableau
303
   * is set to d_initialTableau.
304
   */
305
  bool d_tableauSizeHasBeenModified;
306
  double d_tableauResetDensity;
307
  uint32_t d_tableauResetPeriod;
308
  static const uint32_t s_TABLEAU_RESET_INCREMENT = 5;
309
310
311
  /** This is only used by simplex at the moment. */
312
  context::CDList<std::pair<ConstraintCP, InferenceId>> d_conflicts;
313
314
  /** This is only used by simplex at the moment. */
315
  context::CDO<Node> d_blackBoxConflict;
316
  /** For holding the proof of the above conflict node. */
317
  context::CDO<std::shared_ptr<ProofNode>> d_blackBoxConflictPf;
318
319
  bool isProofEnabled() const;
320
321
 public:
322
  /**
323
   * This adds the constraint a to the queue of conflicts in d_conflicts.
324
   * Both a and ~a must have a proof.
325
   */
326
  void raiseConflict(ConstraintCP a, InferenceId id);
327
328
  // inline void raiseConflict(const ConstraintCPVec& cv){
329
  //   d_conflicts.push_back(cv);
330
  // }
331
332
  // void raiseConflict(ConstraintCP a, ConstraintCP b);
333
  // void raiseConflict(ConstraintCP a, ConstraintCP b, ConstraintCP c);
334
335
  /** This is a conflict that is magically known to hold. */
336
  void raiseBlackBoxConflict(Node bb, std::shared_ptr<ProofNode> pf = nullptr);
337
  /**
338
   * Returns true iff a conflict has been raised. This method is public since
339
   * it is needed by the ArithState class to know whether we are in conflict.
340
   */
341
  bool anyConflict() const;
342
343
 private:
344
16013608
  inline bool conflictQueueEmpty() const {
345
16013608
    return d_conflicts.empty();
346
  }
347
348
  /**
349
   * Outputs the contents of d_conflicts onto d_out.
350
   * The conditions of anyConflict() must hold.
351
   */
352
  void outputConflicts();
353
354
  /**
355
   * A copy of the tableau.
356
   * This is equivalent  to the original tableau if d_tableauSizeHasBeenModified
357
   * is false.
358
   * The set of basic and non-basic variables may differ from d_tableau.
359
   */
360
  Tableau d_smallTableauCopy;
361
362
  /**
363
   * Returns true if all of the basic variables in the simplex queue of
364
   * basic variables that violate their bounds in the current tableau
365
   * are basic in d_smallTableauCopy.
366
   *
367
   * d_tableauSizeHasBeenModified must be false when calling this.
368
   * Simplex's priority queue must be in collection mode.
369
   */
370
  bool safeToReset() const;
371
372
  /** This keeps track of difference equalities. Mostly for sharing. */
373
  ArithCongruenceManager d_congruenceManager;
374
  context::CDO<bool> d_cmEnabled;
375
376
  /** This implements the Simplex decision procedure. */
377
  DualSimplexDecisionProcedure d_dualSimplex;
378
  FCSimplexDecisionProcedure d_fcSimplex;
379
  SumOfInfeasibilitiesSPD d_soiSimplex;
380
  AttemptSolutionSDP d_attemptSolSimplex;
381
382
  bool solveRealRelaxation(Theory::Effort effortLevel);
383
384
  /* Returns true if this is heuristically a good time to try
385
   * to solve the integers.
386
   */
387
  bool attemptSolveInteger(Theory::Effort effortLevel, bool emmmittedLemmaOrSplit);
388
  bool replayLemmas(ApproximateSimplex* approx);
389
  void solveInteger(Theory::Effort effortLevel);
390
  bool safeToCallApprox() const;
391
  SimplexDecisionProcedure& selectSimplex(bool pass1);
392
  SimplexDecisionProcedure* d_pass1SDP;
393
  SimplexDecisionProcedure* d_otherSDP;
394
  /* Sets d_qflraStatus */
395
  void importSolution(const ApproximateSimplex::Solution& solution);
396
  bool solveRelaxationOrPanic(Theory::Effort effortLevel);
397
  context::CDO<int> d_lastContextIntegerAttempted;
398
  bool replayLog(ApproximateSimplex* approx);
399
400
  class ModelException : public Exception {
401
   public:
402
    ModelException(TNode n, const char* msg);
403
    ~ModelException() override;
404
  };
405
406
  /**
407
   * Computes the delta rational value of a term from the current partial
408
   * model. This returns the delta value assignment to the term if it is in the
409
   * partial model. Otherwise, this is computed recursively for arithmetic terms
410
   * from each subterm.
411
   *
412
   * This throws a DeltaRationalException if the value cannot be represented as
413
   * a DeltaRational. This throws a ModelException if there is a term is not in
414
   * the partial model and is not a theory of arithmetic term.
415
   *
416
   * precondition: The linear abstraction of the nodes must be satisfiable.
417
   */
418
  DeltaRational getDeltaValue(TNode term) const
419
      /* throw(DeltaRationalException, ModelException) */;
420
421
  Node axiomIteForTotalDivision(Node div_tot);
422
  Node axiomIteForTotalIntDivision(Node int_div_like);
423
 public:
424
  TheoryArithPrivate(TheoryArith& containing,
425
                     context::Context* c,
426
                     context::UserContext* u,
427
                     OutputChannel& out,
428
                     Valuation valuation,
429
                     const LogicInfo& logicInfo,
430
                     ProofNodeManager* pnm);
431
  ~TheoryArithPrivate();
432
433
  //--------------------------------- initialization
434
  /**
435
   * Returns true if we need an equality engine, see
436
   * Theory::needsEqualityEngine.
437
   */
438
  bool needsEqualityEngine(EeSetupInfo& esi);
439
  /** finish initialize */
440
  void finishInit();
441
  //--------------------------------- end initialization
442
443
  /**
444
   * Does non-context dependent setup for a node connected to a theory.
445
   */
446
  void preRegisterTerm(TNode n);
447
448
  void propagate(Theory::Effort e);
449
  TrustNode explain(TNode n);
450
451
  Rational deltaValueForTotalOrder() const;
452
453
  bool collectModelInfo(TheoryModel* m);
454
  /**
455
   * Collect model values. This is the main method for extracting information
456
   * about how to construct the model. This method relies on the caller for
457
   * processing the map, which is done so that other modules (e.g. the
458
   * non-linear extension) can modify arithModel before it is sent to the model.
459
   *
460
   * @param termSet The set of relevant terms
461
   * @param arithModel Mapping from terms (of real type) to their values. The
462
   * caller should assert equalities to the model for each entry in this map.
463
   */
464
  void collectModelValues(const std::set<Node>& termSet,
465
                          std::map<Node, Node>& arithModel);
466
467
  void shutdown(){ }
468
469
  void presolve();
470
  void notifyRestart();
471
  Theory::PPAssertStatus ppAssert(TrustNode tin,
472
                                  TrustSubstitutionMap& outSubstitutions);
473
  void ppStaticLearn(TNode in, NodeBuilder<>& learned);
474
475
  std::string identify() const { return std::string("TheoryArith"); }
476
477
  EqualityStatus getEqualityStatus(TNode a, TNode b);
478
479
  /** Called when n is notified as being a shared term with TheoryArith. */
480
  void notifySharedTerm(TNode n);
481
482
  Node getModelValue(TNode var);
483
484
485
  std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
486
487
  //--------------------------------- standard check
488
  /** Pre-check, called before the fact queue of the theory is processed. */
489
  bool preCheck(Theory::Effort level);
490
  /** Pre-notify fact. */
491
  void preNotifyFact(TNode atom, bool pol, TNode fact);
492
  /**
493
   * Post-check, called after the fact queue of the theory is processed. Returns
494
   * true if a conflict or lemma was emitted.
495
   */
496
  bool postCheck(Theory::Effort level);
497
  //--------------------------------- end standard check
498
  /**
499
   * Found non-linear? This returns true if this solver ever encountered
500
   * any non-linear terms that were unhandled. Note that this class is not
501
   * responsible for handling non-linear arithmetic. If the owner of this
502
   * class does not handle non-linear arithmetic in another way, then
503
   * setIncomplete should be called on the output channel of TheoryArith.
504
   */
505
  bool foundNonlinear() const;
506
507
 private:
508
  /** The constant zero. */
509
  DeltaRational d_DELTA_ZERO;
510
511
  /** propagates an arithvar */
512
  void propagateArithVar(bool upperbound, ArithVar var );
513
514
  /**
515
   * Using the simpleKind return the ArithVar associated with the assertion.
516
   */
517
  ArithVar determineArithVar(const Polynomial& p) const;
518
  ArithVar determineArithVar(TNode assertion) const;
519
520
  /**
521
   * Splits the disequalities in d_diseq that are violated using lemmas on demand.
522
   * returns true if any lemmas were issued.
523
   * returns false if all disequalities are satisfied in the current model.
524
   */
525
  bool splitDisequalities();
526
527
  /** A Difference variable is known to be 0.*/
528
  void zeroDifferenceDetected(ArithVar x);
529
530
531
  /**
532
   * Looks for the next integer variable without an integer assignment in a
533
   * round-robin fashion. Changes the value of d_nextIntegerCheckVar.
534
   *
535
   * This returns true if all integer variables have integer assignments.
536
   * If this returns false, d_nextIntegerCheckVar does not have an integer
537
   * assignment.
538
   */
539
  bool hasIntegerModel();
540
541
  /**
542
   * Looks for through the variables starting at d_nextIntegerCheckVar
543
   * for the first integer variable that is between its upper and lower bounds
544
   * that has a non-integer assignment.
545
   *
546
   * If assumeBounds is true, skip the check that the variable is in bounds.
547
   *
548
   * If there is no such variable, returns ARITHVAR_SENTINEL;
549
   */
550
  ArithVar nextIntegerViolatation(bool assumeBounds) const;
551
552
  /**
553
   * Issues branches for non-auxiliary integer variables with non-integer assignments.
554
   * Returns a cut for a lemma.
555
   * If there is an integer model, this returns Node::null().
556
   */
557
  TrustNode roundRobinBranch();
558
559
2081
  bool proofsEnabled() const { return d_pnm; }
560
561
 public:
562
  /**
563
   * This requests a new unique ArithVar value for x.
564
   * This also does initial (not context dependent) set up for a variable,
565
   * except for setting up the initial.
566
   *
567
   * If aux is true, this is an auxiliary variable.
568
   * If internal is true, x might not be unique up to a constant multiple.
569
   */
570
  ArithVar requestArithVar(TNode x, bool aux, bool internal);
571
572
public:
573
  const BoundsInfo& boundsInfo(ArithVar basic) const;
574
575
576
private:
577
  /** Initial (not context dependent) sets up for a variable.*/
578
  void setupBasicValue(ArithVar x);
579
580
  /** Initial (not context dependent) sets up for a new auxiliary variable.*/
581
  void setupAuxiliary(TNode left);
582
583
584
  /**
585
   * Assert*(n, orig) takes an bound n that is implied by orig.
586
   * and asserts that as a new bound if it is tighter than the current bound
587
   * and updates the value of a basic variable if needed.
588
   *
589
   * orig must be a literal in the SAT solver so that it can be used for
590
   * conflict analysis.
591
   *
592
   * x is the variable getting the new bound,
593
   * c is the value of the new bound.
594
   *
595
   * If this new bound is in conflict with the other bound,
596
   * a node describing this conflict is returned.
597
   * If this new bound is not in conflict, Node::null() is returned.
598
   */
599
  bool AssertLower(ConstraintP constraint);
600
  bool AssertUpper(ConstraintP constraint);
601
  bool AssertEquality(ConstraintP constraint);
602
  bool AssertDisequality(ConstraintP constraint);
603
604
  /** Tracks the bounds that were updated in the current round. */
605
  DenseSet d_updatedBounds;
606
607
  /** Tracks the basic variables where propagation might be possible. */
608
  DenseSet d_candidateBasics;
609
  DenseSet d_candidateRows;
610
611
3004976
  bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
612
  void clearUpdates();
613
614
  void revertOutOfConflict();
615
616
  void propagateCandidatesNew();
617
  void dumpUpdatedBoundsToRows();
618
  bool propagateCandidateRow(RowIndex rid);
619
  bool propagateMightSucceed(ArithVar v, bool ub) const;
620
  /** Attempt to perform a row propagation where there is at most 1 possible variable.*/
621
  bool attemptSingleton(RowIndex ridx, bool rowUp);
622
  /** Attempt to perform a row propagation where every variable is a potential candidate.*/
623
  bool attemptFull(RowIndex ridx, bool rowUp);
624
  bool tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUp, const DeltaRational& bound);
625
  bool rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, ConstraintP bestImplied);
626
  //void enqueueConstraints(std::vector<ConstraintCP>& out, Node n) const;
627
  //ConstraintCPVec resolveOutPropagated(const ConstraintCPVec& v, const std::set<ConstraintCP>& propagated) const;
628
  void resolveOutPropagated(std::vector<ConstraintCPVec>& confs, const std::set<ConstraintCP>& propagated) const;
629
  void subsumption(std::vector<ConstraintCPVec>& confs) const;
630
631
  Node cutToLiteral(ApproximateSimplex*  approx, const CutInfo& cut) const;
632
  Node branchToNode(ApproximateSimplex* approx, const NodeLog& cut) const;
633
634
  void propagateCandidates();
635
  void propagateCandidate(ArithVar basic);
636
  bool propagateCandidateBound(ArithVar basic, bool upperBound);
637
638
1190
  inline bool propagateCandidateLowerBound(ArithVar basic){
639
1190
    return propagateCandidateBound(basic, false);
640
  }
641
900
  inline bool propagateCandidateUpperBound(ArithVar basic){
642
900
    return propagateCandidateBound(basic, true);
643
  }
644
645
  /**
646
   * Performs a check to see if it is definitely true that setup can be avoided.
647
   */
648
  bool canSafelyAvoidEqualitySetup(TNode equality);
649
650
  /**
651
   * Handles the case splitting for check() for a new assertion.
652
   * Returns a conflict if one was found.
653
   * Returns Node::null if no conflict was found.
654
   *
655
   * @param assertion The assertion that was just popped from the fact queue
656
   * of TheoryArith and given to this class via preNotifyFact.
657
   */
658
  ConstraintP constraintFromFactQueue(TNode assertion);
659
  bool assertionCases(ConstraintP c);
660
661
  /**
662
   * Returns the basic variable with the shorted row containing a non-basic variable.
663
   * If no such row exists, return ARITHVAR_SENTINEL.
664
   */
665
  ArithVar findShortestBasicRow(ArithVar variable);
666
667
  /**
668
   * Debugging only routine!
669
   * Returns true iff every variable is consistent in the partial model.
670
   */
671
  bool entireStateIsConsistent(const std::string& locationHint);
672
  bool unenqueuedVariablesAreConsistent();
673
674
  bool isImpliedUpperBound(ArithVar var, Node exp);
675
  bool isImpliedLowerBound(ArithVar var, Node exp);
676
677
  void internalExplain(TNode n, NodeBuilder<>& explainBuilder);
678
679
680
  void asVectors(const Polynomial& p,
681
                 std::vector<Rational>& coeffs,
682
                 std::vector<ArithVar>& variables);
683
684
  /** Routine for debugging. Print the assertions the theory is aware of. */
685
  void debugPrintAssertions(std::ostream& out) const;
686
  /** Debugging only routine. Prints the model. */
687
  void debugPrintModel(std::ostream& out) const;
688
689
148631
  inline LogicInfo getLogicInfo() const { return d_containing.getLogicInfo(); }
690
1846007
  inline bool done() const { return d_containing.done(); }
691
  inline TNode get() { return d_containing.get(); }
692
336305
  inline bool isLeaf(TNode x) const { return d_containing.isLeaf(x); }
693
503975
  inline TheoryId theoryOf(TNode x) const { return d_containing.theoryOf(x); }
694
  inline void debugPrintFacts() const { d_containing.debugPrintFacts(); }
695
3433924
  inline context::Context* getSatContext() const { return d_containing.getSatContext(); }
696
  void outputTrustedLemma(TrustNode lem, InferenceId id);
697
  void outputLemma(TNode lem, InferenceId id);
698
  void outputTrustedConflict(TrustNode conf, InferenceId id);
699
  void outputConflict(TNode lit, InferenceId id);
700
  void outputPropagate(TNode lit);
701
  void outputRestart();
702
703
  inline bool isSatLiteral(TNode l) const {
704
    return (d_containing.d_valuation).isSatLiteral(l);
705
  }
706
  inline Node getSatValue(TNode n) const {
707
    return (d_containing.d_valuation).getSatValue(n);
708
  }
709
710
  /** Used for replaying approximate simplex */
711
  context::CDQueue<TrustNode> d_approxCuts;
712
  /** Also used for replaying approximate simplex. "approximate cuts temporary storage" */
713
  std::vector<TrustNode> d_acTmp;
714
715
  /** Counts the number of fullCheck calls to arithmetic. */
716
  uint32_t d_fullCheckCounter;
717
  std::vector<ArithVar> cutAllBounded() const;
718
  TrustNode branchIntegerVariable(ArithVar x) const;
719
  void branchVector(const std::vector<ArithVar>& lemmas);
720
721
  context::CDO<unsigned> d_cutCount;
722
  context::CDHashSet<ArithVar, std::hash<ArithVar> > d_cutInContext;
723
724
  context::CDO<bool> d_likelyIntegerInfeasible;
725
726
727
  context::CDO<bool> d_guessedCoeffSet;
728
  ArithRatPairVec d_guessedCoeffs;
729
730
731
  TreeLog* d_treeLog;
732
  TreeLog& getTreeLog();
733
734
735
  ArithVarVec d_replayVariables;
736
  std::vector<ConstraintP> d_replayConstraints;
737
  DenseMap<Rational> d_lhsTmp;
738
739
  /* Approximate simpplex solvers are given a copy of their stats */
740
  ApproximateStatistics* d_approxStats;
741
  ApproximateStatistics& getApproxStats();
742
  context::CDO<int32_t> d_attemptSolveIntTurnedOff;
743
  void turnOffApproxFor(int32_t rounds);
744
  bool getSolveIntegerResource();
745
746
  void tryBranchCut(ApproximateSimplex* approx, int nid, BranchCutInfo& bl);
747
  std::vector<ConstraintCPVec> replayLogRec(ApproximateSimplex* approx, int nid, ConstraintP bc, int depth);
748
749
  std::pair<ConstraintP, ArithVar> replayGetConstraint(const CutInfo& info);
750
  std::pair<ConstraintP, ArithVar> replayGetConstraint(
751
      ApproximateSimplex* approx, const NodeLog& nl);
752
  std::pair<ConstraintP, ArithVar> replayGetConstraint(const DenseMap<Rational>& lhs, Kind k, const Rational& rhs, bool branch);
753
754
  void replayAssert(ConstraintP c);
755
756
  static ConstraintCP vectorToIntHoleConflict(const ConstraintCPVec& conflict);
757
  static void intHoleConflictToVector(ConstraintCP conflicting, ConstraintCPVec& conflict);
758
759
  // Returns true if the node contains a literal
760
  // that is an arithmetic literal and is not a sat literal
761
  // No caching is done so this should likely only
762
  // be called carefully!
763
  bool hasFreshArithLiteral(Node n) const;
764
765
  int32_t d_dioSolveResources;
766
  bool getDioCuttingResource();
767
768
  uint32_t d_solveIntMaybeHelp, d_solveIntAttempts;
769
770
  RationalVector d_farkasBuffer;
771
772
  //---------------- during check
773
  /** Whether there were new facts during preCheck */
774
  bool d_newFacts;
775
  /** The previous status, computed during preCheck */
776
  Result::Sat d_previousStatus;
777
  //---------------- end during check
778
779
  /** These fields are designed to be accessible to TheoryArith methods. */
780
  class Statistics {
781
  public:
782
    IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
783
784
    IntStat d_statUserVariables, d_statAuxiliaryVariables;
785
    IntStat d_statDisequalitySplits;
786
    IntStat d_statDisequalityConflicts;
787
    TimerStat d_simplifyTimer;
788
    TimerStat d_staticLearningTimer;
789
790
    TimerStat d_presolveTime;
791
792
    TimerStat d_newPropTime;
793
794
    IntStat d_externalBranchAndBounds;
795
796
    IntStat d_initialTableauSize;
797
    IntStat d_currSetToSmaller;
798
    IntStat d_smallerSetToCurr;
799
    TimerStat d_restartTimer;
800
801
    TimerStat d_boundComputationTime;
802
    IntStat d_boundComputations, d_boundPropagations;
803
804
    IntStat d_unknownChecks;
805
    IntStat d_maxUnknownsInARow;
806
    AverageStat d_avgUnknownsInARow;
807
808
    IntStat d_revertsOnConflicts;
809
    IntStat d_commitsOnConflicts;
810
    IntStat d_nontrivialSatChecks;
811
812
    IntStat d_replayLogRecCount,
813
      d_replayLogRecConflictEscalation,
814
      d_replayLogRecEarlyExit,
815
      d_replayBranchCloseFailures,
816
      d_replayLeafCloseFailures,
817
      d_replayBranchSkips,
818
      d_mirCutsAttempted,
819
      d_gmiCutsAttempted,
820
      d_branchCutsAttempted,
821
      d_cutsReconstructed,
822
      d_cutsReconstructionFailed,
823
      d_cutsProven,
824
      d_cutsProofFailed,
825
      d_mipReplayLemmaCalls,
826
      d_mipExternalCuts,
827
      d_mipExternalBranch;
828
829
    IntStat d_inSolveInteger,
830
      d_branchesExhausted,
831
      d_execExhausted,
832
      d_pivotsExhausted,
833
      d_panicBranches,
834
      d_relaxCalls,
835
      d_relaxLinFeas,
836
      d_relaxLinFeasFailures,
837
      d_relaxLinInfeas,
838
      d_relaxLinInfeasFailures,
839
      d_relaxLinExhausted,
840
      d_relaxOthers;
841
842
    IntStat d_applyRowsDeleted;
843
    TimerStat d_replaySimplexTimer;
844
845
    TimerStat d_replayLogTimer,
846
      d_solveIntTimer,
847
      d_solveRealRelaxTimer;
848
849
    IntStat d_solveIntCalls,
850
      d_solveStandardEffort;
851
852
    IntStat d_approxDisabled;
853
    IntStat d_replayAttemptFailed;
854
855
    IntStat d_cutsRejectedDuringReplay;
856
    IntStat d_cutsRejectedDuringLemmas;
857
858
    IntegralHistogramStat<uint32_t> d_satPivots;
859
    IntegralHistogramStat<uint32_t> d_unsatPivots;
860
    IntegralHistogramStat<uint32_t> d_unknownPivots;
861
862
863
    IntStat d_solveIntModelsAttempts;
864
    IntStat d_solveIntModelsSuccessful;
865
    TimerStat d_mipTimer;
866
    TimerStat d_lpTimer;
867
868
    IntStat d_mipProofsAttempted;
869
    IntStat d_mipProofsSuccessful;
870
871
    IntStat d_numBranchesFailed;
872
873
874
875
    Statistics();
876
    ~Statistics();
877
  };
878
879
880
  Statistics d_statistics;
881
};/* class TheoryArithPrivate */
882
883
}/* CVC4::theory::arith namespace */
884
}/* CVC4::theory namespace */
885
}/* CVC4 namespace */