CVC3  2.4.1
theory_arith_old.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file theory_arith_old.h
4  *
5  * Author: Clark Barrett
6  *
7  * Created: Thu Jun 14 13:22:11 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_old_h_
22 #define _cvc3__include__theory_arith_old_h_
23 
24 #include "theory_arith.h"
25 #include <set>
26 #include <list>
27 
28 namespace CVC3 {
29 
30 class TheoryArithOld :public TheoryArith {
31  CDList<Theorem> d_diseq; // For concrete model generation
32  CDO<size_t> d_diseqIdx; // Index to the next unprocessed disequality
33  CDMap<Expr, bool> diseqSplitAlready; // Have we eplit on this disequality already
36 
37  //! Data class for the strongest free constant in separation inqualities
38  class FreeConst {
39  private:
41  bool d_strict;
42  public:
43  FreeConst() { }
44  FreeConst(const Rational& r, bool strict): d_r(r), d_strict(strict) { }
45  const Rational& getConst() const { return d_r; }
46  bool strict() const { return d_strict; }
47  };
48  //! Printing
49  friend std::ostream& operator<<(std::ostream& os, const FreeConst& fc);
50 
51  //! Private class for an inequality in the Fourier-Motzkin database
52  class Ineq {
53  private:
54  Theorem d_ineq; //!< The inequality
55  bool d_rhs; //!< Var is isolated on the RHS
56  const FreeConst* d_const; //!< The max/min const for subsumption check
57  //! Default constructor is disabled
58  Ineq() { }
59  public:
60  //! Initial constructor. 'r' is taken from the subsumption database.
61  Ineq(const Theorem& ineq, bool varOnRHS, const FreeConst& c):
62  d_ineq(ineq), d_rhs(varOnRHS), d_const(&c) { }
63  //! Get the inequality
64  const Theorem ineq() const { return d_ineq; }
65  //! Get the max/min constant
66  const FreeConst& getConst() const { return *d_const; }
67  //! Flag whether var is isolated on the RHS
68  bool varOnRHS() const { return d_rhs; }
69  //! Flag whether var is isolated on the LHS
70  bool varOnLHS() const { return !d_rhs; }
71  //! Auto-cast to Theorem
72  operator Theorem() const { return d_ineq; }
73  };
74  //! Printing
75  friend std::ostream& operator<<(std::ostream& os, const Ineq& ineq);
76 
77  //! Database of inequalities with a variable isolated on the right
79 
80  //! Database of inequalities with a variable isolated on the left
82 
83  //! Mapping of inequalities to the largest/smallest free constant
84  /*! The Expr is the original inequality with the free constant
85  * removed and inequality converted to non-strict (for indexing
86  * purposes). I.e. ax<c+t becomes ax<=t. This inequality is mapped
87  * to a pair<c,strict>, the smallest (largest for c+t<ax) constant
88  * among inequalities with the same 'a', 'x', and 't', and a boolean
89  * flag indicating whether the strongest inequality is strict.
90  */
92 
93 // /** Is the problem only difference logic */
94 // CDO<bool> isDL;
95 // CDO<int> total_buf_size;
96 // CDO<int> processed;
97 //
98  // Input buffer to store the incoming inequalities
99  CDList<Theorem> d_buffer_0; //!< Buffer of input inequalities (high priority)
100  CDList<Theorem> d_buffer_1; //!< Buffer of input inequalities (one variable)
101  CDList<Theorem> d_buffer_2; //!< Buffer of input inequalities (small constraints)
102  CDList<Theorem> d_buffer_3; //!< Buffer of input inequalities (big constraint)
103 
104  CDO<size_t> d_bufferIdx_0; //!< Buffer index of the next unprocessed inequality
105  CDO<size_t> d_bufferIdx_1; //!< Buffer index of the next unprocessed inequality
106  CDO<size_t> d_bufferIdx_2; //!< Buffer index of the next unprocessed inequality
107  CDO<size_t> d_bufferIdx_3; //!< Buffer index of the next unprocessed inequality
108 
109  CDO<size_t> diff_logic_size; //!< Number of queries that are just difference logic
110 
111  const int* d_bufferThres; //!< Threshold when the buffer must be processed
112 
113  const bool* d_splitSign; // Whether to split on the signs of non-trivial nonlinear products
114 
115  const int* d_grayShadowThres; //!< Threshold on gray shadow size (ignore it and set incomplete)
116 
117  // Statistics for the variables
118 
119  /*! @brief Mapping of a variable to the number of inequalities where
120  the variable would be isolated on the right */
122 
123  /*! @brief Mapping of a variable to the number of inequalities where
124  the variable would be isolated on the left */
126 
127  //! Set of shared terms (for counterexample generation)
130 
131  //! Set of shared integer variables (i-leaves)
133 
134  //Directed Acyclic Graph representing partial variable ordering for
135  //variable projection over inequalities.
139  bool dfs(const Expr& e1, const Expr& e2);
140  void dfs(const Expr& e1, std::vector<Expr>& output_list);
141  public:
142  void addEdge(const Expr& e1, const Expr& e2);
143  //returns true if e1 < e2, false otherwise.
144  bool lessThan(const Expr& e1, const Expr& e2);
145  //selects those variables which are largest and incomparable among
146  //v1 and puts it into v2
147  void selectLargest(const std::vector<Expr>& v1, std::vector<Expr>& v2);
148  //selects those variables which are smallest and incomparable among
149  //v1, removes them from v1 and puts them into v2.
150  void selectSmallest( std::vector<Expr>& v1, std::vector<Expr>& v2);
151  //returns the list of vertices in the topological order
152  void getVerticesTopological(std::vector<Expr>& output_list);
153  };
154 
156 
157  // Private methods
158 
159  //! Check the term t for integrality.
160  /*! \return a theorem of IS_INTEGER(t) or Null. */
161  Theorem isIntegerThm(const Expr& e);
162 
163  //! A helper method for isIntegerThm()
164  /*! Check if IS_INTEGER(e) is easily derivable from the given 'thm' */
165  Theorem isIntegerDerive(const Expr& isIntE, const Theorem& thm);
166 
167  //! Extract the free constant from an inequality
168  const Rational& freeConstIneq(const Expr& ineq, bool varOnRHS);
169 
170  //! Update the free constant subsumption database with new inequality
171  /*! \return a reference to the max/min constant.
172  *
173  * Also, sets 'subsumed' argument to true if the inequality is
174  * subsumed by an existing inequality.
175  */
176  const FreeConst& updateSubsumptionDB(const Expr& ineq, bool varOnRHS,
177  bool& subsumed);
178  //! Check if the kids of e are fully simplified and canonized (for debugging)
179  bool kidsCanonical(const Expr& e);
180 
181  //! Canonize the expression e, assuming, all children are canonical
182  Theorem canon(const Expr& e);
183 
184  /*! @brief Canonize and reduce e w.r.t. union-find database; assume
185  * all children are canonical */
186  Theorem canonSimplify(const Expr& e);
187 
188  /*! @brief Composition of canonSimplify(const Expr&) by
189  * transitivity: take e0 = e1, canonize and simplify e1 to e2,
190  * return e0 = e2. */
192  return transitivityRule(thm, canonSimplify(thm.getRHS()));
193  }
194 
195  //! Canonize predicate (x = y, x < y, etc.)
196  Theorem canonPred(const Theorem& thm);
197 
198  //! Canonize predicate like canonPred except that the input theorem
199  //! is an equivalent transformation.
200  Theorem canonPredEquiv(const Theorem& thm);
201 
202  //! Solve an equation and return an equivalent Theorem in the solved form
203  Theorem doSolve(const Theorem& e);
204 
205  //! takes in a conjunction equivalence Thm and canonizes it.
207 
208  //! picks the monomial with the smallest abs(coeff) from the input
209  //integer equation.
210  bool pickIntEqMonomial(const Expr& right, Expr& isolated, bool& nonlin);
211 
212  //! processes equalities with 1 or more vars of type REAL
213  Theorem processRealEq(const Theorem& eqn);
214 
215  //! processes equalities whose vars are all of type INT
216  Theorem processIntEq(const Theorem& eqn);
217 
218  //! One step of INT equality processing (aux. method for processIntEq())
219  Theorem processSimpleIntEq(const Theorem& eqn);
220 
221  //! Process inequalities in the buffer
222  void processBuffer();
223 
224  //! Take an inequality and isolate a variable
225  Theorem isolateVariable(const Theorem& inputThm, bool& e1);
226 
227  //! Update the statistics counters for the variable with a coeff. c
228  void updateStats(const Rational& c, const Expr& var);
229 
230  //! Update the statistics counters for the monomial
231  void updateStats(const Expr& monomial);
232 
233  //! Add an inequality to the input buffer. See also d_buffer
234  bool addToBuffer(const Theorem& thm, bool priority = false);
235 
236  /*! @brief Given a canonized term, compute a factor to make all
237  coefficients integer and relatively prime */
238  Expr computeNormalFactor(const Expr& rhs, bool normalizeConstants);
239 
240  //! Normalize an equation (make all coefficients rel. prime integers)
241  Theorem normalize(const Expr& e);
242 
243  //! Normalize an equation (make all coefficients rel. prime integers)
244  /*! accepts a rewrite theorem over eqn|ineqn and normalizes it
245  * and returns a theorem to that effect.
246  */
247  Theorem normalize(const Theorem& thm);
248 
249  Expr pickMonomial(const Expr& right);
250 
251  void getFactors(const Expr& e, std::set<Expr>& factors);
252 
253  public: // ArithTheoremProducer needs these functions, so make them public
254  //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
255  void separateMonomial(const Expr& e, Expr& c, Expr& var);
256 
257  //! Check the term t for integrality (return bool)
258  bool isInteger(const Expr& e)
259  { return
260  isInt(e.getType()) ? true :
261  (isReal(e.getType()) ? false : !(isIntegerThm(e).isNull())); }
262 
263  private:
264 
265  bool lessThanVar(const Expr& isolatedVar, const Expr& var2);
266 
267  //! Check if the term expression is "stale"
268  bool isStale(const Expr& e);
269 
270  //! Check if the inequality is "stale" or subsumed
271  bool isStale(const Ineq& ineq);
272 
273  void projectInequalities(const Theorem& theInequality,bool isolatedVarOnRHS);
274 
275  void assignVariables(std::vector<Expr>&v);
276 
277  void findRationalBound(const Expr& varSide, const Expr& ratSide,
278  const Expr& var,
279  Rational &r);
280 
281  bool findBounds(const Expr& e, Rational& lub, Rational& glb);
282 
283  Theorem normalizeProjectIneqs(const Theorem& ineqThm1,
284  const Theorem& ineqThm2);
285 
286  //! Take a system of equations and turn it into a solved form
287  Theorem solvedForm(const std::vector<Theorem>& solvedEqs);
288 
289  /*! @brief Substitute all vars in term 't' according to the
290  * substitution 'subst' and canonize the result.
291  */
292  Theorem substAndCanonize(const Expr& t, ExprMap<Theorem>& subst);
293 
294  /*! @brief Substitute all vars in the RHS of the equation 'eq' of
295  * the form (x = t) according to the substitution 'subst', and
296  * canonize the result.
297  */
299 
300  //! Traverse 'e' and push all the i-leaves into 'vars' vector
301  void collectVars(const Expr& e, std::vector<Expr>& vars,
302  std::set<Expr>& cache);
303 
304  /*! @brief Check if alpha <= ax & bx <= beta is a finite interval
305  * for integer var 'x', and assert the corresponding constraint
306  */
307  void processFiniteInterval(const Theorem& alphaLEax,
308  const Theorem& bxLEbeta);
309 
310  //! For an integer var 'x', find and process all constraints A <= ax <= A+c
311  void processFiniteIntervals(const Expr& x);
312 
313  //! Recursive setup for isolated inequalities (and other new expressions)
314  void setupRec(const Expr& e);
315 
316 public:
317  TheoryArithOld(TheoryCore* core);
318  ~TheoryArithOld();
319 
320  // Trusted method that creates the proof rules class (used in constructor).
321  // Implemented in arith_theorem_producer.cpp
323 
324  // Theory interface
325  void addSharedTerm(const Expr& e);
326  void assertFact(const Theorem& e);
327  void refineCounterExample();
328  void computeModelBasic(const std::vector<Expr>& v);
329  void computeModel(const Expr& e, std::vector<Expr>& vars);
330  void checkSat(bool fullEffort);
331  Theorem rewrite(const Expr& e);
332  void setup(const Expr& e);
333  void update(const Theorem& e, const Expr& d);
334  Theorem solve(const Theorem& e);
335  void checkAssertEqInvariant(const Theorem& e);
336  void checkType(const Expr& e);
338  bool enumerate, bool computeSize);
339  void computeType(const Expr& e);
340  Type computeBaseType(const Type& t);
341  void computeModelTerm(const Expr& e, std::vector<Expr>& v);
342  Expr computeTypePred(const Type& t, const Expr& e);
343  Expr computeTCC(const Expr& e);
344  ExprStream& print(ExprStream& os, const Expr& e);
345  Expr parseExprOp(const Expr& e);
346 
347 private:
348 
349  /** Map from variables to the maximal (by absolute value) of one of it's coefficients */
352 
353  /** Map from variables to the fixed value of one of it's coefficients */
355 
356  /**
357  * Returns the current maximal coefficient of the variable.
358  *
359  * @param var the variable.
360  */
362 
363  /**
364  * Fixes the current max coefficient to be used in the ordering. If the maximal coefficient
365  * changes in the future, it will not be used in the ordering.
366  *
367  * @param variable the variable
368  * @param max the value to set it to
369  */
370  void fixCurrentMaxCoefficient(Expr variable, Rational max);
371 
372  /**
373  * Among given input variables, select the smallest ones with respect to the coefficients.
374  */
375  void selectSmallestByCoefficient(const std::vector<Expr>& input, std::vector<Expr>& output);
376 
377  /**
378  * Given an inequality theorem check if it is on integers and get rid of the non-integer
379  * constants.
380  */
382 
383  /**
384  * Given an equality theorem check if it is on integers with a non-integer constant. If
385  * yes, return a theorem 0 = 1
386  */
388 
389  /** Keep the expressions that are already in the buffer */
391 
392  /** Strict lower bounds on terms, so that we don't add inequalities to the buffer */
395  /** Strict upper bounds on terms, so that we don't add inequalities to the buffer */
398 
399  /**
400  * Which inequalities have already been projected (on which monomial).
401  * - if we get an update of an inequality that's not been projected, we don't care
402  * it will get projected (it's find)
403  * - when projecting, project the finds, not the originals
404  * - when done projecting add here, both original and the find
405  */
407 
408  /**
409  * Sometimes we know an inequality is in the buffer (as a find of something) and
410  * we don't want it in the buffer, but we do want to pre-process it, so we put it
411  * here.
412  */
414 
415  /**
416  * Are we doing only difference logic?
417  */
419 
420  /**
421  * Takes an inequality theorem and substitutes the rhs for it's find. It also get's normalized.
422  */
423  Theorem inequalityToFind(const Theorem& inequalityThm, bool normalizeRHS);
424 
425  // x -y <= c
426  struct GraphEdge {
430  };
431 
432  /**
433  * Take inequality of the form 0 op t and extract the c1, t1, c2 and t2, such that
434  * c1 <= t1 and t2 <= c2, where c1 and c2 are constants, and t1 and t2 are either
435  * sums of monomials or a monomial.
436  *
437  * @return the number of variables in terms t1 and t2
438  */
439  int extractTermsFromInequality(const Expr& inequality,
440  Rational& c1, Expr& t1,
441  Rational& c2, Expr& t2);
442 
443  void registerAtom(const Expr& e);
444 
446 
447  /** Map from terms to their lower bound (and the original formula expression) */
449 
450  /** Map from terms to their upper bound (and the original formula expression) */
452 
453  /** Map of all the atoms in the formula */
455 
457 
458  public:
459 
460  /**
461  * EpsRational class ecapsulates the rationals with a symbolic small \f$\epsilon\f$ added. Each rational
462  * number is presented as a pair \f$(q, k) = q + k\epsilon\f$, where \f$\epsilon\f$ is treated symbolically.
463  * The operations on the new rationals are defined as
464  * <ul>
465  * <li>\f$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)\f$
466  * <li>\f$a \times (q, k) \equiv (a \times q, a \times k)\f$
467  * <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$
468  * </ul>
469  *
470  * Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can
471  * only be asigned or compared.
472  */
473  class EpsRational {
474 
475  protected:
476 
477  /** Type of rationals, normal and the two infinities */
479 
480  /** The type of this rational */
482 
483  /** The rational part */
485 
486  /** The epsilon multiplier */
488 
489  /**
490  * Private constructor to construt infinities.
491  */
492  EpsRational(RationalType type) : type(type) {}
493 
494  public:
495 
496  /**
497  * Returns if the numbe is finite.
498  */
499  inline bool isFinite() const { return type == FINITE; }
500 
501  /**
502  * Returns if the number is a plain rational.
503  *
504  * @return true if rational, false otherwise
505  */
506  inline bool isRational() const { return k == 0; }
507 
508  /**
509  * Returns if the number is a plain integer.
510  *
511  * @return true if rational, false otherwise
512  */
513  inline bool isInteger() const { return k == 0 && q.isInteger(); }
514 
515  /**
516  * Returns the floor of the number \f$x = q + k \epsilon\f$ using the following fomula
517  * \f[
518  * \lfloor \beta(x) \rfloor =
519  * \begin{cases}
520  * \lfloor q \rfloor & \text{ if } q \notin Z\\
521  * q & \text{ if } q \in Z \text{ and } k \geq 0\\
522  * q - 1 & \text{ if } q \in Z \text{ and } k < 0
523  * \end{cases}
524  * \f]
525  */
526  inline Rational getFloor() const {
527  if (q.isInteger()) {
528  if (k >= 0) return q;
529  else return q - 1;
530  } else
531  // If not an integer, just floor it
532  return floor(q);
533  }
534 
535 
536  /**
537  * Returns the rational part of the number
538  *
539  * @return the rational
540  */
541  inline Rational getRational() const { return q; }
542 
543  /**
544  * Returns the epsilon part of the number
545  *
546  * @return the epsilon
547  */
548  inline Rational getEpsilon() const { return k; }
549 
550  /** The infinity constant */
551  static const EpsRational PlusInfinity;
552  /** The negative infinity constant */
554  /** The zero constant */
555  static const EpsRational Zero;
556 
557 
558  /** The blank constructor */
559  EpsRational() : type(FINITE), q(0), k(0) {}
560 
561  /** Copy constructor */
562  EpsRational(const EpsRational& r) : type(r.type), q(r.q), k(r.k) {}
563 
564  /**
565  * Constructor from a rational, constructs a new pair (q, 0).
566  *
567  * @param q the rational
568  */
569  EpsRational(const Rational& q) : type(FINITE), q(q), k(0) {}
570 
571  /**
572  * Constructor from a rational and a given epsilon multiplier, constructs a
573  * new pair (q, k).
574  *
575  * @param q the rational
576  * @param k the epsilon multiplier
577  */
578  EpsRational(const Rational& q, const Rational& k) : type(FINITE), q(q), k(k) {}
579 
580  /**
581  * Addition operator for two EpsRational numbers.
582  *
583  * @param r the number to be added
584  * @return the sum as defined in the class
585  */
586  inline EpsRational operator + (const EpsRational& r) const {
587  DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
588  DebugAssert(r.type == FINITE, "EpsRational::operator +, adding an infinite number");
589  return EpsRational(q + r.q, k + r.k);
590  }
591 
592  /**
593  * Addition operator for two EpsRational numbers.
594  *
595  * @param r the number to be added
596  * @return the sum as defined in the class
597  */
599  DebugAssert(type == FINITE, "EpsRational::operator +, adding to infinite number");
600  q = q + r.q;
601  k = k + r.k;
602  return *this;
603  }
604 
605  /**
606  * Subtraction operator for two EpsRational numbers.
607  *
608  * @param r the number to be added
609  * @return the sum as defined in the class
610  */
611  inline EpsRational operator - (const EpsRational& r) const {
612  DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
613  DebugAssert(r.type == FINITE, "EpsRational::operator -, subtracting an infinite number");
614  return EpsRational(q - r.q, k - r.k);
615  }
616 
617  /**
618  * Unary minus operator
619  */
621  DebugAssert(type == FINITE, "EpsRational::operator -, subtracting from infinite number");
622  q = -q;
623  k = -k;
624  return *this;
625  }
626 
627 
628  /**
629  * Multiplication operator EpsRational number and a rational number.
630  *
631  * @param a the number to be multiplied
632  * @return the product as defined in the class
633  */
634  inline EpsRational operator * (const Rational& a) const {
635  DebugAssert(type == FINITE, "EpsRational::operator *, multiplying an infinite number");
636  return EpsRational(a * q, a * k);
637  }
638 
639  /**
640  * Division operator EpsRational number and a rational number.
641  *
642  * @param a the number to be multiplied
643  * @return the product as defined in the class
644  */
645  inline EpsRational operator / (const Rational& a) const {
646  DebugAssert(type == FINITE, "EpsRational::operator *, dividing an infinite number");
647  return EpsRational(q / a, k / a);
648  }
649 
650  /**
651  * Equality comparison operator.
652  */
653  inline bool operator == (const EpsRational& r) const { return (q == r.q && k == r.k); }
654 
655  /**
656  * Less than or equal comparison operator.
657  */
658  inline bool operator <= (const EpsRational& r) const {
659  switch (r.type) {
660  case FINITE:
661  if (type == FINITE)
662  // Normal comparison
663  return (q < r.q || (q == r.q && k <= r.k));
664  else
665  // Finite number is bigger only of the negative infinity
666  return type == MINUS_INFINITY;
667  case PLUS_INFINITY:
668  // Everything is less then or equal than +inf
669  return true;
670  case MINUS_INFINITY:
671  // Only -inf is less then or equal than -inf
672  return (type == MINUS_INFINITY);
673  default:
674  // Ohohohohohoooooo, whats up
675  FatalAssert(false, "EpsRational::operator <=, what kind of number is this????");
676  }
677  return false;
678  }
679 
680  /**
681  * Less than comparison operator.
682  */
683  inline bool operator < (const EpsRational& r) const { return !(r <= *this); }
684 
685  /**
686  * Greater than comparison operator.
687  */
688  inline bool operator > (const EpsRational& r) const { return !(*this <= r); }
689 
690  /**
691  * Returns the string representation of the number.
692  *
693  * @return the string representation of the number
694  */
695  std::string toString() const {
696  switch (type) {
697  case FINITE:
698  return "(" + q.toString() + ", " + k.toString() + ")";
699  case PLUS_INFINITY:
700  return "+inf";
701  case MINUS_INFINITY:
702  return "-inf";
703  default:
704  FatalAssert(false, "EpsRational::toString, what kind of number is this????");
705  }
706  return "hm, what am I?";
707  }
708  };
709 
710  struct EdgeInfo {
711  /** The length of this edge */
713  /** The number of edges in this path */
715  /** If this is a summary edge, a vertex in the path */
717  /** If this is an original edge, the theorem that explains it */
719 
720  /** Returnes if the edge is well define (i.e. not +infinity) */
721  bool isDefined() const { return path_length_in_edges != 0; }
722 
724  };
725 
726  /**
727  * Given two vertices in the graph and an path edge, reconstruct all the theorems and put them
728  * in the output vector
729  */
730  void getEdgeTheorems(const Expr& x, const Expr& y, const EdgeInfo& edgeInfo, std::vector<Theorem>& outputTheorems);
731 
732  /**
733  * Returns the current weight of the edge.
734  */
735  EpsRational getEdgeWeight(const Expr& x, const Expr& y);
736 
737  /**
738  * Returns whether a vertex has incoming edges.
739  */
740  bool hasIncoming(const Expr& x);
741 
742  /**
743  * Returns whether a vertex has outgoing edges.
744  */
745  bool hasOutgoing(const Expr& x);
746 
747  protected:
748 
749  /** Threshold on path length to process (ignore bigger than and set incomplete) */
750  const int* d_pathLenghtThres;
751 
752  /** The arithmetic that's using this graph */
754 
755  /** The core theory */
757 
758  /** The arithmetic that is using u us */
760 
761  /** The unsat theorem if available */
763 
764  /** The biggest epsilon from EpsRational we used in paths */
766 
767  /** The smallest rational difference we used in path relaxation */
769 
770  /** The graph itself, maps expressions (x-y) to the edge information */
772 
773  /** Graph of <= paths */
775 
777 
778  /** List of vertices adjacent backwards to a vertex */
780  /** List of vertices adjacent forward to a vertex */
782 
783  /**
784  * Returns the edge (path) info for the given kind
785  *
786  * @param x the starting vertex
787  * @param y the ending vertex
788  * @return the edge information
789  */
790  Graph::ElementReference getEdge(const Expr& x, const Expr& y);
791 
792  /**
793  * Try to update the shortest path from x to z using y.
794  */
795  bool tryUpdate(const Expr& x, const Expr& y, const Expr& z);
796 
797  public:
798 
799  void writeGraph(std::ostream& out);
800 
801  /**
802  * Fills the vector with all the variables (vertices) in the graph
803  */
804  void getVariables(std::vector<Expr>& variables);
805 
807  this->rules = rules;
808  }
809 
811  this->arith = arith;
812  }
813 
814  /**
815  * Class constructor.
816  */
818 
819  /**
820  * Destructor
821  */
823 
824  /**
825  * Returns the reference to the unsat theorem if there is a negative
826  * cycle in the graph.
827  *
828  * @return the unsat theorem
829  */
830 
832 
833  /**
834  * Returns true if there is a negative cycle in the graph.
835  */
836  bool isUnsat();
837 
838  void computeModel();
839 
840  Rational getValuation(const Expr& x);
841 
842 
843  /**
844  * Adds an edge corresponding to the constraint x - y <= c.
845  *
846  * @param x variable x::Difference
847  * @param y variable y
848  * @param c rational c
849  * @param edge_thm the theorem for this edge
850  */
851  void addEdge(const Expr& x, const Expr& y, const Rational& c, const Theorem& edge_thm);
852 
853  /**
854  * Check if there is an edge from x to y
855  */
856  bool existsEdge(const Expr& x, const Expr& y);
857 
858  /**
859  * Check if x is in a cycle
860  */
861  bool inCycle(const Expr& x);
862 
863  /**
864  * Given a shared integer term expand it into the gray shadow on the bounds (if bounded from both sides).
865  */
866  void expandSharedTerm(const Expr& x);
867 
868  protected:
869 
870  /** Whether the variable is in a cycle */
872 
874 
875  /**
876  * Produced the unsat theorem from a cycle x --> x of negative length
877  *
878  * @param x the variable to use for the conflict
879  * @param kind the kind of edges to consider
880  */
881  void analyseConflict(const Expr& x, int kind);
882  };
883 
884  /** The graph for difference logic */
886 
888 
889  /** Index for expanding on shared term equalities */
891  /** Index for expanding on shared term equalities */
893 
894  std::vector<Theorem> multiplicativeSignSplits;
895 
896  int termDegree(const Expr& e);
897 
898  bool canPickEqMonomial(const Expr& right);
899 
900 private:
901 
902  // Keeps all expressions that are bounded for disequality splitting and shared term comparisons
905 
908 
909  // Keeps all expressions that are constrained
912 
914  /** Query the bounds/constrained using cache for leaves */
916  /** Query the bounds/constrained using cashe for leaves, but also see if the value is constrained */
918  /** Query the bounds/constrained by only querying the cache, don't try to figure it out */
920  };
921 
922  /**
923  * Check if the term is bounded. If the term is non-linear, just returns false.
924  */
925  bool isBounded(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
926  bool hasLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getLowerBound(t, queryType).isFinite(); }
927  bool hasUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves) { return getUpperBound(t, queryType).isFinite(); }
928 
929  bool isConstrained(const Expr& t, bool intOnly = true, BoundsQueryType queryType = QueryWithCacheLeaves);
930  bool isConstrainedAbove(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
931  bool isConstrainedBelow(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
932 
933  /**
934  * Check if the term is bounded from above. If the term is non-linear, just returns false.
935  */
936  DifferenceLogicGraph::EpsRational getUpperBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
937 
938  /**
939  * Check if the term is bouned from below. If the term is non-linear, just return false.
940  */
941  DifferenceLogicGraph::EpsRational getLowerBound(const Expr& t, BoundsQueryType queryType = QueryWithCacheLeaves);
942 
943  /**
944  * See whether and which terms are bounded.
945  */
946  int computeTermBounds();
947 
948 public:
949 
950  void updateConstrained(const Expr& t);
951  bool isUnconstrained(const Expr& t);
952 
953  void tryPropagate(const Expr& x, const Expr& y, const DifferenceLogicGraph::EdgeInfo& x_y_edge, int kind);
954 
955  void addMultiplicativeSignSplit(const Theorem& case_split_thm);
956 
957  bool addPairToArithOrder(const Expr& smaller, const Expr& bigger);
958 
959  bool nonlinearSignSplit() const { return *d_splitSign; }
960 
961  /**
962  * Check if equation is nonlinear. An equation is nonlinear if there is at least one nonlinear term in the sum
963  * on either side of the equation.
964  */
965  bool isNonlinearEq(const Expr& e);
966 
967  /**
968  * Check if a sum term is nonlinear
969  */
970  bool isNonlinearSumTerm(const Expr& term);
971 
972  /**
973  * Check if the equality is of the form c + power1^n - power2^n = 0;
974  */
975  bool isPowersEquality(const Expr& nonlinearEq, Expr& power1, Expr& power2);
976 
977  /**
978  * Check if the equality is of the form c - x^n = 0
979  */
980  bool isPowerEquality(const Expr& nonlinearEq, Rational& constant, Expr& power1);
981 
982 };
983 
984 }
985 
986 #endif
EpsRational operator*(const Rational &a) const
Theorem d_ineq
The inequality.
ArithProofRules * createProofRulesOld()
CDMap< Expr, bool > d_varConstrainedMinus
bool lessThanVar(const Expr &isolatedVar, const Expr &var2)
Theorem isolateVariable(const Theorem &inputThm, bool &e1)
Take an inequality and isolate a variable.
bool kidsCanonical(const Expr &e)
Check if the kids of e are fully simplified and canonized (for debugging)
bool isInt(Type t)
Definition: theory_arith.h:174
void processFiniteIntervals(const Expr &x)
For an integer var 'x', find and process all constraints A <= ax <= A+c.
void addSharedTerm(const Expr &e)
Notify theory of a new shared term.
Data structure of expressions in CVC3.
Definition: expr.h:133
This theory handles the built-in logical connectives plus equality. It also handles the registration ...
Definition: theory_core.h:53
void separateMonomial(const Expr &e, Expr &c, Expr &var)
Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn.
CDO< bool > d_inModelCreation
void computeModelTerm(const Expr &e, std::vector< Expr > &v)
Add variables from 'e' to 'v' for constructing a concrete model.
ExprMap< Rational > maxCoefficientRight
ExprMap< CDList< Ineq > * > d_inequalitiesLeftDB
Database of inequalities with a variable isolated on the left.
void updateConstrained(const Expr &t)
void addEdge(const Expr &x, const Expr &y, const Rational &c, const Theorem &edge_thm)
void registerAtom(const Expr &e)
Theory-specific registration of atoms.
friend std::ostream & operator<<(std::ostream &os, const FreeConst &fc)
Printing.
DifferenceLogicGraph::EpsRational getLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
bool addToBuffer(const Theorem &thm, bool priority=false)
Add an inequality to the input buffer. See also d_buffer.
void fixCurrentMaxCoefficient(Expr variable, Rational max)
bool isNonlinearEq(const Expr &e)
This theory handles basic linear arithmetic.
Definition: theory_arith.h:70
DifferenceLogicGraph diffLogicGraph
CDMap< Expr, int > d_countRight
Mapping of a variable to the number of inequalities where the variable would be isolated on the right...
const FreeConst & updateSubsumptionDB(const Expr &ineq, bool varOnRHS, bool &subsumed)
Update the free constant subsumption database with new inequality.
bool isConstrainedAbove(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
bool isStale(const Expr &e)
Check if the term expression is "stale".
T max(T a, T b)
Definition: cvc_util.h:56
const Theorem ineq() const
Get the inequality.
Theorem solve(const Theorem &e)
An optional solver.
MS C++ specific settings.
Definition: type.h:42
bool hasLowerBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
ExprStream & print(ExprStream &os, const Expr &e)
Theory-specific pretty-printing.
const int * d_bufferThres
Threshold when the buffer must be processed.
Expr computeTCC(const Expr &e)
Compute and cache the TCC of e.
void assertFact(const Theorem &e)
Assert a new fact to the decision procedure.
CDMap< Expr, FreeConst > d_freeConstDB
Mapping of inequalities to the largest/smallest free constant.
ExprMap< Rational > fixedMaxCoefficient
CDMap< Expr, DifferenceLogicGraph::EpsRational > termLowerBounded
CDList< Theorem > d_buffer_1
Buffer of input inequalities (one variable)
std::string toString(int base=10) const
Graph::ElementReference getEdge(const Expr &x, const Expr &y)
CDMap< Expr, Rational > termUpperBound
const Rational & freeConstIneq(const Expr &ineq, bool varOnRHS)
Extract the free constant from an inequality.
#define DebugAssert(cond, str)
Definition: debug.h:408
CDList< Theorem > d_diseq
CDO< unsigned > shared_index_2
DifferenceLogicGraph::EpsRational getUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem substAndCanonize(const Expr &t, ExprMap< Theorem > &subst)
Substitute all vars in term 't' according to the substitution 'subst' and canonize the result...
bool dfs(const Expr &e1, const Expr &e2)
CDMap< Expr, bool > d_sharedVars
Set of shared integer variables (i-leaves)
Expr computeNormalFactor(const Expr &rhs, bool normalizeConstants)
Given a canonized term, compute a factor to make all coefficients integer and relatively prime...
CDMap< Expr, Expr > alreadyProjected
Theorem inequalityToFind(const Theorem &inequalityThm, bool normalizeRHS)
Theorem normalizeProjectIneqs(const Theorem &ineqThm1, const Theorem &ineqThm2)
Theorem checkIntegerEquality(const Theorem &thm)
bool hasUpperBound(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem canonSimplify(const Theorem &thm)
Composition of canonSimplify(const Expr&) by transitivity: take e0 = e1, canonize and simplify e1 to ...
Theorem canon(const Expr &e)
Canonize the expression e, assuming, all children are canonical.
Private class for an inequality in the Fourier-Motzkin database.
void updateStats(const Rational &c, const Expr &var)
Update the statistics counters for the variable with a coeff. c.
bool varOnRHS() const
Flag whether var is isolated on the RHS.
CDMap< Expr, bool > termConstrainedAbove
const FreeConst & getConst() const
Get the max/min constant.
bool addPairToArithOrder(const Expr &smaller, const Expr &bigger)
EpsRational getEdgeWeight(const Expr &x, const Expr &y)
void computeType(const Expr &e)
Compute and store the type of e.
void assignVariables(std::vector< Expr > &v)
CDO< size_t > diff_logic_size
Number of queries that are just difference logic.
bool varOnLHS() const
Flag whether var is isolated on the LHS.
void selectSmallestByCoefficient(const std::vector< Expr > &input, std::vector< Expr > &output)
CDMap< Expr, DifferenceLogicGraph::EpsRational > termUpperBounded
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
void refineCounterExample()
Process disequalities from the arrangement for model generation.
std::vector< Theorem > multiplicativeSignSplits
bool isInteger() const
Cardinality finiteTypeInfo(Expr &e, Unsigned &n, bool enumerate, bool computeSize)
Compute information related to finiteness of types.
void checkSat(bool fullEffort)
Check for satisfiability in the theory.
void update(const Theorem &e, const Expr &d)
Notify a theory of a new equality.
Theorem isIntegerDerive(const Expr &isIntE, const Theorem &thm)
A helper method for isIntegerThm()
CDMap< Expr, Theorem > termLowerBoundThm
Theorem canonPredEquiv(const Theorem &thm)
Expr parseExprOp(const Expr &e)
Theory-specific parsing implemented by the DP.
int termDegree(const Expr &e)
CDMap< Expr, Theorem > bufferedInequalities
CDMap< Expr, bool > diseqSplitAlready
void getFactors(const Expr &e, std::set< Expr > &factors)
bool isPowersEquality(const Expr &nonlinearEq, Expr &power1, Expr &power2)
Pretty-printing output stream for Expr. READ THE DOCS BEFORE USING!
Definition: expr_stream.h:110
bool isConstrainedBelow(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
Theorem isIntegerThm(const Expr &e)
Check the term t for integrality.
const Expr & getRHS() const
Definition: theorem.cpp:246
void getEdgeTheorems(const Expr &x, const Expr &y, const EdgeInfo &edgeInfo, std::vector< Theorem > &outputTheorems)
Type computeBaseType(const Type &t)
Compute the base type of the top-level operator of an arbitrary type.
bool tryUpdate(const Expr &x, const Expr &y, const Expr &z)
void selectSmallest(std::vector< Expr > &v1, std::vector< Expr > &v2)
TheoryArithOld(TheoryCore *core)
bool isInteger(const Expr &e)
Check the term t for integrality (return bool)
CDO< unsigned > shared_index_1
bool d_rhs
Var is isolated on the RHS.
Theorem doSolve(const Theorem &e)
Solve an equation and return an equivalent Theorem in the solved form.
void collectVars(const Expr &e, std::vector< Expr > &vars, std::set< Expr > &cache)
Traverse 'e' and push all the i-leaves into 'vars' vector.
bool isNull() const
Definition: theorem.h:164
bool nonlinearSignSplit() const
void computeModel(const Expr &e, std::vector< Expr > &vars)
Compute the value of a compound variable from the more primitive ones.
ArithProofRules * d_rules
bool isUnconstrained(const Expr &t)
ExprMap< std::vector< Expr > > d_edges
void processFiniteInterval(const Theorem &alphaLEax, const Theorem &bxLEbeta)
Check if alpha <= ax & bx <= beta is a finite interval for integer var 'x', and assert the corresponding ...
CDMap< Expr, Rational > termLowerBound
CDMap< Expr, bool > termConstrainedBelow
void checkType(const Expr &e)
Check that e is a valid Type expr.
Theorem processRealEq(const Theorem &eqn)
processes equalities with 1 or more vars of type REAL
Theorem processSimpleIntEq(const Theorem &eqn)
One step of INT equality processing (aux. method for processIntEq())
bool existsEdge(const Expr &x, const Expr &y)
bool isPowerEquality(const Expr &nonlinearEq, Rational &constant, Expr &power1)
ExprMap< Rational > maxCoefficientLeft
static int right(int i)
Definition: minisat_heap.h:54
void addEdge(const Expr &e1, const Expr &e2)
Theorem canonPred(const Theorem &thm)
Canonize predicate (x = y, x < y, etc.)
void projectInequalities(const Theorem &theInequality, bool isolatedVarOnRHS)
Theorem normalize(const Expr &e)
Normalize an equation (make all coefficients rel. prime integers)
bool lessThan(const Expr &e1, const Expr &e2)
CDMap< Expr, bool > d_varConstrainedPlus
void setupRec(const Expr &e)
Recursive setup for isolated inequalities (and other new expressions)
Theorem rafineInequalityToInteger(const Theorem &thm)
bool canPickEqMonomial(const Expr &right)
Ineq(const Theorem &ineq, bool varOnRHS, const FreeConst &c)
Initial constructor. 'r' is taken from the subsumption database.
bool isNonlinearSumTerm(const Expr &term)
EpsRational operator/(const Rational &a) const
CDList< Theorem > d_buffer_0
Buffer of input inequalities (high priority)
Expr computeTypePred(const Type &t, const Expr &e)
Theory specific computation of the subtyping predicate for type t applied to the expression e...
void addMultiplicativeSignSplit(const Theorem &case_split_thm)
bool pickIntEqMonomial(const Expr &right, Expr &isolated, bool &nonlin)
picks the monomial with the smallest abs(coeff) from the input
void analyseConflict(const Expr &x, int kind)
void findRationalBound(const Expr &varSide, const Expr &ratSide, const Expr &var, Rational &r)
void selectLargest(const std::vector< Expr > &v1, std::vector< Expr > &v2)
CDO< size_t > d_bufferIdx_2
Buffer index of the next unprocessed inequality.
CDO< size_t > d_bufferIdx_1
Buffer index of the next unprocessed inequality.
Theorem processIntEq(const Theorem &eqn)
processes equalities whose vars are all of type INT
bool isBounded(const Expr &t, BoundsQueryType queryType=QueryWithCacheLeaves)
CDO< size_t > d_bufferIdx_3
Buffer index of the next unprocessed inequality.
CDList< Expr > d_sharedTermsList
const int * d_grayShadowThres
Threshold on gray shadow size (ignore it and set incomplete)
bool findBounds(const Expr &e, Rational &lub, Rational &glb)
CDMap< Expr, int > d_countLeft
Mapping of a variable to the number of inequalities where the variable would be isolated on the left...
ExprMap< CDList< Ineq > * > d_inequalitiesRightDB
Database of inequalities with a variable isolated on the right.
CDO< size_t > d_bufferIdx_0
Buffer index of the next unprocessed inequality.
ExprMap< std::set< std::pair< Rational, Expr > > > AtomsMap
const Rational & getConst() const
Cardinality
Enum for cardinality of types.
Definition: expr.h:80
CDMap< Expr, bool > dontBuffer
CDMap< Expr, Theorem > termUpperBoundThm
FreeConst(const Rational &r, bool strict)
bool isReal(Type t)
Definition: theory_arith.h:173
bool isConstrained(const Expr &t, bool intOnly=true, BoundsQueryType queryType=QueryWithCacheLeaves)
Data class for the strongest free constant in separation inqualities.
void setup(const Expr &e)
Set up the term e for call-backs when e or its children change.
Theorem canonSimplify(const Expr &e)
Canonize and reduce e w.r.t. union-find database; assume all children are canonical.
Type getType() const
Get the type. Recursively compute if necessary.
Definition: expr.h:1259
CDList< Theorem > d_buffer_3
Buffer of input inequalities (big constraint)
Ineq()
Default constructor is disabled.
void getVerticesTopological(std::vector< Expr > &output_list)
Theorem canonConjunctionEquiv(const Theorem &thm)
takes in a conjunction equivalence Thm and canonizes it.
void tryPropagate(const Expr &x, const Expr &y, const DifferenceLogicGraph::EdgeInfo &x_y_edge, int kind)
CDO< size_t > d_diseqIdx
Theorem solvedForm(const std::vector< Theorem > &solvedEqs)
Take a system of equations and turn it into a solved form.
int extractTermsFromInequality(const Expr &inequality, Rational &c1, Expr &t1, Rational &c2, Expr &t2)
Rational currentMaxCoefficient(Expr var)
EpsRational operator+(const EpsRational &r) const
void computeModelBasic(const std::vector< Expr > &v)
Assign concrete values to basic-type variables in v.
Theorem rewrite(const Expr &e)
Theory-specific rewrite rules.
void getVariables(std::vector< Expr > &variables)
DifferenceLogicGraph(TheoryArithOld *arith, TheoryCore *core, ArithProofRules *rules, Context *context)
ExprMap< bool > formulaAtoms
Theorem transitivityRule(const Theorem &a1_eq_a2, const Theorem &a2_eq_a3)
(a1 == a2) & (a2 == a3) ==> (a1 == a3)
Definition: theory.h:681
Expr pickMonomial(const Expr &right)
CDList< Theorem > d_buffer_2
Buffer of input inequalities (small constraints)
void checkAssertEqInvariant(const Theorem &e)
A debug check used by the primary solver.
EpsRational(const Rational &q, const Rational &k)
void processBuffer()
Process inequalities in the buffer.
CDMap< Expr, bool > d_sharedTerms
Set of shared terms (for counterexample generation)