00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
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.h"
00028
00029 namespace CVC3 {
00030 class TheoryArith;
00031
00032 class ArithTheoremProducerOld: public ArithProofRules, public TheoremProducer {
00033 TheoryArith* d_theoryArith;
00034 private:
00035
00036
00037
00038
00039
00040 Rational modEq(const Rational& i, const Rational& m);
00041
00042 Expr create_t(const Expr& eqn);
00043
00044 Expr create_t2(const Expr& lhs, const Expr& rhs, const Expr& t);
00045
00046 Expr create_t3(const Expr& lhs, const Expr& rhs, const Expr& t);
00047
00048
00049
00050
00051
00052 void sumModM(std::vector<Expr>& summands, const Expr& sum,
00053 const Rational& m, const Rational& divisor);
00054 Expr monomialModM(const Expr& e,
00055 const Rational& m, const Rational& divisor);
00056 void sumMulF(std::vector<Expr>& summands, const Expr& sum,
00057 const Rational& m, const Rational& divisor);
00058 Expr monomialMulF(const Expr& e,
00059 const Rational& m, const Rational& divisor);
00060
00061 Rational f(const Rational& i, const Rational& m);
00062 Expr substitute(const Expr& term, ExprMap<Expr>& eMap);
00063
00064 public:
00065
00066 ArithTheoremProducerOld(TheoremManager* tm, TheoryArith* theoryArith):
00067 TheoremProducer(tm), d_theoryArith(theoryArith) { }
00068
00069
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
00074 Expr darkShadow(const Expr& lhs, const Expr& rhs) {
00075 return d_theoryArith->darkShadow(lhs, rhs);
00076 }
00077
00078
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
00087
00088
00089
00090 virtual Theorem varToMult(const Expr& e);
00091
00092
00093 virtual Theorem uMinusToMult(const Expr& e);
00094
00095
00096 virtual Theorem minusToPlus(const Expr& x, const Expr& y);
00097
00098
00099 virtual Theorem canonUMinusToDivide(const Expr& e);
00100
00101
00102
00103 virtual Theorem canonDivideConst(const Expr& c, const Expr& d);
00104
00105 virtual Theorem canonDivideMult(const Expr& cx, const Expr& d);
00106
00107
00108
00109
00110 virtual Theorem canonDividePlus(const Expr& e, const Expr& d);
00111
00112 virtual Theorem canonDivideVar(const Expr& e1, const Expr& e2);
00113
00114
00115
00116
00117
00118
00119
00120
00121
00122
00123
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
00147
00148
00149
00150
00151
00152 virtual Theorem moveSumConstantRight(const Expr& e);
00153
00154
00155 virtual Theorem canonDivide(const Expr & e);
00156
00157
00158 virtual Theorem canonMult(const Expr & e);
00159
00160
00161 virtual Theorem canonMultTermConst(const Expr& c, const Expr& t);
00162
00163 virtual Theorem canonMultTerm1Term2(const Expr& t1, const Expr& t2);
00164
00165 virtual Theorem canonMultZero(const Expr& e);
00166
00167 virtual Theorem canonMultOne(const Expr& e);
00168
00169 virtual Theorem canonMultConstConst(const Expr& c1, const Expr& c2);
00170
00171 virtual Theorem
00172 canonMultConstTerm(const Expr& c1, const Expr& c2, const Expr&t);
00173
00174 virtual Theorem canonMultConstSum(const Expr& c1, const Expr& sum);
00175
00176 virtual Theorem canonPowConst(const Expr& pow);
00177
00178
00179
00180 virtual Theorem canonFlattenSum(const Expr& e);
00181
00182
00183
00184 virtual Theorem canonComboLikeTerms(const Expr& e);
00185
00186
00187
00188 virtual Theorem constPredicate(const Expr& e);
00189
00190
00191 virtual Theorem rightMinusLeft(const Expr& e);
00192
00193
00194 virtual Theorem leftMinusRight(const Expr& e);
00195
00196
00197 virtual Theorem plusPredicate(const Expr& x,
00198 const Expr& y,
00199 const Expr& z, int kind);
00200
00201
00202 virtual Theorem multEqn(const Expr& x, const Expr& y, const Expr& z);
00203
00204
00205
00206 virtual Theorem multIneqn(const Expr& e, const Expr& z);
00207
00208
00209 virtual Theorem eqToIneq(const Expr& e);
00210
00211
00212 virtual Theorem flipInequality(const Expr& e);
00213
00214
00215
00216
00217
00218 Theorem negatedInequality(const Expr& e);
00219
00220 Theorem realShadow(const Theorem& alphaLTt, const Theorem& tLTbeta);
00221 Theorem realShadowEq(const Theorem& alphaLEt, const Theorem& tLEalpha);
00222 Theorem finiteInterval(const Theorem& aLEt, const Theorem& tLEac,
00223 const Theorem& isInta, const Theorem& isIntt);
00224
00225 Theorem darkGrayShadow2ab(const Theorem& betaLEbx,
00226 const Theorem& axLEalpha,
00227 const Theorem& isIntAlpha,
00228 const Theorem& isIntBeta,
00229 const Theorem& isIntx);
00230
00231 Theorem darkGrayShadow2ba(const Theorem& betaLEbx,
00232 const Theorem& axLEalpha,
00233 const Theorem& isIntAlpha,
00234 const Theorem& isIntBeta,
00235 const Theorem& isIntx);
00236
00237 Theorem expandDarkShadow(const Theorem& darkShadow);
00238 Theorem expandGrayShadow0(const Theorem& grayShadow);
00239 Theorem splitGrayShadow(const Theorem& grayShadow);
00240 Theorem expandGrayShadow(const Theorem& grayShadow);
00241 Theorem expandGrayShadowConst(const Theorem& grayShadow);
00242 Theorem grayShadowConst(const Theorem& g);
00243
00244
00245
00246
00247
00248 Rational constRHSGrayShadow(const Rational& c,
00249 const Rational& b,
00250 const Rational& a);
00251
00252 Theorem lessThanToLE(const Theorem& less, const Theorem& isIntLHS,
00253 const Theorem& isIntRHS, bool changeRight);
00254
00255 Theorem intVarEqnConst(const Expr& eqn, const Theorem& isIntx);
00256
00257 Theorem eqElimIntRule(const Theorem& eqn, const Theorem& isIntx,
00258 const std::vector<Theorem>& isIntVars);
00259
00260 Theorem isIntConst(const Expr& e);
00261
00262 Theorem equalLeaves1(const Theorem& e);
00263 Theorem equalLeaves2(const Theorem& e);
00264 Theorem equalLeaves3(const Theorem& e);
00265 Theorem equalLeaves4(const Theorem& e);
00266
00267 Theorem diseqToIneq(const Theorem& diseq);
00268
00269 Theorem dummyTheorem(const Expr& e);
00270
00271 Theorem oneElimination(const Expr& x);
00272
00273 Theorem clashingBounds(const Theorem& lowerBound, const Theorem& upperBound);
00274
00275 Theorem addInequalities(const Theorem& thm1, const Theorem& thm2);
00276
00277 Theorem implyWeakerInequality(const Expr& expr1, const Expr& expr2);
00278
00279 Theorem implyNegatedInequality(const Expr& expr1, const Expr& expr2);
00280
00281 Theorem integerSplit(const Expr& intVar, const Rational& intPoint);
00282
00283 Theorem trustedRewrite(const Expr& expr1, const Expr& expr2);
00284
00285 Theorem rafineStrictInteger(const Theorem& isIntConstrThm, const Expr& constr);
00286
00287 };
00288
00289 }
00290
00291 #endif