theory_arith.h

Go to the documentation of this file.
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     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 // wrapper around constants to indicate that they should be real
00055   } ArithKinds;
00056 
00057 /*****************************************************************************/
00058 /*!
00059  *\class TheoryArith
00060  *\ingroup Theories
00061  *\brief This theory handles basic linear arithmetic.
00062  *
00063  * Author: Clark Barrett
00064  *
00065  * Created: Sat Feb  8 14:44:32 2003
00066  */
00067 /*****************************************************************************/
00068 class TheoryArith :public Theory {
00069  protected:
00070   Type d_realType;
00071   Type d_intType;
00072 
00073  protected:
00074 
00075   //! Canonize the expression e, assuming all children are canonical
00076   virtual Theorem canon(const Expr& e) = 0;
00077 
00078   //! Canonize the expression e recursively
00079   Theorem canonRec(const Expr& e);
00080 
00081   //! Print a rational in SMT-LIB format
00082   void printRational(ExprStream& os, const Rational& r, bool printAsReal = false);
00083 
00084   //! Whether any ite's appear in the arithmetic part of the term e
00085   bool isAtomicArithTerm(const Expr& e);
00086 
00087   //! simplify leaves and then canonize
00088   Theorem canonSimp(const Expr& e);
00089 
00090   //! helper for checkAssertEqInvariant
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   // Used by translator
00099   //! Return whether e is syntactically identical to a rational constant
00100   bool isSyntacticRational(const Expr& e, Rational& r);
00101   //! Whether any ite's appear in the arithmetic part of the formula e
00102   bool isAtomicArithFormula(const Expr& e);
00103   //! Rewrite an atom to look like x - y op c if possible--for smtlib translation
00104   Expr rewriteToDiff(const Expr& e);
00105 
00106   /*! @brief Composition of canon(const Expr&) by transitivity: take e0 = e1,
00107    * canonize e1 to e2, return e0 = e2. */
00108   Theorem canonThm(const Theorem& thm) {
00109     return transitivityRule(thm, canon(thm.getRHS()));
00110   }
00111 
00112   // ArithTheoremProducer needs this function, so make it public
00113   //! Separate monomial e = c*p1*...*pn into c and 1*p1*...*pn
00114   virtual void separateMonomial(const Expr& e, Expr& c, Expr& var) = 0;
00115 
00116   // Theory interface
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   // Arith constructors
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   // Dark and Gray shadows (for internal use only)
00144   //! Construct the dark shadow expression representing lhs <= rhs
00145   Expr darkShadow(const Expr& lhs, const Expr& rhs) {
00146     return Expr(DARK_SHADOW, lhs, rhs);
00147   }
00148   //! Construct the gray shadow expression representing c1 <= v - e <= c2
00149   /*! Alternatively, v = e + i for some i s.t. c1 <= i <= c2
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 // Arith testers
00158 inline bool isReal(Type t) { return t.getExpr().getKind() == REAL; }
00159 inline bool isInt(Type t) { return t.getExpr().getKind() == INT; }
00160 
00161 // Static arith testers
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 // Static arith constructors
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 // Begin Deepak: 
00195 //! a Mult expr with two or more children
00196 inline Expr multExpr(const std::vector<Expr>& children) {
00197   DebugAssert(children.size() > 0, "multExpr()");
00198   return Expr(MULT, children);
00199 }
00200 //! Power (x^n, or base^{pow}) expressions
00201 inline Expr powExpr(const Expr& pow, const Expr & base)
00202   { return Expr(POW, pow, base);}
00203 // End Deepak
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

Generated on Tue Jul 3 14:33:39 2007 for CVC3 by  doxygen 1.5.1