CVC3

# arith_proof_rules.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file arith_proof_rules.h
00004  * \brief Arithmetic proof rules
00005  *
00006  * Author: Vijay Ganesh, Sergey Berezin
00007  *
00008  * Created: Dec 13 02:09:04 GMT 2002
00009  *
00010  * <hr>
00011  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  *
00017  * <hr>
00018  *
00019  */
00020 /*****************************************************************************/
00021
00022 #ifndef _cvc3__arith_proof_rules_h_
00023 #define _cvc3__arith_proof_rules_h_
00024
00025 #include <vector>
00026
00027 namespace CVC3 {
00028
00029   class Theorem;
00030   class Expr;
00031   class Rational;
00032
00033   class ArithProofRules {
00034   public:
00035     // Destructor
00036     virtual ~ArithProofRules() { }
00037
00038     ////////////////////////////////////////////////////////////////////
00039     // Canonization rules
00040     ////////////////////////////////////////////////////////////////////
00041
00042     //! ==> e = 1 * e
00043     virtual Theorem varToMult(const Expr& e) = 0;
00044
00045     //! ==> -(e) = (-1) * e
00046     virtual Theorem uMinusToMult(const Expr& e) = 0;
00047
00048     //! ==> x - y = x + (-1) * y
00049     virtual Theorem minusToPlus(const Expr& x, const Expr& y) = 0;
00050
00051     //! -(e) ==> e / (-1); takes 'e'
00052     /*! Canon Rule for unary minus: it just converts it to division by
00053      * -1, the result is not yet canonical:
00054      */
00055     virtual Theorem canonUMinusToDivide(const Expr& e) = 0;
00056
00057     /**
00058      * Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first
00059      * sum term (r) must be a rational and t1 ... tn terms must be canonised.
00060      *
00061      * @param e the expression to transform
00062      * @return rewrite theorem representing the transformation
00063      */
00064     virtual Theorem moveSumConstantRight(const Expr& e) = 0;
00065
00066     //! (c) / d ==> (c/d), takes c and d
00067     /*! Canon Rules for division by constant 'd' */
00068     virtual Theorem canonDivideConst(const Expr& c, const Expr& d) = 0;
00069     //! (c * x) / d ==> (c/d) * x, takes (c*x) and d
00070     virtual Theorem canonDivideMult(const Expr& cx, const Expr& d) = 0;
00071     //! (+ c ...)/d ==> push division to all the coefficients.
00072     /*! The result is not canonical, but canonizing the summands will
00073      * make it canonical.
00074      * Takes (+ c ...) and d
00075      */
00076     virtual Theorem canonDividePlus(const Expr& e, const Expr& d) = 0;
00077     //! x / d ==> (1/d) * x, takes x and d
00078     virtual Theorem canonDivideVar(const Expr& e, const Expr& d) = 0;
00079
00080     // Canon Rules for multiplication
00081
00082     // TODO Deepak:
00083     // e == t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a
00084     // 1) Rational constant
00085     // 2) Arithmetic Leaf (var or term from another theory)
00086     // 3) (POW rational leaf)
00087     // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
00088     // 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of
00089     //     type (2) or (3) or (4)
00090     virtual Theorem canonMultMtermMterm(const Expr& e) = 0;
00091     //! Canonize (PLUS t1 ... tn)
00092     virtual Theorem canonPlus(const Expr & e) = 0;
00093     //! Canonize (MULT t1 ... tn)
00094     virtual Theorem canonMult(const Expr & e) = 0;
00095     //! ==> 1/e = e'  where e' is canonical; takes e.
00096     virtual Theorem canonInvert(const Expr & e) = 0;
00097     //! Canonize t1/t2
00098     virtual Theorem canonDivide(const Expr & e) = 0;
00099
00100     //! t*c ==> c*t, takes constant c and term t
00101     virtual Theorem canonMultTermConst(const Expr& c, const Expr& t) = 0;
00102     //! t1*t2 ==> Error, takes t1 and t2 where both are non-constants
00103     virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2) = 0;
00104     //! 0*t ==> 0, takes 0*t
00105     virtual Theorem canonMultZero(const Expr& e) = 0;
00106     //! 1*t ==> t, takes 1*t
00107     virtual Theorem canonMultOne(const Expr& e) = 0;
00108     //! c1*c2 ==> c', takes constant c1*c2
00109     virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2) = 0;
00110     //! c1*(c2*t) ==> c'*t, takes c1 and c2 and t
00111     virtual Theorem
00112       canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t) = 0;
00113     //! c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
00114     virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum) = 0;
00115     //! c^n = c' (compute the constant power expression)
00116     virtual Theorem canonPowConst(const Expr& pow) = 0;
00117
00119     //! flattens the input. accepts a PLUS expr
00120     virtual Theorem canonFlattenSum(const Expr& e) = 0;
00121
00122     //! combine like terms. accepts a flattened PLUS expr
00123     virtual Theorem canonComboLikeTerms(const Expr& e) = 0;
00124
00125     // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
00126     virtual Theorem multEqZero(const Expr& expr) = 0;
00127
00128     // 0 = (^ c x) <=> false if c <=0
00129     //             <=> 0 = x if c > 0
00130     virtual Theorem powEqZero(const Expr& expr) = 0;
00131
00132     // x^n = y^n <=> x = y (if n is odd)
00133     // x^n = y^n <=> x = y OR x = -y (if n is even)
00134     virtual Theorem elimPower(const Expr& expr) = 0;
00135
00136     // x^n = c <=> x = root (if n is odd and root^n = c)
00137     // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
00138     virtual Theorem elimPowerConst(const Expr& expr, const Rational& root) = 0;
00139
00140     // x^n = c <=> false (if n is even and c is negative)
00141     virtual Theorem evenPowerEqNegConst(const Expr& expr) = 0;
00142
00143     // x^n = c <=> false (if x is an integer and c is not a perfect n power)
00144     virtual Theorem intEqIrrational(const Expr& expr, const Theorem& isInt) = 0;
00145
00146     //! e0 \@ e1 <==> true | false, where \@ is {=,<,<=,>,>=}
00147     /*! \param e takes e is (e0\@e1) where e0 and e1 are constants
00148      */
00149     virtual Theorem constPredicate(const Expr& e) = 0;
00150
00151     //! e[0] @ e[1] <==> 0 @ e[1] - e[0], where @ is {=,<,<=,>,>=}
00152     virtual Theorem rightMinusLeft(const Expr& e) = 0;
00153
00154     //! e[0] @ e[1] <==> e[0] - e[1] @ 0, where @ is {=,<,<=,>,>=}
00155     virtual Theorem leftMinusRight(const Expr& e) = 0;
00156
00157     //! x @ y <==> x + z @ y + z, where @ is {=,<,<=,>,>=} (given as 'kind')
00158     virtual Theorem plusPredicate(const Expr& x,
00159           const Expr& y, const Expr& z, int kind) = 0;
00160
00161     //! x = y <==> x * z = y * z, where z is a non-zero constant
00162     virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z) = 0;
00163
00164     // x = y <==> z=0 OR x * 1/z = y * 1/z
00165     virtual Theorem divideEqnNonConst(const Expr& x, const Expr& y, const Expr& z) = 0;
00166
00167     //! Multiplying inequation by a non-zero constant
00168     /*!
00169      * z>0 ==> e[0] @ e[1] <==> e[0]*z @ e[1]*z
00170      *
00171      * z<0 ==> e[0] @ e[1] <==> e[1]*z @ e[0]*z
00172      *
00173      * for @ in {<,<=,>,>=}:
00174      */
00175     virtual Theorem multIneqn(const Expr& e, const Expr& z) = 0;
00176
00177     //! x = y ==> x <= y and x >= y
00178     virtual Theorem eqToIneq(const Expr& e) = 0;
00179
00180     //! "op1 GE|GT op2" <==> op2 LE|LT op1
00181     virtual Theorem flipInequality(const Expr& e) = 0;
00182
00183     //! Propagating negation over <,<=,>,>=
00184     /*! NOT (op1 < op2)  <==> (op1 >= op2)
00185      *
00186      * NOT (op1 <= op2)  <==> (op1 > op2)
00187      *
00188      * NOT (op1 > op2)  <==> (op1 <= op2)
00189      *
00190      * NOT (op1 >= op2)  <==> (op1 < op2)
00191      */
00192     virtual Theorem negatedInequality(const Expr& e) = 0;
00193
00194     //! Real shadow: a <(=) t, t <(=) b ==> a <(=) b
00195     virtual Theorem realShadow(const Theorem& alphaLTt,
00196              const Theorem& tLTbeta) = 0;
00197
00198     //! Projecting a tight inequality: alpha <= t <= alpha ==> t = alpha
00199     virtual Theorem realShadowEq(const Theorem& alphaLEt,
00200          const Theorem& tLEalpha) = 0;
00201
00202     //! Finite interval for integers: a <= t <= a + c ==> G(t, a, 0, c)
00203     virtual Theorem finiteInterval(const Theorem& aLEt,
00204            const Theorem& tLEac,
00205            const Theorem& isInta,
00206            const Theorem& isIntt) = 0;
00207
00208     //! Dark & Gray shadows when a <= b
00209     /*! takes two integer ineqs (i.e. all vars are ints)
00210      * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= a <= b"
00211      * and returns (D or G) and (!D or !G), where
00212      * D = Dark_Shadow(ab-1, b.alpha - a.beta),
00213      * G = Gray_Shadow(a.x, alpha, -(a-1), 0).
00214      */
00215     virtual Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
00216               const Theorem& axLEalpha,
00217               const Theorem& isIntAlpha,
00218               const Theorem& isIntBeta,
00219               const Theorem& isIntx)=0;
00220
00221     //! Dark & Gray shadows when b <= a
00222     /*! takes two integer ineqs (i.e. all vars are ints)
00223      * "|- beta <= b.x" and "|- a.x <= alpha" and checks if "1 <= b < a"
00224      * and returns (D or G) and (!D or !G), where
00225      * D = Dark_Shadow(ab-1, b.alpha - a.beta),
00226      * G = Gray_Shadow(b.x, beta, 0, b-1).
00227      */
00228     virtual Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
00229               const Theorem& axLEalpha,
00230               const Theorem& isIntAlpha,
00231               const Theorem& isIntBeta,
00232               const Theorem& isIntx)=0;
00233
00234     //! DARK_SHADOW(t1, t2) ==> t1 <= t2
00236
00237     //! GRAY_SHADOW(v, e, c, c) ==> v=e+c.
00238     virtual Theorem expandGrayShadow0(const Theorem& g)=0;
00239
00240     // [used to be] GRAY_SHADOW(t1, t2, i) ==> t1 = t2+i OR
00242
00243     //! G(x, e, c1, c2) ==> (G1 or G2) and (!G1 or !G2)
00244     /*! Here G1 = G(x,e,c1,c),
00245      *       G2 = G(x,e,c+1,c2),
00246      *   and  c = floor((c1+c2)/2).
00247      */
00248     virtual Theorem splitGrayShadow(const Theorem& g)=0;
00249
00250
00251     virtual Theorem splitGrayShadowSmall(const Theorem& g)=0;
00252
00253     //! G(x, e, c1, c2) ==> e+c1 <= x AND x <= e+c2
00254     virtual Theorem expandGrayShadow(const Theorem& g)=0;
00255
00256     //! Optimized rules: GRAY_SHADOW(a*x, c, c1, c2) ==> [expansion]
00257     /*! Implements three versions of the rule:
00258      *
00260      *         {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a)
00261      *          \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\f]
00262      *
00263      * where the conclusion may become FALSE or without the
00264      * GRAY_SHADOW part, depending on the values of a, c and i.
00265      */
00266     virtual Theorem expandGrayShadowConst(const Theorem& g)=0;
00267     //! |- G(ax, c, c1, c2) ==> |- G(x, 0, ceil((c1+c)/a), floor((c2+c)/a))
00268     /*! In the case the new c1 > c2, return |- FALSE */
00269     virtual Theorem grayShadowConst(const Theorem& g)=0;
00270
00271     //! a,b: INT; a < b ==> a <= b-1 [or a+1 <= b]
00272     /*! Takes a Theorem(\\alpha < \\beta) and returns
00273      *  Theorem(\\alpha < \\beta <==> \\alpha <= \\beta -1)
00274      * or Theorem(\\alpha < \\beta <==> \\alpha + 1 <= \\beta),
00275      * depending on which side must be changed (changeRight flag)
00276      */
00277     virtual Theorem lessThanToLE(const Theorem& less,
00278          const Theorem& isIntLHS,
00279          const Theorem& isIntRHS,
00280          bool changeRight)=0;
00281
00282     virtual Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
00283            const Theorem& isIntRHS, bool changeRight) = 0;
00284
00285
00286     /*! \param eqn is an equation 0 = a.x or 0 = c + a.x, where x is integer
00287      * \param isIntx is a proof of IS_INTEGER(x)
00288      *
00289      * \return the theorem 0 = c + a.x <==> x=-c/a if -c/a is int else
00290      *  return the theorem 0 = c + a.x <==> false.
00291      *
00292      * It also handles the special case of 0 = a.x <==> x = 0
00293      */
00294     virtual Theorem intVarEqnConst(const Expr& eqn,
00295            const Theorem& isIntx) = 0;
00296     /*! IS_INTEGER(x) <=> EXISTS (y : INT) y = x
00297      * where x is not already known to be an integer.
00298      */
00299     virtual Theorem IsIntegerElim(const Theorem& isIntx) = 0;
00300
00301     /*! @brief Equality elimination rule for integers:
00303      *          \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})}
00304      *     {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i}
00306      * \f]
00307      * See the detailed description for explanations.
00308      *
00309      * This rule implements a step in the iterative algorithm for
00310      * eliminating integer equality.  The terms in the rule are
00311      * defined as follows:
00312      *
00313      * \f[\begin{array}{rcl}
00314      *       t_{2} & = &
00315      *          -(C\ \mathbf{mod}\  m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\  m)
00316      *             \cdot x_{i}-m\cdot\sigma(t))\\ & & \\
00317      *       t_{3} & = &
00318      *         \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i}
00319      *           -a\cdot\sigma(t)\\ & & \\
00320      *       t & = &
00321      *          (C\ \mathbf{mod}\  m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\  m)
00322      *             \cdot x_{i}+x)/m\\ & & \\
00323      *       m & = & a+1\\ & & \\
00324      *       \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m}
00325      *       +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\  m\\ & & \\
00326      *       i\ \mathbf{mod}\  m & = & i-m\left\lfloor\frac{i}{m}
00327      *          +\frac{1}{2}\right\rfloor
00328      *    \end{array}
00329      * \f]
00330      *
00331      * All the variables and coefficients are integer, and a >= 2.
00332      *
00333      * \param eqn is the equation
00334      *   \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
00335      *
00336      */
00337
00338     /*
00339     virtual Theorem eqElimIntRule(const Expr& eqn,
00340           const Theorem& isIntLHS,
00341           const Theorem& isIntRHS) = 0;
00342     //! a <=> b  ==>  c AND a <=> c AND b.  Takes "a <=> b" and "c".
00343     virtual Theorem cANDaIffcANDb(const Theorem& thm,
00344           const Expr& solvedEq) = 0;
00345     virtual Theorem substSolvedFormRule(const Expr& e1,
00346           ExprMap<Expr>& eMap) = 0;
00347     virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0;
00348     */
00349
00350     ///////////////////////////////////////////////////////////////////////
00351     // Alternative implementation of integer equality elimination
00352     ///////////////////////////////////////////////////////////////////////
00353
00354     /*! @brief
00357      *          \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}}
00358      *      {\Gamma,\Gamma',\bigcup_i\Gamma_i\models
00359      *         \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)}
00360      * \f]
00362      *
00363      * This rule implements a step in the iterative algorithm for
00364      * eliminating integer equality.  The terms in the rule are
00365      * defined as follows:
00366      *
00367      * \f[\begin{array}{rcl}
00368      *       t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\
00369      *       t_{2}(y) & = &
00370      *          -(C\ \mathbf{mod}\  m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\  m)
00371      *             \cdot x_{i}-m\cdot y)\\ & & \\
00372      *       t_{3}(y) & = &
00373      *         \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i}
00374      *           -a\cdot y\\ & & \\
00375      *       m & = & a+1\\ & & \\
00376      *       \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m}
00377      *       +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\  m\\ & & \\
00378      *       i\ \mathbf{mod}\  m & = & i-m\left\lfloor\frac{i}{m}
00379      *          +\frac{1}{2}\right\rfloor
00380      *    \end{array}
00381      * \f]
00382      *
00383      * All the variables and coefficients are integer, and a >= 2.
00384      *
00385      * \param eqn is the equation ax=t:
00386      *   \f[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\f]
00387      *
00388      * \param isIntx is a Theorem deriving the integrality of the
00389      * LHS variable: IS_INTEGER(x)
00390      *
00391      * \param isIntVars is a vector of Theorems deriving the
00392      * integrality of all variables on the RHS
00393      */
00394     virtual Theorem eqElimIntRule(const Theorem& eqn,
00395           const Theorem& isIntx,
00396           const std::vector<Theorem>& isIntVars) = 0;
00397
00398     /*!
00399      * @brief return e <=> TRUE/FALSE for e == IS_INTEGER(c), where c
00400      * is a constant
00401      *
00402      * \param e is a predicate IS_INTEGER(c) where c is a rational constant
00403      */
00404     virtual Theorem isIntConst(const Expr& e) = 0;
00405
00406     virtual Theorem equalLeaves1(const Theorem& thm) = 0;
00407     virtual Theorem equalLeaves2(const Theorem& thm) = 0;
00408     virtual Theorem equalLeaves3(const Theorem& thm) = 0;
00409     virtual Theorem equalLeaves4(const Theorem& thm) = 0;
00410
00411     //! x /= y  ==>  (x < y) OR (x > y)
00412     /*! Used in concrete model generation */
00413     virtual Theorem diseqToIneq(const Theorem& diseq) = 0;
00414
00415     virtual Theorem dummyTheorem(const Expr& e) = 0;
00416
00417     virtual Theorem oneElimination(const Expr& x) = 0;
00418
00419     virtual Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound) = 0;
00420
00421     virtual Theorem addInequalities(const Theorem& thm1, const Theorem& thm2) = 0;
00422     virtual Theorem addInequalities(const std::vector<Theorem>& thms) = 0;
00423
00424     virtual Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2) = 0;
00425
00426     virtual Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2) = 0;
00427
00428     virtual Theorem integerSplit(const Expr& intVar, const Rational& intPoint) = 0;
00429
00430     virtual Theorem trustedRewrite(const Expr& expr1, const Expr& expr2) = 0;
00431
00432     virtual Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr) = 0;
00433
00434     virtual Theorem simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS) = 0;
00435
00436     virtual Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr) = 0;
00437
00438     virtual Theorem cycleConflict(const std::vector<Theorem>& inequalitites) = 0;
00439
00440     virtual Theorem implyEqualities(const std::vector<Theorem>& inequalities) = 0;
00441
00442     virtual Theorem implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0;
00443
00444     virtual Theorem implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied) = 0;
00445
00447
00448     virtual Theorem compactNonLinearTerm(const Expr& nonLinear) = 0;
00449
00450     virtual Theorem nonLinearIneqSignSplit(const Theorem& ineqThm) = 0;
00451
00452     virtual Theorem implyDiffLogicBothBounds(const Expr& x, std::vector<Theorem>& c1_le_x, Rational c1,
00453                          std::vector<Theorem>& x_le_c2, Rational c2) = 0;
00454
00455     virtual Theorem powerOfOne(const Expr& e) = 0;
00456
00457     virtual Theorem rewriteLeavesConst(const Expr& e);
00458
00459   }; // end of class ArithProofRules
00460 } // end of namespace CVC3
00461
00462 #endif