CVC3  2.4.1
arith_proof_rules.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file arith_proof_rules.h
4  * \brief Arithmetic proof rules
5  *
6  * Author: Vijay Ganesh, Sergey Berezin
7  *
8  * Created: Dec 13 02:09:04 GMT 2002
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__arith_proof_rules_h_
23 #define _cvc3__arith_proof_rules_h_
24 
25 #include <vector>
26 
27 namespace CVC3 {
28 
29  class Theorem;
30  class Expr;
31  class Rational;
32 
34  public:
35  // Destructor
36  virtual ~ArithProofRules() { }
37 
38  ////////////////////////////////////////////////////////////////////
39  // Canonization rules
40  ////////////////////////////////////////////////////////////////////
41 
42  //! ==> e = 1 * e
43  virtual Theorem varToMult(const Expr& e) = 0;
44 
45  //! ==> -(e) = (-1) * e
46  virtual Theorem uMinusToMult(const Expr& e) = 0;
47 
48  //! ==> x - y = x + (-1) * y
49  virtual Theorem minusToPlus(const Expr& x, const Expr& y) = 0;
50 
51  //! -(e) ==> e / (-1); takes 'e'
52  /*! Canon Rule for unary minus: it just converts it to division by
53  * -1, the result is not yet canonical:
54  */
55  virtual Theorem canonUMinusToDivide(const Expr& e) = 0;
56 
57  /**
58  * Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first
59  * sum term (r) must be a rational and t1 ... tn terms must be canonised.
60  *
61  * @param e the expression to transform
62  * @return rewrite theorem representing the transformation
63  */
64  virtual Theorem moveSumConstantRight(const Expr& e) = 0;
65 
66  //! (c) / d ==> (c/d), takes c and d
67  /*! Canon Rules for division by constant 'd' */
68  virtual Theorem canonDivideConst(const Expr& c, const Expr& d) = 0;
69  //! (c * x) / d ==> (c/d) * x, takes (c*x) and d
70  virtual Theorem canonDivideMult(const Expr& cx, const Expr& d) = 0;
71  //! (+ c ...)/d ==> push division to all the coefficients.
72  /*! The result is not canonical, but canonizing the summands will
73  * make it canonical.
74  * Takes (+ c ...) and d
75  */
76  virtual Theorem canonDividePlus(const Expr& e, const Expr& d) = 0;
77  //! x / d ==> (1/d) * x, takes x and d
78  virtual Theorem canonDivideVar(const Expr& e, const Expr& d) = 0;
79 
80  // Canon Rules for multiplication
81 
82  // TODO Deepak:
83  // e == t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a
84  // 1) Rational constant
85  // 2) Arithmetic Leaf (var or term from another theory)
86  // 3) (POW rational leaf)
87  // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
88  // 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of
89  // type (2) or (3) or (4)
90  virtual Theorem canonMultMtermMterm(const Expr& e) = 0;
91  //! Canonize (PLUS t1 ... tn)
92  virtual Theorem canonPlus(const Expr & e) = 0;
93  //! Canonize (MULT t1 ... tn)
94  virtual Theorem canonMult(const Expr & e) = 0;
95  //! ==> 1/e = e' where e' is canonical; takes e.
96  virtual Theorem canonInvert(const Expr & e) = 0;
97  //! Canonize t1/t2
98  virtual Theorem canonDivide(const Expr & e) = 0;
99 
100  //! t*c ==> c*t, takes constant c and term t
101  virtual Theorem canonMultTermConst(const Expr& c, const Expr& t) = 0;
102  //! t1*t2 ==> Error, takes t1 and t2 where both are non-constants
103  virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2) = 0;
104  //! 0*t ==> 0, takes 0*t
105  virtual Theorem canonMultZero(const Expr& e) = 0;
106  //! 1*t ==> t, takes 1*t
107  virtual Theorem canonMultOne(const Expr& e) = 0;
108  //! c1*c2 ==> c', takes constant c1*c2
109  virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2) = 0;
110  //! c1*(c2*t) ==> c'*t, takes c1 and c2 and t
111  virtual Theorem
112  canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t) = 0;
113  //! c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
114  virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum) = 0;
115  //! c^n = c' (compute the constant power expression)
116  virtual Theorem canonPowConst(const Expr& pow) = 0;
117 
118  // Rules for addition
119  //! flattens the input. accepts a PLUS expr
120  virtual Theorem canonFlattenSum(const Expr& e) = 0;
121 
122  //! combine like terms. accepts a flattened PLUS expr
123  virtual Theorem canonComboLikeTerms(const Expr& e) = 0;
124 
125  // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
126  virtual Theorem multEqZero(const Expr& expr) = 0;
127 
128  // 0 = (^ c x) <=> false if c <=0
129  // <=> 0 = x if c > 0
130  virtual Theorem powEqZero(const Expr& expr) = 0;
131 
132  // x^n = y^n <=> x = y (if n is odd)
133  // x^n = y^n <=> x = y OR x = -y (if n is even)
134  virtual Theorem elimPower(const Expr& expr) = 0;
135 
136  // x^n = c <=> x = root (if n is odd and root^n = c)
137  // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
138  virtual Theorem elimPowerConst(const Expr& expr, const Rational& root) = 0;
139 
140  // x^n = c <=> false (if n is even and c is negative)
141  virtual Theorem evenPowerEqNegConst(const Expr& expr) = 0;
142 
143  // x^n = c <=> false (if x is an integer and c is not a perfect n power)
144  virtual Theorem intEqIrrational(const Expr& expr, const Theorem& isInt) = 0;
145 
146  //! e0 \@ e1 <==> true | false, where \@ is {=,<,<=,>,>=}
147  /*! \param e takes e is (e0\@e1) where e0 and e1 are constants
148  */
149  virtual Theorem constPredicate(const Expr& e) = 0;
150 
151  //! e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
152  virtual Theorem rightMinusLeft(const Expr& e) = 0;
153 
154  //! e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
155  virtual Theorem leftMinusRight(const Expr& e) = 0;
156 
157  //! x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
158  virtual Theorem plusPredicate(const Expr& x,
159  const Expr& y, const Expr& z, int kind) = 0;
160 
161  //! x = y <==> x * z = y * z, where z is a non-zero constant
162  virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z) = 0;
163 
164  // x = y <==> z=0 OR x * 1/z = y * 1/z
165  virtual Theorem divideEqnNonConst(const Expr& x, const Expr& y, const Expr& z) = 0;
166 
167  //! Multiplying inequation by a non-zero constant
168  /*!
169  * z>0 ==> e[0] @ e[1] <==> e[0]*z @ e[1]*z
170  *
171  * z<0 ==> e[0] @ e[1] <==> e[1]*z @ e[0]*z
172  *
173  * for @ in {<,<=,>,>=}:
174  */
175  virtual Theorem multIneqn(const Expr& e, const Expr& z) = 0;
176 
177  //! x = y ==> x <= y and x >= y
178  virtual Theorem eqToIneq(const Expr& e) = 0;
179 
180  //! "op1 GE|GT op2" <==> op2 LE|LT op1
181  virtual Theorem flipInequality(const Expr& e) = 0;
182 
183  //! Propagating negation over <,<=,>,>=
184  /*! NOT (op1 < op2) <==> (op1 >= op2)
185  *
186  * NOT (op1 <= op2) <==> (op1 > op2)
187  *
188  * NOT (op1 > op2) <==> (op1 <= op2)
189  *
190  * NOT (op1 >= op2) <==> (op1 < op2)
191  */
192  virtual Theorem negatedInequality(const Expr& e) = 0;
193 
194  //! Real shadow: a <(=) t, t <(=) b ==> a <(=) b
195  virtual Theorem realShadow(const Theorem& alphaLTt,
196  const Theorem& tLTbeta) = 0;
197 
198  //! Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha
199  virtual Theorem realShadowEq(const Theorem& alphaLEt,
200  const Theorem& tLEalpha) = 0;
201 
202  //! Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
203  virtual Theorem finiteInterval(const Theorem& aLEt,
204  const Theorem& tLEac,
205  const Theorem& isInta,
206  const Theorem& isIntt) = 0;
207 
208  //! Dark & Gray shadows when a <= b
209  /*! takes two integer ineqs (i.e. all vars are ints)
210  * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= a <= b"
211  * and returns (D or G) and (!D or !G), where
212  * D = Dark_Shadow(ab-1, b.alpha - a.beta),
213  * G = Gray_Shadow(a.x, alpha, -(a-1), 0).
214  */
215  virtual Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
216  const Theorem& axLEalpha,
217  const Theorem& isIntAlpha,
218  const Theorem& isIntBeta,
219  const Theorem& isIntx)=0;
220 
221  //! Dark & Gray shadows when b <= a
222  /*! takes two integer ineqs (i.e. all vars are ints)
223  * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= b < a"
224  * and returns (D or G) and (!D or !G), where
225  * D = Dark_Shadow(ab-1, b.alpha - a.beta),
226  * G = Gray_Shadow(b.x, beta, 0, b-1).
227  */
228  virtual Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
229  const Theorem& axLEalpha,
230  const Theorem& isIntAlpha,
231  const Theorem& isIntBeta,
232  const Theorem& isIntx)=0;
233 
234  //! DARK_SHADOW(t1, t2) ==> t1 <= t2
235  virtual Theorem expandDarkShadow(const Theorem& darkShadow)=0;
236 
237  //! GRAY_SHADOW(v, e, c, c) ==> v=e+c.
238  virtual Theorem expandGrayShadow0(const Theorem& g)=0;
239 
240  // [used to be] GRAY_SHADOW(t1, t2, i) ==> t1 = t2+i OR
241  // GRAY_SHADOW(t1, t2, i+/-1)
242 
243  //! G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
244  /*! Here G1 = G(x,e,c1,c),
245  * G2 = G(x,e,c+1,c2),
246  * and c = floor((c1+c2)/2).
247  */
248  virtual Theorem splitGrayShadow(const Theorem& g)=0;
249 
250 
251  virtual Theorem splitGrayShadowSmall(const Theorem& g)=0;
252 
253  //! G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2
254  virtual Theorem expandGrayShadow(const Theorem& g)=0;
255 
256  //! Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]
257  /*! Implements three versions of the rule:
258  *
259  * \f[\frac{\mathrm{GRAY\_SHADOW}(ax,c,c1,c2)}
260  * {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a)
261  * \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\f]
262  *
263  * where the conclusion may become FALSE or without the
264  * GRAY_SHADOW part, depending on the values of a, c and i.
265  */
266  virtual Theorem expandGrayShadowConst(const Theorem& g)=0;
267  //! |- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
268  /*! In the case the new c1 > c2, return |- FALSE */
269  virtual Theorem grayShadowConst(const Theorem& g)=0;
270 
271  //! a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]
272  /*! Takes a Theorem(\\alpha < \\beta) and returns
273  * Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
274  * or Theorem(\\alpha < \\beta <==> \\alpha + 1 <= \\beta),
275  * depending on which side must be changed (changeRight flag)
276  */
277  virtual Theorem lessThanToLE(const Theorem& less,
278  const Theorem& isIntLHS,
279  const Theorem& isIntRHS,
280  bool changeRight)=0;
281 
282  virtual Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
283  const Theorem& isIntRHS, bool changeRight) = 0;
284 
285 
286  /*! \param eqn is an equation 0 = a.x or 0 = c + a.x, where x is integer
287  * \param isIntx is a proof of IS_INTEGER(x)
288  *
289  * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
290  * return the theorem 0 = c + a.x <==> false.
291  *
292  * It also handles the special case of 0 = a.x <==> x = 0
293  */
294  virtual Theorem intVarEqnConst(const Expr& eqn,
295  const Theorem& isIntx) = 0;
296  /*! IS_INTEGER(x) <=> EXISTS (y : INT) y = x
297  * where x is not already known to be an integer.
298  */
299  virtual Theorem IsIntegerElim(const Theorem& isIntx) = 0;
300 
301  /*! @brief Equality elimination rule for integers:
302  * \f[\frac{\mathsf{int}(a\cdot x)\quad
303  * \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})}
304  * {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i}
305  * \quad\equiv\quad x=t_{2}\wedge 0=t_{3}}
306  * \f]
307  * See the detailed description for explanations.
308  *
309  * This rule implements a step in the iterative algorithm for
310  * eliminating integer equality. The terms in the rule are
311  * defined as follows:
312  *
313  * \f[\begin{array}{rcl}
314  * t_{2} & = &
315  * -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m)
316  * \cdot x_{i}-m\cdot\sigma(t))\\ & & \\
317  * t_{3} & = &
318  * \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i}
319  * -a\cdot\sigma(t)\\ & & \\
320  * t & = &
321  * (C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m)
322  * \cdot x_{i}+x)/m\\ & & \\
323  * m & = & a+1\\ & & \\
324  * \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m}
325  * +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\
326  * i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m}
327  * +\frac{1}{2}\right\rfloor
328  * \end{array}
329  * \f]
330  *
331  * All the variables and coefficients are integer, and a >= 2.
332  *
333  * \param eqn is the equation
334  * \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
335  *
336  */
337 
338  /*
339  virtual Theorem eqElimIntRule(const Expr& eqn,
340  const Theorem& isIntLHS,
341  const Theorem& isIntRHS) = 0;
342  //! a <=> b ==> c AND a <=> c AND b. Takes "a <=> b" and "c".
343  virtual Theorem cANDaIffcANDb(const Theorem& thm,
344  const Expr& solvedEq) = 0;
345  virtual Theorem substSolvedFormRule(const Expr& e1,
346  ExprMap<Expr>& eMap) = 0;
347  virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0;
348  */
349 
350  ///////////////////////////////////////////////////////////////////////
351  // Alternative implementation of integer equality elimination
352  ///////////////////////////////////////////////////////////////////////
353 
354  /*! @brief
355  * \f[\frac{\Gamma\models ax=t\quad
356  * \Gamma'\models\mathsf{int}(x)\quad
357  * \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}}
358  * {\Gamma,\Gamma',\bigcup_i\Gamma_i\models
359  * \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)}
360  * \f]
361  * See detailed docs for more information.
362  *
363  * This rule implements a step in the iterative algorithm for
364  * eliminating integer equality. The terms in the rule are
365  * defined as follows:
366  *
367  * \f[\begin{array}{rcl}
368  * t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\
369  * t_{2}(y) & = &
370  * -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m)
371  * \cdot x_{i}-m\cdot y)\\ & & \\
372  * t_{3}(y) & = &
373  * \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i}
374  * -a\cdot y\\ & & \\
375  * m & = & a+1\\ & & \\
376  * \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m}
377  * +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\
378  * i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m}
379  * +\frac{1}{2}\right\rfloor
380  * \end{array}
381  * \f]
382  *
383  * All the variables and coefficients are integer, and a >= 2.
384  *
385  * \param eqn is the equation ax=t:
386  * \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
387  *
388  * \param isIntx is a Theorem deriving the integrality of the
389  * LHS variable: IS_INTEGER(x)
390  *
391  * \param isIntVars is a vector of Theorems deriving the
392  * integrality of all variables on the RHS
393  */
394  virtual Theorem eqElimIntRule(const Theorem& eqn,
395  const Theorem& isIntx,
396  const std::vector<Theorem>& isIntVars) = 0;
397 
398  /*!
399  * @brief return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c
400  * is a constant
401  *
402  * \param e is a predicate IS_INTEGER(c) where c is a rational constant
403  */
404  virtual Theorem isIntConst(const Expr& e) = 0;
405 
406  virtual Theorem equalLeaves1(const Theorem& thm) = 0;
407  virtual Theorem equalLeaves2(const Theorem& thm) = 0;
408  virtual Theorem equalLeaves3(const Theorem& thm) = 0;
409  virtual Theorem equalLeaves4(const Theorem& thm) = 0;
410 
411  //! x /= y ==> (x < y) OR (x > y)
412  /*! Used in concrete model generation */
413  virtual Theorem diseqToIneq(const Theorem& diseq) = 0;
414 
415  virtual Theorem dummyTheorem(const Expr& e) = 0;
416 
417  virtual Theorem oneElimination(const Expr& x) = 0;
418 
419  virtual Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) = 0;
420 
421  virtual Theorem addInequalities(const Theorem& thm1, const Theorem& thm2) = 0;
422  virtual Theorem addInequalities(const std::vector<Theorem>& thms) = 0;
423 
424  virtual Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2) = 0;
425 
426  virtual Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2) = 0;
427 
428  virtual Theorem integerSplit(const Expr& intVar, const Rational& intPoint) = 0;
429 
430  virtual Theorem trustedRewrite(const Expr& expr1, const Expr& expr2) = 0;
431 
432  virtual Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) = 0;
433 
434  virtual Theorem simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) = 0;
435 
436  virtual Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) = 0;
437 
438  virtual Theorem cycleConflict(const std::vector<Theorem>& inequalitites) = 0;
439 
440  virtual Theorem implyEqualities(const std::vector<Theorem>& inequalities) = 0;
441 
442  virtual Theorem implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0;
443 
444  virtual Theorem implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0;
445 
446  virtual Theorem expandGrayShadowRewrite(const Expr& theShadow) = 0;
447 
448  virtual Theorem compactNonLinearTerm(const Expr& nonLinear) = 0;
449 
450  virtual Theorem nonLinearIneqSignSplit(const Theorem& ineqThm) = 0;
451 
452  virtual Theorem implyDiffLogicBothBounds(const Expr& x, std::vector<Theorem>& c1_le_x, Rational c1,
453  std::vector<Theorem>& x_le_c2, Rational c2) = 0;
454 
455  virtual Theorem powerOfOne(const Expr& e) = 0;
456 
457  virtual Theorem rewriteLeavesConst(const Expr& e);
458 
459  }; // end of class ArithProofRules
460 } // end of namespace CVC3
461 
462 #endif
virtual Theorem eqToIneq(const Expr &e)=0
x = y ==> x <= y and x >= y
virtual Theorem multEqn(const Expr &x, const Expr &y, const Expr &z)=0
x = y <==> x * z = y * z, where z is a non-zero constant
virtual Theorem implyNegatedInequality(const Expr &expr1, const Expr &expr2)=0
virtual Theorem expandGrayShadowConst(const Theorem &g)=0
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
virtual Theorem IsIntegerElim(const Theorem &isIntx)=0
virtual Theorem elimPower(const Expr &expr)=0
virtual Theorem uMinusToMult(const Expr &e)=0
==> -(e) = (-1) * e
virtual Theorem implyEqualities(const std::vector< Theorem > &inequalities)=0
virtual Theorem equalLeaves1(const Theorem &thm)=0
bool isInt(Type t)
Definition: theory_arith.h:174
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem canonDivideConst(const Expr &c, const Expr &d)=0
(c) / d ==> (c/d), takes c and d
virtual Theorem splitGrayShadowSmall(const Theorem &g)=0
virtual Theorem canonMultOne(const Expr &e)=0
1*t ==> t, takes 1*t
virtual Theorem canonMultConstSum(const Expr &c1, const Expr &sum)=0
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
virtual Theorem constPredicate(const Expr &e)=0
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem negatedInequality(const Expr &e)=0
Propagating negation over <,<=,>,>=.
virtual Theorem compactNonLinearTerm(const Expr &nonLinear)=0
virtual Theorem canonMultMtermMterm(const Expr &e)=0
virtual Theorem canonInvert(const Expr &e)=0
==> 1/e = e' where e' is canonical; takes e.
virtual Theorem canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)=0
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
virtual Theorem canonMultTermConst(const Expr &c, const Expr &t)=0
t*c ==> c*t, takes constant c and term t
virtual Theorem multEqZero(const Expr &expr)=0
virtual Theorem intVarEqnConst(const Expr &eqn, const Theorem &isIntx)=0
virtual Theorem implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0
virtual Theorem equalLeaves3(const Theorem &thm)=0
virtual Theorem rightMinusLeft(const Expr &e)=0
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
virtual Theorem canonPowConst(const Expr &pow)=0
c^n = c' (compute the constant power expression)
virtual Theorem canonMultTerm1Term2(const Expr &t1, const Expr &t2)=0
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Theorem trustedRewrite(const Expr &expr1, const Expr &expr2)=0
virtual Theorem elimPowerConst(const Expr &expr, const Rational &root)=0
virtual Theorem splitGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
virtual Theorem canonDividePlus(const Expr &e, const Expr &d)=0
(+ c ...)/d ==> push division to all the coefficients.
virtual Theorem powerOfOne(const Expr &e)=0
virtual Theorem clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)=0
virtual Theorem finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)=0
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
virtual Theorem simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)=0
virtual Theorem canonDivide(const Expr &e)=0
Canonize t1/t2.
virtual Theorem plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind)=0
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
virtual Theorem canonMultZero(const Expr &e)=0
0*t ==> 0, takes 0*t
virtual Theorem dummyTheorem(const Expr &e)=0
bool isIntx(const Expr &e, const Rational &x)
virtual Theorem implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)=0
virtual Theorem canonDivideMult(const Expr &cx, const Expr &d)=0
(c * x) / d ==> (c/d) * x, takes (c*x) and d
virtual Theorem cycleConflict(const std::vector< Theorem > &inequalitites)=0
virtual Theorem moveSumConstantRight(const Expr &e)=0
virtual Theorem eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)=0
Equality elimination rule for integers: See the detailed description for explanations.
virtual Theorem equalLeaves4(const Theorem &thm)=0
virtual Theorem expandGrayShadowRewrite(const Expr &theShadow)=0
virtual Theorem rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)=0
virtual Theorem expandDarkShadow(const Theorem &darkShadow)=0
DARK_SHADOW(t1, t2) ==> t1 <= t2.
virtual Theorem grayShadowConst(const Theorem &g)=0
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
virtual Theorem canonUMinusToDivide(const Expr &e)=0
-(e) ==> e / (-1); takes 'e'
virtual Theorem intEqIrrational(const Expr &expr, const Theorem &isInt)=0
virtual Theorem multIneqn(const Expr &e, const Expr &z)=0
Multiplying inequation by a non-zero constant.
virtual Theorem expandGrayShadow0(const Theorem &g)=0
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0
virtual Theorem minusToPlus(const Expr &x, const Expr &y)=0
==> x - y = x + (-1) * y
virtual Theorem flipInequality(const Expr &e)=0
"op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem isIntConst(const Expr &e)=0
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
virtual Theorem equalLeaves2(const Theorem &thm)=0
virtual Theorem intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)=0
virtual Theorem oneElimination(const Expr &x)=0
virtual Theorem addInequalities(const Theorem &thm1, const Theorem &thm2)=0
virtual Theorem leftMinusRight(const Expr &e)=0
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
virtual Theorem darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0
Dark & Gray shadows when b <= a.
virtual Theorem varToMult(const Expr &e)=0
==> e = 1 * e
virtual Theorem realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)=0
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
virtual Theorem implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)=0
virtual Theorem canonMultConstConst(const Expr &c1, const Expr &c2)=0
c1*c2 ==> c', takes constant c1*c2
virtual Theorem nonLinearIneqSignSplit(const Theorem &ineqThm)=0
virtual Theorem canonPlus(const Expr &e)=0
Canonize (PLUS t1 ... tn)
virtual Theorem rewriteLeavesConst(const Expr &e)
virtual Theorem implyWeakerInequality(const Expr &expr1, const Expr &expr2)=0
virtual Theorem darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)=0
Dark & Gray shadows when a <= b.
virtual Theorem integerSplit(const Expr &intVar, const Rational &intPoint)=0
virtual Theorem realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)=0
Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha.
virtual Theorem canonFlattenSum(const Expr &e)=0
flattens the input. accepts a PLUS expr
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
virtual Theorem evenPowerEqNegConst(const Expr &expr)=0
virtual Theorem canonDivideVar(const Expr &e, const Expr &d)=0
x / d ==> (1/d) * x, takes x and d
virtual Theorem powEqZero(const Expr &expr)=0
virtual Theorem lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)=0
a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]
virtual Theorem canonMult(const Expr &e)=0
Canonize (MULT t1 ... tn)
virtual Theorem canonComboLikeTerms(const Expr &e)=0
combine like terms. accepts a flattened PLUS expr
virtual Theorem expandGrayShadow(const Theorem &g)=0
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
virtual Theorem diseqToIneq(const Theorem &diseq)=0
x /= y ==> (x < y) OR (x > y)
virtual Theorem divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z)=0