Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/dio_solver.h	Lines:	30	39	76.9 %
Date:	2021-11-07	Branches:	18	112	16.1 %


/******************************************************************************
 * Top contributors (to current version):
 *   Tim King, Morgan Deters, Mathias Preiner
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * A Diophantine equation solver for the theory of arithmetic.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
#define CVC5__THEORY__ARITH__DIO_SOLVER_H

#include <unordered_map>
#include <utility>
#include <vector>

#include "context/cdlist.h"
#include "context/cdmaybe.h"
#include "context/cdo.h"
#include "context/cdqueue.h"
#include "smt/env_obj.h"
#include "theory/arith/normal_form.h"
#include "util/rational.h"
#include "util/statistics_stats.h"

namespace cvc5 {
namespace context {
class Context;
}
namespace theory {
namespace arith {

class DioSolver : protected EnvObj
{
 private:
  typedef size_t TrailIndex;
  typedef size_t InputConstraintIndex;
  typedef size_t SubIndex;

  std::vector<Variable> d_proofVariablePool;
  /** Sat context dependent. */
  context::CDO<size_t> d_lastUsedProofVariable;

  /**
   * The set of input constraints is stored in a CDList.
   * Each constraint point to an element of the trail.
   */
  struct InputConstraint {
    Node d_reason;
    TrailIndex d_trailPos;
    InputConstraint(Node reason, TrailIndex pos) : d_reason(reason), d_trailPos(pos) {}
  };
  context::CDList<InputConstraint> d_inputConstraints;

  /**
   * This is the next input constraint to handle.
   */
  context::CDO<size_t> d_nextInputConstraintToEnqueue;


  /**
   * We maintain a map from the variables associated with proofs to an input constraint.
   * These variables can then be used in polynomial manipulations.
   */
  typedef std::unordered_map<Node, InputConstraintIndex>
      NodeToInputConstraintIndexMap;
  NodeToInputConstraintIndexMap d_varToInputConstraintMap;

  Node proofVariableToReason(const Variable& v) const{
    Assert(d_varToInputConstraintMap.find(v.getNode())
           != d_varToInputConstraintMap.end());
    InputConstraintIndex pos = (*(d_varToInputConstraintMap.find(v.getNode()))).second;
    Assert(pos < d_inputConstraints.size());
    return d_inputConstraints[pos].d_reason;
  }

  /**
   * The main work horse of the algorithm, the trail of constraints.
   * Each constraint is a SumPair that implicitly represents an equality against 0.
   *   d_trail[i].d_eq = (+ c (+ [(* coeff var)])) representing (+ [(* coeff var)]) = -c
   * Each constraint has a proof in terms of a linear combination of the input constraints.
   *   d_trail[i].d_proof
   *
   * Each Constraint also a monomial in d_eq.getPolynomial()
   * of minimal absolute value by the coefficients.
   * d_trail[i].d_minimalMonomial
   *
   * See Alberto's paper for how linear proofs are maintained for the abstract
   * state machine in rules (7), (8) and (9).
   */
  struct Constraint {
    SumPair d_eq;
    Polynomial d_proof;
    Monomial d_minimalMonomial;
    Constraint(const SumPair& eq, const Polynomial& p) :
      d_eq(eq), d_proof(p), d_minimalMonomial(d_eq.getPolynomial().selectAbsMinimum())
    {}
  };
  context::CDList<Constraint> d_trail;

  // /** Compare by d_minimal. */
  // struct TrailMinimalCoefficientOrder {
  //   const context::CDList<Constraint>& d_trail;
  //   TrailMinimalCoefficientOrder(const context::CDList<Constraint>& trail):
  //     d_trail(trail)
  //   {}

  //   bool operator()(TrailIndex i, TrailIndex j){
  //     return d_trail[i].d_minimalMonomial.absLessThan(d_trail[j].d_minimalMonomial);
  //   }
  // };

  /**
   * A substitution is stored as a constraint in the trail together with
   * the variable to be eliminated, and a fresh variable if one was introduced.
   * The variable d_subs[i].d_eliminated is substituted using the implicit equality in
   * d_trail[d_subs[i].d_constraint]
   *  - d_subs[i].d_eliminated is normalized to have coefficient -1 in
   *    d_trail[d_subs[i].d_constraint].
   *  - d_subs[i].d_fresh is either Node::null() or it is variable it is normalized
   *    to have coefficient 1 in d_trail[d_subs[i].d_constraint].
   */
  struct Substitution {
    Node d_fresh;
    Variable d_eliminated;
    TrailIndex d_constraint;
    Substitution(Node f, const Variable& e, TrailIndex c) :
      d_fresh(f), d_eliminated(e), d_constraint(c)
    {}
  };
  context::CDList<Substitution> d_subs;

  /**
   * This is the queue of constraints to be processed in the current context level.
   * This is to be empty upon entering solver and cleared upon leaving the solver.
   *
   * All elements in currentF:
   * - are fully substituted according to d_subs.
   * - !isConstant().
   * - If the element is (+ constant (+ [(* coeff var)] )), then the gcd(coeff) = 1
   */
  std::deque<TrailIndex> d_currentF;
  context::CDList<TrailIndex> d_savedQueue;
  context::CDO<size_t> d_savedQueueIndex;
  context::CDMaybe<TrailIndex> d_conflictIndex;

  /**
   * Drop derived constraints with a coefficient length larger than
   * the maximum input constraints length than 2**MAX_GROWTH_RATE.
   */
  context::CDO<uint32_t> d_maxInputCoefficientLength;
  static const uint32_t MAX_GROWTH_RATE = 3;

  /** Returns true if the element on the trail should be dropped.*/
  bool anyCoefficientExceedsMaximum(TrailIndex j) const;

  /**
   * Is true if decomposeIndex has been used in this context.
   */
  context::CDO<bool> d_usedDecomposeIndex;

  context::CDO<SubIndex> d_lastPureSubstitution;
  context::CDO<SubIndex> d_pureSubstitionIter;

  /**
   * Decomposition lemma queue.
   */
  context::CDQueue<TrailIndex> d_decompositionLemmaQueue;

