CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file theory_arith.h 00004 * 00005 * Author: Clark Barrett 00006 * 00007 * Created: Fri Jan 17 18:34:55 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 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 // New constants 00033 REAL_CONST = 30, // wrapper around constants to indicate that they should be real 00034 NEGINF = 31, 00035 POSINF = 32, 00036 00037 REAL = 3000, 00038 INT, 00039 SUBRANGE, 00040 00041 UMINUS, 00042 PLUS, 00043 MINUS, 00044 MULT, 00045 DIVIDE, 00046 POW, 00047 INTDIV, 00048 MOD, 00049 LT, 00050 LE, 00051 GT, 00052 GE, 00053 IS_INTEGER, 00054 DARK_SHADOW, 00055 GRAY_SHADOW 00056 00057 } ArithKinds; 00058 00059 /*****************************************************************************/ 00060 /*! 00061 *\class TheoryArith 00062 *\ingroup Theories 00063 *\brief This theory handles basic linear arithmetic. 00064 * 00065 * Author: Clark Barrett 00066 * 00067 * Created: Sat Feb 8 14:44:32 2003 00068 */ 00069 /*****************************************************************************/ 00070 class TheoryArith :public Theory { 00071 protected: 00072 Type d_realType; 00073 Type d_intType; 00074 std::vector<int> d_kinds; 00075 00076 protected: 00077 00078 //! Canonize the expression e, assuming all children are canonical 00079 virtual Theorem canon(const Expr& e) = 0; 00080 00081 //! Canonize the expression e recursively 00082 Theorem canonRec(const Expr& e); 00083 00084 //! Print a rational in SMT-LIB format 00085 void printRational(ExprStream& os, const Rational& r, bool printAsReal = false); 00086 00087 //! Whether any ite's appear in the arithmetic part of the term e 00088 bool isAtomicArithTerm(const Expr& e); 00089 00090 //! simplify leaves and then canonize 00091 Theorem canonSimp(const Expr& e); 00092 00093 //! helper for checkAssertEqInvariant 00094 bool recursiveCanonSimpCheck(const Expr& e); 00095 00096 public: 00097 TheoryArith(TheoryCore* core, const std::string& name) 00098 : Theory(core, name) {} 00099 ~TheoryArith() {} 00100 00101 virtual void addMultiplicativeSignSplit(const Theorem& case_split_thm) {}; 00102 00103 /** 00104 * Record that smaller should be smaller than bigger in the variable order. 00105 * Should be implemented in decision procedures that support it. 00106 */ 00107 virtual bool addPairToArithOrder(const Expr& smaller, const Expr& bigger) { return true; }; 00108 00109 // Used by translator 00110 //! Return whether e is syntactically identical to a rational constant 00111 bool isSyntacticRational(const Expr& e, Rational& r); 00112 //! Whether any ite's appear in the arithmetic part of the formula e 00113 bool isAtomicArithFormula(const Expr& e); 00114 //! Rewrite an atom to look like x - y op c if possible--for smtlib translation 00115 Expr rewriteToDiff(const Expr& e); 00116 00117 /*! @brief Composition of canon(const Expr&) by transitivity: take e0 = e1, 00118 * canonize e1 to e2, return e0 = e2. */ 00119 Theorem canonThm(const Theorem& thm) { 00120 return transitivityRule(thm, canon(thm.getRHS())); 00121 } 00122 00123 // ArithTheoremProducer needs this function, so make it public 00124 //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn 00125 virtual void separateMonomial(const Expr& e, Expr& c, Expr& var) = 0; 00126 00127 // Theory interface 00128 virtual void addSharedTerm(const Expr& e) = 0; 00129 virtual void assertFact(const Theorem& e) = 0; 00130 virtual void refineCounterExample() = 0; 00131 virtual void computeModelBasic(const std::vector<Expr>& v) = 0; 00132 virtual void computeModel(const Expr& e, std::vector<Expr>& vars) = 0; 00133 virtual void checkSat(bool fullEffort) = 0; 00134 virtual Theorem rewrite(const Expr& e) = 0; 00135 virtual void setup(const Expr& e) = 0; 00136 virtual void update(const Theorem& e, const Expr& d) = 0; 00137 virtual Theorem solve(const Theorem& e) = 0; 00138 virtual void checkAssertEqInvariant(const Theorem& e) = 0; 00139 virtual void checkType(const Expr& e) = 0; 00140 virtual Cardinality finiteTypeInfo(Expr& e, Unsigned& n, 00141 bool enumerate, bool computeSize) = 0; 00142 virtual void computeType(const Expr& e) = 0; 00143 virtual Type computeBaseType(const Type& t) = 0; 00144 virtual void computeModelTerm(const Expr& e, std::vector<Expr>& v) = 0; 00145 virtual Expr computeTypePred(const Type& t, const Expr& e) = 0; 00146 virtual Expr computeTCC(const Expr& e) = 0; 00147 virtual ExprStream& print(ExprStream& os, const Expr& e) = 0; 00148 virtual Expr parseExprOp(const Expr& e) = 0; 00149 00150 // Arith constructors 00151 Type realType() { return d_realType; } 00152 Type intType() { return d_intType;} 00153 Type subrangeType(const Expr& l, const Expr& r) 00154 { return Type(Expr(SUBRANGE, l, r)); } 00155 Expr rat(Rational r) { return getEM()->newRatExpr(r); } 00156 // Dark and Gray shadows (for internal use only) 00157 //! Construct the dark shadow expression representing lhs <= rhs 00158 Expr darkShadow(const Expr& lhs, const Expr& rhs) { 00159 return Expr(DARK_SHADOW, lhs, rhs); 00160 } 00161 //! Construct the gray shadow expression representing c1 <= v - e <= c2 00162 /*! Alternatively, v = e + i for some i s.t. c1 <= i <= c2 00163 */ 00164 Expr grayShadow(const Expr& v, const Expr& e, 00165 const Rational& c1, const Rational& c2) { 00166 return Expr(GRAY_SHADOW, v, e, rat(c1), rat(c2)); 00167 } 00168 bool leavesAreNumConst(const Expr& e); 00169 }; 00170 00171 // Arith testers 00172 inline bool isReal(Type t) { return t.getExpr().getKind() == REAL; } 00173 inline bool isInt(Type t) { return t.getExpr().getKind() == INT; } 00174 00175 // Static arith testers 00176 inline bool isRational(const Expr& e) { return e.isRational(); } 00177 inline bool isIntegerConst(const Expr& e) 00178 { return e.isRational() && e.getRational().isInteger(); } 00179 inline bool isUMinus(const Expr& e) { return e.getKind() == UMINUS; } 00180 inline bool isPlus(const Expr& e) { return e.getKind() == PLUS; } 00181 inline bool isMinus(const Expr& e) { return e.getKind() == MINUS; } 00182 inline bool isMult(const Expr& e) { return e.getKind() == MULT; } 00183 inline bool isDivide(const Expr& e) { return e.getKind() == DIVIDE; } 00184 inline bool isPow(const Expr& e) { return e.getKind() == POW; } 00185 inline bool isLT(const Expr& e) { return e.getKind() == LT; } 00186 inline bool isLE(const Expr& e) { return e.getKind() == LE; } 00187 inline bool isGT(const Expr& e) { return e.getKind() == GT; } 00188 inline bool isGE(const Expr& e) { return e.getKind() == GE; } 00189 inline bool isDarkShadow(const Expr& e) { return e.getKind() == DARK_SHADOW;} 00190 inline bool isGrayShadow(const Expr& e) { return e.getKind() == GRAY_SHADOW;} 00191 inline bool isIneq(const Expr& e) 00192 { return isLT(e) || isLE(e) || isGT(e) || isGE(e); } 00193 inline bool isIntPred(const Expr& e) { return e.getKind() == IS_INTEGER; } 00194 00195 // Static arith constructors 00196 inline Expr uminusExpr(const Expr& child) 00197 { return Expr(UMINUS, child); } 00198 inline Expr plusExpr(const Expr& left, const Expr& right) 00199 { return Expr(PLUS, left, right); } 00200 inline Expr plusExpr(const std::vector<Expr>& children) { 00201 DebugAssert(children.size() > 0, "plusExpr()"); 00202 return Expr(PLUS, children); 00203 } 00204 inline Expr minusExpr(const Expr& left, const Expr& right) 00205 { return Expr(MINUS, left, right); } 00206 inline Expr multExpr(const Expr& left, const Expr& right) 00207 { return Expr(MULT, left, right); } 00208 // Begin Deepak: 00209 //! a Mult expr with two or more children 00210 inline Expr multExpr(const std::vector<Expr>& children) { 00211 DebugAssert(children.size() > 0, "multExpr()"); 00212 return Expr(MULT, children); 00213 } 00214 //! Power (x^n, or base^{pow}) expressions 00215 inline Expr powExpr(const Expr& pow, const Expr & base) 00216 { return Expr(POW, pow, base);} 00217 // End Deepak 00218 inline Expr divideExpr(const Expr& left, const Expr& right) 00219 { return Expr(DIVIDE, left, right); } 00220 inline Expr ltExpr(const Expr& left, const Expr& right) 00221 { return Expr(LT, left, right); } 00222 inline Expr leExpr(const Expr& left, const Expr& right) 00223 { return Expr(LE, left, right); } 00224 inline Expr gtExpr(const Expr& left, const Expr& right) 00225 { return Expr(GT, left, right); } 00226 inline Expr geExpr(const Expr& left, const Expr& right) 00227 { return Expr(GE, left, right); } 00228 00229 inline Expr operator-(const Expr& child) 00230 { return uminusExpr(child); } 00231 inline Expr operator+(const Expr& left, const Expr& right) 00232 { return plusExpr(left, right); } 00233 inline Expr operator-(const Expr& left, const Expr& right) 00234 { return minusExpr(left, right); } 00235 inline Expr operator*(const Expr& left, const Expr& right) 00236 { return multExpr(left, right); } 00237 inline Expr operator/(const Expr& left, const Expr& right) 00238 { return divideExpr(left, right); } 00239 00240 } 00241 00242 #endif