00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021 #ifndef _cvc3__include__theory_arith_h_
00022 #define _cvc3__include__theory_arith_h_
00023
00024 #include "theory.h"
00025 #include "cdmap.h"
00026
00027 namespace CVC3 {
00028
00029 class ArithProofRules;
00030
00031 typedef enum {
00032 REAL = 3000,
00033 INT,
00034 SUBRANGE,
00035
00036 UMINUS,
00037 PLUS,
00038 MINUS,
00039 MULT,
00040 DIVIDE,
00041 POW,
00042 INTDIV,
00043 MOD,
00044 LT,
00045 LE,
00046 GT,
00047 GE,
00048 IS_INTEGER,
00049 NEGINF,
00050 POSINF,
00051 DARK_SHADOW,
00052 GRAY_SHADOW,
00053
00054 REAL_CONST
00055 } ArithKinds;
00056
00057
00058
00059
00060
00061
00062
00063
00064
00065
00066
00067
00068 class TheoryArith :public Theory {
00069 protected:
00070 Type d_realType;
00071 Type d_intType;
00072
00073 protected:
00074
00075
00076 virtual Theorem canon(const Expr& e) = 0;
00077
00078
00079 Theorem canonRec(const Expr& e);
00080
00081
00082 void printRational(ExprStream& os, const Rational& r, bool printAsReal = false);
00083
00084
00085 bool isAtomicArithTerm(const Expr& e);
00086
00087
00088 Theorem canonSimp(const Expr& e);
00089
00090
00091 bool recursiveCanonSimpCheck(const Expr& e);
00092
00093 public:
00094 TheoryArith(TheoryCore* core, const std::string& name)
00095 : Theory(core, name) {}
00096 ~TheoryArith() {}
00097
00098
00099
00100 bool isSyntacticRational(const Expr& e, Rational& r);
00101
00102 bool isAtomicArithFormula(const Expr& e);
00103
00104 Expr rewriteToDiff(const Expr& e);
00105
00106
00107
00108 Theorem canonThm(const Theorem& thm) {
00109 return transitivityRule(thm, canon(thm.getRHS()));
00110 }
00111
00112
00113
00114 virtual void separateMonomial(const Expr& e, Expr& c, Expr& var) = 0;
00115
00116
00117 virtual void addSharedTerm(const Expr& e) = 0;
00118 virtual void assertFact(const Theorem& e) = 0;
00119 virtual void refineCounterExample() = 0;
00120 virtual void computeModelBasic(const std::vector<Expr>& v) = 0;
00121 virtual void computeModel(const Expr& e, std::vector<Expr>& vars) = 0;
00122 virtual void checkSat(bool fullEffort) = 0;
00123 virtual Theorem rewrite(const Expr& e) = 0;
00124 virtual void setup(const Expr& e) = 0;
00125 virtual void update(const Theorem& e, const Expr& d) = 0;
00126 virtual Theorem solve(const Theorem& e) = 0;
00127 virtual void checkAssertEqInvariant(const Theorem& e) = 0;
00128 virtual void checkType(const Expr& e) = 0;
00129 virtual void computeType(const Expr& e) = 0;
00130 virtual Type computeBaseType(const Type& t) = 0;
00131 virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v) = 0;
00132 virtual Expr computeTypePred(const Type& t, const Expr& e) = 0;
00133 virtual Expr computeTCC(const Expr& e) = 0;
00134 virtual ExprStream& print(ExprStream& os, const Expr& e) = 0;
00135 virtual Expr parseExprOp(const Expr& e) = 0;
00136
00137
00138 Type realType() { return d_realType; }
00139 Type intType() { return d_intType;}
00140 Type subrangeType(const Expr& l, const Expr& r)
00141 { return Type(Expr(SUBRANGE, l, r)); }
00142 Expr rat(Rational r) { return getEM()->newRatExpr(r); }
00143
00144
00145 Expr darkShadow(const Expr& lhs, const Expr& rhs) {
00146 return Expr(DARK_SHADOW, lhs, rhs);
00147 }
00148
00149
00150
00151 Expr grayShadow(const Expr& v, const Expr& e,
00152 const Rational& c1, const Rational& c2) {
00153 return Expr(GRAY_SHADOW, v, e, rat(c1), rat(c2));
00154 }
00155 };
00156
00157
00158 inline bool isReal(Type t) { return t.getExpr().getKind() == REAL; }
00159 inline bool isInt(Type t) { return t.getExpr().getKind() == INT; }
00160
00161
00162 inline bool isRational(const Expr& e) { return e.isRational(); }
00163 inline bool isIntegerConst(const Expr& e)
00164 { return e.isRational() && e.getRational().isInteger(); }
00165 inline bool isUMinus(const Expr& e) { return e.getKind() == UMINUS; }
00166 inline bool isPlus(const Expr& e) { return e.getKind() == PLUS; }
00167 inline bool isMinus(const Expr& e) { return e.getKind() == MINUS; }
00168 inline bool isMult(const Expr& e) { return e.getKind() == MULT; }
00169 inline bool isDivide(const Expr& e) { return e.getKind() == DIVIDE; }
00170 inline bool isPow(const Expr& e) { return e.getKind() == POW; }
00171 inline bool isLT(const Expr& e) { return e.getKind() == LT; }
00172 inline bool isLE(const Expr& e) { return e.getKind() == LE; }
00173 inline bool isGT(const Expr& e) { return e.getKind() == GT; }
00174 inline bool isGE(const Expr& e) { return e.getKind() == GE; }
00175 inline bool isDarkShadow(const Expr& e) { return e.getKind() == DARK_SHADOW;}
00176 inline bool isGrayShadow(const Expr& e) { return e.getKind() == GRAY_SHADOW;}
00177 inline bool isIneq(const Expr& e)
00178 { return isLT(e) || isLE(e) || isGT(e) || isGE(e); }
00179 inline bool isIntPred(const Expr& e) { return e.getKind() == IS_INTEGER; }
00180
00181
00182 inline Expr uminusExpr(const Expr& child)
00183 { return Expr(UMINUS, child); }
00184 inline Expr plusExpr(const Expr& left, const Expr& right)
00185 { return Expr(PLUS, left, right); }
00186 inline Expr plusExpr(const std::vector<Expr>& children) {
00187 DebugAssert(children.size() > 0, "plusExpr()");
00188 return Expr(PLUS, children);
00189 }
00190 inline Expr minusExpr(const Expr& left, const Expr& right)
00191 { return Expr(MINUS, left, right); }
00192 inline Expr multExpr(const Expr& left, const Expr& right)
00193 { return Expr(MULT, left, right); }
00194
00195
00196 inline Expr multExpr(const std::vector<Expr>& children) {
00197 DebugAssert(children.size() > 0, "multExpr()");
00198 return Expr(MULT, children);
00199 }
00200
00201 inline Expr powExpr(const Expr& pow, const Expr & base)
00202 { return Expr(POW, pow, base);}
00203
00204 inline Expr divideExpr(const Expr& left, const Expr& right)
00205 { return Expr(DIVIDE, left, right); }
00206 inline Expr ltExpr(const Expr& left, const Expr& right)
00207 { return Expr(LT, left, right); }
00208 inline Expr leExpr(const Expr& left, const Expr& right)
00209 { return Expr(LE, left, right); }
00210 inline Expr gtExpr(const Expr& left, const Expr& right)
00211 { return Expr(GT, left, right); }
00212 inline Expr geExpr(const Expr& left, const Expr& right)
00213 { return Expr(GE, left, right); }
00214
00215 inline Expr operator-(const Expr& child)
00216 { return uminusExpr(child); }
00217 inline Expr operator+(const Expr& left, const Expr& right)
00218 { return plusExpr(left, right); }
00219 inline Expr operator-(const Expr& left, const Expr& right)
00220 { return minusExpr(left, right); }
00221 inline Expr operator*(const Expr& left, const Expr& right)
00222 { return multExpr(left, right); }
00223 inline Expr operator/(const Expr& left, const Expr& right)
00224 { return divideExpr(left, right); }
00225
00226 }
00227
00228 #endif