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