theory_arith.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theory_arith.cpp
00004  * 
00005  * Author: Clark Barrett, Vijay Ganesh.
00006  * 
00007  * Created: Fri Jan 17 18:39:18 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 
00022 #include "theory_arith.h"
00023 #include "theory_core.h"
00024 #include "translator.h"
00025 
00026 
00027 using namespace std;
00028 using namespace CVC3;
00029 
00030 
00031 Theorem TheoryArith::canonRec(const Expr& e)
00032 {
00033   if (isLeaf(e)) return reflexivityRule(e);
00034   int ar = e.arity();
00035   if (ar > 0) {
00036     vector<Theorem> newChildrenThm;
00037     vector<unsigned> changed;
00038     for(int k = 0; k < ar; ++k) {
00039       // Recursively canonize the kids
00040       Theorem thm = canonRec(e[k]);
00041       if (thm.getLHS() != thm.getRHS()) {
00042   newChildrenThm.push_back(thm);
00043   changed.push_back(k);
00044       }
00045     }
00046     if(changed.size() > 0) {
00047       return canonThm(substitutivityRule(e, changed, newChildrenThm));
00048     }
00049   }
00050   return canon(e);
00051 }
00052 
00053 
00054 void TheoryArith::printRational(ExprStream& os, const Rational& r,
00055                                 bool printAsReal)
00056 {
00057   // Print rational
00058   if (r.isInteger()) {
00059     if (r < 0) {
00060       os << "(" << push << "-" << space << (-r).toString();
00061       if (printAsReal) os << ".0";
00062       os << push << ")";
00063     }
00064     else {
00065       os << r.toString();
00066       if (printAsReal) os << ".0";
00067     }
00068   }
00069   else {
00070     os << "(" << push << "/ ";
00071     Rational tmp = r.getNumerator();
00072     if (tmp < 0) {
00073       os << "(" << push << "-" << space << (-tmp).toString();
00074       if (printAsReal) os << ".0";
00075       os << push << ")";
00076     }
00077     else {
00078       os << tmp.toString();
00079       if (printAsReal) os << ".0";
00080     }
00081     os << space;
00082     tmp = r.getDenominator();
00083     DebugAssert(tmp > 0 && tmp.isInteger(), "Unexpected rational denominator");
00084     os << tmp.toString();
00085     if (printAsReal) os << ".0";
00086     os << push << ")";
00087   }
00088 }
00089 
00090 
00091 bool TheoryArith::isAtomicArithTerm(const Expr& e)
00092 {
00093   switch (e.getKind()) {
00094     case RATIONAL_EXPR:
00095       return true;
00096     case ITE:
00097       return false;
00098     case UMINUS:
00099     case PLUS:
00100     case MINUS:
00101     case MULT:
00102     case DIVIDE:
00103     case POW:
00104     case INTDIV:
00105     case MOD: {
00106       int i=0, iend=e.arity();
00107       for(; i!=iend; ++i) {
00108         if (!isAtomicArithTerm(e[i])) return false;
00109       }
00110       break;
00111     }
00112     default:
00113       break;
00114   }
00115   return true;
00116 }
00117 
00118 
00119 bool TheoryArith::isAtomicArithFormula(const Expr& e)
00120 {
00121   switch (e.getKind()) {
00122     case LT:
00123     case GT:
00124     case LE:
00125     case GE:
00126     case EQ:
00127       return isAtomicArithTerm(e[0]) && isAtomicArithTerm(e[1]);
00128   }
00129   return false;
00130 }
00131 
00132 
00133 bool TheoryArith::isSyntacticRational(const Expr& e, Rational& r)
00134 {
00135   if (e.getKind() == REAL_CONST) {
00136     r = e[0].getRational();
00137     return true;
00138   }
00139   else if (e.isRational()) {
00140     r = e.getRational();
00141     return true;
00142   }
00143   else if (isUMinus(e)) {
00144     if (isSyntacticRational(e[0], r)) {
00145       r = -r;
00146       return true;
00147     }
00148   }
00149   else if (isDivide(e)) {
00150     Rational num;
00151     if (isSyntacticRational(e[0], num)) {
00152       Rational den;
00153       if (isSyntacticRational(e[1], den)) {
00154         if (den != 0) {
00155           r = num / den;
00156           return true;
00157         }
00158       }
00159     }
00160   }
00161   return false;
00162 }
00163 
00164 
00165 Expr TheoryArith::rewriteToDiff(const Expr& e)
00166 {
00167   Expr tmp = e[0] - e[1];
00168   tmp = canonRec(tmp).getRHS();
00169   switch (tmp.getKind()) {
00170     case RATIONAL_EXPR: {
00171       Rational r = tmp.getRational();
00172       switch (e.getKind()) {
00173         case LT:
00174           if (r < 0) return trueExpr();
00175           else return falseExpr();
00176         case LE:
00177           if (r <= 0) return trueExpr();
00178           else return falseExpr();
00179         case GT:
00180           if (r > 0) return trueExpr();
00181           else return falseExpr();
00182         case GE:
00183           if (r >= 0) return trueExpr();
00184           else return falseExpr();
00185         case EQ:
00186           if (r == 0) return trueExpr();
00187           else return falseExpr();
00188       }
00189     }
00190     case MULT:
00191       DebugAssert(tmp[0].isRational(), "Unexpected term structure from canon");
00192       if (tmp[0].getRational() != -1) return e;
00193       return Expr(e.getOp(), theoryCore()->getTranslator()->zeroVar() - tmp[1], rat(0));
00194     case PLUS: {
00195       DebugAssert(tmp[0].isRational(), "Unexpected term structure from canon");
00196       Rational c = tmp[0].getRational();
00197       Expr x, y;
00198       if (tmp.arity() == 2) {
00199         if (tmp[1].getKind() == MULT) {
00200           x = theoryCore()->getTranslator()->zeroVar();
00201           y = tmp[1];
00202         }
00203         else {
00204           x = tmp[1];
00205           y = rat(-1) * theoryCore()->getTranslator()->zeroVar();
00206         }
00207       }
00208       else if (tmp.arity() == 3) {
00209         if (tmp[1].getKind() == MULT) {
00210           x = tmp[2];
00211           y = tmp[1];
00212         }
00213         else if (tmp[2].getKind() == MULT) {
00214           x = tmp[1];
00215           y = tmp[2];
00216         }
00217         else return e;
00218       }
00219       else return e;
00220       if (x.getKind() == MULT) return e;
00221       DebugAssert(y[0].isRational(), "Unexpected term structure from canon");
00222       if (y[0].getRational() != -1) return e;
00223       return Expr(e.getOp(), x - y[1], getEM()->newRatExpr(-c));
00224     }
00225     default:
00226       return Expr(e.getOp(), tmp - theoryCore()->getTranslator()->zeroVar(), rat(0));
00227       break;
00228   }
00229   return e;
00230 }
00231 
00232 
00233 Theorem TheoryArith::canonSimp(const Expr& e)
00234 {
00235   DebugAssert(canonRec(e).getRHS() == e, "canonSimp expects input to be canonized");
00236   int ar = e.arity();
00237   if (isLeaf(e)) return find(e);
00238   if (ar > 0) {
00239     vector<Theorem> newChildrenThm;
00240     vector<unsigned> changed;
00241     Theorem thm;
00242     for (int k = 0; k < ar; ++k) {
00243       thm = canonSimp(e[k]);
00244       if (thm.getLHS() != thm.getRHS()) {
00245         newChildrenThm.push_back(thm);
00246         changed.push_back(k);
00247       }
00248     }
00249     if(changed.size() > 0)
00250       return canonThm(substitutivityRule(e, changed, newChildrenThm));
00251   }
00252   return reflexivityRule(e);
00253 }
00254 
00255 
00256 bool TheoryArith::recursiveCanonSimpCheck(const Expr& e)
00257 {
00258   if (e.hasFind()) return true;
00259   if (e != canonSimp(e).getRHS()) return false;
00260   Expr::iterator i = e.begin(), iend = e.end();
00261   for (; i != iend; ++i)
00262     if (!recursiveCanonSimpCheck(*i)) return false;
00263   return true;
00264 }

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