Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/arith/dio_solver.h	Lines:	30	39	76.9 %
Date:	2021-05-22	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 "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 {
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(context::Context* ctxt);

  /** 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);


  void debugPrintTrail(TrailIndex i) const;

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