CVC3

translator.cpp

Go to the documentation of this file.
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 <cctype>
00024 
00025 #include "translator.h"
00026 #include "expr.h"
00027 #include "theory_core.h"
00028 #include "theory_uf.h"
00029 #include "theory_arith.h"
00030 #include "theory_bitvector.h"
00031 #include "theory_array.h"
00032 #include "theory_quant.h"
00033 #include "theory_records.h"
00034 #include "theory_simulate.h"
00035 #include "theory_datatype.h"
00036 #include "theory_datatype_lazy.h"
00037 #include "smtlib_exception.h"
00038 #include "command_line_flags.h"
00039 
00040 
00041 using namespace std;
00042 using namespace CVC3;
00043 
00044 
00045 string Translator::fileToSMTLIBIdentifier(const string& filename)
00046 {
00047   string tmpName;
00048   string::size_type pos = filename.rfind("/");
00049   if (pos == string::npos) {
00050     tmpName = filename;
00051   }
00052   else {
00053     tmpName = filename.substr(pos+1);
00054   }
00055   char c = tmpName[0];
00056   string res;
00057   if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z')) {
00058     res = "B_";
00059   }
00060   for (unsigned i = 0; i < tmpName.length(); ++i) {
00061     c = tmpName[i];
00062     if ((c < 'A' || c > 'Z') && (c < 'a' || c > 'z') &&
00063         (c < '0' || c > '9') && (c != '.' && c != '_')) {
00064       c = '_';
00065     }
00066     res += c;
00067   }
00068   return res;
00069 }
00070 
00071 
00072 Expr Translator::preprocessRec(const Expr& e, ExprMap<Expr>& cache)
00073 {
00074   ExprMap<Expr>::iterator i(cache.find(e));
00075   if(i != cache.end()) {
00076     return (*i).second;
00077   }
00078 
00079   if (d_theoryCore->getFlags()["liftITE"].getBool() &&
00080       e.isPropAtom() && e.containsTermITE()) {
00081     Theorem thm = d_theoryCore->getCommonRules()->liftOneITE(e);
00082     return preprocessRec(thm.getRHS(), cache);
00083   }
00084 
00085   if (e.isClosure()) {
00086     Expr newBody = preprocessRec(e.getBody(), cache);
00087     Expr e2(e);
00088     if (newBody != e.getBody()) {
00089       e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody);
00090     }
00091     d_theoryCore->theoryOf(e2)->setUsed();
00092     cache[e] = e2;
00093     return e2;
00094   }
00095 
00096   Expr e2(e);
00097   vector<Expr> children;
00098   bool diff = false;
00099 
00100   for(int k = 0; k < e.arity(); ++k) {
00101     // Recursively preprocess the kids
00102     Expr child = preprocessRec(e[k], cache);
00103     if (child != e[k]) diff = true;
00104     children.push_back(child);
00105   }
00106   if (diff) {
00107     e2 = Expr(e.getOp(), children);
00108   }
00109 
00110   Rational r;
00111   switch (e2.getKind()) {
00112     case RATIONAL_EXPR:
00113       if (d_convertToBV) {
00114         Rational r = e2.getRational();
00115         if (!r.isInteger()) {
00116           FatalAssert(false, "Cannot convert non-integer constant to BV");
00117         }
00118         Rational limit = pow(d_convertToBV-1, (Rational)2);
00119         if (r >= limit) {
00120           FatalAssert(false, "Cannot convert to BV: integer too big");
00121         }
00122         else if (r < -limit) {
00123           FatalAssert(false, "Cannot convert to BV: integer too small");
00124         }
00125         e2 = d_theoryBitvector->signed_newBVConstExpr(r, d_convertToBV);
00126         break;
00127       }
00128 
00129     case READ:
00130       if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) {
00131         if (e2[1].getKind() != UCONST) break;
00132         map<string, Type>::iterator i = d_arrayConvertMap->find(e2[1].getName());
00133         if (i == d_arrayConvertMap->end()) {
00134           (*d_arrayConvertMap)[e2[1].getName()] = *d_indexType;
00135         }
00136         else {
00137           if ((*i).second != (*d_indexType)) {
00138             d_unknown = true;
00139           }
00140         }
00141       }
00142       break;
00143 
00144     case WRITE:
00145       if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) {
00146         map<string, Type>::iterator i;
00147         if (e2[1].getKind() == UCONST) {
00148           i = d_arrayConvertMap->find(e2[1].getName());
00149           if (i == d_arrayConvertMap->end()) {
00150             (*d_arrayConvertMap)[e2[1].getName()] = *d_indexType;
00151           }
00152           else {
00153             if ((*i).second != (*d_indexType)) {
00154               d_unknown = true;
00155               break;
00156             }
00157           }
00158         }
00159         if (e2[2].getKind() != UCONST) break;
00160         i = d_arrayConvertMap->find(e2[2].getName());
00161         if (i == d_arrayConvertMap->end()) {
00162           (*d_arrayConvertMap)[e2[2].getName()] = *d_elementType;
00163         }
00164         else {
00165           if ((*i).second != (*d_elementType)) {
00166             d_unknown = true;
00167           }
00168         }
00169       }
00170       break;
00171 
00172     case APPLY:
00173       // Expand lambda applications
00174       if (e2.getOpKind() == LAMBDA) {
00175         Expr lambda(e2.getOpExpr());
00176         Expr body(lambda.getBody());
00177         const vector<Expr>& vars = lambda.getVars();
00178         FatalAssert(vars.size() == (size_t)e2.arity(),
00179                     "wrong number of arguments applied to lambda\n");
00180         body = body.substExpr(vars, e2.getKids());
00181         e2 = preprocessRec(body, cache);
00182       }
00183       break;
00184 
00185     case EQ:
00186       if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType())
00187         break;
00188       if (d_theoryCore->getFlags()["convert2array"].getBool() &&
00189           ((e2[0].getKind() == UCONST && d_arrayConvertMap->find(e2[0].getName()) == d_arrayConvertMap->end()) ||
00190           (e2[1].getKind() == UCONST && d_arrayConvertMap->find(e2[1].getName()) == d_arrayConvertMap->end()))) {
00191         d_equalities.push_back(e2);
00192       }
00193       goto arith_rewrites;
00194 
00195     case UMINUS:
00196       if (d_convertToBV) {
00197         e2 = Expr(BVUMINUS, e2[0]);
00198         break;
00199       }
00200       if (d_theoryArith->isSyntacticRational(e2, r)) {
00201         e2 = preprocessRec(d_em->newRatExpr(r), cache);
00202         break;
00203       }
00204       goto arith_rewrites;
00205 
00206     case DIVIDE:
00207       if (d_convertToBV) {
00208         FatalAssert(false, "Conversion of DIVIDE to BV not implemented yet");
00209         break;
00210       }
00211       if (d_theoryArith->isSyntacticRational(e2, r)) {
00212         e2 = preprocessRec(d_em->newRatExpr(r), cache);
00213         break;
00214       }
00215       else if (d_convertArith && e2[1].isRational()) {
00216         r = e2[1].getRational();
00217         if (r != 0) {
00218           e2 = d_em->newRatExpr(1/r) * e2[0];
00219           e2 = preprocessRec(e2, cache);
00220           break;
00221         }
00222       }
00223       goto arith_rewrites;
00224 
00225     case MINUS:
00226       if (d_convertToBV) {
00227         e2 = Expr(BVSUB, e2[0], e2[1]);
00228         break;
00229       }
00230       if (d_convertArith) {
00231         if (e2[0].isRational() && e2[1].isRational()) {
00232           e2 = d_em->newRatExpr(e2[0].getRational() - e2[1].getRational());
00233           break;
00234         }
00235       }
00236       goto arith_rewrites;
00237 
00238     case PLUS:
00239       if (d_convertToBV) {
00240         e2 = Expr(Expr(BVPLUS, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids());
00241         break;
00242       }
00243       if (d_convertArith) {
00244         // Flatten and combine constants
00245         vector<Expr> terms;
00246         bool changed = false;
00247         int numConst = 0;
00248         r = 0;
00249         Expr::iterator i = e2.begin(), iend = e2.end();
00250         for(; i!=iend; ++i) {
00251           if ((*i).getKind() == PLUS) {
00252             changed = true;
00253             Expr::iterator i2 = (*i).begin(), i2end = (*i).end();
00254             for (; i2 != i2end; ++i2) {
00255               if ((*i2).isRational()) {
00256                 r += (*i2).getRational();
00257                 numConst++;
00258               }
00259               else terms.push_back(*i2);
00260             }
00261           }
00262           else {
00263             if ((*i).isRational()) {
00264               r += (*i).getRational();
00265               numConst++;
00266               if (numConst > 1) changed = true;
00267             }
00268             else terms.push_back(*i);
00269           }
00270         }
00271         if (terms.size() == 0) {
00272           e2 = preprocessRec(d_em->newRatExpr(r), cache);
00273           break;
00274         }
00275         else if (terms.size() == 1) {
00276           if (r == 0) {
00277             e2 = terms[0];
00278             break;
00279           }
00280           else if (r < 0) {
00281             e2 = preprocessRec(Expr(MINUS, terms[0], d_em->newRatExpr(-r)), cache);
00282             break;
00283           }
00284         }
00285         if (changed) {
00286           if (r != 0) terms.push_back(d_em->newRatExpr(r));
00287           e2 = preprocessRec(Expr(PLUS, terms), cache);
00288           break;
00289         }
00290       }
00291       goto arith_rewrites;
00292 
00293     case MULT:
00294       if (d_convertToBV) {
00295         e2 = Expr(Expr(BVMULT, d_em->newRatExpr(d_convertToBV)).mkOp(), e2.getKids());
00296         break;
00297       }
00298       if (d_convertArith) {
00299         // Flatten and combine constants
00300         vector<Expr> terms;
00301         bool changed = false;
00302         int numConst = 0;
00303         r = 1;
00304         Expr::iterator i = e2.begin(), iend = e2.end();
00305         for(; i!=iend; ++i) {
00306           if ((*i).getKind() == MULT) {
00307             changed = true;
00308             Expr::iterator i2 = (*i).begin(), i2end = (*i).end();
00309             for (; i2 != i2end; ++i2) {
00310               if ((*i2).isRational()) {
00311                 r *= (*i2).getRational();
00312                 numConst++;
00313               }
00314               else terms.push_back(*i2);
00315             }
00316           }
00317           else {
00318             if ((*i).isRational()) {
00319               r *= (*i).getRational();
00320               numConst++;
00321               if (numConst > 1) changed = true;
00322             }
00323             else terms.push_back(*i);
00324           }
00325         }
00326         if (r == 0) {
00327           e2 = preprocessRec(d_em->newRatExpr(0), cache);
00328           break;
00329         }
00330         else if (terms.size() == 0) {
00331           e2 = preprocessRec(d_em->newRatExpr(r), cache);
00332           break;
00333         }
00334         else if (terms.size() == 1) {
00335           if (r == 1) {
00336             e2 = terms[0];
00337             break;
00338           }
00339         }
00340         if (changed) {
00341           if (r != 1) terms.push_back(d_em->newRatExpr(r));
00342           e2 = preprocessRec(Expr(MULT, terms), cache);
00343           break;
00344         }
00345       }
00346       goto arith_rewrites;
00347 
00348     case POW:
00349       if (d_convertToBV) {
00350         FatalAssert(false, "Conversion of POW to BV not implemented");
00351         break;
00352       }
00353       if (d_convertArith && e2[0].isRational()) {
00354         r = e2[0].getRational();
00355         if (r.isInteger() && r.getNumerator() == 2) {
00356           e2 = preprocessRec(e2[1] * e2[1], cache);
00357           break;
00358         }
00359       }
00360       // fall through
00361 
00362     case LT:
00363       if (d_convertToBV) {
00364         e2 = Expr(BVSLT, e2[0], e2[1]);
00365         break;
00366       }
00367 
00368     case GT:
00369       if (d_convertToBV) {
00370         e2 = Expr(BVSLT, e2[1], e2[0]);
00371         break;
00372       }
00373 
00374     case LE:
00375       if (d_convertToBV) {
00376         e2 = Expr(BVSLE, e2[0], e2[1]);
00377         break;
00378       }
00379 
00380     case GE:
00381       if (d_convertToBV) {
00382         e2 = Expr(BVSLE, e2[1], e2[0]);
00383         break;
00384       }
00385       
00386 
00387     case INTDIV:
00388     case MOD:
00389 
00390   arith_rewrites:
00391       if (d_iteLiftArith) {
00392         diff = false;
00393         children.clear();
00394         vector<Expr> children2;
00395         Expr cond;
00396         for (int k = 0; k < e2.arity(); ++k) {
00397           if (e2[k].getKind() == ITE && !diff) {
00398             diff = true;
00399             cond = e2[k][0];
00400             children.push_back(e2[k][1]);
00401             children2.push_back(e2[k][2]);
00402           }
00403           else {
00404             children.push_back(e2[k]);
00405             children2.push_back(e2[k]);
00406           }
00407         }
00408         if (diff) {
00409           Expr thenpart = Expr(e2.getOp(), children);
00410           Expr elsepart = Expr(e2.getOp(), children2);
00411           e2 = cond.iteExpr(thenpart, elsepart);
00412           e2 = preprocessRec(e2, cache);
00413           break;
00414         }
00415       }
00416 
00417       if (d_convertToDiff != "" && d_theoryArith->isAtomicArithFormula(e2)) {
00418         Expr e3 = d_theoryArith->rewriteToDiff(e2);
00419         if (e2 != e3) {
00420           DebugAssert(e3 == d_theoryArith->rewriteToDiff(e3), "Expected idempotent rewrite");
00421           e2 = preprocessRec(e3, cache);
00422         }
00423         break;
00424       }
00425 
00426       break;
00427     default:
00428       if (d_convertToBV && isInt(e2.getType())) {
00429         FatalAssert(e2.isVar(), "Cannot convert non-variables yet");
00430         e2 = d_theoryCore->newVar(e2.getName()+"_bv", d_theoryBitvector->newBitvectorType(d_convertToBV));
00431       }
00432 
00433       break;
00434   }
00435 
00436   // Figure out language
00437   switch (e2.getKind()) {
00438     case RATIONAL_EXPR:
00439       r = e2.getRational();
00440       if (r.isInteger()) {
00441         d_intConstUsed = true;
00442       }
00443       else {
00444         d_realUsed = true;
00445       }
00446       if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
00447       break;
00448     case IS_INTEGER:
00449       d_realUsed = true;
00450       d_intUsed = true;
00451       break;
00452     case PLUS: {
00453       if (e2.arity() == 2) {
00454         int nonconst = 0, isconst = 0;
00455         Expr::iterator i = e2.begin(), iend = e2.end();
00456         for(; i!=iend; ++i) {
00457           if ((*i).isRational()) {
00458             if ((*i).getRational() <= 0) {
00459               d_UFIDL_ok = false;
00460               break;
00461             }
00462             else ++isconst;
00463           }
00464           else ++nonconst;
00465         }
00466         if (nonconst > 1 || isconst > 1)
00467           d_UFIDL_ok = false;
00468       }
00469       else d_UFIDL_ok = false;
00470       if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
00471       break;
00472     }
00473     case MINUS:
00474       if (!e2[1].isRational() || e2[1].getRational() <= 0) {
00475         d_UFIDL_ok = false;
00476       }
00477       if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
00478       break;
00479     case UMINUS:
00480       d_UFIDL_ok = false;
00481       if (d_langUsed == NOT_USED) d_langUsed = TERMS_ONLY;
00482       break;
00483     case MULT: {
00484       d_UFIDL_ok = false;
00485       if (d_langUsed == NONLINEAR) break;
00486       d_langUsed = LINEAR;
00487       bool nonconst = false;
00488       for (int i=0; i!=e2.arity(); ++i) {
00489         if (e2[i].isRational()) continue;
00490         if (nonconst) {
00491           d_langUsed = NONLINEAR;
00492           break;
00493         }
00494         nonconst = true;
00495       }
00496       break;
00497     }
00498     case POW:
00499     case DIVIDE:
00500       d_unknown = true;
00501       break;
00502 
00503     case EQ:
00504       if (d_theoryArith->getBaseType(e2[0]) != d_theoryArith->realType() ||
00505           (e2[0].getType() == d_theoryArith->intType() && d_theoryCore->getFlags()["convert2array"].getBool()))
00506         break;
00507     case LT:
00508     case GT:
00509     case LE:
00510     case GE:
00511       if (d_langUsed >= LINEAR) break;
00512       if (!d_theoryArith->isAtomicArithFormula(e2)) {
00513         d_langUsed = LINEAR;
00514         break;
00515       }
00516       if (e2[0].getKind() == MINUS &&
00517           d_theoryArith->isLeaf(e2[0][0]) &&
00518           d_theoryArith->isLeaf(e2[0][1]) &&
00519           e2[1].isRational()) {
00520         d_langUsed = DIFF_ONLY;
00521         break;
00522       }
00523       if (d_theoryArith->isLeaf(e2[0]) &&
00524           d_theoryArith->isLeaf(e2[1])) {
00525         d_langUsed = DIFF_ONLY;
00526         break;
00527       }
00528       d_langUsed = LINEAR;
00529       break;
00530     default:
00531       break;
00532   }
00533 
00534   switch (e2.getKind()) {
00535     case EQ:
00536     case NOT:
00537       break;
00538     case UCONST:
00539       if (e2.arity() == 0) break;
00540     default:
00541       d_theoryCore->theoryOf(e2)->setUsed();
00542   }
00543 
00544   cache[e] = e2;
00545   return e2;
00546 }
00547 
00548 
00549 Expr Translator::preprocess(const Expr& e, ExprMap<Expr>& cache)
00550 {
00551   Expr result;
00552   try {
00553     result = preprocessRec(e, cache);
00554   } catch (SmtlibException& ex) {
00555     cerr << "Error while processing the formula:\n"
00556          << e.toString() << endl;
00557     throw ex;
00558   }
00559   return result;
00560 }
00561 
00562 
00563 Expr Translator::preprocess2Rec(const Expr& e, ExprMap<Expr>& cache, Type desiredType)
00564 {
00565   TRACE("smtlib2-linear", "preprocess2Rec: ", e, "");
00566   ExprMap<Expr>::iterator i(cache.find(e));
00567   if(i != cache.end()) {
00568     if ((desiredType.isNull() &&
00569          (*i).second.getType() != d_theoryArith->realType()) ||
00570         (*i).second.getType() == desiredType) {
00571       return (*i).second;
00572     }
00573   }
00574 
00575   if (e.isClosure()) {
00576     Expr newBody = preprocess2Rec(e.getBody(), cache, Type());
00577     Expr e2(e);
00578     if (newBody != e.getBody()) {
00579       e2 = d_em->newClosureExpr(e.getKind(), e.getVars(), newBody);
00580     }
00581     cache[e] = e2;
00582     return e2;
00583   }
00584 
00585   bool forceReal = false;
00586   if (desiredType == d_theoryArith->intType() &&
00587       e.getType() != d_theoryArith->intType()) {
00588     d_unknown = true;
00589 //     throw SmtlibException("Unable to separate int and real "+
00590 //                           e.getType().getExpr().toString()+
00591 //                           "\n\nwhile processing the term:\n"+
00592 //                           e.toString(PRESENTATION_LANG));
00593   }
00594 
00595   // Try to force type-compliance
00596   switch (e.getKind()) {
00597     case EQ:
00598     case LT:
00599     case GT:
00600     case LE:
00601     case GE:
00602       if (e[0].getType() != e[1].getType()) {
00603         if (e[0].getType() != d_theoryArith->intType() &&
00604             e[1].getType() != d_theoryArith->intType()) {
00605           d_unknown = true;
00606           throw SmtlibException("Expected each side to be REAL or INT, but we got lhs: "+
00607                                 e[0].getType().getExpr().toString()+" and rhs: "+
00608                                 e[1].getType().getExpr().toString()+
00609                                 "\n\nwhile processing the term:\n"+
00610                                 e.toString());
00611         }
00612         forceReal = true;
00613         break;
00614       case ITE:
00615       case UMINUS:
00616       case PLUS:
00617       case MINUS:
00618       case MULT:
00619         if (desiredType == d_theoryArith->realType())
00620           forceReal = true;
00621         break;
00622       case DIVIDE:
00623         forceReal = true;
00624         break;
00625       default:
00626         break;
00627     }
00628   }
00629 
00630   Expr e2(e);
00631   vector<Expr> children;
00632   bool diff = false;
00633 
00634   Type funType;
00635   if (e.isApply()) {
00636     funType = e.getOpExpr().getType();
00637     if (funType.getExpr().getKind() == ANY_TYPE) funType = Type();
00638   }
00639   else if (e.getKind() == WRITE) {
00640     // an array store is like a function ARRAY -> INDEX -> ELEMENT -> ARRAY
00641     vector<Type> kids;
00642     kids.push_back(e.getType());
00643     kids.push_back(e.getType()[0]);
00644     kids.push_back(e.getType()[1]);
00645     funType = Type::funType(kids, e.getType());
00646   }
00647 
00648   for(int k = 0; k < e.arity(); ++k) {
00649     Type t;
00650     if (forceReal && e[k].getType() == d_theoryArith->intType())
00651       t = d_theoryArith->realType();
00652     else if (!funType.isNull()) t = funType[k];
00653     // Recursively preprocess the kids
00654     Expr child = preprocess2Rec(e[k], cache, t);
00655     if (child != e[k]) diff = true;
00656     children.push_back(child);
00657   }
00658   if (diff) {
00659     e2 = Expr(e.getOp(), children);
00660   }
00661   else if (e2.getKind() == RATIONAL_EXPR && d_realUsed && d_intUsed) {
00662     if (e2.getType() == d_theoryArith->realType() ||
00663         (e2.getType() == d_theoryArith->intType() &&
00664          desiredType == d_theoryArith->realType()))
00665       e2 = Expr(REAL_CONST, e2);
00666   }
00667   if (e2.getKind() == MULT) {
00668     // SMT-LIBv2 is strict about where * is permitted in linear logics
00669     if (d_langUsed > NOT_USED && d_langUsed <= LINEAR &&
00670         d_em->getOutputLang() == SMTLIB_V2_LANG) {
00671       Expr e2save = e2;
00672       TRACE("smtlib2-linear", "SMT-LIBv2 linearizing: ", e2save, "");
00673       FatalAssert(e2.arity() > 1, "Unary MULT not permitted here");
00674       // combine constants to form a linear term
00675       Expr trm;// the singular, non-constant term in the MULT
00676       Rational constCoef = 1;// constant coefficient
00677       bool realConst = false;
00678       bool trmFirst = false;
00679       for(int i = 0; i < e2.arity(); ++i) {
00680         Expr x = e2[i];
00681         if(x.getKind() == REAL_CONST) {
00682           x = x[0];
00683           realConst = true;
00684           DebugAssert(x.isRational(), "unexpected REAL_CONST-wrapped kind");
00685         }
00686         if(x.isRational()) {
00687           constCoef *= x.getRational();
00688         } else {
00689           FatalAssert(trm.isNull(), "translating with LINEAR restriction, but found > 1 non-constant under MULT");
00690           trm = x;
00691           trmFirst = (i == 0);
00692         }
00693       }
00694 
00695       // First, do no harm: if it was a binary MULT already in correct shape
00696       // for SMT-LIBv2 linear logics, use it.
00697       if( !( e2.arity() == 2 && !trm.isNull() &&
00698              (trm.isApply() || trm.getKind() == READ || trm.isVar()) ) ) {
00699         // Otherwise, there are several cases, enumerated below.
00700 
00701         Expr coef = d_em->newRatExpr(constCoef);
00702         if(realConst) {
00703           // if any part of the coefficient was wrapped with REAL_CONST to
00704           // force printing as a real (e.g. "1.0"), then wrap the combined
00705           // coefficient
00706           coef = Expr(REAL_CONST, coef);
00707         }
00708 
00709         if(trm.isNull()) {
00710           // Case 1: entirely constant; the mult goes away
00711           TRACE("smtlib2-linear", "(1) constant", "", "");
00712           e2 = coef;
00713         } else if(constCoef == 1) {
00714           // Case 2: unit coefficient; the mult goes away
00715           TRACE("smtlib2-linear", "(2) unit coefficient: ", trm, "");
00716           e2 = trm;
00717         } else if(trm.getKind() == PLUS || trm.getKind() == MINUS) {
00718           // Case 3: have to distribute the MULT over PLUS/MINUS
00719           TRACE("smtlib2-linear", "(3) mult over plus/minus: ", trm, "");
00720           vector<Expr> kids;
00721           for(int i = 0; i < trm.arity(); ++i) {
00722             Expr trmi(MULT, coef, trm[i]);
00723             trmi = preprocess2Rec(trmi, cache, desiredType);
00724             kids.push_back(trmi);
00725           }
00726           e2 = Expr(trm.getKind(), kids);
00727         } else if(trm.getKind() == MULT) {
00728           // Case 4: have to distribute MULT over MULT
00729           TRACE("smtlib2-linear", "(4) mult over mult: ", trm, "");
00730           vector<Expr> kids;
00731           kids.push_back(coef);
00732           for(int i = 0; i < trm.arity(); ++i) {
00733             kids.push_back(trm[i]);
00734           }
00735           e2 = Expr(MULT, kids);
00736           e2 = preprocess2Rec(e2, cache, desiredType);
00737         } else if(trm.getKind() == ITE) {
00738           // Case 5: have to distribute MULT over ITE
00739           TRACE("smtlib2-linear", "(5) mult over ite: ", trm, "");
00740           Expr thn = Expr(MULT, coef, trm[1]);
00741           Expr els = Expr(MULT, coef, trm[2]);
00742           thn = preprocess2Rec(thn, cache, desiredType);
00743           els = preprocess2Rec(els, cache, desiredType);
00744           e2 = Expr(ITE, trm[0], thn, els);
00745         } else {
00746           // Default case: 
00747           TRACE("smtlib2-linear", "(*) coef, trm: ", coef, trm);
00748           // don't change order if not necessary (makes it easier to inspect the translation)
00749           if(trmFirst) {
00750             e2 = Expr(MULT, trm, coef);
00751           } else {
00752             e2 = Expr(MULT, coef, trm);
00753           }
00754           FatalAssert(trm.isVar(), string("translating with LINEAR restriction, but found malformed MULT over term that's not a free constant: ") + e2.toString());
00755         }
00756       } else {
00757         TRACE("smtlib2-linear", "(x) no handling necessary: ", trm, "");
00758       }
00759       TRACE("smtlib2-linear", "SMT-LIBv2 linearized: ", e2save, "");
00760       TRACE("smtlib2-linear", "                into: ", e2, "");
00761     }
00762   }
00763 
00764   if (!desiredType.isNull() && e2.getType() != desiredType) {
00765     if(isInt(e2.getType()) && isReal(desiredType) && !d_intUsed) {
00766       // the implicit cast is ok here
00767     } else {
00768       d_unknown = true;
00769       throw SmtlibException("Type error: expected "+
00770                             desiredType.getExpr().toString()+
00771                             " but instead got "+
00772                             e2.getType().getExpr().toString()+
00773                             "\n\nwhile processing term:\n"+
00774                             e.toString());
00775     }
00776   }
00777 
00778   cache[e] = e2;
00779   return e2;
00780 }
00781 
00782 
00783 Expr Translator::preprocess2(const Expr& e, ExprMap<Expr>& cache)
00784 {
00785   Expr result;
00786   try {
00787     result = preprocess2Rec(e, cache, Type());
00788   } catch (SmtlibException& ex) {
00789     cerr << "Error while processing the formula:\n"
00790          << e.toString() << endl;
00791     throw ex;
00792   }
00793   return result;
00794 }
00795 
00796 
00797 
00798 
00799 bool Translator::containsArray(const Expr& e)
00800 {
00801   if (e.getKind() == ARRAY) return true;
00802   Expr::iterator i = e.begin(), iend=e.end();
00803   for(; i!=iend; ++i) if (containsArray(*i)) return true;
00804   return false;
00805 }
00806 
00807 
00808 Translator::Translator(ExprManager* em,
00809                        const bool& translate,
00810                        const bool& real2int,
00811                        const bool& convertArith,
00812                        const string& convertToDiff,
00813                        bool iteLiftArith,
00814                        const string& expResult,
00815                        const string& category,
00816                        bool convertArray,
00817                        bool combineAssump,
00818                        int convertToBV)
00819   : d_em(em), d_translate(translate),
00820     d_real2int(real2int),
00821     d_convertArith(convertArith),
00822     d_convertToDiff(convertToDiff),
00823     d_iteLiftArith(iteLiftArith),
00824     d_expResult(expResult),
00825     d_category(category),
00826     d_convertArray(convertArray),
00827     d_combineAssump(combineAssump),
00828     d_dump(false), d_dumpFileOpen(false),
00829     d_intIntArray(false), d_intRealArray(false), d_intIntRealArray(false),
00830     d_ax(false), d_unknown(false),
00831     d_realUsed(false), d_intUsed(false), d_intConstUsed(false),
00832     d_langUsed(NOT_USED), d_UFIDL_ok(true), d_arithUsed(false),
00833     d_zeroVar(NULL), d_convertToBV(convertToBV)
00834 {
00835   d_arrayConvertMap = new map<string, Type>;
00836 }
00837 
00838 
00839 Translator::~Translator()
00840 {
00841   delete d_arrayConvertMap;
00842 }
00843 
00844 
00845 bool Translator::start(const string& dumpFile)
00846 {
00847   if (d_translate && (d_em->getOutputLang() == SMTLIB_LANG)) {
00848     d_dump = true;
00849     if (dumpFile == "") {
00850       d_osdump = &cout;
00851     }
00852     else {
00853       d_osdumpFile.open(dumpFile.c_str());
00854       if(!d_osdumpFile)
00855         throw Exception("cannot open a log file: "+dumpFile);
00856       else {
00857         d_dumpFileOpen = true;
00858         d_osdump = &d_osdumpFile;
00859       }
00860     }
00861 
00862     string tmpName;
00863     string::size_type pos = dumpFile.rfind("/");
00864     if (pos == string::npos) {
00865       tmpName = "README";
00866     }
00867     else {
00868       tmpName = dumpFile.substr(0,pos+1) + "README";
00869     }
00870     d_tmpFile.open(tmpName.c_str());
00871 
00872       *d_osdump << "(benchmark " << fileToSMTLIBIdentifier(dumpFile) << endl
00873           << "  :source {" << endl;
00874 
00875       char c;
00876       if (d_tmpFile.is_open()) {
00877         d_tmpFile.get(c);
00878         while (!d_tmpFile.eof()) {
00879           if ( c == '{' || c == '}' ) {
00880             *d_osdump << '\\';
00881           }
00882           *d_osdump << c;
00883           d_tmpFile.get(c);
00884         }
00885       }
00886       else {
00887         *d_osdump << "Source unknown";
00888       }
00889       *d_osdump << endl;
00890 
00891       *d_osdump << "}" << endl;
00892 
00893     d_tmpFile.close();
00894   }
00895   else if (d_translate && d_em->getOutputLang() == SPASS_LANG) {
00896     d_dump = true;
00897     if (dumpFile == "") {
00898       d_osdump = &cout;
00899     }
00900     else {
00901       d_osdumpFile.open(dumpFile.c_str());
00902       if(!d_osdumpFile)
00903         throw Exception("cannot open a log file: "+dumpFile);
00904       else {
00905         d_dumpFileOpen = true;
00906         d_osdump = &d_osdumpFile;
00907       }
00908     }
00909 
00910     *d_osdump << "begin_problem(Unknown). " << endl;
00911     *d_osdump << endl;
00912     *d_osdump << "list_of_descriptions. " << endl;
00913     *d_osdump << "name({* " <<  fileToSMTLIBIdentifier(dumpFile) << " *}). " << endl;
00914     *d_osdump << "author({* CVC2SPASS translator *})." << endl;
00915     //end of SPASS
00916   }
00917   else {
00918     if (dumpFile == "") {
00919       if (d_translate) {
00920         d_osdump = &cout;
00921         d_dump = true;
00922       }
00923     }
00924     else {
00925       d_osdumpFile.open(dumpFile.c_str());
00926       if(!d_osdumpFile)
00927         throw Exception("cannot open a log file: "+dumpFile);
00928       else {
00929         d_dump = true;
00930         d_dumpFileOpen = true;
00931         d_osdump = &d_osdumpFile;
00932       }
00933     }
00934   }
00935   return d_dump;
00936 }
00937 
00938 
00939 void Translator::dump(const Expr& e, bool dumpOnly)
00940 {
00941   DebugAssert(d_dump, "dump called unexpectedly");
00942   if (!dumpOnly || !d_translate) {
00943     if (d_convertArray && e.getKind() == CONST &&
00944         e.arity() == 2) {
00945       if (e[1].getKind() == ARRAY) {
00946         if (containsArray(e[1][0]) ||
00947             containsArray(e[1][1])) {
00948           throw Exception("convertArray failed because of nested arrays in"+
00949                           e[1].toString());
00950         }
00951         Expr funType = Expr(ARROW, e[1][0], e[1][1]);
00952         Expr outExpr = Expr(CONST, e[0], funType);
00953         d_dumpExprs.push_back(outExpr);
00954       }
00955       else if (containsArray(e[1])) {
00956         throw Exception("convertArray failed becauase of use of arrays in"+
00957                         e[1].toString());
00958       }
00959       else {
00960         d_dumpExprs.push_back(e);
00961       }
00962     }
00963     else {
00964       d_dumpExprs.push_back(e);
00965     }
00966   }
00967 }
00968 
00969 
00970 bool Translator::dumpAssertion(const Expr& e)
00971 {
00972   Expr outExpr = Expr(ASSERT, e);
00973   d_dumpExprs.push_back(outExpr);
00974   return d_translate;
00975 }
00976 
00977 
00978 bool Translator::dumpQuery(const Expr& e)
00979 {
00980   Expr outExpr = Expr(QUERY, e);
00981   d_dumpExprs.push_back(outExpr);
00982   return d_translate;
00983 }
00984 
00985 
00986 void Translator::dumpQueryResult(QueryResult qres)
00987 {
00988   if( d_translate && d_em->getOutputLang() == SMTLIB_LANG ) {
00989     *d_osdump << "  :status ";
00990     switch( qres ) {
00991     case UNSATISFIABLE:
00992       *d_osdump << "unsat" << endl;
00993       break;
00994     case SATISFIABLE:
00995       *d_osdump << "sat" << endl;
00996       break;
00997     default:
00998       *d_osdump << "unknown" << endl;
00999       break;
01000     }
01001   } else if( d_translate && d_em->getOutputLang() == SMTLIB_V2_LANG ) {
01002     *d_osdump << "(set-info :status ";
01003     switch( qres ) {
01004     case UNSATISFIABLE:
01005       *d_osdump << "unsat";
01006       break;
01007     case SATISFIABLE:
01008       *d_osdump << "sat";
01009       break;
01010     default:
01011       *d_osdump << "unknown";
01012       break;
01013     }
01014     *d_osdump << ")" << endl;
01015   } else if( d_translate && d_em->getOutputLang() == SPASS_LANG ) {
01016     *d_osdump << "status(";
01017     switch( qres ) {
01018     case UNSATISFIABLE:
01019       *d_osdump << "unsatisfiable";
01020       break;
01021     case SATISFIABLE:
01022       *d_osdump << "satisfiable";
01023       break;
01024     default:
01025       *d_osdump << "unknown";
01026       break;
01027     }
01028     *d_osdump << ")." << endl;
01029   }
01030 }
01031 
01032 
01033 /*
01034 Expr Translator::spassPreprocess(const Expr& e, ExprMap<Expr>& mapping,
01035                                  vector<Expr>& functions,
01036                                  vector<Expr>& predicates)
01037 {
01038   if(e.getKind() == LET) {
01039     if(e.arity() != 2) {
01040       throw SmtlibException("Translator::spassPreprocess(): LET with arity != 2 not supported");
01041     }
01042     char name[80];
01043     snprintf(name, sizeof(name), "_cvc3_let%u", mapping.size());
01044     Expr id(ID, d_em->newStringExpr(name));
01045     cout << "ENCOUNTERED A LET:" << endl << id << endl;
01046     mapping.insert(e[0][0], e[0][1]);
01047     functions.push_back(Expr(CONST, id, e[1].getType().getExpr()));
01048     return spassPreprocess(e[1], mapping, functions, predicates);
01049   //} else if(e.getKind() == x) {
01050   } else if(e.arity() > 0) {
01051     vector<Expr> args;
01052     for(int i = 0, iend = e.arity(); i < iend; ++i) {
01053       args.push_back(spassPreprocess(e[i], mapping, functions, predicates));
01054     }
01055     Expr out(e.getOp(), args);
01056     return out;
01057   }
01058   return e;
01059 }
01060 */
01061 
01062 
01063 Expr Translator::processType(const Expr& e)
01064 {
01065   switch (e.getKind()) {
01066     case TYPEDECL:
01067       return e;
01068     case INT:
01069       if (d_convertToBV) {
01070         return d_theoryBitvector->newBitvectorType(d_convertToBV).getExpr();
01071       }
01072       if (d_theoryCore->getFlags()["convert2array"].getBool()) {
01073         return d_elementType->getExpr();
01074       }
01075       d_intUsed = true;
01076       break;
01077     case REAL:
01078       if (d_real2int) {
01079         d_intUsed = true;
01080         return d_theoryArith->intType().getExpr();
01081       }
01082       else {
01083         d_realUsed = true;
01084       }
01085       break;
01086     case SUBRANGE:
01087       d_unknown = true;
01088       break;
01089     case ARRAY:
01090       if (d_theoryCore->getFlags()["convert2array"].getBool()) {
01091         d_ax = true;
01092         return d_arrayType->getExpr();
01093       }
01094       if (e[0].getKind() == TYPEDECL) {
01095         DebugAssert(e[0].arity() == 1, "expected arity 1");
01096         if (e[0][0].getString() == "Index") {
01097           if (e[1].getKind() == TYPEDECL) {
01098             DebugAssert(e[1].arity() == 1, "expected arity 1");
01099             if (e[1][0].getString() == "Element") {
01100               d_ax = true;
01101               break;
01102             }
01103           }
01104         }
01105       }
01106       else if (isInt(Type(e[0]))) {
01107         if (isInt(Type(e[1]))) {
01108           d_intIntArray = true;
01109           break;
01110         }
01111         else if (isReal(Type(e[1]))) {
01112           d_intRealArray = true;
01113           break;
01114         }
01115         else if (isArray(Type(e[1])) &&
01116                  isInt(Type(e[1][0])) &&
01117                  isReal(Type(e[1][1]))) {
01118           d_intIntRealArray = true;
01119           break;
01120         }
01121       }
01122       else if (e[0].getKind() == BITVECTOR &&
01123                e[1].getKind() == BITVECTOR) {
01124         break;
01125       }
01126       d_unknown = true;
01127       break;
01128     default:
01129       break;
01130   }
01131   d_theoryCore->theoryOf(e)->setUsed();
01132   if (e.arity() == 0) return e;
01133   bool changed = false;
01134   vector<Expr> vec;
01135   for (int i = 0; i < e.arity(); ++i) {
01136     vec.push_back(processType(e[i]));
01137     if (vec.back() != e[i]) changed = true;
01138   }
01139   if (changed)
01140     return Expr(e.getOp(), vec);
01141   return e;
01142 }
01143 
01144 
01145 void Translator::finish()
01146 {
01147   bool qf_uf = false;
01148 
01149   if (d_translate) {
01150 
01151     if (d_em->getOutputLang() == SPASS_LANG) {
01152       *d_osdump << "status(";
01153       if (d_expResult == "invalid" ||
01154           d_expResult == "satisfiable" ||
01155           d_expResult == "sat")
01156         *d_osdump << "satisfiable";
01157       else if (d_expResult == "valid" ||
01158                d_expResult == "unsatisfiable" ||
01159                d_expResult == "unsat")
01160         *d_osdump << "unsatisfiable";
01161       else if (d_expResult != "")
01162         *d_osdump << "unknown";
01163       else if (status() == "invalid" ||
01164                status() == "satisfiable" ||
01165                status() == "sat")
01166         *d_osdump << "satisfiable";
01167       else if (status() == "valid" ||
01168                status() == "unsatisfiable" ||
01169                status() == "unsat")
01170         *d_osdump << "unsatisfiable";
01171       else *d_osdump << "unknown";
01172       *d_osdump << ")." << endl;
01173       *d_osdump << "description({* Unknown *})." << endl;
01174       *d_osdump << "end_of_list." << endl;
01175 
01176       vector<Expr> functions, predicates, sorts;
01177 
01178       for(vector<Expr>::reverse_iterator i = d_dumpExprs.rbegin(), iend = d_dumpExprs.rend(); i != iend; ++i) {
01179         Expr e = *i;
01180         switch(e.getKind()) {
01181         case TYPE:
01182           sorts.push_back(e);
01183           d_dumpExprs.erase(i.base() - 1);
01184           break;
01185         case CONST:
01186           if(e.arity() == 2) {
01187             if (e[1].getKind() == BOOLEAN ||
01188                 (e[1].getKind() == ARROW && e[1][e[1].arity()-1].getKind() == BOOLEAN)) {
01189               predicates.push_back(e);
01190             } else {
01191               functions.push_back(e);
01192             }
01193             d_dumpExprs.erase(i.base() - 1);
01194           } else {
01195             throw SmtlibException("Translator::finish: SPASS_LANG: CONST not implemented for arity != 2");
01196           }
01197           break;
01198         case ANNOTATION:
01199           if (d_theoryCore->getFlags()["trans-skip-difficulty"].getBool() &&
01200               e[0].getKind() == STRING_EXPR && e[0].getString() == "difficulty") {
01201             // do nothing; skip the difficulty annotation
01202           } else {
01203             *d_osdump << "%% ";
01204             *d_osdump << e[0];
01205             if (e.arity() > 1) {
01206               *d_osdump << ": " << e[1];
01207             }
01208           }
01209           d_dumpExprs.erase(i.base() - 1);
01210           break;
01211 
01212           /*
01213         case ASSERT:
01214         case QUERY: {
01215           ExprMap<Expr> m;
01216           *i = Expr(e.getKind(), spassPreprocess(e[0], m, functions, predicates));
01217           break;
01218         }
01219           */
01220 
01221         default:
01222           //*d_osdump << "DOING NOTHING FOR: " << e << endl;
01223           break;
01224         }
01225       }
01226 
01227       // add some built-ins for the translation
01228       // only arity matters for SPASS; the real type of _cvc3_ite is Bool -> 'a -> 'a -> 'a
01229       //Expr cvc3ite(CONST, Expr(ID, d_em->newStringExpr("_cvc3_ite")),
01230       //Expr(ARROW, vector<Expr>(4, d_theoryArith->intType().getExpr())));
01231       // only arity matters for SPASS; the real type of _cvc3_xor is
01232       // Bool -> Bool -> Bool, but we can't represent Bool-arg'ed
01233       // functions
01234       /*
01235       Expr cvc3xor(CONST, Expr(ID, d_em->newStringExpr("_cvc3_xor")),
01236                    Expr(ARROW, vector<Expr>(2, d_theoryArith->intType().getExpr())));
01237       //functions.push_back(cvc3ite);
01238       predicates.push_back(cvc3xor);
01239       */
01240 
01241       *d_osdump << endl;
01242       *d_osdump << "list_of_symbols." << endl;
01243       if(!functions.empty()) {
01244         *d_osdump << "functions[";
01245         vector<Expr>::reverse_iterator i = functions.rbegin(), iend = functions.rend();
01246         while(i != iend) {
01247           Expr e = *i;
01248           string name = e[0][0].getString();
01249           if(isReal(d_theoryCore->getBaseType(Type(e[1])))) {
01250             // SPASS guys want "np" prefix on arith vars
01251             name = "np" + name;
01252           }
01253           *d_osdump << "(" << name << "," << ( e[1].getKind() == ARROW ? e[1].arity()-1 : e[1].arity() ) << ")";
01254           if(++i != iend) {
01255             *d_osdump << ",";
01256           }
01257         }
01258         *d_osdump << "]." << endl;
01259       }
01260       if(!predicates.empty()) {
01261         *d_osdump << "predicates[";
01262         vector<Expr>::reverse_iterator i = predicates.rbegin(), iend = predicates.rend();
01263         while(i != iend) {
01264           Expr e = *i;
01265           *d_osdump << "(" << e[0][0].getString() << "," << e[1].arity() << ")";
01266           if(++i != iend) {
01267             *d_osdump << ",";
01268           }
01269         }
01270         *d_osdump << "]." << endl;
01271       }
01272       if(!sorts.empty()) {
01273         *d_osdump << "sorts[";
01274         vector<Expr>::reverse_iterator i = sorts.rbegin(), iend = sorts.rend();
01275         while(i != iend) {
01276           Expr e = *i;
01277           *d_osdump << e[0][0].getString();
01278           if(++i != iend) {
01279             *d_osdump << ",";
01280           }
01281         }
01282         *d_osdump << "]." << endl;
01283       }
01284       *d_osdump << "end_of_list." << endl;
01285 
01286       /*
01287       *d_osdump << endl;
01288       *d_osdump << "list_of_declarations." << endl;
01289       *d_osdump << "end_of_list." << endl;
01290       */
01291 
01292       // define an ITE operator for the translation
01293       /*
01294       *d_osdump << endl;
01295       *d_osdump << "list_of_formulae(axioms)." << endl;
01296       *d_osdump << "formula( forall([A,B],equiv(_cvc3_xor(A,B),not(equal(A,B)))) )." << endl;
01297       // *d_osdump << "formula(forall([A,B],equal(_cvc3_ite(\ntrue\n,A,B),A)))." << endl;
01298       // *d_osdump << "formula(forall([A,B],equal(_cvc3_ite(\nfalse\n,A,B),B)))." << endl;
01299       *d_osdump << "end_of_list." << endl;
01300       */
01301 
01302       *d_osdump << endl;
01303       *d_osdump << "list_of_formulae(conjectures)." << endl;
01304     }
01305 
01306     if (d_em->getOutputLang() == SMTLIB_LANG) {
01307       // Print the rest of the preamble for smt-lib benchmarks
01308 
01309       // Get status from expResult flag
01310       *d_osdump << "  :status ";
01311       if (d_expResult == "invalid" ||
01312           d_expResult == "satisfiable")
01313         *d_osdump << "sat";
01314       else if (d_expResult == "valid" ||
01315                d_expResult == "unsatisfiable")
01316         *d_osdump << "unsat";
01317       else if (status() != "") {
01318         *d_osdump << status();
01319       }
01320       else *d_osdump << "unknown";
01321       *d_osdump << endl;
01322 
01323       // difficulty
01324       //      *d_osdump << "  :difficulty { unknown }" << endl;
01325 
01326       // category
01327       if (category() != "") {
01328         *d_osdump << "  :category { ";
01329         *d_osdump << category() << " }" << endl;
01330       }
01331 
01332       // Create types for theory QF_AX if needed
01333       if (d_theoryCore->getFlags()["convert2array"].getBool()) {
01334         d_indexType = new Type(d_theoryCore->newTypeExpr("Index"));
01335         d_elementType = new Type(d_theoryCore->newTypeExpr("Element"));
01336         d_arrayType = new Type(arrayType(*d_indexType, *d_elementType));
01337       }
01338     }
01339 
01340     // Preprocess and compute logic for smt-lib
01341 
01342     if (!d_theoryCore->getFlags()["trans-skip-pp"].getBool())
01343     {
01344       ExprMap<Expr> cache;
01345       // Step 1: preprocess asserts, queries, and types
01346       vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
01347       for (; i != iend; ++i) {
01348         Expr e = *i;
01349         switch (e.getKind()) {
01350           case ASSERT: {
01351             Expr e2 = preprocess(e[0], cache);
01352             if (e[0] == e2) break;
01353             e2.getType();
01354             *i = Expr(ASSERT, e2);
01355             break;
01356           }
01357           case QUERY: {
01358             Expr e2 = preprocess(e[0].negate(), cache);
01359             if (e[0].negate() == e2) break;
01360             e2.getType();
01361             *i = Expr(QUERY, e2.negate());
01362             break;
01363           }
01364           case CONST: {
01365             DebugAssert(e.arity() == 2, "Expected CONST with arity 2");
01366             if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
01367             Expr e2 = processType(e[1]);
01368             if (e[1] == e2) break;
01369             if (d_convertToBV) {
01370               Expr newName = Expr(ID, d_em->newStringExpr(e[0][0].getString()+"_bv"));
01371               *i = Expr(CONST, newName, e2);
01372             }
01373             else {
01374               *i = Expr(CONST, e[0], e2);
01375             }
01376             break;
01377           }
01378           default:
01379             break;
01380         }
01381       }
01382     }
01383 
01384     if (d_zeroVar) {
01385       d_dumpExprs.insert(d_dumpExprs.begin(),
01386                          Expr(CONST, Expr(ID, d_em->newStringExpr("cvc3Zero")),
01387                               processType(d_zeroVar->getType().getExpr())));
01388     }
01389 
01390     // Type inference over equality
01391     if (!d_unknown && d_theoryCore->getFlags()["convert2array"].getBool()) {
01392       bool changed;
01393       do {
01394         changed = false;
01395         unsigned i;
01396         for (i = 0; i < d_equalities.size(); ++i) {
01397           if (d_equalities[i][0].getKind() == UCONST &&
01398               d_arrayConvertMap->find(d_equalities[i][0].getName()) == d_arrayConvertMap->end()) {
01399             if (d_equalities[i][1].getKind() == READ) {
01400               changed = true;
01401               (*d_arrayConvertMap)[d_equalities[i][0].getName()] = *d_elementType;
01402             }
01403             else if (d_equalities[i][1].getKind() == UCONST) {
01404               map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][1].getName());
01405               if (it != d_arrayConvertMap->end()) {
01406                 changed = true;
01407                 (*d_arrayConvertMap)[d_equalities[i][0].getName()] = (*it).second;
01408               }
01409             }
01410           }
01411           else if (d_equalities[i][1].getKind() == UCONST &&
01412                    d_arrayConvertMap->find(d_equalities[i][1].getName()) == d_arrayConvertMap->end()) {
01413             if (d_equalities[i][0].getKind() == READ) {
01414               changed = true;
01415               (*d_arrayConvertMap)[d_equalities[i][1].getName()] = *d_elementType;
01416             }
01417             else if (d_equalities[i][0].getKind() == UCONST) {
01418               map<string, Type>::iterator it = d_arrayConvertMap->find(d_equalities[i][0].getName());
01419               if (it != d_arrayConvertMap->end()) {
01420                 changed = true;
01421                 (*d_arrayConvertMap)[d_equalities[i][1].getName()] = (*it).second;
01422               }
01423             }
01424           }
01425         }
01426       } while (changed);
01427     }
01428 
01429     if (d_em->getOutputLang() == SMTLIB_LANG ||
01430         d_em->getOutputLang() == SMTLIB_V2_LANG) {
01431 
01432       // Step 2: If both int and real are used, try to separate them
01433       if ((!d_unknown && (d_intUsed && d_realUsed)) ||
01434           d_theoryCore->getFlags()["convert2array"].getBool() ||
01435           ( d_em->getOutputLang() == SMTLIB_V2_LANG &&
01436             d_langUsed > NOT_USED && d_langUsed <= LINEAR )) {
01437         ExprMap<Expr> cache;
01438         vector<Expr>::iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
01439         for (; i != iend; ++i) {
01440           Expr e = *i;
01441           switch (e.getKind()) {
01442             case ASSERT: {
01443               if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
01444               Expr e2 = preprocess2(e[0], cache);
01445               e2.getType();
01446               *i = Expr(ASSERT, e2);
01447               break;
01448             }
01449             case QUERY: {
01450               if (d_theoryCore->getFlags()["convert2array"].getBool()) break;
01451               Expr e2 = preprocess2(e[0].negate(), cache);
01452               e2.getType();
01453               *i = Expr(QUERY, e2.negate());
01454               break;
01455             }
01456             case CONST: {
01457               if (!d_theoryCore->getFlags()["convert2array"].getBool()) break;
01458               map<string, Type>::iterator it = d_arrayConvertMap->find(e[0][0].getString());
01459               if (it != d_arrayConvertMap->end()) {
01460                 *i = Expr(CONST, e[0], (*it).second.getExpr());
01461               }
01462               else {
01463                 Expr e2 = processType(e[1]);
01464                 if (e[1] == e2) break;
01465                 *i = Expr(CONST, e[0], e2);
01466               }
01467               break;
01468             }
01469             default:
01470               break;
01471           }
01472         }
01473       }
01474       d_arithUsed = d_realUsed || d_intUsed || d_intConstUsed || (d_langUsed != NOT_USED);
01475 
01476       // Step 3: Go through the cases and figure out the right logic
01477       if (d_em->getOutputLang() == SMTLIB_LANG) {
01478         *d_osdump << "  :logic ";
01479       }
01480       else {// d_em->getOutputLang() == SMTLIB_V2_LANG
01481         *d_osdump << "(set-logic ";
01482       }
01483       if (d_unknown ||
01484           d_theoryRecords->theoryUsed() ||
01485           d_theorySimulate->theoryUsed() ||
01486           d_theoryDatatype->theoryUsed()) {
01487         *d_osdump << "unknown";
01488       }
01489       else {
01490         if ((d_ax && (d_arithUsed ||
01491                       d_theoryBitvector->theoryUsed() ||
01492                       d_theoryUF->theoryUsed())) ||
01493             (d_intIntArray && d_realUsed) ||
01494             (d_arithUsed && d_theoryBitvector->theoryUsed())) {
01495           *d_osdump << "unknown";
01496         }
01497         else {
01498           bool QF = false;
01499           bool A = false;
01500           bool UF = false;
01501           bool promote = d_theoryCore->getFlags()["promote"].getBool();
01502 
01503           if (!d_theoryQuant->theoryUsed()) {
01504             QF = true;
01505             *d_osdump << "QF_";
01506           }
01507 
01508           if (d_theoryArray->theoryUsed() && !d_convertArray) {
01509             A = true;
01510             *d_osdump << "A";
01511           }
01512 
01513           // Promote undefined subset logics
01514           else if (promote &&
01515                    !QF &&
01516                    !(d_arithUsed && d_realUsed && !d_intUsed && d_langUsed <= LINEAR) &&
01517                    !(d_arithUsed && !d_realUsed && d_intUsed && d_langUsed == NONLINEAR)) {
01518             A = true;
01519             *d_osdump << "A";
01520           }
01521 
01522           if (d_theoryUF->theoryUsed() ||
01523               (d_theoryArray->theoryUsed() && d_convertArray)) {
01524             UF = true;
01525             *d_osdump << "UF";
01526           }
01527 
01528           // Promote undefined subset logics
01529             else if (promote &&
01530                      !QF &&
01531                      !(d_arithUsed && d_realUsed && !d_intUsed && d_langUsed <= LINEAR)) {
01532               UF = true;
01533               *d_osdump << "UF";
01534             }
01535 
01536           if (d_arithUsed) {
01537             if (d_intUsed && d_realUsed) {
01538               if (d_langUsed < NONLINEAR) {
01539                 *d_osdump << "LIRA";
01540               }
01541               else *d_osdump << "NIRA";
01542             }
01543             else if (d_realUsed) {
01544               if (d_langUsed <= DIFF_ONLY) {
01545 
01546                 // Promote undefined subset logics
01547                  if (promote && !QF) {
01548                    *d_osdump << "LRA";
01549                  } else
01550 
01551                   *d_osdump << "RDL";
01552               }
01553               else if (d_langUsed <= LINEAR) {
01554                   *d_osdump << "LRA";
01555               }
01556               else {
01557 
01558                 // Promote undefined subset logics
01559                  if (promote && !QF) {
01560                    *d_osdump << "NIRA";
01561                  } else
01562 
01563                   *d_osdump << "NRA";
01564               }
01565             }
01566             else {
01567               if (QF && !A && UF && d_langUsed <= LINEAR) {
01568                 if (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok) {
01569                   *d_osdump << "IDL";
01570                 }
01571                 else {
01572                   *d_osdump << "LIA";
01573                 }
01574               }
01575               else if (d_langUsed <= DIFF_ONLY) {
01576 
01577                 // Promote undefined subset logics
01578                 if (promote && !QF) {
01579                   *d_osdump << "LIA";
01580                 }
01581                 else if (A) {
01582                   if (!UF) {
01583                     UF = true;
01584                     *d_osdump << "UF";
01585                   }
01586                   *d_osdump << "LIA";
01587                 } else
01588 
01589                   *d_osdump << "IDL";
01590               }
01591               else if (d_langUsed <= LINEAR) {
01592 
01593                 // Promote undefined subset logics
01594                  if (promote && QF && A && !UF) {
01595                    UF = true;
01596                    *d_osdump << "UF";
01597                  }
01598 
01599                 if (QF && !A && (!d_realUsed && d_langUsed <= LINEAR && d_UFIDL_ok)) {
01600                   *d_osdump << "UFIDL";
01601                 }
01602                 else {
01603                   *d_osdump << "LIA";
01604                 }
01605               }
01606               else {
01607                   *d_osdump << "NIA";
01608               }
01609             }
01610           }
01611           else if (d_theoryBitvector->theoryUsed()) {
01612 
01613             // Promote undefined subset logics
01614             if (promote && A && QF && !UF) {
01615               UF = true;
01616               *d_osdump << "UF";
01617             }
01618 
01619             *d_osdump << "BV";
01620           }
01621           else {
01622 
01623             if (d_ax) {
01624               *d_osdump << "X";
01625             }
01626 
01627             // Promote undefined subset logics
01628             else if (promote && (!QF || (A && UF))) {
01629               *d_osdump << "LIA";
01630             } else {
01631 
01632               // Default logic
01633               if (!A && !UF) {
01634                 UF = true;
01635                 *d_osdump << "UF";
01636               }
01637               qf_uf = QF && UF && (!A);
01638             }
01639           }
01640         }
01641       }
01642       if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
01643         *d_osdump << ")";
01644       }
01645       *d_osdump << endl;
01646     }
01647 
01648     if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
01649       // Print the rest of the set-info commands
01650 
01651       if (source() != "") {
01652         *d_osdump << "(set-info :source "
01653                   << quoteAnnotation(source())
01654                   << ')' << endl;
01655       }
01656 
01657       *d_osdump << "(set-info :smt-lib-version 2.0)" << endl;
01658 
01659       // Remove leading and trailing spaces from category
01660       string c = category();
01661       size_t i = 0, j = c.size();
01662       while (c[i] == ' ') {
01663         ++i; --j;
01664       }
01665       while (j > 0 && c[i+j-1] == ' ') --j;
01666       if (j > 0) {
01667         c = c.substr(i,j);
01668         *d_osdump << "(set-info :category \"" << c << "\")" << endl;
01669       }
01670 
01671 //       if (benchName() != "") {
01672 //         *d_osdump << "(set-info :name \"" << benchName() << "\")" << endl;
01673 //       }
01674 
01675       // Get status from expResult flag
01676       *d_osdump << "(set-info :status ";
01677       if (d_expResult == "invalid" ||
01678           d_expResult == "satisfiable")
01679         *d_osdump << "sat";
01680       else if (d_expResult == "valid" ||
01681                d_expResult == "unsatisfiable")
01682         *d_osdump << "unsat";
01683       else if (status() != "") {
01684         *d_osdump << status();
01685       }
01686       else *d_osdump << "unknown";
01687       *d_osdump << ")" << endl;
01688 
01689       // Create types for theory QF_AX if needed
01690       if (d_theoryCore->getFlags()["convert2array"].getBool()) {
01691         d_indexType = new Type(d_theoryCore->newTypeExpr("Index"));
01692         d_elementType = new Type(d_theoryCore->newTypeExpr("Element"));
01693         d_arrayType = new Type(arrayType(*d_indexType, *d_elementType));
01694       }
01695     }
01696   }
01697 
01698   if (d_dump) {
01699     // Dump the actual expressions
01700     vector<Expr>::const_iterator i = d_dumpExprs.begin(), iend = d_dumpExprs.end();
01701     vector<Expr> assumps;
01702     bool skip_diff = d_theoryCore->getFlags()["trans-skip-difficulty"].getBool();
01703     for (; i != iend; ++i) {
01704       Expr e = *i;
01705       switch (e.getKind()) {
01706         case ASSERT: {
01707           if (d_combineAssump) {
01708             assumps.push_back(e[0]);
01709           }
01710           else {
01711             *d_osdump << e << endl;
01712           }
01713           break;
01714         }
01715         case QUERY: {
01716           if (!assumps.empty()) {
01717             assumps.push_back(e[0].negate());
01718             e = Expr(QUERY, Expr(NOT, Expr(AND, assumps)));
01719           }
01720           *d_osdump << e << endl;
01721           break;
01722         }
01723         default:
01724           if (d_em->getOutputLang() == SMTLIB_LANG &&
01725               qf_uf && e.getKind() == TYPE && e[0].getKind() == RAW_LIST &&
01726               e[0][0].getKind() == ID && e[0][0][0].getKind() == STRING_EXPR &&
01727               e[0][0][0].getString() == "U")
01728             break;
01729           if (d_em->getOutputLang() == SMTLIB_LANG &&
01730               d_ax && e.getKind() == TYPE && e[0].getKind() == RAW_LIST &&
01731               e[0][0].getKind() == ID && e[0][0][0].getKind() == STRING_EXPR &&
01732               ( e[0][0][0].getString() == "Index" ||
01733                 e[0][0][0].getString() == "Element" ))
01734             break;
01735           if (skip_diff && e.getKind() == ANNOTATION && e[0].getKind() == STRING_EXPR &&
01736               e[0].getString() == "difficulty")
01737             break;
01738           if (d_em->getOutputLang() == SMTLIB_V2_LANG &&
01739               (e.getKind() == CONST && e[0].getKind() == ID) &&
01740               (d_realUsed || d_intUsed)) {
01741             if (e[0][0].getString() == "abs") {
01742               // [MGD] Some benchmarks define their own abs, but we have to
01743               // rename it in the benchmark becuase in SMTLIBv2 the Reals and
01744               // Ints and Reals_Ints theories define abs.
01745               d_replaceSymbols["abs"] = "abs_";
01746             } else if (e[0][0].getString() == "mod") {
01747               // ditto for mod
01748               d_replaceSymbols["mod"] = "mod_";
01749             }
01750           }
01751           *d_osdump << e << endl;
01752           break;
01753       }
01754     }
01755   }
01756   if (d_translate) {
01757     if (d_em->getOutputLang() == SMTLIB_LANG) {
01758       *d_osdump << ")" << endl;
01759     }
01760     else if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
01761       *d_osdump << "(exit)" << endl;
01762     }
01763 
01764     if (d_em->getOutputLang() == SPASS_LANG) {
01765       *d_osdump << "end_of_list." << endl;
01766       *d_osdump << endl;
01767       *d_osdump << "list_of_settings(SPASS)." << endl
01768                 << "{*" << endl
01769                 << "set_flag(Auto,1).    % auto configuration" << endl
01770                 << "set_flag(Splits,-1). % enable Splitting" << endl
01771                 << "set_flag(RVAA,1).    % enable variable assignment abstraction for LA" << endl
01772                 << "set_flag(RInput,0).  % no input reduction" << endl
01773                 << "set_flag(Sorts,0).   % no Sorts" << endl
01774                 << "set_flag(ISHy,0).    % no Hyper Resolution" << endl
01775                 << "set_flag(IOHy,0).    % no Hyper Resolution" << endl
01776                 << "set_flag(RTer,0).    % no Terminator" << endl
01777                 << "set_flag(RCon,0).    % no Condensation" << endl
01778                 << "set_flag(RFRew,1).   % no Contextual Rewriting" << endl
01779                 << "set_flag(RBRew,1).   % no Contextual Rewriting" << endl
01780                 << "*}" << endl
01781                 << "end_of_list." << endl;
01782       *d_osdump << endl;
01783       *d_osdump << "end_problem." << endl;
01784     }
01785   }
01786 
01787   if (d_dumpFileOpen) d_osdumpFile.close();
01788   if (d_zeroVar) delete d_zeroVar;
01789 }
01790 
01791 
01792 const string Translator::fixConstName(const string& s)
01793 {
01794   if (d_em->getOutputLang() == SMTLIB_LANG) {
01795     if (s[0] == '_') {
01796       return "smt"+s;
01797     }
01798   }
01799   std::hash_map<string, string, HashString>::iterator i = d_replaceSymbols.find(s);
01800   return (i == d_replaceSymbols.end()) ? s : (*i).second;
01801 }
01802 
01803 
01804 const string Translator::escapeSymbol(const string& s)
01805 {
01806   if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
01807     if (s.length() == 0 || isdigit(s[0]))
01808       return "|" + s + "|";
01809     // This is the legal set of SMTLIB v2 symbol characters from page
01810     // 20 of the SMT-LIB v2.0 spec.  If any character in the symbol
01811     // string falls outside this set, the symbol must be |-delimited.
01812     if(s.find_first_not_of("abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789~!@$%^&*_-+=<>.?/") != string::npos)
01813       return "|" + s + "|";
01814   }
01815   return s;
01816 }
01817 
01818 const string Translator::quoteAnnotation(const string& s)
01819 {
01820   if(s.find('|') == string::npos) {
01821     return "|" + s + "|";
01822   } else {
01823     stringstream sb;
01824     sb << '"';
01825     for(string::const_iterator i = s.begin(); i != s.end(); ++i) {
01826       char c = *i;
01827       if(c == '"')
01828         sb << "\\\"";
01829       else
01830         sb << *i;
01831     }
01832     sb << '"';
01833     return sb.str();
01834   }
01835 }
01836 
01837 
01838 bool Translator::printArrayExpr(ExprStream& os, const Expr& e)
01839 {
01840   if (e.getKind() == ARRAY) {
01841     if (d_convertArray) {
01842       os << Expr(ARROW, e[0], e[1]);
01843       return true;
01844     }
01845     if (d_em->getOutputLang() == SMTLIB_V2_LANG) {
01846       DebugAssert( e.arity() == 2, "expected arity 2");
01847       os << push << "(Array" << space << nodag << e[0] << space << nodag << e[1] << ")" << pop;
01848       return true;
01849     }
01850     if (d_em->getOutputLang() != SMTLIB_LANG) return false;
01851     if (e[0].getKind() == TYPEDECL) {
01852       DebugAssert(e[0].arity() == 1, "expected arity 1");
01853       if (e[0][0].getString() == "Index") {
01854         if (e[1].getKind() == TYPEDECL) {
01855           DebugAssert(e[1].arity() == 1, "expected arity 1");
01856           if (e[1][0].getString() == "Element") {
01857             os << "Array";
01858             return true;
01859           }
01860         }
01861       }
01862     }
01863     else if (isInt(Type(e[0]))) {
01864       if (isInt(Type(e[1]))) {
01865         d_intIntArray = true;
01866         os << "Array";
01867         return true;
01868       }
01869       else if (isReal(Type(e[1]))) {
01870         d_intRealArray = true;
01871         os << "Array1";
01872         return true;
01873       }
01874       else if (isArray(Type(e[1])) &&
01875                isInt(Type(e[1][0])) &&
01876                isReal(Type(e[1][1]))) {
01877         d_intIntRealArray = true;
01878         os << "Array2";
01879         return true;
01880       }
01881     }
01882     else if (e[0].getKind() == BITVECTOR &&
01883              e[1].getKind() == BITVECTOR) {
01884       os << "Array[";
01885       os << d_theoryBitvector->getBitvectorTypeParam(Type(e[0]));
01886       os << ":";
01887       os << d_theoryBitvector->getBitvectorTypeParam(Type(e[1]));
01888       os << "]";
01889       return true;
01890     }
01891     os << "UnknownArray";
01892     d_unknown = true;
01893     return true;
01894   }
01895 
01896   switch (e.getKind()) {
01897     case READ:
01898       if (d_convertArray) {
01899         if (e[0].getKind() == UCONST) {
01900           os << Expr(d_em->newSymbolExpr(e[0].getName(), UFUNC).mkOp(), e[1]);
01901           return true;
01902         }
01903         else if (e[0].getKind() == WRITE) {
01904           throw Exception("READ of WRITE not implemented yet for convertArray");
01905         }
01906         else {
01907           throw Exception("Unexpected case for convertArray");
01908         }
01909       }
01910       break;
01911     case WRITE:
01912       if (d_convertArray) {
01913         throw Exception("WRITE expression encountered while attempting "
01914                         "to convert arrays to uninterpreted functions");
01915       }
01916       break;
01917     case ARRAY_LITERAL:
01918       if (d_convertArray) {
01919         throw Exception("ARRAY_LITERAL expression encountered while attempting"
01920                         " to convert arrays to uninterpreted functions");
01921       }
01922       break;
01923     default:
01924       throw Exception("Unexpected case in printArrayExpr");
01925       break;
01926   }
01927   return false;
01928 }
01929 
01930 
01931 Expr Translator::zeroVar()
01932 {
01933   if (!d_zeroVar) {
01934     d_zeroVar = new Expr();
01935     if (d_convertToDiff == "int") {
01936       *d_zeroVar = d_theoryCore->newVar("cvc3Zero", d_theoryArith->intType().getExpr());
01937     }
01938     else if (d_convertToDiff == "real") {
01939       *d_zeroVar = d_theoryCore->newVar("cvc3Zero", d_theoryArith->realType().getExpr());
01940     }
01941   }
01942   return *d_zeroVar;
01943 }