CVC3  2.4.1
arith_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  * \file arith_theorem_producer.h
4  * \brief TRUSTED implementation of 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_theorem_producer_h_
23 #define _cvc3__arith_theorem_producer_h_
24 
25 #include "arith_proof_rules.h"
26 #include "theorem_producer.h"
27 #include "theory_arith_new.h"
28 
29 namespace CVC3 {
30  class TheoryArithNew;
31 
34  private:
35  /*! \name Auxiliary functions for eqElimIntRule()
36  * Methods that compute the subterms used in eqElimIntRule()
37  *@{
38  */
39  //! Compute the special modulus: i - m*floor(i/m+1/2)
40  Rational modEq(const Rational& i, const Rational& m);
41  //! Create the term 't'. See eqElimIntRule().
42  Expr create_t(const Expr& eqn);
43  //! Create the term 't2'. See eqElimIntRule().
44  Expr create_t2(const Expr& lhs, const Expr& rhs, const Expr& t);
45  //! Create the term 't3'. See eqElimIntRule().
46  Expr create_t3(const Expr& lhs, const Expr& rhs, const Expr& t);
47  /*! @brief Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the
48  * vector of similar monomials (in 'summands') with coefficients
49  * mod(a_i, m). If divide flag is true, the coefficients will be
50  * mod(a_i,m)/m.
51  */
52  void sumModM(std::vector<Expr>& summands, const Expr& sum,
53  const Rational& m, const Rational& divisor);
54  Expr monomialModM(const Expr& e,
55  const Rational& m, const Rational& divisor);
56  void sumMulF(std::vector<Expr>& summands, const Expr& sum,
57  const Rational& m, const Rational& divisor);
58  Expr monomialMulF(const Expr& e,
59  const Rational& m, const Rational& divisor);
60  //! Compute floor(i/m+1/2) + mod(i,m)
61  Rational f(const Rational& i, const Rational& m);
62  Expr substitute(const Expr& term, ExprMap<Expr>& eMap);
63 
64  /*@}*/
65  public:
66  //! Constructor
68  TheoremProducer(tm), d_theoryArith(theoryArith) { }
69 
70  //! Create Expr from Rational (for convenience)
71  Expr rat(Rational r) { return d_em->newRatExpr(r); }
72  Type realType() { return d_theoryArith->realType(); }
73  Type intType() { return d_theoryArith->intType(); }
74  //! Construct the dark shadow expression representing lhs <= rhs
75  Expr darkShadow(const Expr& lhs, const Expr& rhs) {
76  return d_theoryArith->darkShadow(lhs, rhs);
77  }
78  //! Construct the gray shadow expression representing c1 <= v - e <= c2
79  /*! Alternatively, v = e + i for some i s.t. c1 <= i <= c2
80  */
81  Expr grayShadow(const Expr& v, const Expr& e,
82  const Rational& c1, const Rational& c2) {
83  return d_theoryArith->grayShadow(v, e, c1, c2);
84  }
85 
86  ////////////////////////////////////////////////////////////////////
87  // Canonization rules
88  ////////////////////////////////////////////////////////////////////
89 
90  // ==> x = 1 * x
91  virtual Theorem varToMult(const Expr& e);
92 
93  // ==> -(e) = (-1) * e
94  virtual Theorem uMinusToMult(const Expr& e);
95 
96  // ==> x - y = x + (-1) * y
97  virtual Theorem minusToPlus(const Expr& x, const Expr& y);
98 
99  // Rule for unary minus: it just converts it to division by -1,
100  virtual Theorem canonUMinusToDivide(const Expr& e);
101 
102  // Rules for division by constant 'd'
103  // (c) / d ==> (c/d), takes c and d
104  virtual Theorem canonDivideConst(const Expr& c, const Expr& d);
105  // (c * x) / d ==> (c/d) * x, takes (c*x) and d
106  virtual Theorem canonDivideMult(const Expr& cx, const Expr& d);
107  // (+ c ...)/d ==> push division to all the coefficients.
108  // The result is not canonical, but canonizing the summands will
109  // make it canonical.
110  // Takes (+ c ...) and d
111  virtual Theorem canonDividePlus(const Expr& e, const Expr& d);
112  // x / d ==> (1/d) * x, takes x and d
113  virtual Theorem canonDivideVar(const Expr& e1, const Expr& e2);
114 
115  // Canon Rules for multiplication
116 
117  // TODO Deepak:
118  // t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a
119  // 1) Rational constant
120  // 2) Arithmetic Leaf (var or term from another theory)
121  // 3) (POW rational leaf)
122  // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
123  // 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of
124  // type (2) or (3) or (4)
125 
126  static bool greaterthan(const Expr &, const Expr &);
127  virtual Expr simplifiedMultExpr(std::vector<Expr> & mulKids);
128  virtual Expr canonMultConstMult(const Expr & c, const Expr & e);
129  virtual Expr canonMultConstPlus(const Expr & e1, const Expr & e2);
130  virtual Expr canonMultPowPow(const Expr & e1, const Expr & e2);
131  virtual Expr canonMultPowLeaf(const Expr & e1, const Expr & e2);
132  virtual Expr canonMultLeafLeaf(const Expr & e1, const Expr & e2);
133  virtual Expr canonMultLeafOrPowMult(const Expr & e1, const Expr & e2);
134  virtual Expr canonCombineLikeTerms(const std::vector<Expr> & sumExprs);
135  virtual Expr
136  canonMultLeafOrPowOrMultPlus(const Expr & e1, const Expr & e2);
137  virtual Expr canonMultPlusPlus(const Expr & e1, const Expr & e2);
138  virtual Theorem canonMultMtermMterm(const Expr& e);
139  virtual Theorem canonPlus(const Expr & e);
140  virtual Theorem canonInvertConst(const Expr & e);
141  virtual Theorem canonInvertLeaf(const Expr & e);
142  virtual Theorem canonInvertPow(const Expr & e);
143  virtual Theorem canonInvertMult(const Expr & e);
144  virtual Theorem canonInvert(const Expr & e);
145 
146  /**
147  * Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first
148  * sum term (r) must be a rational and t1 ... tn terms must be canonised.
149  *
150  * @param e the expression to transform
151  * @return rewrite theorem representing the transformation
152  */
153  virtual Theorem moveSumConstantRight(const Expr& e);
154 
155  /** e[0]/e[1] ==> e[0]*(e[1])^-1 */
156  virtual Theorem canonDivide(const Expr & e);
157 
158  /** Multiply out the operands of the multiplication (each of them is expected to be canonised */
159  virtual Theorem canonMult(const Expr & e);
160 
161  // t*c ==> c*t, takes constant c and term t
162  virtual Theorem canonMultTermConst(const Expr& c, const Expr& t);
163  // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
164  virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2);
165  // 0*t ==> 0, takes 0*t
166  virtual Theorem canonMultZero(const Expr& e);
167  // 1*t ==> t, takes 1*t
168  virtual Theorem canonMultOne(const Expr& e);
169  // c1*c2 ==> c', takes constant c1*c2
170  virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
171  // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
172  virtual Theorem
173  canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t);
174  // c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
175  virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum);
176  // c^n = c' (compute the constant power expression)
177  virtual Theorem canonPowConst(const Expr& pow);
178 
179  // Rules for addition
180  // flattens the input. accepts a PLUS expr
181  virtual Theorem canonFlattenSum(const Expr& e);
182 
183  // Rules for addition
184  // combine like terms. accepts a flattened PLUS expr
185  virtual Theorem canonComboLikeTerms(const Expr& e);
186 
187  // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
188  virtual Theorem multEqZero(const Expr& expr);
189 
190  // 0 = (^ c x) <=> false if c <=0
191  // <=> 0 = x if c > 0
192  virtual Theorem powEqZero(const Expr& expr);
193 
194  // x^n = y^n <=> x = y (if n is odd)
195  // x^n = y^n <=> x = y OR x = -y (if n is even)
196  virtual Theorem elimPower(const Expr& expr);
197 
198  // x^n = c <=> x = root (if n is odd and root^n = c)
199  // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
200  virtual Theorem elimPowerConst(const Expr& expr, const Rational& root);
201 
202  // x^n = c <=> false (if n is even and c is negative)
203  virtual Theorem evenPowerEqNegConst(const Expr& expr);
204 
205  // x^n = c <=> false (if x is an integer and c is not a perfect n power)
206  virtual Theorem intEqIrrational(const Expr& expr, const Theorem& isInt);
207 
208  // e[0] kind e[1] <==> true when e[0] kind e[1],
209  // false when e[0] !kind e[1], for constants only
210  virtual Theorem constPredicate(const Expr& e);
211 
212  // e[0] kind e[1] <==> 0 kind e[1] - e[0]
213  virtual Theorem rightMinusLeft(const Expr& e);
214 
215  // e[0] kind e[1] <==> e[0] - e[1] kind 0
216  virtual Theorem leftMinusRight(const Expr& e);
217 
218  // x kind y <==> x + z kind y + z
219  virtual Theorem plusPredicate(const Expr& x,
220  const Expr& y,
221  const Expr& z, int kind);
222 
223  // x = y <==> x * z = y * z
224  virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z);
225 
226  // x = y <==> z=0 OR x * 1/z = y * 1/z
227  virtual Theorem divideEqnNonConst(const Expr& x, const Expr& y, const Expr& z);
228 
229  // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
230  // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
231  virtual Theorem multIneqn(const Expr& e, const Expr& z);
232 
233  // x = y ==> x <= y and x >= y
234  virtual Theorem eqToIneq(const Expr& e);
235 
236  // "op1 GE|GT op2" <==> op2 LE|LT op1
237  virtual Theorem flipInequality(const Expr& e);
238 
239  // NOT (op1 LT op2) <==> (op1 GE op2)
240  // NOT (op1 LE op2) <==> (op1 GT op2)
241  // NOT (op1 GT op2) <==> (op1 LE op2)
242  // NOT (op1 GE op2) <==> (op1 LT op2)
243  Theorem negatedInequality(const Expr& e);
244 
245  Theorem realShadow(const Theorem& alphaLTt, const Theorem& tLTbeta);
246  Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
247  Theorem finiteInterval(const Theorem& aLEt, const Theorem& tLEac,
248  const Theorem& isInta, const Theorem& isIntt);
249 
250  Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
251  const Theorem& axLEalpha,
252  const Theorem& isIntAlpha,
253  const Theorem& isIntBeta,
254  const Theorem& isIntx);
255 
256  Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
257  const Theorem& axLEalpha,
258  const Theorem& isIntAlpha,
259  const Theorem& isIntBeta,
260  const Theorem& isIntx);
261 
268  Theorem grayShadowConst(const Theorem& g);
269 
270  //! Implements j(c,b,a)
271  /*! accepts 3 integers a,b,c and returns
272  * (b > 0)? (c+b) mod a : (a - (c+b)) mod a
273  */
275  const Rational& b,
276  const Rational& a);
277 
278  Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
279  const Theorem& isIntRHS, bool changeRight);
280 
281  Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
282  const Theorem& isIntRHS, bool changeRight);
283 
284  Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
285 
287  Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
288  const std::vector<Theorem>& isIntVars);
289 
290  Theorem isIntConst(const Expr& e);
291 
292  Theorem equalLeaves1(const Theorem& e);
293  Theorem equalLeaves2(const Theorem& e);
294  Theorem equalLeaves3(const Theorem& e);
295  Theorem equalLeaves4(const Theorem& e);
296 
297  Theorem diseqToIneq(const Theorem& diseq);
298 
299  Theorem dummyTheorem(const Expr& e);
300 
301  Theorem oneElimination(const Expr& x);
302 
303  Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound);
304 
305  Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
306  Theorem addInequalities(const std::vector<Theorem>& thms);
307 
308  Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2);
309 
310  Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2);
311 
312  Theorem integerSplit(const Expr& intVar, const Rational& intPoint);
313 
314  Theorem trustedRewrite(const Expr& expr1, const Expr& expr2);
315 
316  Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
317 
318  Theorem simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS);
319 
320  Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr);
321 
322  Theorem cycleConflict(const std::vector<Theorem>& inequalitites);
323 
324  Theorem implyEqualities(const std::vector<Theorem>& inequalities);
325 
326  Theorem implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied);
327 
328  Theorem implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied);
329 
330  Theorem expandGrayShadowRewrite(const Expr& theShadow);
331 
332  Theorem compactNonLinearTerm(const Expr& nonLinear);
333 
334  Theorem nonLinearIneqSignSplit(const Theorem& ineqThm);
335 
336  Theorem implyDiffLogicBothBounds(const Expr& x, std::vector<Theorem>& c1_le_x, Rational c1,
337  std::vector<Theorem>& x_le_c2, Rational c2);
338 
339  Theorem powerOfOne(const Expr& e);
340 
341  }; // end of class ArithTheoremProducer
342 
343 } // end of namespace CVC3
344 
345 #endif
Theorem eqElimIntRule(const Theorem &eqn, const Theorem &isIntx, const std::vector< Theorem > &isIntVars)
Equality elimination rule for integers: See the detailed description for explanations.
virtual Theorem canonPowConst(const Expr &pow)
c^n = c' (compute the constant power expression)
Theorem trustedRewrite(const Expr &expr1, const Expr &expr2)
bool isInt(Type t)
Definition: theory_arith.h:174
Theorem equalLeaves4(const Theorem &e)
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Expr simplifiedMultExpr(std::vector< Expr > &mulKids)
Expr monomialMulF(const Expr &e, const Rational &m, const Rational &divisor)
Compute the special modulus: i - m*floor(i/m+1/2)
virtual Theorem canonUMinusToDivide(const Expr &e)
-(e) ==> e / (-1); takes 'e'
Theorem equalLeaves3(const Theorem &e)
virtual Theorem canonDividePlus(const Expr &e, const Expr &d)
(+ c ...)/d ==> push division to all the coefficients.
virtual Expr canonMultConstPlus(const Expr &e1, const Expr &e2)
Rational modEq(const Rational &i, const Rational &m)
Compute the special modulus: i - m*floor(i/m+1/2)
ArithTheoremProducer(TheoremManager *tm, TheoryArithNew *theoryArith)
Constructor.
Expr grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
Construct the gray shadow expression representing c1 <= v - e <= c2.
Definition: theory_arith.h:165
Theorem integerSplit(const Expr &intVar, const Rational &intPoint)
Theorem simpleIneqInt(const Expr &ineq, const Theorem &isIntRHS)
virtual Theorem intEqIrrational(const Expr &expr, const Theorem &isInt)
virtual Theorem leftMinusRight(const Expr &e)
e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
virtual Theorem canonPlus(const Expr &e)
Canonize (PLUS t1 ... tn)
virtual Theorem canonMultOne(const Expr &e)
1*t ==> t, takes 1*t
Expr substitute(const Expr &term, ExprMap< Expr > &eMap)
Compute the special modulus: i - m*floor(i/m+1/2)
void sumMulF(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)
Compute the special modulus: i - m*floor(i/m+1/2)
Theorem equalLeaves2(const Theorem &e)
MS C++ specific settings.
Definition: type.h:42
Rational f(const Rational &i, const Rational &m)
Compute floor(i/m+1/2) + mod(i,m)
Theorem lessThanToLE(const Theorem &less, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)
virtual Theorem elimPower(const Expr &expr)
virtual Theorem canonInvert(const Expr &e)
==> 1/e = e' where e' is canonical; takes e.
Theorem implyNegatedInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)
virtual Theorem canonDivide(const Expr &e)
Theorem expandGrayShadow0(const Theorem &grayShadow)
GRAY_SHADOW(v, e, c, c) ==> v=e+c.
virtual Theorem elimPowerConst(const Expr &expr, const Rational &root)
virtual Theorem multEqZero(const Expr &expr)
virtual Theorem minusToPlus(const Expr &x, const Expr &y)
==> x - y = x + (-1) * y
virtual Expr canonMultPowPow(const Expr &e1, const Expr &e2)
virtual Theorem powEqZero(const Expr &expr)
Theorem realShadowEq(const Theorem &alphaLEt, const Theorem &tLEalpha)
alpha <= t <= alpha ==> t = alpha
virtual Expr canonMultLeafLeaf(const Expr &e1, const Expr &e2)
Theorem intVarEqnConst(const Expr &eqn, const Theorem &isIntx)
Theorem expandDarkShadow(const Theorem &darkShadow)
virtual Theorem canonDivideVar(const Expr &e1, const Expr &e2)
x / d ==> (1/d) * x, takes x and d
bool isIntx(const Expr &e, const Rational &x)
static bool greaterthan(const Expr &, const Expr &)
virtual Theorem canonFlattenSum(const Expr &e)
flattens the input. accepts a PLUS expr
Theorem isIntConst(const Expr &e)
return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c is a constant
virtual Expr canonMultLeafOrPowMult(const Expr &e1, const Expr &e2)
Theorem implyWeakerInequality(const Expr &expr1, const Expr &expr2)
virtual Theorem multEqn(const Expr &x, const Expr &y, const Expr &z)
x = y <==> x * z = y * z, where z is a non-zero constant
Theorem intEqualityRationalConstant(const Theorem &isIntConstrThm, const Expr &constr)
virtual Theorem canonMultZero(const Expr &e)
0*t ==> 0, takes 0*t
virtual Theorem plusPredicate(const Expr &x, const Expr &y, const Expr &z, int kind)
x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
virtual Theorem canonInvertConst(const Expr &e)
Theorem grayShadowConst(const Theorem &g)
|- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
virtual Theorem varToMult(const Expr &e)
==> e = 1 * e
Expr create_t3(const Expr &lhs, const Expr &rhs, const Expr &t)
Create the term 't3'. See eqElimIntRule().
virtual Theorem canonDivideConst(const Expr &c, const Expr &d)
(c) / d ==> (c/d), takes c and d
Theorem clashingBounds(const Theorem &lowerBound, const Theorem &upperBound)
Theorem implyWeakerInequalityDiffLogic(const std::vector< Theorem > &antecedentThms, const Expr &implied)
Theorem diseqToIneq(const Theorem &diseq)
x /= y ==> (x < y) OR (x > y)
virtual Theorem canonComboLikeTerms(const Expr &e)
combine like terms. accepts a flattened PLUS expr
virtual Theorem canonMultMtermMterm(const Expr &e)
Theorem negatedInequality(const Expr &e)
Propagating negation over <,<=,>,>=.
Theorem IsIntegerElim(const Theorem &isIntx)
Theorem implyDiffLogicBothBounds(const Expr &x, std::vector< Theorem > &c1_le_x, Rational c1, std::vector< Theorem > &x_le_c2, Rational c2)
Expr monomialModM(const Expr &e, const Rational &m, const Rational &divisor)
Compute the special modulus: i - m*floor(i/m+1/2)
Expr grayShadow(const Expr &v, const Expr &e, const Rational &c1, const Rational &c2)
Construct the gray shadow expression representing c1 <= v - e <= c2.
virtual Theorem canonMultTermConst(const Expr &c, const Expr &t)
t*c ==> c*t, takes constant c and term t
virtual Theorem flipInequality(const Expr &e)
"op1 GE|GT op2" <==> op2 LE|LT op1
virtual Theorem moveSumConstantRight(const Expr &e)
Theorem equalLeaves1(const Theorem &e)
Theorem expandGrayShadow(const Theorem &grayShadow)
G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2.
virtual Expr canonMultConstMult(const Expr &c, const Expr &e)
Expr newRatExpr(const Rational &r)
Definition: expr_manager.h:471
Theorem expandGrayShadowConst(const Theorem &grayShadow)
Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion].
Theorem addInequalities(const Theorem &thm1, const Theorem &thm2)
Theorem realShadow(const Theorem &alphaLTt, const Theorem &tLTbeta)
Real shadow: a <(=) t, t <(=) b ==> a <(=) b.
Theorem oneElimination(const Expr &x)
virtual Theorem canonMultConstSum(const Expr &c1, const Expr &sum)
c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
Theorem implyEqualities(const std::vector< Theorem > &inequalities)
virtual Theorem canonMultTerm1Term2(const Expr &t1, const Expr &t2)
t1*t2 ==> Error, takes t1 and t2 where both are non-constants
virtual Expr canonMultPlusPlus(const Expr &e1, const Expr &e2)
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Definition: theory_arith.h:159
Expr rat(Rational r)
Create Expr from Rational (for convenience)
virtual Theorem canonMult(const Expr &e)
virtual Theorem canonDivideMult(const Expr &cx, const Expr &d)
(c * x) / d ==> (c/d) * x, takes (c*x) and d
Theorem rafineStrictInteger(const Theorem &isIntConstrThm, const Expr &constr)
Theorem splitGrayShadowSmall(const Theorem &grayShadow)
virtual Theorem constPredicate(const Expr &e)
e0 @ e1 <==> true | false, where @ is {=,<,<=,>,>=}
virtual Theorem canonInvertLeaf(const Expr &e)
virtual Theorem canonMultConstConst(const Expr &c1, const Expr &c2)
c1*c2 ==> c', takes constant c1*c2
Expr darkShadow(const Expr &lhs, const Expr &rhs)
Construct the dark shadow expression representing lhs <= rhs.
Theorem implyNegatedInequality(const Expr &expr1, const Expr &expr2)
virtual Theorem canonMultConstTerm(const Expr &c1, const Expr &c2, const Expr &t)
c1*(c2*t) ==> c'*t, takes c1 and c2 and t
Theorem nonLinearIneqSignSplit(const Theorem &ineqThm)
virtual Expr canonCombineLikeTerms(const std::vector< Expr > &sumExprs)
Arithmetic proof rules.
void sumModM(std::vector< Expr > &summands, const Expr &sum, const Rational &m, const Rational &divisor)
Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the vector of similar monomials (in 'summands') wit...
Theorem splitGrayShadow(const Theorem &grayShadow)
G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
Theorem finiteInterval(const Theorem &aLEt, const Theorem &tLEac, const Theorem &isInta, const Theorem &isIntt)
Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
Theorem expandGrayShadowRewrite(const Expr &theShadow)
Theorem lessThanToLERewrite(const Expr &ineq, const Theorem &isIntLHS, const Theorem &isIntRHS, bool changeRight)
Theorem cycleConflict(const std::vector< Theorem > &inequalitites)
virtual Theorem evenPowerEqNegConst(const Expr &expr)
Theorem darkGrayShadow2ba(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)
Dark & Gray shadows when b <= a.
virtual Theorem eqToIneq(const Expr &e)
x = y ==> x <= y and x >= y
virtual Theorem divideEqnNonConst(const Expr &x, const Expr &y, const Expr &z)
virtual Theorem multIneqn(const Expr &e, const Expr &z)
Multiplying inequation by a non-zero constant.
Rational pow(Rational pow, const Rational &base)
Raise 'base' into the power of 'pow' (pow must be an integer)
Definition: rational.h:159
Definition: expr.cpp:35
virtual Theorem canonInvertPow(const Expr &e)
Theorem darkGrayShadow2ab(const Theorem &betaLEbx, const Theorem &axLEalpha, const Theorem &isIntAlpha, const Theorem &isIntBeta, const Theorem &isIntx)
Dark & Gray shadows when a <= b.
virtual Expr canonMultLeafOrPowOrMultPlus(const Expr &e1, const Expr &e2)
Expr create_t(const Expr &eqn)
Create the term 't'. See eqElimIntRule().
virtual Theorem canonInvertMult(const Expr &e)
virtual Theorem uMinusToMult(const Expr &e)
==> -(e) = (-1) * e
Rational constRHSGrayShadow(const Rational &c, const Rational &b, const Rational &a)
Implements j(c,b,a)
Theorem compactNonLinearTerm(const Expr &nonLinear)
virtual Expr canonMultPowLeaf(const Expr &e1, const Expr &e2)
Expr create_t2(const Expr &lhs, const Expr &rhs, const Expr &t)
Create the term 't2'. See eqElimIntRule().
virtual Theorem rightMinusLeft(const Expr &e)
e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}