arith_theorem_producer_old.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file arith_theorem_producer_old.h
00004  * \brief TRUSTED implementation of 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_theorem_producer_old_h_
00023 #define _cvc3__arith_theorem_producer_old_h_
00024 
00025 #include "arith_proof_rules.h"
00026 #include "theorem_producer.h"
00027 #include "theory_arith_old.h"
00028 
00029 namespace CVC3 {
00030 
00031   class ArithTheoremProducerOld: public ArithProofRules, public TheoremProducer {
00032     TheoryArithOld* d_theoryArith;
00033   private:
00034     /*! \name Auxiliary functions for eqElimIntRule()
00035      * Methods that compute the subterms used in eqElimIntRule()
00036      *@{
00037      */
00038     //! Compute the special modulus: i - m*floor(i/m+1/2)
00039     Rational modEq(const Rational& i, const Rational& m);
00040     //! Create the term 't'.  See eqElimIntRule().
00041     Expr create_t(const Expr& eqn);
00042     //! Create the term 't2'.  See eqElimIntRule().
00043     Expr create_t2(const Expr& lhs, const Expr& rhs, const Expr& t);
00044     //! Create the term 't3'.  See eqElimIntRule().
00045     Expr create_t3(const Expr& lhs, const Expr& rhs, const Expr& t);
00046     /*! @brief Takes sum = a_0 + a_1*x_1+...+a_n*x_n and returns the
00047      * vector of similar monomials (in 'summands') with coefficients
00048      * mod(a_i, m).  If divide flag is true, the coefficients will be
00049      * mod(a_i,m)/m.
00050      */
00051     void sumModM(std::vector<Expr>& summands, const Expr& sum,
00052      const Rational& m, const Rational& divisor);
00053     Expr monomialModM(const Expr& e,
00054           const Rational& m, const Rational& divisor);
00055     void sumMulF(std::vector<Expr>& summands, const Expr& sum,
00056      const Rational& m, const Rational& divisor);
00057     Expr monomialMulF(const Expr& e,
00058           const Rational& m, const Rational& divisor);
00059     //! Compute floor(i/m+1/2) + mod(i,m)
00060     Rational f(const Rational& i, const Rational& m);
00061     Expr substitute(const Expr& term, ExprMap<Expr>& eMap);
00062     void getLeaves(const Expr& e, std::set<Rational>& s, ExprHashMap<bool>& cache);
00063     /*@}*/
00064   public:
00065     //! Constructor
00066     ArithTheoremProducerOld(TheoremManager* tm, TheoryArithOld* theoryArith):
00067       TheoremProducer(tm), d_theoryArith(theoryArith) { }
00068 
00069     //! Create Expr from Rational (for convenience)
00070     Expr rat(Rational r) { return d_em->newRatExpr(r); }
00071     Type realType() { return d_theoryArith->realType(); }
00072     Type intType() { return d_theoryArith->intType(); }
00073     //! Construct the dark shadow expression representing lhs <= rhs
00074     Expr darkShadow(const Expr& lhs, const Expr& rhs) {
00075       return d_theoryArith->darkShadow(lhs, rhs);
00076     }
00077     //! Construct the gray shadow expression representing c1 <= v - e <= c2
00078     /*! Alternatively, v = e + i for some i s.t. c1 <= i <= c2
00079      */
00080     Expr grayShadow(const Expr& v, const Expr& e,
00081         const Rational& c1, const Rational& c2) {
00082       return d_theoryArith->grayShadow(v, e, c1, c2);
00083     }
00084 
00085     ////////////////////////////////////////////////////////////////////
00086     // Canonization rules
00087     ////////////////////////////////////////////////////////////////////
00088 
00089     // ==> x = 1 * x
00090     virtual Theorem varToMult(const Expr& e);
00091 
00092     // ==> -(e) = (-1) * e
00093     virtual Theorem uMinusToMult(const Expr& e);
00094 
00095     // ==> x - y = x + (-1) * y
00096     virtual Theorem minusToPlus(const Expr& x, const Expr& y);
00097 
00098     // Rule for unary minus: it just converts it to division by -1,
00099     virtual Theorem canonUMinusToDivide(const Expr& e);
00100 
00101     // Rules for division by constant 'd'
00102     // (c) / d ==> (c/d), takes c and d
00103     virtual Theorem canonDivideConst(const Expr& c, const Expr& d);
00104     // (c * x) / d ==> (c/d) * x, takes (c*x) and d
00105     virtual Theorem canonDivideMult(const Expr& cx, const Expr& d);
00106     // (+ c ...)/d ==> push division to all the coefficients.
00107     // The result is not canonical, but canonizing the summands will
00108     // make it canonical.
00109     // Takes (+ c ...) and d
00110     virtual Theorem canonDividePlus(const Expr& e, const Expr& d);
00111     // x / d ==> (1/d) * x, takes x and d
00112     virtual Theorem canonDivideVar(const Expr& e1, const Expr& e2);
00113 
00114     // Canon Rules for multiplication
00115 
00116     // TODO Deepak:
00117     // t1 * t2 where t1 and t2 are canonized expressions, i.e. it can be a
00118     // 1) Rational constant
00119     // 2) Arithmetic Leaf (var or term from another theory)
00120     // 3) (POW rational leaf)
00121     // 4) (MULT rational mterm'_1 ...) where each mterm' is of type (2) or (3)
00122     // 5) (PLUS rational sterm_1 sterm_2 ...) where each sterm is of
00123     //     type (2) or (3) or (4)
00124 
00125     static bool greaterthan(const Expr &, const Expr &);
00126     virtual Expr simplifiedMultExpr(std::vector<Expr> & mulKids);
00127     virtual Expr canonMultConstMult(const Expr & c, const Expr & e);
00128     virtual Expr canonMultConstPlus(const Expr & e1, const Expr & e2);
00129     virtual Expr canonMultPowPow(const Expr & e1, const Expr & e2);
00130     virtual Expr canonMultPowLeaf(const Expr & e1, const Expr & e2);
00131     virtual Expr canonMultLeafLeaf(const Expr & e1, const Expr & e2);
00132     virtual Expr canonMultLeafOrPowMult(const Expr & e1, const Expr & e2);
00133     virtual Expr canonCombineLikeTerms(const std::vector<Expr> & sumExprs);
00134     virtual Expr
00135   canonMultLeafOrPowOrMultPlus(const Expr & e1, const Expr & e2);
00136     virtual Expr canonMultPlusPlus(const Expr & e1, const Expr & e2);
00137     virtual Theorem canonMultMtermMterm(const Expr& e);
00138     virtual Theorem canonPlus(const Expr & e);
00139     virtual Theorem canonInvertConst(const Expr & e);
00140     virtual Theorem canonInvertLeaf(const Expr & e);
00141     virtual Theorem canonInvertPow(const Expr & e);
00142     virtual Theorem canonInvertMult(const Expr & e);
00143     virtual Theorem canonInvert(const Expr & e);
00144 
00145     /**
00146      * Transform e = (SUM r t1 ... tn) @ 0 into (SUM t1 ... tn) @ -r. The first
00147      * sum term (r) must be a rational and t1 ... tn terms must be canonised.
00148      *
00149      * @param e the expression to transform
00150      * @return rewrite theorem representing the transformation
00151      */
00152     virtual Theorem moveSumConstantRight(const Expr& e);
00153 
00154     /** e[0]/e[1] ==> e[0]*(e[1])^-1 */
00155     virtual Theorem canonDivide(const Expr & e);
00156 
00157     /** Multiply out the operands of the multiplication (each of them is expected to be canonised */
00158     virtual Theorem canonMult(const Expr & e);
00159 
00160     // t*c ==> c*t, takes constant c and term t
00161     virtual Theorem canonMultTermConst(const Expr& c, const Expr& t);
00162     // t1*t2 ==> Error, takes t1 and t2 where both are non-constants
00163     virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2);
00164     // 0*t ==> 0, takes 0*t
00165     virtual Theorem canonMultZero(const Expr& e);
00166     // 1*t ==> t, takes 1*t
00167     virtual Theorem canonMultOne(const Expr& e);
00168     // c1*c2 ==> c', takes constant c1*c2
00169     virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
00170     // c1*(c2*t) ==> c'*t, takes c1 and c2 and t
00171     virtual Theorem
00172       canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t);
00173     // c1*(+ c2 v1 ...) ==> (+ c' c1v1 ...), takes c1 and the sum
00174     virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum);
00175     // c^n = c' (compute the constant power expression)
00176     virtual Theorem canonPowConst(const Expr& pow);
00177 
00178     // Rules for addition
00179     // flattens the input. accepts a PLUS expr
00180     virtual Theorem canonFlattenSum(const Expr& e);
00181 
00182     // Rules for addition
00183     // combine like terms. accepts a flattened PLUS expr
00184     virtual Theorem canonComboLikeTerms(const Expr& e);
00185 
00186     // 0 = (* e1 e2 ...) <=> 0 = e1 OR 0 = e2 OR ...
00187     virtual Theorem multEqZero(const Expr& expr);
00188 
00189     // 0 = (^ c x) <=> false if c <=0
00190     //             <=> 0 = x if c > 0
00191     virtual Theorem powEqZero(const Expr& expr);
00192 
00193     // x^n = y^n <=> x = y (if n is odd)
00194     // x^n = y^n <=> x = y OR x = -y (if n is even)
00195     virtual Theorem elimPower(const Expr& expr);
00196 
00197     // x^n = c <=> x = root (if n is odd and root^n = c)
00198     // x^n = c <=> x = root OR x = -root (if n is even and root^n = c)
00199     virtual Theorem elimPowerConst(const Expr& expr, const Rational& root);
00200 
00201     // x^n = c <=> false (if n is even and c is negative)
00202     virtual Theorem evenPowerEqNegConst(const Expr& expr);
00203 
00204     // x^n = c <=> false (if x is an integer and c is not a perfect n power)
00205     virtual Theorem intEqIrrational(const Expr& expr, const Theorem& isInt);
00206 
00207     // e[0] kind e[1] <==> true when e[0] kind e[1],
00208     // false when e[0] !kind e[1], for constants only
00209     virtual Theorem constPredicate(const Expr& e);
00210 
00211     // e[0] kind e[1] <==> 0 kind e[1] - e[0]
00212     virtual Theorem rightMinusLeft(const Expr& e);
00213 
00214     // e[0] kind e[1] <==> e[0] - e[1] kind 0
00215     virtual Theorem leftMinusRight(const Expr& e);
00216 
00217     // x kind y <==> x + z kind y + z
00218     virtual Theorem plusPredicate(const Expr& x,
00219           const Expr& y,
00220           const Expr& z, int kind);
00221 
00222     // x = y <==> x * z = y * z
00223     virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z);
00224 
00225     // x = y <==> z=0 OR x * 1/z = y * 1/z
00226     virtual Theorem divideEqnNonConst(const Expr& x, const Expr& y, const Expr& z);
00227 
00228     // if z is +ve, return e[0] LT|LE|GT|GE e[1] <==> e[0]*z LT|LE|GT|GE e[1]*z
00229     // if z is -ve, return e[0] LT|LE|GT|GE e[1] <==> e[1]*z LT|LE|GT|GE e[0]*z
00230     virtual Theorem multIneqn(const Expr& e, const Expr& z);
00231 
00232     // x = y ==> x <= y and x >= y
00233     virtual Theorem eqToIneq(const Expr& e);
00234 
00235     // "op1 GE|GT op2" <==> op2 LE|LT op1
00236     virtual Theorem flipInequality(const Expr& e);
00237 
00238     // NOT (op1 LT op2)  <==> (op1 GE op2)
00239     // NOT (op1 LE op2)  <==> (op1 GT op2)
00240     // NOT (op1 GT op2)  <==> (op1 LE op2)
00241     // NOT (op1 GE op2)  <==> (op1 LT op2)
00242     Theorem negatedInequality(const Expr& e);
00243 
00244     Theorem realShadow(const Theorem& alphaLTt, const Theorem& tLTbeta);
00245     Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
00246     Theorem finiteInterval(const Theorem& aLEt, const Theorem& tLEac,
00247          const Theorem& isInta, const Theorem& isIntt);
00248 
00249     Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
00250             const Theorem& axLEalpha,
00251             const Theorem& isIntAlpha,
00252             const Theorem& isIntBeta,
00253             const Theorem& isIntx);
00254 
00255     Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
00256             const Theorem& axLEalpha,
00257             const Theorem& isIntAlpha,
00258             const Theorem& isIntBeta,
00259             const Theorem& isIntx);
00260 
00261     Theorem expandDarkShadow(const Theorem& darkShadow);
00262     Theorem expandGrayShadow0(const Theorem& grayShadow);
00263     Theorem splitGrayShadow(const Theorem& grayShadow);
00264     Theorem splitGrayShadowSmall(const Theorem& grayShadow);
00265     Theorem expandGrayShadow(const Theorem& grayShadow);
00266     Theorem expandGrayShadowConst(const Theorem& grayShadow);
00267     Theorem grayShadowConst(const Theorem& g);
00268 
00269     //! Implements j(c,b,a)
00270     /*! accepts 3 integers a,b,c and returns
00271      *  (b > 0)? (c+b) mod a :  (a - (c+b)) mod a
00272      */
00273     Rational constRHSGrayShadow(const Rational& c,
00274         const Rational& b,
00275         const Rational& a);
00276 
00277     Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
00278        const Theorem& isIntRHS, bool changeRight);
00279 
00280     Theorem lessThanToLERewrite(const Expr& ineq, const Theorem& isIntLHS,
00281            const Theorem& isIntRHS, bool changeRight);
00282 
00283 
00284     Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
00285     Theorem IsIntegerElim(const Theorem& isIntx);
00286 
00287     Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
00288         const std::vector<Theorem>& isIntVars);
00289 
00290     Theorem isIntConst(const Expr& e);
00291 
00292     Theorem equalLeaves1(const Theorem& e);
00293     Theorem equalLeaves2(const Theorem& e);
00294     Theorem equalLeaves3(const Theorem& e);
00295     Theorem equalLeaves4(const Theorem& e);
00296 
00297     Theorem diseqToIneq(const Theorem& diseq);
00298 
00299     Theorem dummyTheorem(const Expr& e);
00300 
00301     Theorem oneElimination(const Expr& x);
00302 
00303     Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound);
00304 
00305     Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
00306     Theorem addInequalities(const std::vector<Theorem>& thms);
00307 
00308     Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2);
00309 
00310     Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2);
00311 
00312     Theorem integerSplit(const Expr& intVar, const Rational& intPoint);
00313 
00314     Theorem trustedRewrite(const Expr& expr1, const Expr& expr2);
00315 
00316     Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
00317 
00318     Theorem simpleIneqInt(const Expr& ineq, const Theorem& isIntRHS);
00319 
00320     Theorem intEqualityRationalConstant(const Theorem& isIntConstrThm, const Expr& constr);
00321 
00322     Theorem cycleConflict(const std::vector<Theorem>& inequalitites);
00323 
00324     Theorem implyEqualities(const std::vector<Theorem>& inequalities);
00325 
00326     Theorem implyWeakerInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied);
00327 
00328     Theorem implyNegatedInequalityDiffLogic(const std::vector<Theorem>& antecedentThms, const Expr& implied);
00329 
00330     Theorem expandGrayShadowRewrite(const Expr& theShadow);
00331 
00332     Theorem compactNonLinearTerm(const Expr& nonLinear);
00333 
00334     Theorem nonLinearIneqSignSplit(const Theorem& ineqThm);
00335 
00336     Theorem implyDiffLogicBothBounds(const Expr& x, std::vector<Theorem>& c1_le_x, Rational c1,
00337                        std::vector<Theorem>& x_le_c2, Rational c2);
00338 
00339     Theorem powerOfOne(const Expr& e);
00340 
00341     Theorem rewriteLeavesConst(const Expr& e);
00342 
00343   }; // end of class ArithTheoremProducerOld
00344 
00345 } // end of namespace CVC3
00346 
00347 #endif

Generated on Wed Nov 18 16:13:28 2009 for CVC3 by  doxygen 1.5.2