public:

  /** Construct a Diophantine equation solver with the given context. */
 DioSolver(Env& env);

 /** Returns true if the substitutions use no new variables. */
 bool hasMorePureSubstitutions() const
 {
   return d_pureSubstitionIter < d_lastPureSubstitution;
  }

  Node nextPureSubstitution();

  /**
   * Adds an equality to the queue of the DioSolver.
   * orig is blamed in a conflict.
   * orig can either be of the form (= p c) or (and ub lb).
   * where ub is either (leq p c) or (not (> p [- c 1])), and
   * where lb is either (geq p c) or (not (< p [+ c 1]))
   *
   * If eq cannot be used, this constraint is dropped.
   */
  void pushInputConstraint(const Comparison& eq, Node reason);

  /**
   * Processes the queue looking for any conflict.
   * If a conflict is found, this returns conflict.
   * Otherwise, it returns null.
   * The conflict is guarenteed to be over literals given in addEquality.
   */
  Node processEquationsForConflict();

  /**
   * Processes the queue looking for an integer unsatisfiable cutting plane.
   * If such a plane is found this returns an entailed plane using no
   * fresh variables.
   */
  SumPair processEquationsForCut();

private:
  /** Returns true if the TrailIndex refers to a element in the trail. */
  bool inRange(TrailIndex i) const{
    return i < d_trail.size();
  }

  Node columnGcdIsOne() const;


  /**
   * Returns true if the context dependent flag for conflicts
   * has been raised.
   */
  bool inConflict() const { return d_conflictIndex.isSet(); }

  /** Raises a conflict at the index ti. */
  void raiseConflict(TrailIndex ti){
    Assert(!inConflict());
    d_conflictIndex.set(ti);
  }

  /** Returns the conflict index. */
  TrailIndex getConflictIndex() const{
    Assert(inConflict());
    return d_conflictIndex.get();
  }

  /**
   * Allocates a "unique" proof variable.
   * This variable is fresh with respect to the context.
   * Returns index of the variable in d_variablePool;
   */
  size_t allocateProofVariable();


  /** Empties the unproccessed input constraints into the queue. */
  void enqueueInputConstraints();

  /**
   * Returns true if an input equality is in the map.
   * This is expensive and is only for debug assertions.
   */
  bool debugEqualityInInputEquations(Node eq);

  /** Applies the substitution at subIndex to currentF. */
  void subAndReduceCurrentFByIndex(SubIndex d_subIndex);

  /**
   * Takes as input a TrailIndex i and an integer that divides d_trail[i].d_eq, and
   * returns a TrailIndex j s.t.
   *   d_trail[j].d_eq = (1/g) d_trail[i].d_eq
   * and
   *   d_trail[j].d_proof = (1/g) d_trail[i].d_proof.
   *
   * g must be non-zero.
   *
   * This corresponds to an application of Alberto's rule (7).
   */
  TrailIndex scaleEqAtIndex(TrailIndex i, const Integer& g);


  /**
   * Takes as input TrailIndex's i and j and Integer's q and r and a TrailIndex k s.t.
   *   d_trail[k].d_eq == d_trail[i].d_eq * q + d_trail[j].d_eq * r
   * and
   *   d_trail[k].d_proof == d_trail[i].d_proof * q + d_trail[j].d_proof * r
   *
   * This corresponds to an application of Alberto's rule (8).
   */
  TrailIndex combineEqAtIndexes(TrailIndex i, const Integer& q, TrailIndex j, const Integer& r);

  /**
   * Decomposes the equation at index ti of trail by the variable
   * with the lowest coefficient.
   * This corresponds to an application of Alberto's rule (9).
   *
   * Returns a pair of a SubIndex and a TrailIndex.
   * The SubIndex is the index of a newly introduced substition.
   */
  std::pair<SubIndex, TrailIndex> decomposeIndex(TrailIndex ti);

  /** Solves the index at ti for the value in minimumMonomial. */
  std::pair<SubIndex, TrailIndex> solveIndex(TrailIndex ti);

  /** Prints the queue for debugging purposes to Debug("arith::dio"). */
  void printQueue();

  /**
   * Exhaustively applies all substitutions discovered to an element of the trail.
   * Returns a TrailIndex corresponding to the substitutions being applied.
   */
  TrailIndex applyAllSubstitutionsToIndex(TrailIndex i);

  /**
   * Applies a substitution to an element in the trail.
   */
  TrailIndex applySubstitution(SubIndex s, TrailIndex i);

  /**
   * Reduces the trail node at i by the gcd of the variables.
   * Returns the new trail element.
   *
   * This raises the conflict flag if unsat is detected.
   */
  TrailIndex reduceByGCD(TrailIndex i);

  /**
   * Returns true if i'th element in the trail is trivially true.
   * (0 = 0)
   */
  bool triviallySat(TrailIndex t);

  /**
   * Returns true if i'th element in the trail is trivially unsatisfiable.
   * (1 = 0)
   */
  bool triviallyUnsat(TrailIndex t);

  /** Returns true if the gcd of the i'th element of the trail is 1.*/
  bool gcdIsOne(TrailIndex t);

  bool debugAnySubstitionApplies(TrailIndex t);
  bool debugSubstitutionApplies(SubIndex si, TrailIndex ti);


  /** Returns true if the queue of nodes to process is empty. */
  bool queueEmpty() const;

  bool queueConditions(TrailIndex t);


  void pushToQueueBack(TrailIndex t){
    Assert(queueConditions(t));
    d_currentF.push_back(t);
  }

  void pushToQueueFront(TrailIndex t){
    Assert(queueConditions(t));
    d_currentF.push_front(t);
  }

  /**
   * Moves the minimum Constraint by absolute value of the minimum coefficient to
   * the front of the queue.
   */
  void moveMinimumByAbsToQueueFront();

  void saveQueue();

  TrailIndex impliedGcdOfOne();


  /**
   * Processing the current set of equations.
   *
   * decomposeIndex() rule is only applied if allowDecomposition is true.
   */
  bool processEquations(bool allowDecomposition);

  /**
   * Constructs a proof from any d_trail[i] in terms of input literals.
   */
  Node proveIndex(TrailIndex i);

  /**
   * Returns the SumPair in d_trail[i].d_eq with all of the fresh variables purified out.
   */
  SumPair purifyIndex(TrailIndex i);

