CVC3  2.4.1
theory_arith_new.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith_new.h
4  *
5  * Author: Dejan Jovanovic
6  *
7  * Created: Thu Jun 14 13:38:16 2007
8  *
9  * <hr>
10  *
11  * License to use, copy, modify, sell and/or distribute this software
12  * and its documentation for any purpose is hereby granted without
13  * royalty, subject to the terms and conditions defined in the \ref
14  * LICENSE file provided with this distribution.
15  *
16  * <hr>
17  *
18  */
19 /*****************************************************************************/
20 
21 #ifndef _cvc3__include__theory_arith_new_h_
22 #define _cvc3__include__theory_arith_new_h_
23 
24 #include "theory_arith.h"
25 
26 #include <hash_fun.h>
27 #include <hash_map.h>
28 #include <queryresult.h>
29 #include <map>
30 
31 namespace CVC3 {
32 
33 
34 /**
35  * This theory handles basic linear arithmetic.
36  *
37  * @author Clark Barrett
38  *
39  * @since Sat Feb 8 14:44:32 2003
40  */
41 class TheoryArithNew :public TheoryArith {
42 
43  /** For concrete model generation */
45  /** Index to the next unprocessed disequality */
49 
50  /** Data class for the strongest free constant in separation inqualities **/
51  class FreeConst {
52  private:
54  bool d_strict;
55  public:
56  FreeConst() { }
57  FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
58  const Rational& getConst() const { return d_r; }
59  bool strict() const { return d_strict; }
60  };
61  //! Printing
62  friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
63  //! Private class for an inequality in the Fourier-Motzkin database
64  class Ineq {
65  private:
66  Theorem d_ineq; //!< The inequality
67  bool d_rhs; //!< Var is isolated on the RHS
68  const FreeConst* d_const; //!< The max/min const for subsumption check
69  //! Default constructor is disabled
70  Ineq() { }
71  public:
72  //! Initial constructor. 'r' is taken from the subsumption database.
73  Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
74  d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
75  //! Get the inequality
76  const Theorem& ineq() const { return d_ineq; }
77  //! Get the max/min constant
78  const FreeConst& getConst() const { return *d_const; }
79  //! Flag whether var is isolated on the RHS
80  bool varOnRHS() const { return d_rhs; }
81  //! Flag whether var is isolated on the LHS
82  bool varOnLHS() const { return !d_rhs; }
83  //! Auto-cast to Theorem
84  operator Theorem() const { return d_ineq; }
85  };
86  //! Printing
87  friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
88  //! Database of inequalities with a variable isolated on the right
90  //! Database of inequalities with a variable isolated on the left
92  //! Mapping of inequalities to the largest/smallest free constant
93  /*! The Expr is the original inequality with the free constant
94  * removed and inequality converted to non-strict (for indexing
95  * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped
96  * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
97  * among inequalities with the same 'a', 'x', and 't', and a boolean
98  * flag indicating whether the strongest inequality is strict.
99  */
101  // Input buffer to store the incoming inequalities
102  CDList<Theorem> d_buffer; //!< Buffer of input inequalities
103  CDO<size_t> d_bufferIdx; //!< Buffer index of the next unprocessed inequality
104  const int* d_bufferThres; //!< Threshold when the buffer must be processed
105  // Statistics for the variables
106  /*! @brief Mapping of a variable to the number of inequalities where
107  the variable would be isolated on the right */
109  /*! @brief Mapping of a variable to the number of inequalities where
110  the variable would be isolated on the left */
112  //! Set of shared terms (for counterexample generation)
114  //! Set of shared integer variables (i-leaves)
116  //Directed Acyclic Graph representing partial variable ordering for
117  //variable projection over inequalities.
121  bool dfs(const Expr& e1, const Expr& e2);
122  public:
123  void addEdge(const Expr& e1, const Expr& e2);
124  //returns true if e1 < e2, false otherwise.
125  bool lessThan(const Expr& e1, const Expr& e2);
126  //selects those variables which are largest and incomparable among
127  //v1 and puts it into v2
128  void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
129  //selects those variables which are smallest and incomparable among
130  //v1, removes them from v1 and puts them into v2.
131  void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
132 
133  };
134 
136 
137  // Private methods
138  //! Check the term t for integrality.
139  /*! \return a theorem of IS_INTEGER(t) or Null. */
140  Theorem isIntegerThm(const Expr& e);
141  //! A helper method for isIntegerThm()
142  /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
143  Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
144  //! Check if the kids of e are fully simplified and canonized (for debugging)
145  bool kidsCanonical(const Expr& e);
146 
147  //! Canonize the expression e, assuming all children are canonical
148  Theorem canon(const Expr& e);
149  /*! @brief Canonize and reduce e w.r.t. union-find database; assume
150  * all children are canonical */
151  Theorem canonSimplify(const Expr& e);
152  /*! @brief Composition of canonSimplify(const Expr&) by
153  * transitivity: take e0 = e1, canonize and simplify e1 to e2,
154  * return e0 = e2. */
156  return transitivityRule(thm, canonSimplify(thm.getRHS()));
157  }
158  //! Canonize predicate (x = y, x < y, etc.)
159  Theorem canonPred(const Theorem& thm);
160  //! Canonize predicate like canonPred except that the input theorem
161  //! is an equivalent transformation.
162  Theorem canonPredEquiv(const Theorem& thm);
163  //! Solve an equation and return an equivalent Theorem in the solved form
164  Theorem doSolve(const Theorem& e);
165  //! takes in a conjunction equivalence Thm and canonizes it.
167  //! picks the monomial with the smallest abs(coeff) from the input
168  //integer equation.
170  //! processes equalities with 1 or more vars of type REAL
171  Theorem processRealEq(const Theorem& eqn);
172  //! processes equalities whose vars are all of type INT
173  Theorem processIntEq(const Theorem& eqn);
174  //! One step of INT equality processing (aux. method for processIntEq())
175  Theorem processSimpleIntEq(const Theorem& eqn);
176  //! Take an inequality and isolate a variable
177  Theorem isolateVariable(const Theorem& inputThm, bool& e1);
178  //! Update the statistics counters for the variable with a coeff. c
179  void updateStats(const Rational& c, const Expr& var);
180  //! Update the statistics counters for the monomial
181  void updateStats(const Expr& monomial);
182  //! Add an inequality to the input buffer. See also d_buffer
183  void addToBuffer(const Theorem& thm);
184  Expr pickMonomial(const Expr& right);
185  public: // ArithTheoremProducer needs this function, so make it public
186  //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
187  void separateMonomial(const Expr& e, Expr& c, Expr& var);
188  //! Check the term t for integrality (return bool)
189  bool isInteger(const Expr& e) { return !(isIntegerThm(e).isNull()); }
190  private:
191  bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
192  //! Check if the term expression is "stale"
193  bool isStale(const Expr& e);
194  //! Check if the inequality is "stale" or subsumed
195  bool isStale(const Ineq& ineq);
196  void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
197  void assignVariables(std::vector<Expr>&v);
198  void findRationalBound(const Expr& varSide, const Expr& ratSide,
199  const Expr& var,
200  Rational &r);
201  bool findBounds(const Expr& e, Rational& lub, Rational& glb);
202 
203  Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
204  const Theorem& ineqThm2);
205  //! Take a system of equations and turn it into a solved form
206  Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
207  /*! @brief Substitute all vars in term 't' according to the
208  * substitution 'subst' and canonize the result.
209  */
210  Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
211  /*! @brief Substitute all vars in the RHS of the equation 'eq' of
212  * the form (x = t) according to the substitution 'subst', and
213  * canonize the result.
214  */
216  //! Traverse 'e' and push all the i-leaves into 'vars' vector
217  void collectVars(const Expr& e, std::vector<Expr>& vars,
218  std::set<Expr>& cache);
219  /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
220  * for integer var 'x', and assert the corresponding constraint
221  */
222  void processFiniteInterval(const Theorem& alphaLEax,
223  const Theorem& bxLEbeta);
224  //! For an integer var 'x', find and process all constraints A <= ax <= A+c
225  void processFiniteIntervals(const Expr& x);
226  //! Recursive setup for isolated inequalities (and other new expressions)
227  void setupRec(const Expr& e);
228 
229 public:
230  TheoryArithNew(TheoryCore* core);
231  ~TheoryArithNew();
232 
233  // Trusted method that creates the proof rules class (used in constructor).
234  // Implemented in arith_theorem_producer.cpp
236 
237  // Theory interface
238  void addSharedTerm(const Expr& e);
239  void assertFact(const Theorem& e);
240  void refineCounterExample();
241  void computeModelBasic(const std::vector<Expr>& v);
242  void computeModel(const Expr& e, std::vector<Expr>& vars);
243  void checkSat(bool fullEffort);
244  Theorem rewrite(const Expr& e);
245  void setup(const Expr& e);
246  void update(const Theorem& e, const Expr& d);
247  Theorem solve(const Theorem& e);
248  void checkAssertEqInvariant(const Theorem& e);
249  void checkType(const Expr& e);
251  bool enumerate, bool computeSize);
252  void computeType(const Expr& e);
253  Type computeBaseType(const Type& t);
254  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
255  Expr computeTypePred(const Type& t, const Expr& e);
256  Expr computeTCC(const Expr& e);
257  ExprStream& print(ExprStream& os, const Expr& e);
258  virtual Expr parseExprOp(const Expr& e);
259 
260  // DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN
261 
262  public:
263 
264  /**
265  * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational
266  * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.
267  * The operations on the new rationals are defined as
268  * <ul>
269  * <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$
270  * <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$
271  * <li>\f$(q_1, k_1) \leq (q_2, k_2) \equiv (q_1 < q_2) \vee (q_1 = q_2 \wedge k_1 \leq k_2)\f$
272  * </ul>
273  *
274  * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can
275  * only be asigned or compared.
276  */
277  class EpsRational {
278 
279  protected:
280 
281  /** Type of rationals, normal and the two infinities */
283 
284  /** The type of this rational */
286 
287  /** The rational part */
289 
290  /** The epsilon multiplier */
292 
293  /**
294  * Private constructor to construt infinities.
295  */
296  EpsRational(RationalType type) : type(type) {}
297 
298  public:
299 
300  /**
301  * Returns if the number is a plain rational.
302  *
303  * @return true if rational, false otherwise
304  */
305  inline bool isRational() const { return k == 0; }
306 
307  /**
308  * Returns if the number is a plain integer.
309  *
310  * @return true if rational, false otherwise
311  */
312  inline bool isInteger() const { return k == 0 && q.isInteger(); }
313 
314  /**
315  * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following formula
316  * \f[
317  * \lfloor \beta(x) \rfloor = \left\{
318  * \begin{tabular}{ll}
319  * $\lfloor q \rfloor$ & $\mathrm{if\ } q \notin Z$\\
320  * $q$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k \geq 0$\\
321  * $q - 1$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k < 0$
322  * \end{tabular}\right.
323  * \f]
324  */
325  inline Rational getFloor() const {
326  if (q.isInteger()) {
327  if (k >= 0) return q;
328  else return q - 1;
329  } else
330  // If not an integer, just floor it
331  return floor(q);
332  }
333 
334 
335  /**
336  * Returns the rational part of the number
337  *
338  * @return the rational
339  */
340  inline Rational getRational() const { return q; }
341 
342  /** The infinity constant */
343  static const EpsRational PlusInfinity;
344  /** The negative infinity constant */
346  /** The zero constant */
347  static const EpsRational Zero;
348 
349 
350  /** The blank constructor */
351  EpsRational() : type(FINITE), q(0), k(0) {}
352 
353  /** Copy constructor */
354  EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {}
355 
356  /**
357  * Constructor from a rational, constructs a new pair (q, 0).
358  *
359  * @param q the rational
360  */
361  EpsRational(const Rational q) : type(FINITE), q(q), k(0) {}
362 
363  /**
364  * Constructor from a rational and a given epsilon multiplier, constructs a
365  * new pair (q, k).
366  *
367  * @param q the rational
368  * @param k the epsilon multiplier
369  */
370  EpsRational(const Rational q, const Rational k) : type(FINITE), q(q), k(k) {}
371 
372  /**
373  * Addition operator for two EpsRational numbers.
374  *
375  * @param r the number to be added
376  * @return the sum as defined in the class
377  */
378  inline EpsRational operator + (const EpsRational& r) const {
379  DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
380  DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number");
381  return EpsRational(q + r.q, k + r.k);
382  }
383 
384  /**
385  * Addition operator for two EpsRational numbers.
386  *
387  * @param r the number to be added
388  * @return the sum as defined in the class
389  */
391  DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
392  q = q + r.q;
393  k = k + r.k;
394  return *this;
395  }
396 
397  /**
398  * Subtraction operator for two EpsRational numbers.
399  *
400  * @param r the number to be added
401  * @return the sum as defined in the class
402  */
403  inline EpsRational operator - (const EpsRational& r) const {
404  DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
405  DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number");
406  return EpsRational(q - r.q, k - r.k);
407  }
408 
409  /**
410  * Multiplication operator EpsRational number and a rational number.
411  *
412  * @param a the number to be multiplied
413  * @return the product as defined in the class
414  */
415  inline EpsRational operator * (const Rational& a) const {
416  DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number");
417  return EpsRational(a * q, a * k);
418  }
419 
420  /**
421  * Division operator EpsRational number and a rational number.
422  *
423  * @param a the number to be multiplied
424  * @return the product as defined in the class
425  */
426  inline EpsRational operator / (const Rational& a) const {
427  DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number");
428  return EpsRational(q / a, k / a);
429  }
430 
431  /**
432  * Equality comparison operator.
433  */
434  inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
435 
436  /**
437  * Less than or equal comparison operator.
438  */
439  inline bool operator <= (const EpsRational& r) const {
440  switch (r.type) {
441  case FINITE:
442  if (type == FINITE)
443  // Normal comparison
444  return (q < r.q || (q == r.q && k <= r.k));
445  else
446  // Finite number is bigger only of the negative infinity
447  return type == MINUS_INFINITY;
448  case PLUS_INFINITY:
449  // Everything is less then or equal than +inf
450  return true;
451  case MINUS_INFINITY:
452  // Only -inf is less then or equal than -inf
453  return (type == MINUS_INFINITY);
454  default:
455  // Ohohohohohoooooo, whats up
456  FatalAssert(false, "EpsRational::operator <=, what kind of number is this????");
457  }
458  return false;
459  }
460 
461  /**
462  * Less than comparison operator.
463  */
464  inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
465 
466  /**
467  * Greater than comparison operator.
468  */
469  inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
470 
471  /**
472  * Returns the string representation of the number.
473  *
474  * @return the string representation of the number
475  */
476  std::string toString() const {
477  switch (type) {
478  case FINITE:
479  return "(" + q.toString() + ", " + k.toString() + ")";
480  case PLUS_INFINITY:
481  return "+inf";
482  case MINUS_INFINITY:
483  return "-inf";
484  default:
485  FatalAssert(false, "EpsRational::toString, what kind of number is this????");
486  }
487  return "hm, what am I?";
488  }
489  };
490 
491  /**
492  * Registers the atom given from the core. This atoms are stored so that they can be used
493  * for theory propagation.
494  *
495  * @param e the expression (atom) that is part of the input formula
496  */
497  void registerAtom(const Expr& e);
498 
499  private:
500 
501  /** A set of all integer variables */
502  std::set<Expr> intVariables;
503 
504  /**
505  * Return a Gomory cut plane derivation of the variable $x_i$. Mixed integer
506  * Gomory cut can be constructed if
507  * <ul>
508  * <li>\f$x_i\f$ is a integer basic variable with a non-integer value
509  * <li>all non-basic variables in the row of \f$x_i\f$ are assigned to their
510  * upper or lower bounds
511  * <li>all the values on the right side of the row have rational values (non
512  * eps-rational values)
513  * </ul>
514  */
515  Theorem deriveGomoryCut(const Expr& x_i);
516 
517  /**
518  * Tries to rafine the integer constraint of the theorem. For example,
519  * x < 1 is rewritten as x <= 0, and x <(=) 1.5 is rewritten as x <= 1.
520  * The constraint should be in the normal form.
521  *
522  * @param thm the derivation of the constraint
523  */
525 
526  /** Are we consistent or not */
528 
529  /** The theorem explaining the inconsistency */
531 
532  /**
533  * The structure necessaty to hold the bounds.
534  */
535  struct BoundInfo {
536  /** The bound itself */
538  /** The assertion theoreem of the bound */
540 
541  /** Constructor */
542  BoundInfo(const EpsRational& bound, const Theorem& thm): bound(bound), theorem(thm) {}
543 
544  /** The empty constructor for the map */
545  BoundInfo(): bound(0), theorem() {}
546 
547  /**
548  * The comparator, just if we need it. Compares first by expressions then by bounds
549  */
550  bool operator < (const BoundInfo& bI) const {
551  // Get tje expressoins
552  const Expr& expr1 = (theorem.isRewrite() ? theorem.getRHS() : theorem.getExpr());
553  const Expr& expr2 = (bI.theorem.isRewrite() ? bI.theorem.getRHS() : bI.theorem.getExpr());
554 
555  std::cout << expr1 << " @ " << expr2 << std::endl;
556 
557  // Compare first by the expressions (right sides of expressions)
558  if (expr1[1] == expr2[1])
559  // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations)
560  if (bound == bI.bound && expr1.getKind() != expr2.getKind())
561  return expr1.getKind() == LE; // LE before GE -- only case that can happen
562  else
563  return bound < bI.bound;
564  else
565  // Return the expression comparison
566  return expr1[1] < expr2[1];
567  }
568  };
569 
570 
571  /**
572  * The structure necessaty to hold the bounds on expressions (for theory propagation).
573  */
574  struct ExprBoundInfo {
575  /** The bound itself */
577  /** The assertion theoreem of the bound */
579 
580  /** Constructor */
581  ExprBoundInfo(const EpsRational& bound, const Expr& e): bound(bound), e(e) {}
582 
583  /** The empty constructor for the map */
585 
586  /**
587  * The comparator, just if we need it. Compares first by expressions then by bounds
588  */
589  bool operator < (const ExprBoundInfo& bI) const {
590 
591  // Compare first by the expressions (right sides of expressions)
592  if (e[1] == bI.e[1])
593  // If the same, just return the bound comparison (plus a trick to order equal bounds, different relations)
594  if (bound == bI.bound && e.getKind() != bI.e.getKind())
595  return e.getKind() == LE; // LE before GE -- only case that can happen
596  else
597  return bound < bI.bound;
598  else
599  // Return the expression comparison
600  return e[1] < bI.e[1];
601  }
602  };
603 
604  /** The map from variables to lower bounds (these must be backtrackable) */
606  /** The map from variables to upper bounds (these must be backtrackable) */
608  /** The current real valuation of the variables (these must be backtrackable for the last succesefull checkSAT!!!) */
610 
612  //typedef google::sparse_hash_map<Expr, Theorem, Hash::hash<Expr> > TebleauxMap;
613  //typedef std::map<Expr, Theorem> TebleauxMap;
614 
615  typedef std::set<Expr> SetOfVariables;
617 
618  /** Maps variables to sets of variables that depend on it in the tableaux */
620 
621  /** The tableaux, a map from basic variables to the expressions over the non-basic ones (theorems that explain them how we got there) */
623 
624  /** Additional tableaux map from expressions asserted to the corresponding theorems explaining the introduction of the new variables */
626 
627  /** A set containing all the unsatisfied basic variables */
628  std::set<Expr> unsatBasicVariables;
629 
630  /** The vector to keep the assignments from fresh variables to expressions they represent */
631  std::vector<Expr> assertedExpr;
632  /** The backtrackable number of fresh variables asserted so far */
634 
635  /** A set of BoundInfo objects */
636  typedef std::set<ExprBoundInfo> BoundInfoSet;
637 
638  /** Internal variable to see wheather to propagate or not */
639  bool propagate;
640 
641  /**
642  * Propagate all that is possible from given assertion and its bound
643  */
644  void propagateTheory(const Expr& assertExpr, const EpsRational& bound, const EpsRational& oldBound);
645 
646  /**
647  * Store all the atoms from the formula in this set. It is searchable by an expression
648  * and the bound. To get all the implied atoms, one just has to go up (down) and check if the
649  * atom or it's negation are implied.
650  */
652 
653  /**
654  * Adds var to the dependencies sets of all the variables in the sum.
655  *
656  * @param var the variable on the left side
657  * @param sum the sum that defines the variable
658  */
659  void updateDependenciesAdd(const Expr& var, const Expr& sum);
660 
661  /**
662  * Remove var from the dependencies sets of all the variables in the sum.
663  *
664  * @param var the variable on the left side
665  * @param sum the sum that defines the variable
666  */
667  void updateDependenciesRemove(const Expr& var, const Expr& sum);
668 
669  /**
670  * Updates the dependencies if a right side of an expression in the tableaux is changed. For example,
671  * if oldExpr is x + y and newExpr is y + z, var will be added to the dependency list of z, and removed
672  * from the dependency list of x.
673  *
674  * @param oldExpr the old right side of the tableaux
675  * @param newExpr the new right side of the tableaux
676  * @param var the variable that is defined by these two expressions
677  * @param skipVar a variable to skip when going through the expressions
678  */
679  void updateDependencies(const Expr& oldExpr, const Expr& newExpr, const Expr& var, const Expr& skipVar);
680 
681  /**
682  * Update the values of variables that have appeared in the tableaux due to backtracking.
683  */
684  void updateFreshVariables();
685 
686  /**
687  * Updates the value of variable var by computing the value of expression e.
688  *
689  * @param var the variable to update
690  * @param e the expression to compute
691  */
692  void updateValue(const Expr& var, const Expr& e);
693 
694  /**
695  * Returns a string representation of the tableaux.
696  *
697  * @return tableaux as string
698  */
699  std::string tableauxAsString() const;
700 
701  /**
702  * Returns a string representation of the unsat variables.
703  *
704  * @return unsat as string
705  */
706  std::string unsatAsString() const;
707 
708  /**
709  * Returns a string representation of the current bounds.
710  *
711  * @return tableaux as string
712  */
713  std::string boundsAsString();
714 
715  /**
716  * Gets the equality of the fresh variable tableaux variable corresponding to this expression. If the expression has already been
717  * asserted, the coresponding variable is returned, othervise a fresh variable is created and the theorem is returned.
718  *
719  * @param leftSide the left side of the asserted constraint
720  * @return the equality theorem s = leftSide
721  */
722  Theorem getVariableIntroThm(const Expr& leftSide);
723 
724  /**
725  * Find the coefficient standing by the variable var in the expression expr. Expresion is expected to be
726  * in canonical form, i.e either a rational constant, an arithmetic leaf (i.e. variable or term from some
727  * other theory), (MULT rat leaf) where rat is a non-zero rational constant, leaf is an arithmetic leaf or
728  * (PLUS \f$const term_0 term_1 ... term_n\f$) where each \f$term_i\f$ is either a leaf or (MULT \f$rat leaf\f$)
729  * and each leaf in \f$term_i\f$ must be strictly greater than the leaf in \f$term_{i+1}\f$.
730  *
731  * @param var the variable
732  * @param expr the expression to search in
733  */
734  const Rational& findCoefficient(const Expr& var, const Expr& expr);
735 
736  /**
737  * Return true iof the given variable is basic in the tableaux, i.e. it is on the left side, expressed
738  * in terms of the non-basic variables.
739  *
740  * @param x the variable to be checked
741  * @return true if the variable is basic, false if the variable is non-basic
742  */
743  bool isBasic(const Expr& x) const;
744 
745  /**
746  * Returns the coefficient at a_ij in the current tableaux, i.e. the coefficient
747  * at x_j in the row of x_i.
748  *
749  * @param x_i a basic variable
750  * @param x_j a non-basic variable
751  * @return the reational coefficient
752  */
753  Rational getTableauxEntry(const Expr& x_i, const Expr& x_j);
754 
755  /**
756  * Swaps a basic variable \f$x_r\f$ and a non-basic variable \f$x_s\f$ such
757  * that ars \f$a_{rs} \neq 0\f$. After pivoting, \f$x_s\f$ becomes basic and \f$x_r\f$ becomes non-basic.
758  * The tableau is updated by replacing equation \f[x_r = \sum_{x_j \in N}{a_{rj}xj}\f] with
759  * \f[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\f] and this equation
760  * is used to eliminate \f$x_s\f$ from the rest of the tableau by substitution.
761  *
762  * @param x_r a basic variable
763  * @param x_s a non-basic variable
764  */
765  void pivot(const Expr& x_r, const Expr& x_s);
766 
767  /**
768  * Sets the value of a non-basic variable \f$x_i\f$ to \f$v\f$ and adjusts the value of all
769  * the basic variables so that all equations remain satisfied.
770  *
771  * @param x_i a non-basic variable
772  * @param v the value to set the variable \f$x_i\f$ to
773  */
774  void update(const Expr& x_i, const EpsRational& v);
775 
776  /**
777  * Pivots the basic variable \f$x_i\f$ and the non-basic variable \f$x_j\f$. It also sets \f$x_i\f$ to \f$v\f$ and adjusts all basic
778  * variables to keep the equations satisfied.
779  *
780  * @param x_i a basic variable
781  * @param x_j a non-basic variable
782  * @param v the valie to assign to x_i
783  */
784  void pivotAndUpdate(const Expr& x_i, const Expr& x_j, const EpsRational& v);
785 
786  /**
787  * Asserts a new upper bound constraint on a variable and performs a simple check for consistency (not complete).
788  *
789  * @param x_i the variable to assert the bound on
790  * @param c the bound to assert
791  */
792  QueryResult assertUpper(const Expr& x_i, const EpsRational& c, const Theorem& thm);
793 
794  /**
795  * Asserts a new lower bound constraint on a variable and performs a simple check for consistency (not complete).
796  *
797  * @param x_i the variable to assert the bound on
798  * @param c the bound to assert
799  */
800  QueryResult assertLower(const Expr& x_i, const EpsRational& c, const Theorem& thm);
801 
802  /**
803  * Asserts a new equality constraint on a variable by asserting both upper and lower bounds.
804  *
805  * @param x_i the variable to assert the bound on
806  * @param c the bound to assert
807  */
808  QueryResult assertEqual(const Expr& x_i, const EpsRational& c, const Theorem& thm);
809 
810  /**
811  * Type of noramlization GCD = 1 or just first coefficient 1
812  */
814 
815  /**
816  * Given a canonized term, compute a factor to make all coefficients integer and relatively prime
817  */
819 
820  /**
821  * Normalize an equation (make all coefficients rel. prime integers)
822  */
824 
825  /**
826  * Normalize an equation (make all coefficients rel. prime integers) accepts a rewrite theorem over
827  * eqn|ineqn and normalizes it and returns a theorem to that effect.
828  */
830 
831  /**
832  * Canonise the equation using the tebleaux equations, i.e. replace all the tableaux right sides
833  * with the corresponding left sides and canonise the result.
834  *
835  * @param eq the equation to canonise
836  * @return the explaining theorem
837  */
839 
840  /**
841  * Canonise the sum using the tebleaux equations, i.e. replace all the tableaux right sides
842  * with the corresponding left sides and canonise the result.
843  *
844  * @param sum the canonised sum to canonise
845  * @return the explaining theorem
846  */
848 
849  /**
850  * Sustitute the given equation everywhere in the tableaux.
851  *
852  * @param eq the equation to use for substitution
853  */
854  void substAndCanonizeTableaux(const Theorem& eq);
855 
856  /**
857  * Given an equality eq: \f$\sum a_i x_i = y\f$ and a variable $var$ that appears in
858  * on the left hand side, pivots $y$ and $var$ so that $y$ comes to the right-hand
859  * side.
860  *
861  * @param eq the proof of the equality
862  * @param var the variable to move to the right-hand side
863  */
864  Theorem pivotRule(const Theorem& eq, const Expr& var);
865 
866  /**
867  * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
868  * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
869  * <ul>
870  * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
871  * <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
872  * </ul>
873  * Then, the explanation clause to be returned is
874  * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \;
875  * x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_i \leq x_i \right\rbrace\f]
876  *
877  * @param var_it the variable that caused the clash
878  * @return the theorem explainang the clash
879  */
881 
882  /**
883  * Knowing that the tableaux row for \f$x_i\f$ is the problematic one, generate the
884  * explanation clause. The variables in the row of \f$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}\f$ are separated to
885  * <ul>
886  * <li>\f$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace\f$
887  * <li>\f$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace\f$
888  * </ul>
889  * Then, the explanation clause to be returned is
890  * \f[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \;
891  * x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace x_i \leq u_i \right\rbrace\f]
892  *
893  * @param var_it the variable that caused the clash
894  * @return the theorem explainang the clash
895  */
897 
898  Theorem addInequalities(const Theorem& le_1, const Theorem& le_2);
899 
900  /**
901  * Check the satisfiability
902  */
904 
905  /**
906  * Check the satisfiability of integer constraints
907  */
909 
910  /**
911  * The last lemma that we asserted to check the integer satisfiability. We don't do checksat until
912  * the lemma split has been asserted.
913  */
915 
916  public:
917 
918  /**
919  * Gets the current lower bound on variable x.
920  *
921  * @param x the variable
922  * @return the current lower bound on x
923  */
924  EpsRational getLowerBound(const Expr& x) const;
925 
926  /**
927  * Get the current upper bound on variable x.
928  *
929  * @param x the variable
930  * @return the current upper bound on x
931  */
932  EpsRational getUpperBound(const Expr& x) const;
933 
934  /**
935  * Gets the theorem of the current lower bound on variable x.
936  *
937  * @param x the variable
938  * @return the current lower bound on x
939  */
940  Theorem getLowerBoundThm(const Expr& x) const;
941 
942  /**
943  * Get the theorem of the current upper bound on variable x.
944  *
945  * @param x the variable
946  * @return the current upper bound on x
947  */
948  Theorem getUpperBoundThm(const Expr& x) const;
949 
950  /**
951  * Gets the current valuation of variable x (beta).
952  *
953  * @param x the variable
954  * @return the current value of variable x
955  */
956  EpsRational getBeta(const Expr& x);
957 
958  // DDDDDDDDDDDDDDDDDDDDDDDDEEEEEEEEEEEEEEEEEEEEEEEJJJJJJJJJJJJJJJJJJJJJAAAAAAAAAAAAAAAAAAAAAAANNNNNNNNNNNNNNNNNNNNNNN
959 
960 };
961 
962 }
963 
964 #endif