CVC3 2.2
|
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 thm = canonThm(substitutivityRule(e, changed, newChildrenThm)); 00251 return transitivityRule(thm, find(thm.getRHS())); 00252 } 00253 else return find(e); 00254 } 00255 return find(e); 00256 } 00257 00258 00259 bool TheoryArith::recursiveCanonSimpCheck(const Expr& e) 00260 { 00261 if (e.hasFind()) return true; 00262 if (e != canonSimp(e).getRHS()) return false; 00263 Expr::iterator i = e.begin(), iend = e.end(); 00264 for (; i != iend; ++i) 00265 if (!recursiveCanonSimpCheck(*i)) return false; 00266 return true; 00267 } 00268 00269 00270 bool TheoryArith::leavesAreNumConst(const Expr& e) 00271 { 00272 DebugAssert(e.isTerm() || 00273 (e.isPropAtom() && theoryOf(e) == this), 00274 "Expected term or arith prop atom"); 00275 00276 if (e.validTerminalsConstFlag()) { 00277 return e.getTerminalsConstFlag(); 00278 } 00279 00280 if (e.isRational()) { 00281 e.setTerminalsConstFlag(true); 00282 return true; 00283 } 00284 00285 if (e.isAtomic() && isLeaf(e)) { 00286 e.setTerminalsConstFlag(false); 00287 return false; 00288 } 00289 00290 DebugAssert(e.arity() > 0, "Expected non-zero arity"); 00291 int k = 0; 00292 00293 if (e.isITE()) { 00294 k = 1; 00295 } 00296 00297 for (; k < e.arity(); ++k) { 00298 if (!leavesAreNumConst(e[k])) { 00299 e.setTerminalsConstFlag(false); 00300 return false; 00301 } 00302 } 00303 e.setTerminalsConstFlag(true); 00304 return true; 00305 } 00306 00307