public:
  bool hasMoreDecompositionLemmas() const{
    return !d_decompositionLemmaQueue.empty();
  }
  Node nextDecompositionLemma() {
    Assert(hasMoreDecompositionLemmas());
    TrailIndex front = d_decompositionLemmaQueue.front();
    d_decompositionLemmaQueue.pop();
    return trailIndexToEquality(front);
  }
private:
  Node trailIndexToEquality(TrailIndex i) const;
  void addTrailElementAsLemma(TrailIndex i);

public:

  /** These fields are designed to be accessible to TheoryArith methods. */
  class Statistics {
  public:

    IntStat d_conflictCalls;
    IntStat d_cutCalls;

    IntStat d_cuts;
    IntStat d_conflicts;

    TimerStat d_conflictTimer;
    TimerStat d_cutTimer;

    Statistics();
  };

  Statistics d_statistics;
}; /* class DioSolver */

}  // namespace arith
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__ARITH__DIO_SOLVER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Tim King, Morgan Deters, Mathias Preiner
4		*
5		* This file is part of the cvc5 project.
6		*
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.
11		* ****************************************************************************
12		*
13		* A Diophantine equation solver for the theory of arithmetic.
14		*/
15
16		#include "cvc5_private.h"
17
18		#ifndef CVC5__THEORY__ARITH__DIO_SOLVER_H
19		#define CVC5__THEORY__ARITH__DIO_SOLVER_H
20
21		#include <unordered_map>
22		#include <utility>
23		#include <vector>
24
25		#include "context/cdlist.h"
26		#include "context/cdmaybe.h"
27		#include "context/cdo.h"
28		#include "context/cdqueue.h"
29		#include "smt/env_obj.h"
30		#include "theory/arith/normal_form.h"
31		#include "util/rational.h"
32		#include "util/statistics_stats.h"
33
34		namespace cvc5 {
35		namespace context {
36		class Context;
37		}
38		namespace theory {
39		namespace arith {
40
41	15268	class DioSolver : protected EnvObj
42		{
43		private:
44		typedef size_t TrailIndex;
45		typedef size_t InputConstraintIndex;
46		typedef size_t SubIndex;
47
48		std::vector<Variable> d_proofVariablePool;
49		/** Sat context dependent. */
50		context::CDO<size_t> d_lastUsedProofVariable;
51
52		/**
53		* The set of input constraints is stored in a CDList.
54		* Each constraint point to an element of the trail.
55		*/
56	131157	struct InputConstraint {
57		Node d_reason;
58		TrailIndex d_trailPos;
59	43719	InputConstraint(Node reason, TrailIndex pos) : d_reason(reason), d_trailPos(pos) {}
60		};
61		context::CDList<InputConstraint> d_inputConstraints;
62
63		/**
64		* This is the next input constraint to handle.
65		*/
66		context::CDO<size_t> d_nextInputConstraintToEnqueue;
67
68
69		/**
70		* We maintain a map from the variables associated with proofs to an input constraint.
71		* These variables can then be used in polynomial manipulations.
72		*/
73		typedef std::unordered_map<Node, InputConstraintIndex>
74		NodeToInputConstraintIndexMap;
75		NodeToInputConstraintIndexMap d_varToInputConstraintMap;
76
77	393	Node proofVariableToReason(const Variable& v) const{
78	393	Assert(d_varToInputConstraintMap.find(v.getNode())
79		!= d_varToInputConstraintMap.end());
80	393	InputConstraintIndex pos = (*(d_varToInputConstraintMap.find(v.getNode()))).second;
81	393	Assert(pos < d_inputConstraints.size());
82	393	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	357351	struct Constraint {
100		SumPair d_eq;
101		Polynomial d_proof;
102		Monomial d_minimalMonomial;
103	119117	Constraint(const SumPair& eq, const Polynomial& p) :
104	119117	d_eq(eq), d_proof(p), d_minimalMonomial(d_eq.getPolynomial().selectAbsMinimum())
105	119117	{}
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	80793	struct Substitution {
132		Node d_fresh;
133		Variable d_eliminated;
134		TrailIndex d_constraint;
135	26931	Substitution(Node f, const Variable& e, TrailIndex c) :
136	26931	d_fresh(f), d_eliminated(e), d_constraint(c)
137	26931	{}
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(Env& env);
182
183		/** Returns true if the substitutions use no new variables. */
184		bool hasMorePureSubstitutions() const
185		{
186		return d_pureSubstitionIter < d_lastPureSubstitution;
187		}
188
189		Node nextPureSubstitution();
190
191		/**
192		* Adds an equality to the queue of the DioSolver.
193		* orig is blamed in a conflict.
194		* orig can either be of the form (= p c) or (and ub lb).
195		* where ub is either (leq p c) or (not (> p [- c 1])), and
196		* where lb is either (geq p c) or (not (< p [+ c 1]))
197		*
198		* If eq cannot be used, this constraint is dropped.
199		*/
200		void pushInputConstraint(const Comparison& eq, Node reason);
201
202		/**
203		* Processes the queue looking for any conflict.
204		* If a conflict is found, this returns conflict.
205		* Otherwise, it returns null.
206		* The conflict is guarenteed to be over literals given in addEquality.
207		*/
208		Node processEquationsForConflict();
209
210		/**
211		* Processes the queue looking for an integer unsatisfiable cutting plane.
212		* If such a plane is found this returns an entailed plane using no
213		* fresh variables.
214		*/
215		SumPair processEquationsForCut();
216
217		private:
218		/** Returns true if the TrailIndex refers to a element in the trail. */
219	27055	bool inRange(TrailIndex i) const{
220	27055	return i < d_trail.size();
221		}
222
223		Node columnGcdIsOne() const;
224
225
226		/**
227		* Returns true if the context dependent flag for conflicts
228		* has been raised.
229		*/
230	1082798	bool inConflict() const { return d_conflictIndex.isSet(); }
231
232		/** Raises a conflict at the index ti. */
233	1705	void raiseConflict(TrailIndex ti){
234	1705	Assert(!inConflict());
235	1705	d_conflictIndex.set(ti);
236	1705	}
237
238		/** Returns the conflict index. */
239	1705	TrailIndex getConflictIndex() const{
240	1705	Assert(inConflict());
241	1705	return d_conflictIndex.get();
242		}
243
244		/**
245		* Allocates a "unique" proof variable.
246		* This variable is fresh with respect to the context.
247		* Returns index of the variable in d_variablePool;
248		*/
249		size_t allocateProofVariable();
250
251
252		/** Empties the unproccessed input constraints into the queue. */
253		void enqueueInputConstraints();
254
255		/**
256		* Returns true if an input equality is in the map.
257		* This is expensive and is only for debug assertions.
258		*/
259		bool debugEqualityInInputEquations(Node eq);
260
261		/** Applies the substitution at subIndex to currentF. */
262		void subAndReduceCurrentFByIndex(SubIndex d_subIndex);
263
264		/**
265		* Takes as input a TrailIndex i and an integer that divides d_trail[i].d_eq, and
266		* returns a TrailIndex j s.t.
267		* d_trail[j].d_eq = (1/g) d_trail[i].d_eq
268		* and
269		* d_trail[j].d_proof = (1/g) d_trail[i].d_proof.
270		*
271		* g must be non-zero.
272		*
273		* This corresponds to an application of Alberto's rule (7).
274		*/
275		TrailIndex scaleEqAtIndex(TrailIndex i, const Integer& g);
276
277
278		/**
279		* Takes as input TrailIndex's i and j and Integer's q and r and a TrailIndex k s.t.
280		* d_trail[k].d_eq == d_trail[i].d_eq * q + d_trail[j].d_eq * r
281		* and
282		* d_trail[k].d_proof == d_trail[i].d_proof * q + d_trail[j].d_proof * r
283		*
284		* This corresponds to an application of Alberto's rule (8).
285		*/
286		TrailIndex combineEqAtIndexes(TrailIndex i, const Integer& q, TrailIndex j, const Integer& r);
287
288		/**
289		* Decomposes the equation at index ti of trail by the variable
290		* with the lowest coefficient.
291		* This corresponds to an application of Alberto's rule (9).
292		*
293		* Returns a pair of a SubIndex and a TrailIndex.
294		* The SubIndex is the index of a newly introduced substition.
295		*/
296		std::pair<SubIndex, TrailIndex> decomposeIndex(TrailIndex ti);
297
298		/** Solves the index at ti for the value in minimumMonomial. */
299		std::pair<SubIndex, TrailIndex> solveIndex(TrailIndex ti);
300
301		/** Prints the queue for debugging purposes to Debug("arith::dio"). */
302		void printQueue();
303
304		/**
305		* Exhaustively applies all substitutions discovered to an element of the trail.
306		* Returns a TrailIndex corresponding to the substitutions being applied.
307		*/
308		TrailIndex applyAllSubstitutionsToIndex(TrailIndex i);
309
310		/**
311		* Applies a substitution to an element in the trail.
312		*/
313		TrailIndex applySubstitution(SubIndex s, TrailIndex i);
314
315		/**
316		* Reduces the trail node at i by the gcd of the variables.
317		* Returns the new trail element.
318		*
319		* This raises the conflict flag if unsat is detected.
320		*/
321		TrailIndex reduceByGCD(TrailIndex i);
322
323		/**
324		* Returns true if i'th element in the trail is trivially true.
325		* (0 = 0)
326		*/
327		bool triviallySat(TrailIndex t);
328
329		/**
330		* Returns true if i'th element in the trail is trivially unsatisfiable.
331		* (1 = 0)
332		*/
333		bool triviallyUnsat(TrailIndex t);
334
335		/** Returns true if the gcd of the i'th element of the trail is 1.*/
336		bool gcdIsOne(TrailIndex t);
337
338		bool debugAnySubstitionApplies(TrailIndex t);
339		bool debugSubstitutionApplies(SubIndex si, TrailIndex ti);
340
341
342		/** Returns true if the queue of nodes to process is empty. */
343		bool queueEmpty() const;
344
345		bool queueConditions(TrailIndex t);
346
347
348	40082	void pushToQueueBack(TrailIndex t){
349	40082	Assert(queueConditions(t));
350	40082	d_currentF.push_back(t);
351	40082	}
352
353		void pushToQueueFront(TrailIndex t){
354		Assert(queueConditions(t));
355		d_currentF.push_front(t);
356		}
357
358		/**
359		* Moves the minimum Constraint by absolute value of the minimum coefficient to
360		* the front of the queue.
361		*/
362		void moveMinimumByAbsToQueueFront();
363
364		void saveQueue();
365
366		TrailIndex impliedGcdOfOne();
367
368
369		/**
370		* Processing the current set of equations.
371		*
372		* decomposeIndex() rule is only applied if allowDecomposition is true.
373		*/
374		bool processEquations(bool allowDecomposition);
375
376		/**
377		* Constructs a proof from any d_trail[i] in terms of input literals.
378		*/
379		Node proveIndex(TrailIndex i);
380
381		/**
382		* Returns the SumPair in d_trail[i].d_eq with all of the fresh variables purified out.
383		*/
384		SumPair purifyIndex(TrailIndex i);
385
386		public:
387		bool hasMoreDecompositionLemmas() const{
388		return !d_decompositionLemmaQueue.empty();
389		}
390		Node nextDecompositionLemma() {
391		Assert(hasMoreDecompositionLemmas());
392		TrailIndex front = d_decompositionLemmaQueue.front();
393		d_decompositionLemmaQueue.pop();
394		return trailIndexToEquality(front);
395		}
396		private:
397		Node trailIndexToEquality(TrailIndex i) const;
398		void addTrailElementAsLemma(TrailIndex i);
399
400		public:
401
402		/** These fields are designed to be accessible to TheoryArith methods. */
403		class Statistics {
404		public:
405
406		IntStat d_conflictCalls;
407		IntStat d_cutCalls;
408
409		IntStat d_cuts;
410		IntStat d_conflicts;
411
412		TimerStat d_conflictTimer;
413		TimerStat d_cutTimer;
414
415		Statistics();
416		};
417
418		Statistics d_statistics;
419		}; /* class DioSolver */
420
421		} // namespace arith
422		} // namespace theory
423		} // namespace cvc5
424
425		#endif /* CVC5__THEORY__ARITH__DIO_SOLVER_H */