CVC3 2.2
|
00001 /*****************************************************************************/ 00002 /*! 00003 * \file translator.cpp 00004 * \brief Description: Code for translation between languages 00005 * 00006 * Author: Clark Barrett 00007 * 00008 * Created: Sat Jun 25 18:06:52 2005 00009 * 00010 * <hr> 00011 * 00012 * License to use, copy, modify, sell and/or distribute this software 00013 * and its documentation for any purpose is hereby granted without 00014 * royalty, subject to the terms and conditions defined in the \ref 00015 * LICENSE file provided with this distribution. 00016 * 00017 * <hr> 00018 * 00019 */ 00020 /*****************************************************************************/ 00021 00022 00023 #include "translator.h" 00024 #include "expr.h" 00025 #include "theory_core.h" 00026 #include "theory_uf.h" 00027 #include "theory_arith.h" 00028 #include "theory_bitvector.h" 00029 #include "theory_array.h" 00030 #include "theory_quant.h" 00031 #include "theory_records.h" 00032 #include "theory_simulate.h" 00033 #include "theory_datatype.h" 00034 #include "theory_datatype_lazy.h" 00035 #include "smtlib_exception.h" 00036 #include "command_line_flags.h" 00037 00038 00039 using namespace std; 00040 using namespace CVC3; 00041 00042 00043 string Translator::fileToSMTLIBIdentifier(const string& filename) 00044 { 00045 string tmpName; 00046 string::size_type pos = filename.rfind("/"); 00047 if (pos == string::npos) { 00048 tmpName = filename; 00049 } 00050 else { 00051 tmpName = filename.substr(pos+1); 00052 } 00053 char c = tmpName[0]; 00054 string res; 00055 if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z')) { 00056 res = "B_"; 00057 } 00058 for (unsigned i = 0; i < tmpName.length(); ++i) { 00059 c = tmpName[i]; 00060 if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z') && 00061 (c < '0' || c > '9') && (c != '.' && c != '_')) { 00062 c = '_'; 00063 } 00064 res += c; 00065 } 00066 return res; 00067 } 00068 00069 00070 Expr Translator::preprocessRec(const Expr& e, ExprMap<Expr>& cache) 00071 { 00072 ExprMap<Expr>::iterator i(cache.find(e)); 00073 if(i != cache.end()) { 00074 return (*i).second; 00075 } 00076 00077 if (e.isClosure()) { 00078 Expr newBody = preprocessRec(e.getBody(), cache); 00079 Expr e2(e); 00080 if (newBody != e.getBody()) { 00081 e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody); 00082 } 00083 d_theoryCore->theoryOf(e2)->setUsed(); 00084 cache[e] = e2; 00085 return e2; 00086 } 00087 00088 Expr e2(e); 00089 vector<Expr> children; 00090 bool diff = false; 00091 00092 for(int k = 0; k < e.arity(); ++k) { 00093 // Recursively preprocess the kids 00094 Expr child = preprocessRec(e[k], cache); 00095 if (child != e[k]) diff = true; 00096 children.push_back(child); 00097 } 00098 if (diff) { 00099 e2 = Expr(e.getOp(), children); 00100 } 00101 00102 Rational r; 00103 switch (e2.getKind()) { 00104 case RATIONAL_EXPR: 00105 if (d_convertToBV) { 00106 Rational r = e2.getRational(); 00107 if (!r.isInteger()) { 00108 FatalAssert(false, "Cannot convert non-integer constant to BV"); 00109 } 00110 Rational limit = pow(d_convertToBV-1, 2); 00111 if (r >= limit) { 00112 FatalAssert(false, "Cannot convert to BV: integer too big"); 00113 } 00114 else if (r < -limit) { 00115 FatalAssert(false, "Cannot convert to BV: integer too small"); 00116 } 00117 e2 = d_theoryBitvector->signed_newBVConstExpr(r, d_convertToBV); 00118 break; 00119 } 00120 00121 case READ: 00122 if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) { 00123 if (e2[1].getKind() != UCONST) break; 00124 map<string, Type>::iterator i = d_arrayConvertMap->find(e2[1].getName()); 00125 if (i == d_arrayConvertMap->end()) { 00126 (*d_arrayConvertMap)[e2[1].getName()] = *d_indexType; 00127 } 00128 else { 00129 if ((*i).second != (*d_indexType)) { 00130 d_unknown = true; 00131 } 00132 } 00133 } 00134 break; 00135 00136 case WRITE: 00137 if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) { 00138 map<string, Type>::iterator i; 00139 if (e2[1].getKind() == UCONST) { 00140 i = d_arrayConvertMap->find(e2[1].getName()); 00141 if (i == d_arrayConvertMap->end()) { 00142 (*d_arrayConvertMap)[e2[1].getName()] = *d_indexType; 00143 } 00144 else { 00145 if ((*i).second != (*d_indexType)) { 00146 d_unknown = true; 00147 break; 00148 } 00149 } 00150 } 00151 if (e2[2].getKind() != UCONST) break; 00152 i = d_arrayConvertMap->find(e2[2].getName()); 00153 if (i == d_arrayConvertMap->end()) { 00154 (*d_arrayConvertMap)[e2[2].getName()] = *d_elementType; 00155 } 00156 else { 00157 if ((*i).second != (*d_elementType)) { 00158 d_unknown = true; 00159 } 00160 } 00161 } 00162 break; 00163 00164 case APPLY: 00165 // Expand lambda applications 00166 if (e2.getOpKind() == LAMBDA) { 00167 Expr lambda(e2.getOpExpr()); 00168 Expr body(lambda.getBody()); 00169 const vector<Expr>& vars = lambda.getVars(); 00170 FatalAssert(vars.size() == (size_t)e2.arity(), 00171 "wrong number of arguments applied to lambda\n"); 00172 body = body.substExpr(vars, e2.getKids()); 00173 e2 = preprocessRec(body, cache); 00174 } 00175 break; 00176 00177 case EQ: 00178 if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType()) 00179 break; 00180 if (d_theoryCore->getFlags()["convert2array"].getBool() && 00181 ((e2[0].getKind() == UCONST && d_arrayConvertMap->find(e2[0].getName()) == d_arrayConvertMap->end()) || 00182 (e2[1].getKind() == UCONST && d_arrayConvertMap->find(e2[1].getName()) == d_arrayConvertMap->end()))) { 00183 d_equalities.push_back(e2); 00184 } 00185 goto arith_rewrites; 00186 00187 case UMINUS: 00188 if (d_convertToBV) { 00189 e2 = Expr(BVUMINUS, e2[0]); 00190 break; 00191 } 00192 if (d_theoryArith->isSyntacticRational(e2, r)) { 00193 e2 = preprocessRec(d_em->newRatExpr(r), cache); 00194 break; 00195 } 00196 goto arith_rewrites; 00197 00198 case DIVIDE: 00199 if (d_convertToBV) { 00200 FatalAssert(false, "Conversion of DIVIDE to BV not implemented yet"); 00201 break; 00202 } 00203 if (d_theoryArith->isSyntacticRational(e2, r)) { 00204 e2 = preprocessRec(d_em->newRatExpr(r), cache); 00205 break; 00206 } 00207 else if (d_convertArith && e2[1].isRational()) { 00208 r = e2[1].getRational(); 00209 if (r != 0) { 00210 e2 = d_em->newRatExpr(1/r) * e2[0]; 00211 e2 = preprocessRec(e2, cache); 00212 break; 00213 } 00214 } 00215 goto arith_rewrites; 00216 00217 case MINUS: 00218 if (d_convertToBV) { 00219 e2 = Expr(BVSUB, e2[0], e2[1]); 00220 break; 00221 } 00222 if (d_convertArith) { 00223 if (e2[0].isRational() && e2[1].isRational()) { 00224 e2 = d_em->newRatExpr(e2[0].getRational() - e2[1].getRational()); 00225 break; 00226 } 00227 } 00228 goto arith_rewrites; 00229 00230 case PLUS: 00231 if (d_convertToBV) { 00232 e2 = Expr(Expr(BVPLUS, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids()); 00233 break; 00234 } 00235 if (d_convertArith) { 00236 // Flatten and combine constants 00237 vector<Expr> terms; 00238 bool changed = false; 00239 int numConst = 0; 00240 r = 0; 00241 Expr::iterator i = e2.begin(), iend = e2.end(); 00242 for(; i!=iend; ++i) { 00243 if ((*i).getKind() == PLUS) { 00244 changed = true; 00245 Expr::iterator i2 = (*i).begin(), i2end = (*i).end(); 00246 for (; i2 != i2end; ++i2) { 00247 if ((*i2).isRational()) { 00248 r += (*i2).getRational(); 00249 numConst++; 00250 } 00251 else terms.push_back(*i2); 00252 } 00253 } 00254 else { 00255 if ((*i).isRational()) { 00256 r += (*i).getRational(); 00257 numConst++; 00258 if (numConst > 1) changed = true; 00259 } 00260 else terms.push_back(*i); 00261 } 00262 } 00263 if (terms.size() == 0) { 00264 e2 = preprocessRec(d_em->newRatExpr(r), cache); 00265 break; 00266 } 00267 else if (terms.size() == 1) { 00268 if (r == 0) { 00269 e2 = terms[0]; 00270 break; 00271 } 00272 else if (r < 0) { 00273 e2 = preprocessRec(Expr(MINUS, terms[0], d_em->newRatExpr(-r)), cache); 00274 break; 00275 } 00276 } 00277 if (changed) { 00278 if (r != 0) terms.push_back(d_em->newRatExpr(r)); 00279 e2 = preprocessRec(Expr(PLUS, terms), cache); 00280 break; 00281 } 00282 } 00283 goto arith_rewrites; 00284 00285 case MULT: 00286 if (d_convertToBV) { 00287 e2 = Expr(Expr(BVMULT, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids()); 00288 break; 00289 } 00290 if (d_convertArith) { 00291 // Flatten and combine constants 00292 vector<Expr> terms; 00293 bool changed = false; 00294 int numConst = 0; 00295 r = 1; 00296 Expr::iterator i = e2.begin(), iend = e2.end(); 00297 for(; i!=iend; ++i) { 00298 if ((*i).getKind() == MULT) { 00299 changed = true; 00300 Expr::iterator i2 = (*i).begin(), i2end = (*i).end(); 00301 for (; i2 != i2end; ++i2) { 00302 if ((*i2).isRational()) { 00303 r *= (*i2).getRational(); 00304 numConst++; 00305 } 00306 else terms.push_back(*i2); 00307 } 00308 } 00309 else { 00310 if ((*i).isRational()) { 00311 r *= (*i).getRational(); 00312 numConst++; 00313 if (numConst > 1) changed = true; 00314 } 00315 else terms.push_back(*i); 00316 } 00317 } 00318 if (r == 0) { 00319 e2 = preprocessRec(d_em->newRatExpr(0), cache); 00320 break; 00321 } 00322 else if (terms.size() == 0) { 00323 e2 = preprocessRec(d_em->newRatExpr(r), cache); 00324 break; 00325 } 00326 else if (terms.size() == 1) { 00327 if (r == 1) { 00328 e2 = terms[0]; 00329 break; 00330 } 00331 } 00332 if (changed) { 00333 if (r != 1) terms.push_back(d_em->newRatExpr(r)); 00334 e2 = preprocessRec(Expr(MULT, terms), cache); 00335 break; 00336 } 00337 } 00338 goto arith_rewrites; 00339 00340 case POW: 00341 if (d_convertToBV) { 00342 FatalAssert(false, "Conversion of POW to BV not implemented"); 00343 break; 00344 } 00345 if (d_convertArith && e2[0].isRational()) { 00346 r = e2[0].getRational(); 00347 if (r.isInteger() && r.getNumerator() == 2) { 00348 e2 = preprocessRec(e2[1] * e2[1], cache); 00349 break; 00350 } 00351 } 00352 // fall through 00353 00354 case LT: 00355 if (d_convertToBV) { 00356 e2 = Expr(BVSLT, e2[0], e2[1]); 00357 break; 00358 } 00359 00360 case GT: 00361 if (d_convertToBV) { 00362 e2 = Expr(BVSLT, e2[1], e2[0]); 00363 break; 00364 } 00365 00366 case LE: 00367 if (d_convertToBV) { 00368 e2 = Expr(BVSLE, e2[0], e2[1]); 00369 break; 00370 } 00371 00372 case GE: 00373 if (d_convertToBV) { 00374 e2 = Expr(BVSLE, e2[1], e2[0]); 00375 break; 00376 } 00377 00378 00379 case INTDIV: 00380 case MOD: 00381 00382 arith_rewrites: 00383 if (d_iteLiftArith) { 00384 diff = false; 00385 children.clear(); 00386 vector<Expr> children2; 00387 Expr cond; 00388 for (int k = 0; k < e2.arity(); ++k) { 00389 if (e2[k].getKind() == ITE && !diff) { 00390 diff = true; 00391 cond = e2[k][0]; 00392 children.push_back(e2[k][1]); 00393 children2.push_back(e2[k][2]); 00394 } 00395 else { 00396 children.push_back(e2[k]); 00397 children2.push_back(e2[k]); 00398 } 00399 } 00400 if (diff) { 00401 Expr thenpart = Expr(e2.getOp(), children); 00402 Expr elsepart = Expr(e2.getOp(), children2); 00403 e2 = cond.iteExpr(thenpart, elsepart); 00404 e2 = preprocessRec(e2, cache); 00405 break; 00406 } 00407 } 00408 00409 if (d_convertToDiff != "" && d_theoryArith->isAtomicArithFormula(e2)) { 00410 Expr e3 = d_theoryArith->rewriteToDiff(e2); 00411 if (e2 != e3) { 00412 DebugAssert(e3 == d_theoryArith->rewriteToDiff(e3), "Expected idempotent rewrite"); 00413 e2 = preprocessRec(e3, cache); 00414 } 00415 break; 00416 } 00417 00418 break; 00419 default: 00420 if (d_convertToBV && isInt(e2.getType())) { 00421 FatalAssert(e2.isVar(), "Cannot convert non-variables yet"); 00422 e2 = d_theoryCore->newVar(e2.getName()+"_bv", d_theoryBitvector->newBitvectorType(d_convertToBV)); 00423 } 00424 00425 break; 00426 } 00427 00428 // Figure out language 00429 switch (e2.getKind()) { 00430 case RATIONAL_EXPR: 00431 r = e2.getRational(); 00432 if (r.isInteger()) { 00433 d_intConstUsed = true; 00434 } 00435 else { 00436 d_realUsed = true; 00437 } 00438 if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY; 00439 break; 00440 case IS_INTEGER: 00441 d_unknown = true; 00442 break; 00443 case PLUS: { 00444 if (e2.arity() == 2) { 00445 int nonconst = 0, isconst = 0; 00446 Expr::iterator i = e2.begin(), iend = e2.end(); 00447 for(; i!=iend; ++i) { 00448 if ((*i).isRational()) { 00449 if ((*i).getRational() <= 0) { 00450 d_UFIDL_ok = false; 00451 break; 00452 } 00453 else ++isconst; 00454 } 00455 else ++nonconst; 00456 } 00457 if (nonconst > 1 || isconst > 1) 00458 d_UFIDL_ok = false; 00459 } 00460 else d_UFIDL_ok = false; 00461 if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY; 00462 break; 00463 } 00464 case MINUS: 00465 if (!e2[1].isRational() || e2[1].getRational() <= 0) { 00466 d_UFIDL_ok = false; 00467 } 00468 if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY; 00469 break; 00470 case UMINUS: 00471 d_UFIDL_ok = false; 00472 if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY; 00473 break; 00474 case MULT: { 00475 d_UFIDL_ok = false; 00476 if (d_langUsed == NONLINEAR) break; 00477 d_langUsed = LINEAR; 00478 bool nonconst = false; 00479 for (int i=0; i!=e2.arity(); ++i) { 00480 if (e2[i].isRational()) continue; 00481 if (nonconst) { 00482 d_langUsed = NONLINEAR; 00483 break; 00484 } 00485 nonconst = true; 00486 } 00487 break; 00488 } 00489 case POW: 00490 case DIVIDE: 00491 d_unknown = true; 00492 break; 00493 00494 case EQ: 00495 if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType() || 00496 (e2[0].getType() == d_theoryArith->intType() && d_theoryCore->getFlags()["convert2array"].getBool())) 00497 break; 00498 case LT: 00499 case GT: 00500 case LE: 00501 case GE: 00502 if (d_langUsed >= LINEAR) break; 00503 if (!d_theoryArith->isAtomicArithFormula(e2)) { 00504 d_langUsed = LINEAR; 00505 break; 00506 } 00507 if (e2[0].getKind() == MINUS && 00508 d_theoryArith->isLeaf(e2[0][0]) && 00509 d_theoryArith->isLeaf(e2[0][1]) && 00510 e2[1].isRational()) { 00511 d_langUsed = DIFF_ONLY; 00512 break; 00513 } 00514 if (d_theoryArith->isLeaf(e2[0]) && 00515 d_theoryArith->isLeaf(e2[1])) { 00516 d_langUsed = DIFF_ONLY; 00517 break; 00518 } 00519 d_langUsed = LINEAR; 00520 break; 00521 default: 00522 break; 00523 } 00524 00525 switch (e2.getKind()) { 00526 case EQ: 00527 case NOT: 00528 break; 00529 case UCONST: 00530 if (e2.arity() == 0) break; 00531 default: 00532 d_theoryCore->theoryOf(e2)->setUsed(); 00533 } 00534 00535 cache[e] = e2; 00536 return e2; 00537 } 00538 00539 00540 Expr Translator::preprocess(const Expr& e, ExprMap<Expr>& cache) 00541 { 00542 Expr result; 00543 try { 00544 result = preprocessRec(e, cache); 00545 } catch (SmtlibException& ex) { 00546 cerr << "Error while processing the formula:\n" 00547 << e.toString() << endl; 00548 throw ex; 00549 } 00550 return result; 00551 } 00552 00553 00554 Expr Translator::preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType) 00555 { 00556 ExprMap<Expr>::iterator i(cache.find(e)); 00557 if(i != cache.end()) { 00558 if ((desiredType.isNull() && 00559 (*i).second.getType() != d_theoryArith->realType()) || 00560 (*i).second.getType() == desiredType) { 00561 return (*i).second; 00562 } 00563 } 00564 00565 if (e.isClosure()) { 00566 Expr newBody = preprocess2Rec(e.getBody(), cache, Type()); 00567 Expr e2(e); 00568 if (newBody != e.getBody()) { 00569 e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody); 00570 } 00571 cache[e] = e2; 00572 return e2; 00573 } 00574 00575 bool forceReal = false; 00576 if (desiredType == d_theoryArith->intType() && 00577 e.getType() != d_theoryArith->intType()) { 00578 d_unknown = true; 00579 // throw SmtlibException("Unable to separate int and real "+ 00580 // e.getType().getExpr().toString()+ 00581 // "\n\nwhile processing the term:\n"+ 00582 // e.toString(PRESENTATION_LANG)); 00583 } 00584 00585 // Try to force type-compliance 00586 switch (e.getKind()) { 00587 case EQ: 00588 case LT: 00589 case GT: 00590 case LE: 00591 case GE: 00592 if (e[0].getType() != e[1].getType()) { 00593 if (e[0].getType() != d_theoryArith->intType() && 00594 e[1].getType() != d_theoryArith->intType()) { 00595 d_unknown = true; 00596 throw SmtlibException("Expected each side to be REAL or INT, but we got lhs: "+ 00597 e[0].getType().getExpr().toString()+" and rhs: "+ 00598 e[1].getType().getExpr().toString()+ 00599 "\n\nwhile processing the term:\n"+ 00600 e.toString()); 00601 } 00602 forceReal = true; 00603 break; 00604 case ITE: 00605 case UMINUS: 00606 case PLUS: 00607 case MINUS: 00608 case MULT: 00609 if (desiredType == d_theoryArith->realType()) 00610 forceReal = true; 00611 break; 00612 case DIVIDE: 00613 forceReal = true; 00614 break; 00615 default: 00616 break; 00617 } 00618 } 00619 00620 Expr e2(e); 00621 vector<Expr> children; 00622 bool diff = false; 00623 00624 Type funType; 00625 if (e.isApply()) { 00626 funType = e.getOpExpr().getType(); 00627 if (funType.getExpr().getKind() == ANY_TYPE) funType = Type(); 00628 } 00629 00630 for(int k = 0; k < e.arity(); ++k) { 00631 Type t; 00632 if (forceReal && e[k].getType() == d_theoryArith->intType()) 00633 t = d_theoryArith->realType(); 00634 else if (!funType.isNull()) t = funType[k]; 00635 // Recursively preprocess the kids 00636 Expr child = preprocess2Rec(e[k], cache, t); 00637 if (child != e[k]) diff = true; 00638 children.push_back(child); 00639 } 00640 if (diff) { 00641 e2 = Expr(e.getOp(), children); 00642 } 00643 else if (e2.getKind() == RATIONAL_EXPR) { 00644 if (e2.getType() == d_theoryArith->realType() || 00645 (e2.getType() == d_theoryArith->intType() && 00646 desiredType == d_theoryArith->realType())) 00647 e2 = Expr(REAL_CONST, e2); 00648 } 00649 if (!desiredType.isNull() && e2.getType() != desiredType) { 00650 d_unknown = true; 00651 throw SmtlibException("Type error: expected "+ 00652 desiredType.getExpr().toString()+ 00653 " but instead got "+ 00654 e2.getType().getExpr().toString()+ 00655 "\n\nwhile processing term:\n"+ 00656 e.toString()); 00657 } 00658 00659 cache[e] = e2; 00660 return e2; 00661 } 00662 00663 00664 Expr Translator::preprocess2(const Expr& e, ExprMap<Expr>& cache) 00665 { 00666 Expr result; 00667 try { 00668 result = preprocess2Rec(e, cache, Type()); 00669 } catch (SmtlibException& ex) { 00670 cerr << "Error while processing the formula:\n" 00671 << e.toString() << endl; 00672 throw ex; 00673 } 00674 return result; 00675 } 00676 00677 00678 00679 00680 bool Translator::containsArray(const Expr& e) 00681 { 00682 if (e.getKind() == ARRAY) return true; 00683 Expr::iterator i = e.begin(), iend=e.end(); 00684 for(; i!=iend; ++i) if (containsArray(*i)) return true; 00685 return false; 00686 } 00687 00688 00689 Translator::Translator(ExprManager* em, 00690 const bool& translate, 00691 const bool& real2int, 00692 const bool& convertArith, 00693 const string& convertToDiff, 00694 bool iteLiftArith, 00695 const string& expResult, 00696 const string& category, 00697 bool convertArray, 00698 bool combineAssump, 00699 int convertToBV) 00700 : d_em(em), d_translate(translate), 00701 d_real2int(real2int), 00702 d_convertArith(convertArith), 00703 d_convertToDiff(convertToDiff), 00704 d_iteLiftArith(iteLiftArith), 00705 d_expResult(expResult), 00706 d_category(category), 00707 d_convertArray(convertArray), 00708 d_combineAssump(combineAssump), 00709 d_dump(false), d_dumpFileOpen(false), 00710 d_intIntArray(false), d_intRealArray(false), d_intIntRealArray(false), 00711 d_ax(false), d_unknown(false), 00712 d_realUsed(false), d_intUsed(false), d_intConstUsed(false), 00713 d_langUsed(NOT_USED), d_UFIDL_ok(true), d_arithUsed(false), 00714 d_zeroVar(NULL), d_convertToBV(convertToBV) 00715 { 00716 d_arrayConvertMap = new map<string, Type>; 00717 } 00718 00719 00720 Translator::~Translator() 00721 { 00722 delete d_arrayConvertMap; 00723 } 00724 00725 00726 bool Translator::start(const string& dumpFile) 00727 { 00728 if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00729 d_dump = true; 00730 if (dumpFile == "") { 00731 d_osdump = &cout; 00732 } 00733 else { 00734 d_osdumpFile.open(dumpFile.c_str()); 00735 if(!d_osdumpFile) 00736 throw Exception("cannot open a log file: "+dumpFile); 00737 else { 00738 d_dumpFileOpen = true; 00739 d_osdump = &d_osdumpFile; 00740 } 00741 } 00742 *d_osdump << 00743 "(benchmark " << fileToSMTLIBIdentifier(dumpFile) << endl << 00744 " :source {" << endl; 00745 string tmpName; 00746 string::size_type pos = dumpFile.rfind("/"); 00747 if (pos == string::npos) { 00748 tmpName = "README"; 00749 } 00750 else { 00751 tmpName = dumpFile.substr(0,pos+1) + "README"; 00752 } 00753 d_tmpFile.open(tmpName.c_str()); 00754 char c; 00755 if (d_tmpFile.is_open()) { 00756 d_tmpFile.get(c); 00757 while (!d_tmpFile.eof()) { 00758 if (c == '{' || c == '}') *d_osdump << '\\'; 00759 *d_osdump << c; 00760 d_tmpFile.get(c); 00761 } 00762 d_tmpFile.close(); 00763 } 00764 else { 00765 *d_osdump << "Source unknown"; 00766 } 00767 *d_osdump << endl;// << 00768 // "This benchmark was automatically translated into SMT-LIB format from" << endl << 00769 // "CVC format using CVC3" << endl; 00770 *d_osdump << "}" << endl; 00771 00772 } 00773 else { 00774 if (dumpFile == "") { 00775 if (d_translate) { 00776 d_osdump = &cout; 00777 d_dump = true; 00778 } 00779 } 00780 else { 00781 d_osdumpFile.open(dumpFile.c_str()); 00782 if(!d_osdumpFile) 00783 throw Exception("cannot open a log file: "+dumpFile); 00784 else { 00785 d_dump = true; 00786 d_dumpFileOpen = true; 00787 d_osdump = &d_osdumpFile; 00788 } 00789 } 00790 } 00791 return d_dump; 00792 } 00793 00794 00795 void Translator::dump(const Expr& e, bool dumpOnly) 00796 { 00797 DebugAssert(d_dump, "dump called unexpectedly"); 00798 if (!dumpOnly || !d_translate) { 00799 if (d_convertArray && e.getKind() == CONST && 00800 e.arity() == 2) { 00801 if (e[1].getKind() == ARRAY) { 00802 if (containsArray(e[1][0]) || 00803 containsArray(e[1][1])) { 00804 throw Exception("convertArray failed because of nested arrays in"+ 00805 e[1].toString()); 00806 } 00807 Expr funType = Expr(ARROW, e[1][0], e[1][1]); 00808 Expr outExpr = Expr(CONST, e[0], funType); 00809 if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00810 d_dumpExprs.push_back(outExpr); 00811 } 00812 else { 00813 *d_osdump << outExpr << endl; 00814 } 00815 } 00816 else if (containsArray(e[1])) { 00817 throw Exception("convertArray failed becauase of use of arrays in"+ 00818 e[1].toString()); 00819 } 00820 else if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00821 d_dumpExprs.push_back(e); 00822 } 00823 else *d_osdump << e << endl; 00824 } 00825 else if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00826 d_dumpExprs.push_back(e); 00827 } 00828 else *d_osdump << e << endl; 00829 } 00830 } 00831 00832 00833 bool Translator::dumpAssertion(const Expr& e) 00834 { 00835 Expr outExpr = Expr(ASSERT, e); 00836 if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00837 d_dumpExprs.push_back(outExpr); 00838 } 00839 else { 00840 *d_osdump << outExpr << endl; 00841 } 00842 return d_translate; 00843 } 00844 00845 00846 bool Translator::dumpQuery(const Expr& e) 00847 { 00848 Expr outExpr = Expr(QUERY, e); 00849 if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00850 d_dumpExprs.push_back(outExpr); 00851 } 00852 else { 00853 *d_osdump << outExpr << endl; 00854 } 00855 return d_translate; 00856 } 00857 00858 00859 void Translator::dumpQueryResult(QueryResult qres) 00860 { 00861 if(d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00862 *d_osdump << " :status "; 00863 switch (qres) { 00864 case UNSATISFIABLE: 00865 *d_osdump << "unsat" << endl; 00866 break; 00867 case SATISFIABLE: 00868 *d_osdump << "sat" << endl; 00869 break; 00870 default: 00871 *d_osdump << "unknown" << endl; 00872 break; 00873 } 00874 } 00875 } 00876 00877 00878 Expr Translator::processType(const Expr& e) 00879 { 00880 switch (e.getKind()) { 00881 case TYPEDECL: 00882 return e; 00883 case INT: 00884 if (d_convertToBV) { 00885 return d_theoryBitvector->newBitvectorType(d_convertToBV).getExpr(); 00886 } 00887 if (d_theoryCore->getFlags()["convert2array"].getBool()) { 00888 return d_elementType->getExpr(); 00889 } 00890 d_intUsed = true; 00891 break; 00892 case REAL: 00893 if (d_real2int) { 00894 d_intUsed = true; 00895 return d_theoryArith->intType().getExpr(); 00896 } 00897 else { 00898 d_realUsed = true; 00899 } 00900 break; 00901 case SUBRANGE: 00902 d_unknown = true; 00903 break; 00904 case ARRAY: 00905 if (d_theoryCore->getFlags()["convert2array"].getBool()) { 00906 d_ax = true; 00907 return d_arrayType->getExpr(); 00908 } 00909 if (e[0].getKind() == TYPEDECL) { 00910 DebugAssert(e[0].arity() == 1, "expected arity 1"); 00911 if (e[0][0].getString() == "Index") { 00912 if (e[1].getKind() == TYPEDECL) { 00913 DebugAssert(e[1].arity() == 1, "expected arity 1"); 00914 if (e[1][0].getString() == "Element") { 00915 d_ax = true; 00916 break; 00917 } 00918 } 00919 } 00920 } 00921 else if (isInt(Type(e[0]))) { 00922 if (isInt(Type(e[1]))) { 00923 d_intIntArray = true; 00924 break; 00925 } 00926 else if (isReal(Type(e[1]))) { 00927 d_intRealArray = true; 00928 break; 00929 } 00930 else if (isArray(Type(e[1])) && 00931 isInt(Type(e[1][0])) && 00932 isReal(Type(e[1][1]))) { 00933 d_intIntRealArray = true; 00934 break; 00935 } 00936 } 00937 else if (e[0].getKind() == BITVECTOR && 00938 e[1].getKind() == BITVECTOR) { 00939 break; 00940 } 00941 d_unknown = true; 00942 break; 00943 default: 00944 break; 00945 } 00946 d_theoryCore->theoryOf(e)->setUsed(); 00947 if (e.arity() == 0) return e; 00948 bool changed = false; 00949 vector<Expr> vec; 00950 for (int i = 0; i < e.arity(); ++i) { 00951 vec.push_back(processType(e[i])); 00952 if (vec.back() != e[i]) changed = true; 00953 } 00954 if (changed) 00955 return Expr(e.getOp(), vec); 00956 return e; 00957 } 00958 00959 00960 void Translator::finish() 00961 { 00962 if (d_translate && d_em->getOutputLang() == SMTLIB_LANG) { 00963 00964 // Print the rest of the preamble for smt-lib benchmarks 00965 00966 // Get status from expResult flag 00967 *d_osdump << " :status "; 00968 if (d_expResult == "invalid" || 00969 d_expResult == "satisfiable") 00970 *d_osdump << "sat"; 00971 else if (d_expResult == "valid" || 00972 d_expResult == "unsatisfiable") 00973 *d_osdump << "unsat"; 00974 else *d_osdump << "unknown"; 00975 *d_osdump << endl; 00976 00977 // difficulty 00978 *d_osdump << " :difficulty { unknown }" << endl; 00979 00980 // category 00981 *d_osdump << " :category { "; 00982 *d_osdump << d_category << " }" << endl; 00983 00984 // Create types for theory QF_AX if needed 00985 if (d_theoryCore->getFlags()["convert2array"].getBool()) { 00986 d_indexType = new Type(d_theoryCore->newTypeExpr("Index")); 00987 d_elementType = new Type(d_theoryCore->newTypeExpr("Element")); 00988 d_arrayType = new Type(arrayType(*d_indexType, *d_elementType)); 00989 } 00990 00991 // Compute logic for smt-lib 00992 bool qf_uf = false; 00993 { 00994 { 00995 ExprMap<Expr> cache; 00996 // Step 1: preprocess asserts, queries, and types 00997 vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end(); 00998 for (; i != iend; ++i) { 00999 Expr e = *i; 01000 switch (e.getKind()) { 01001 case ASSERT: { 01002 Expr e2 = preprocess(e[0], cache); 01003 if (e[0] == e2) break; 01004 e2.getType(); 01005 *i = Expr(ASSERT, e2); 01006 break; 01007 } 01008 case QUERY: { 01009 Expr e2 = preprocess(e[0].negate(), cache); 01010 if (e[0].negate() == e2) break; 01011 e2.getType(); 01012 *i = Expr(QUERY, e2.negate()); 01013 break; 01014 } 01015 case CONST: { 01016 DebugAssert(e.arity() == 2, "Expected CONST with arity 2"); 01017 if (d_theoryCore->getFlags()["convert2array"].getBool()) break; 01018 Expr e2 = processType(e[1]); 01019 if (e[1] == e2) break; 01020 if (d_convertToBV) { 01021 Expr newName = Expr(ID, d_em->newStringExpr(e[0][0].getString()+"_bv")); 01022 *i = Expr(CONST, newName, e2); 01023 } 01024 else { 01025 *i = Expr(CONST, e[0], e2); 01026 } 01027 break; 01028 } 01029 default: 01030 break; 01031 } 01032 } 01033 } 01034 01035 if (d_zeroVar) { 01036 d_dumpExprs.insert(d_dumpExprs.begin(), 01037 Expr(CONST, Expr(ID, d_em->newStringExpr("cvc3Zero")), 01038 processType(d_zeroVar->getType().getExpr()))); 01039 } 01040 01041 // Type inference over equality 01042 if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) { 01043 bool changed; 01044 do { 01045 changed = false; 01046 unsigned i; 01047 for (i = 0; i < d_equalities.size(); ++i) { 01048 if (d_equalities[i][0].getKind() == UCONST && 01049 d_arrayConvertMap->find(d_equalities[i][0].getName()) == d_arrayConvertMap->end()) { 01050 if (d_equalities[i][1].getKind() == READ) { 01051 changed = true; 01052 (*d_arrayConvertMap)[d_equalities[i][0].getName()] = *d_elementType; 01053 } 01054 else if (d_equalities[i][1].getKind() == UCONST) { 01055 map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][1].getName()); 01056 if (it != d_arrayConvertMap->end()) { 01057 changed = true; 01058 (*d_arrayConvertMap)[d_equalities[i][0].getName()] = (*it).second; 01059 } 01060 } 01061 } 01062 else if (d_equalities[i][1].getKind() == UCONST && 01063 d_arrayConvertMap->find(d_equalities[i][1].getName()) == d_arrayConvertMap->end()) { 01064 if (d_equalities[i][0].getKind() == READ) { 01065 changed = true; 01066 (*d_arrayConvertMap)[d_equalities[i][1].getName()] = *d_elementType; 01067 } 01068 else if (d_equalities[i][0].getKind() == UCONST) { 01069 map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][0].getName()); 01070 if (it != d_arrayConvertMap->end()) { 01071 changed = true; 01072 (*d_arrayConvertMap)[d_equalities[i][1].getName()] = (*it).second; 01073 } 01074 } 01075 } 01076 } 01077 } while (changed); 01078 } 01079 01080 // Step 2: If both int and real are used, try to separate them 01081 if ((!d_unknown && (d_intUsed && d_realUsed)) || (d_theoryCore->getFlags()["convert2array"].getBool())) { 01082 ExprMap<Expr> cache; 01083 vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end(); 01084 for (; i != iend; ++i) { 01085 Expr e = *i; 01086 switch (e.getKind()) { 01087 case ASSERT: { 01088 if (d_theoryCore->getFlags()["convert2array"].getBool()) break; 01089 Expr e2 = preprocess2(e[0], cache); 01090 e2.getType(); 01091 *i = Expr(ASSERT, e2); 01092 break; 01093 } 01094 case QUERY: { 01095 if (d_theoryCore->getFlags()["convert2array"].getBool()) break; 01096 Expr e2 = preprocess2(e[0].negate(), cache); 01097 e2.getType(); 01098 *i = Expr(QUERY, e2.negate()); 01099 break; 01100 } 01101 case CONST: { 01102 if (!d_theoryCore->getFlags()["convert2array"].getBool()) break; 01103 map<string, Type>::iterator it = d_arrayConvertMap->find(e[0][0].getString()); 01104 if (it != d_arrayConvertMap->end()) { 01105 *i = Expr(CONST, e[0], (*it).second.getExpr()); 01106 } 01107 else { 01108 Expr e2 = processType(e[1]); 01109 if (e[1] == e2) break; 01110 *i = Expr(CONST, e[0], e2); 01111 } 01112 break; 01113 } 01114 default: 01115 break; 01116 } 01117 } 01118 } 01119 d_arithUsed = d_realUsed || d_intUsed || d_intConstUsed || (d_langUsed != NOT_USED); 01120 01121 // Step 3: Go through the cases and figure out the right logic 01122 *d_osdump << " :logic "; 01123 if (d_unknown || 01124 d_theoryRecords->theoryUsed() || 01125 d_theorySimulate->theoryUsed() || 01126 d_theoryDatatype->theoryUsed()) { 01127 *d_osdump << "unknown"; 01128 } 01129 else { 01130 if ((d_ax && (d_arithUsed || 01131 d_theoryBitvector->theoryUsed() || 01132 d_theoryUF->theoryUsed())) || 01133 (d_intIntArray && d_realUsed) || 01134 (d_arithUsed && d_theoryBitvector->theoryUsed())) { 01135 *d_osdump << "unknown"; 01136 } 01137 else { 01138 bool QF = false; 01139 bool A = false; 01140 bool UF = false; 01141 01142 if (!d_theoryQuant->theoryUsed()) { 01143 QF = true; 01144 *d_osdump << "QF_"; 01145 } 01146 01147 if (d_theoryArray->theoryUsed() && !d_convertArray) { 01148 A = true; 01149 *d_osdump << "A"; 01150 } 01151 01152 // Promote undefined subset logics 01153 // else if (!QF && !d_theoryBitvector->theoryUsed()) { 01154 // A = true; 01155 // *d_osdump << "A"; 01156 // } 01157 01158 if (d_theoryUF->theoryUsed() || 01159 (d_theoryArray->theoryUsed() && d_convertArray)) { 01160 UF = true; 01161 *d_osdump << "UF"; 01162 } 01163 01164 // Promote undefined subset logics 01165 // else if (!QF && 01166 // !d_theoryBitvector->theoryUsed()) { 01167 // UF = true; 01168 // *d_osdump << "UF"; 01169 // } 01170 01171 if (d_arithUsed) { 01172 if (d_intUsed && d_realUsed) { 01173 if (d_langUsed < NONLINEAR) { 01174 *d_osdump << "LIRA"; 01175 } 01176 else *d_osdump << "NIRA"; 01177 } 01178 else if (d_realUsed) { 01179 if (d_langUsed <= DIFF_ONLY) { 01180 01181 // Promote undefined subset logics 01182 // if (!QF) { 01183 // *d_osdump << "LIRA"; 01184 // } else 01185 01186 *d_osdump << "RDL"; 01187 } 01188 else if (d_langUsed <= LINEAR) { 01189 01190 // Promote undefined subset logics 01191 // if (!QF) { 01192 // *d_osdump << "LIRA"; 01193 // } else 01194 01195 *d_osdump << "LRA"; 01196 } 01197 else { 01198 01199 // Promote undefined subset logics 01200 // if (!QF) { 01201 // *d_osdump << "NIRA"; 01202 // } else 01203 01204 *d_osdump << "NRA"; 01205 } 01206 } 01207 else { 01208 if (QF && !A && UF && d_langUsed <= LINEAR) { 01209 if (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok) { 01210 *d_osdump << "IDL"; 01211 } 01212 else { 01213 *d_osdump << "LIA"; 01214 } 01215 } 01216 else if (d_langUsed <= DIFF_ONLY) { 01217 01218 // Promote undefined subset logics 01219 if (!QF) { 01220 *d_osdump << "LIA"; 01221 } 01222 else if (A) { 01223 if (!UF) { 01224 UF = true; 01225 *d_osdump << "UF"; 01226 } 01227 *d_osdump << "LIA"; 01228 } else 01229 01230 *d_osdump << "IDL"; 01231 } 01232 else if (d_langUsed <= LINEAR) { 01233 01234 // Promote undefined subset logics 01235 // if (QF && A && !UF) { 01236 // UF = true; 01237 // *d_osdump << "UF"; 01238 // } 01239 01240 if (QF && !A && (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok)) { 01241 *d_osdump << "UFIDL"; 01242 } 01243 else { 01244 *d_osdump << "LIA"; 01245 } 01246 } 01247 else { 01248 01249 // Promote undefined subset logics 01250 // if (!QF) { 01251 // *d_osdump << "NIRA"; 01252 // } else 01253 01254 *d_osdump << "NIA"; 01255 } 01256 } 01257 } 01258 else if (d_theoryBitvector->theoryUsed()) { 01259 01260 // Promote undefined subset logics 01261 if (A && QF && !UF) { 01262 UF = true; 01263 *d_osdump << "UF"; 01264 } 01265 01266 *d_osdump << "BV";//[" << d_theoryBitvector->getMaxSize() << "]"; 01267 } 01268 else { 01269 01270 if (d_ax) { 01271 *d_osdump << "X"; 01272 } 01273 01274 // Promote undefined subset logics 01275 else if (!QF || (A && UF)) { 01276 *d_osdump << "LIA"; 01277 } else { 01278 01279 // Default logic 01280 if (!A && !UF) { 01281 UF = true; 01282 *d_osdump << "UF"; 01283 } 01284 qf_uf = QF && UF && (!A); 01285 } 01286 } 01287 } 01288 } 01289 } 01290 *d_osdump << endl; 01291 01292 // Dump the actual expressions 01293 01294 vector<Expr>::const_iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end(); 01295 vector<Expr> assumps; 01296 for (; i != iend; ++i) { 01297 Expr e = *i; 01298 switch (e.getKind()) { 01299 case ASSERT: { 01300 if (d_combineAssump) { 01301 assumps.push_back(e[0]); 01302 } 01303 else { 01304 *d_osdump << " :assumption" << endl; 01305 *d_osdump << e[0] << endl; 01306 } 01307 break; 01308 } 01309 case QUERY: { 01310 *d_osdump << " :formula" << endl; 01311 if (!assumps.empty()) { 01312 assumps.push_back(e[0].negate()); 01313 e = Expr(AND, assumps); 01314 *d_osdump << e << endl; 01315 } 01316 else { 01317 *d_osdump << e[0].negate() << endl; 01318 } 01319 break; 01320 } 01321 default: 01322 if (qf_uf && e.getKind() == TYPE && e[0].getKind() == RAW_LIST && 01323 e[0][0].getKind() == ID && e[0][0][0].getKind() == STRING_EXPR && 01324 e[0][0][0].getString() == "U") 01325 break; 01326 *d_osdump << e << endl; 01327 break; 01328 } 01329 } 01330 *d_osdump << ")" << endl; 01331 } 01332 01333 if (d_dumpFileOpen) d_osdumpFile.close(); 01334 if (d_zeroVar) delete d_zeroVar; 01335 } 01336 01337 01338 const string Translator::fixConstName(const string& s) 01339 { 01340 if (d_em->getOutputLang() == SMTLIB_LANG) { 01341 if (s[0] == '_') { 01342 return "smt"+s; 01343 } 01344 } 01345 return s; 01346 } 01347 01348 01349 bool Translator::printArrayExpr(ExprStream& os, const Expr& e) 01350 { 01351 if (e.getKind() == ARRAY) { 01352 if (d_convertArray) { 01353 os << Expr(ARROW, e[0], e[1]); 01354 return true; 01355 } 01356 if (d_em->getOutputLang() != SMTLIB_LANG) return false; 01357 if (e[0].getKind() == TYPEDECL) { 01358 DebugAssert(e[0].arity() == 1, "expected arity 1"); 01359 if (e[0][0].getString() == "Index") { 01360 if (e[1].getKind() == TYPEDECL) { 01361 DebugAssert(e[1].arity() == 1, "expected arity 1"); 01362 if (e[1][0].getString() == "Element") { 01363 os << "Array"; 01364 return true; 01365 } 01366 } 01367 } 01368 } 01369 else if (isInt(Type(e[0]))) { 01370 if (isInt(Type(e[1]))) { 01371 d_intIntArray = true; 01372 os << "Array"; 01373 return true; 01374 } 01375 else if (isReal(Type(e[1]))) { 01376 d_intRealArray = true; 01377 os << "Array1"; 01378 return true; 01379 } 01380 else if (isArray(Type(e[1])) && 01381 isInt(Type(e[1][0])) && 01382 isReal(Type(e[1][1]))) { 01383 d_intIntRealArray = true; 01384 os << "Array2"; 01385 return true; 01386 } 01387 } 01388 else if (e[0].getKind() == BITVECTOR && 01389 e[1].getKind() == BITVECTOR) { 01390 os << "Array["; 01391 os << d_theoryBitvector->getBitvectorTypeParam(Type(e[0])); 01392 os << ":"; 01393 os << d_theoryBitvector->getBitvectorTypeParam(Type(e[1])); 01394 os << "]"; 01395 return true; 01396 } 01397 os << "UnknownArray"; 01398 d_unknown = true; 01399 return true; 01400 } 01401 01402 switch (e.getKind()) { 01403 case READ: 01404 if (d_convertArray) { 01405 if (e[0].getKind() == UCONST) { 01406 os << Expr(d_em->newSymbolExpr(e[0].getName(), UFUNC).mkOp(), e[1]); 01407 return true; 01408 } 01409 else if (e[0].getKind() == WRITE) { 01410 throw Exception("READ of WRITE not implemented yet for convertArray"); 01411 } 01412 else { 01413 throw Exception("Unexpected case for convertArray"); 01414 } 01415 } 01416 break; 01417 case WRITE: 01418 if (d_convertArray) { 01419 throw Exception("WRITE expression encountered while attempting " 01420 "to convert arrays to uninterpreted functions"); 01421 } 01422 break; 01423 case ARRAY_LITERAL: 01424 if (d_convertArray) { 01425 throw Exception("ARRAY_LITERAL expression encountered while attempting" 01426 " to convert arrays to uninterpreted functions"); 01427 } 01428 break; 01429 default: 01430 throw Exception("Unexpected case in printArrayExpr"); 01431 break; 01432 } 01433 return false; 01434 } 01435 01436 01437 Expr Translator::zeroVar() 01438 { 01439 if (!d_zeroVar) { 01440 d_zeroVar = new Expr(); 01441 if (d_convertToDiff == "int") { 01442 *d_zeroVar = d_theoryCore->newVar("cvc3Zero", d_theoryArith->intType().getExpr()); 01443 } 01444 else if (d_convertToDiff == "real") { 01445 *d_zeroVar = d_theoryCore->newVar("cvc3Zero", d_theoryArith->realType().getExpr()); 01446 } 01447 } 01448 return *d_zeroVar; 01449 }