vc_cmd.cpp

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file vc_cmd.cpp
00004  * 
00005  * Author: Clark Barrett
00006  * 
00007  * Created: Fri Dec 13 22:39:02 2002
00008  *
00009  * <hr>
00010  * License to use, copy, modify, sell and/or distribute this software
00011  * and its documentation for any purpose is hereby granted without
00012  * royalty, subject to the terms and conditions defined in the \ref
00013  * LICENSE file provided with this distribution.
00014  * 
00015  * <hr>
00016  * 
00017  */
00018 /*****************************************************************************/
00019 
00020 #include <fstream>
00021 #include "vc_cmd.h"
00022 #include "vc.h"
00023 #include "parser.h"
00024 #include "eval_exception.h"
00025 #include "typecheck_exception.h"
00026 #include "command_line_flags.h"
00027 #include "expr_stream.h"
00028 
00029 using namespace std;
00030 using namespace CVC3;
00031 
00032 VCCmd::VCCmd(ValidityChecker* vc, Parser* parser)
00033   : d_vc(vc), d_parser(parser), d_name_of_cur_ctxt("DEFAULT")
00034 {
00035   d_map[d_name_of_cur_ctxt.c_str()] = d_vc->getCurrentContext();
00036 }
00037 
00038 VCCmd::~VCCmd() { }
00039 
00040 void VCCmd::findAxioms(const Expr& e,  ExprMap<bool>& skolemAxioms,
00041            ExprMap<bool>& visited) {
00042   if(visited.count(e)>0)
00043     return;
00044   else visited[e] = true;
00045   if(e.isSkolem()) {
00046     skolemAxioms.insert(e.getExistential(), true);
00047     return;
00048   }
00049   if(e.isClosure()) {
00050     findAxioms(e.getBody(), skolemAxioms, visited);
00051   }
00052   if(e.arity()>0) {
00053     Expr::iterator end = e.end();
00054     for(Expr::iterator i = e.begin(); i!=end; ++i)
00055       findAxioms(*i, skolemAxioms, visited);
00056   }
00057   
00058 }
00059 
00060 Expr VCCmd::skolemizeAx(const Expr& e)
00061 {
00062   vector<Expr>vars;
00063   const vector<Expr>boundVars = e.getVars(); 
00064   for(unsigned int i=0; i<boundVars.size(); i++) {
00065     Expr skolV(e.skolemExpr(i));
00066     vars.push_back(skolV);
00067   }
00068   Expr sub = e.getBody().substExpr(boundVars, vars);
00069   return e.iffExpr(sub);
00070 }
00071 
00072 bool VCCmd::evaluateNext()
00073 {
00074 readAgain:
00075   if(d_parser->done()) return false; // No more commands
00076   Expr e;
00077   try {
00078     TRACE_MSG("commands", "** [commands] Parsing command...");
00079     e = d_parser->next();
00080     TRACE("commands verbose", "evaluateNext(", e, ")");
00081   } 
00082   catch(Exception& e) {
00083     cerr << "*** " << e << endl;
00084     IF_DEBUG(++(debugger.counter("parse errors")));
00085   }
00086   // The parser may return a Null Expr in case of parse errors or end
00087   // of file.  The right thing to do is to ignore it and repeat
00088   // reading.
00089   if(e.isNull()) {
00090     TRACE_MSG("commands", "** [commands] Null command; read again");
00091     goto readAgain;
00092   }
00093 
00094   return evaluateCommand(e);
00095 }
00096 
00097 void VCCmd::reportResult(QueryResult qres, bool checkingValidity)
00098 {
00099   if (d_vc->getFlags()["printResults"].getBool()) {
00100     if (d_vc->getEM()->getOutputLang() == SMTLIB_LANG) {
00101       switch (qres) {
00102         case VALID:
00103           cout << "unsat" << endl;
00104           break;
00105         case INVALID:
00106           cout << "sat" << endl;
00107           break;
00108         case ABORT:
00109         case UNKNOWN:
00110           cout << "unknown" << endl;
00111           break;
00112         default:
00113           FatalAssert(false, "Unexpected case");
00114       }
00115     }
00116     else {
00117       switch (qres) {
00118         case VALID:
00119           cout << (checkingValidity ? "Valid." : "Unsatisfiable.") << endl;
00120           break;
00121         case INVALID:
00122           cout << (checkingValidity ? "Invalid." : "Satisfiable.") << endl;
00123           break;
00124         case ABORT:
00125           cout << "Unknown: resource limit exhausted." << endl;
00126           break;
00127         case UNKNOWN: {
00128           // Vector of reasons in case of incomplete result
00129           vector<string> reasons;
00130           IF_DEBUG(bool b =) d_vc->incomplete(reasons);
00131           DebugAssert(b, "Expected incompleteness");
00132           cout << "Unknown.\n\n";
00133           cout << "CVC3 was incomplete in this example due to:";
00134           for(vector<string>::iterator i=reasons.begin(), iend=reasons.end();
00135               i!=iend; ++i)
00136             cout << "\n * " << (*i);
00137           cout << endl << endl;
00138           break;
00139         }
00140         default:
00141           FatalAssert(false, "Unexpected case");
00142       }
00143     }
00144     cout << flush;
00145   }
00146 //     d_vc->printStatistics();
00147 //     exit(0);
00148 }
00149 
00150 
00151 bool VCCmd::evaluateCommand(const Expr& e0)
00152 {
00153   TRACE("commands", "evaluateCommand(", e0.toString(PRESENTATION_LANG), ") {");
00154   Expr e(e0);
00155   if(e.getKind() != RAW_LIST || e.arity() == 0 || e[0].getKind() != ID)
00156     throw EvalException("Invalid command: "+e.toString());
00157   const string& kindName = e[0][0].getString();
00158   int kind = d_vc->getEM()->getKind(kindName);
00159   if(kind == NULL_KIND)
00160     throw EvalException("Unknown command: "+e.toString());
00161   switch(kind) {
00162   case CONST: { // (CONST (id_1 ... id_n) type) or (CONST id type)
00163     if(e.arity() == 3) {
00164       Type t(d_vc->parseExpr(e[2]));
00165       vector<Expr> vars;
00166       if(e[1].getKind() == RAW_LIST)
00167   vars = e[1].getKids();
00168       else
00169   vars.push_back(e[1]);
00170       for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) {
00171   if((*i).getKind() != ID)
00172     throw EvalException("Constant name must be an identifier: "
00173             +i->toString());
00174       }
00175       if (t.isFunction()) {
00176   for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
00177       i!=iend; ++i) {
00178     Op op = d_vc->createOp((*i)[0].getString(), t);
00179     TRACE("commands", "evaluateNext: declare new uninterpreted function: ",
00180     op, "");
00181   }
00182       }
00183       else {
00184   for(vector<Expr>::iterator i=vars.begin(), iend=vars.end();
00185       i!=iend; ++i) {
00186     // Add to variable list
00187     Expr v = d_vc->varExpr((*i)[0].getString(), t);
00188     TRACE_MSG("commands", "** [commands] Declare new variable");
00189     TRACE("commands verbose", "evaluateNext: declare new UCONST: ",
00190     v, "");
00191   }
00192       }
00193     } else if(e.arity() == 4) { // Constant definition (CONST id type def)
00194       TRACE_MSG("commands", "** [commands] Define new constant");
00195       // Set the type for later typechecking
00196       DebugAssert(e[1].getKind() == ID, "Expected ID kind");
00197       Type t(d_vc->parseExpr(e[2]));
00198       Expr def(d_vc->parseExpr(e[3]));
00199       
00200       if(t.isFunction()) {
00201   d_vc->createOp(e[1][0].getString(), t, def);
00202   TRACE("commands verbose", "evaluateNext: define new function: ",
00203         e[1][0].getString(), "");
00204       } else {
00205   d_vc->varExpr(e[1][0].getString(), t, def);
00206   TRACE("commands verbose", "evaluateNext: define new variable: ",
00207         e[1][0].getString(), "");
00208       }
00209     } else 
00210       throw EvalException("Wrong number of arguments in CONST: "+e.toString());
00211     break;
00212   }
00213   case DEFUN: { // (DEFUN name ((x y z type1) ... ) resType [ body ])
00214     if(e.arity() != 5 && e.arity() != 4)
00215       throw EvalException
00216   ("DEFUN requires 3 or 4 arguments:"
00217    " (DEFUN f (args) type [ body ]):\n\n  "
00218    +e.toString());
00219     if(e[2].getKind() != RAW_LIST)
00220       throw EvalException
00221   ("2nd argument of DEFUN must be a list of arguments:\n\n  "
00222    +e.toString());
00223 
00224     // Build a CONST declaration and parse it recursively
00225 
00226     // Build the function type
00227     vector<Expr> argTps;
00228     for(Expr::iterator i=e[2].begin(), iend=e[2].end(); i!=iend; ++i) {
00229       if(i->getKind() != RAW_LIST || i->arity() < 2)
00230   throw EvalException
00231     ("DEFUN: bad argument declaration:\n\n  "+i->toString()
00232      +"\n\nIn the following statement:\n\n  "
00233      +e.toString());
00234       Expr tp((*i)[i->arity()-1]);
00235       for(int j=0, jend=i->arity()-1; j<jend; ++j)
00236   argTps.push_back(tp);
00237     }
00238     argTps.push_back(e[3]);
00239     Expr fnType = d_vc->listExpr("ARROW", argTps);
00240     Expr newDecl; // The resulting transformed declaration
00241     if(e.arity() == 5) {
00242       // Build the LAMBDA expression
00243       Expr lambda(d_vc->listExpr("LAMBDA", e[2], e[4]));
00244       // Construct the (CONST name fnType lambda) declaration
00245       newDecl = d_vc->listExpr("CONST", e[1], fnType, lambda);
00246     } else {
00247       newDecl = d_vc->listExpr("CONST", e[1], fnType);
00248     }
00249     // Parse the new declaration
00250     return evaluateCommand(newDecl);
00251     break;
00252   }
00253   case TYPEDEF: {
00254     DebugAssert(e.arity() == 3, "Bad TYPEDEF");
00255     Expr def(d_vc->parseExpr(e[2]));
00256     Type t = d_vc->createType(e[1][0].getString(), def);
00257     TRACE("commands", "evaluateNext: declare new TYPEDEF: ", t, "");
00258   }
00259     break;
00260   case TYPE: {
00261     if(e.arity() < 2)
00262       throw EvalException("Bad TYPE declaration: "+e.toString());
00263     Expr::iterator i=e.begin(), iend=e.end();
00264     ++i; // Skip "TYPE" symbol
00265     for(; i!=iend; ++i) {
00266       if(i->getKind() != ID)
00267   throw EvalException("Type name must be an identifier: "+i->toString());
00268       Type t = d_vc->createType((*i)[0].getString());
00269       TRACE("commands", "evaluateNext: declare new TYPEDECL: ", t, "");
00270     }
00271   }
00272     break;
00273   case ASSERT: {
00274     if(e.arity() != 2)
00275       throw EvalException("ASSERT requires exactly one argument, but is given "
00276         +int2string(e.arity()-1)+":\n "+e.toString());
00277     TRACE_MSG("commands", "** [commands] Asserting formula");
00278     d_vc->assertFormula(d_vc->parseExpr(e[1]));
00279     break;
00280   }
00281   case QUERY: {
00282     if(e.arity() != 2)
00283       throw EvalException("QUERY requires exactly one argument, but is given "
00284         +int2string(e.arity()-1)+":\n "+e.toString());
00285     TRACE_MSG("commands", "** [commands] Query formula");
00286     QueryResult qres = d_vc->query(d_vc->parseExpr(e[1]));
00287 
00288     reportResult(qres);
00289     break;
00290   }
00291   case CHECKSAT: {
00292     QueryResult qres;
00293     TRACE_MSG("commands", "** [commands] CheckSat");
00294     if (e.arity() == 1) {
00295       qres = d_vc->checkUnsat(d_vc->trueExpr());
00296     }
00297     else if (e.arity() == 2) {
00298       qres = d_vc->checkUnsat(d_vc->parseExpr(e[1]));
00299     }
00300     else {
00301       throw EvalException("CHECKSAT requires no more than one argument, but is given "
00302         +int2string(e.arity()-1)+":\n "+e.toString());
00303     }
00304     reportResult(qres, false);
00305     break;
00306   }
00307   case CONTINUE: {
00308     if (e.arity() != 1) {
00309       throw EvalException("CONTINUE takes no arguments");
00310     }
00311     TRACE_MSG("commands", "** [commands] Continue");
00312     QueryResult qres = d_vc->checkContinue();
00313     if (d_vc->getFlags()["printResults"].getBool()) {
00314       switch (qres) {
00315         case VALID:
00316           cout << "No more models found." << endl;
00317           break;
00318         case INVALID:
00319           cout << "Model found" << endl;
00320           break;
00321         case ABORT:
00322           cout << "Unknown: resource limit exhausted." << endl;
00323           break;
00324         case UNKNOWN: {
00325           // Vector of reasons in case of incomplete result
00326           vector<string> reasons;
00327           IF_DEBUG(bool b =) d_vc->incomplete(reasons);
00328           DebugAssert(b, "Expected incompleteness");
00329           cout << "Unknown.\n\n";
00330           cout << "CVC3 was incomplete in this example due to:";
00331           for(vector<string>::iterator i=reasons.begin(), iend=reasons.end();
00332               i!=iend; ++i)
00333             cout << "\n * " << (*i);
00334           cout << endl << endl;
00335           break;
00336         }
00337         default:
00338           FatalAssert(false, "Unexpected case");
00339       }
00340       cout << flush;          
00341     }
00342     break;
00343   }
00344   case RESTART: {
00345     if(e.arity() != 2)
00346       throw EvalException("RESTART requires exactly one argument, but is given "
00347         +int2string(e.arity()-1)+":\n "+e.toString());
00348     TRACE_MSG("commands", "** [commands] Restart formula");
00349     QueryResult qres = d_vc->restart(d_vc->parseExpr(e[1]));
00350     reportResult(qres);
00351     break;
00352   }
00353   case TRANSFORM: {
00354     if(e.arity() != 2)
00355       throw EvalException
00356   ("TRANSFORM requires exactly one argument, but is given "
00357    +int2string(e.arity()-1)+":\n "+e.toString());
00358     TRACE_MSG("commands", "** [commands] Transforming expression");
00359     Expr ee = d_vc->parseExpr(e[1]);
00360     e = d_vc->simplify(ee);
00361     if (d_vc->getFlags()["printResults"].getBool()) d_vc->printExpr(e);
00362     break;
00363   }
00364   case PRINT:
00365     if(e.arity() != 2)
00366       throw EvalException
00367   ("PRINT requires exactly one argument, but is given "
00368    +int2string(e.arity()-1)+":\n "+e.toString());
00369     d_vc->printExpr(d_vc->parseExpr(e[1]));
00370     break;
00371   case PUSH:
00372   case POP:
00373   case PUSH_SCOPE:
00374   case POP_SCOPE: {
00375     int arg;
00376     if (e.arity() == 1) arg = 1;
00377     else {
00378       DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR,
00379                   "Bad argument to "+kindName);
00380       arg = e[1].getRational().getInt();
00381       if(arg <= 0)
00382         throw EvalException("Argument to PUSH or POP is <= 0");
00383     }
00384     if (kind == PUSH) {
00385       for (int i = 0; i < arg; i++) {
00386         d_vc->push();
00387       }
00388     }
00389     else if (kind == POP) {
00390       if(arg > d_vc->stackLevel())
00391         throw EvalException("Argument to POP is out of range:\n"
00392                             " current stack level = "
00393                             +int2string(d_vc->stackLevel())
00394                             +"\n argument = "
00395                             +int2string(arg));
00396       for (int i = 0; i < arg; i++) {
00397         d_vc->pop();
00398       }
00399     }
00400     else if (kind == PUSH_SCOPE) {
00401       for (int i = 0; i < arg; i++) {
00402         d_vc->pushScope();
00403       }
00404     }
00405     else if (kind == POP_SCOPE) {
00406       if(arg >= d_vc->scopeLevel())
00407         throw EvalException("Argument to POP_SCOPE is out of range:\n"
00408                             " current scope = "
00409                             +int2string(d_vc->scopeLevel())
00410                             +"\n argument = "
00411                             +int2string(arg));
00412       for (int i = 0; i < arg; i++) {
00413         d_vc->popScope();
00414       }
00415     }
00416     break;
00417   }
00418   case POPTO:
00419   case POPTO_SCOPE: {
00420     int arg;
00421     if (e.arity() == 1) arg = 0;
00422     else {
00423       DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR,
00424                   "Bad argument to "+kindName);
00425       arg = e[1].getRational().getInt();
00426     }
00427     if (kind == POPTO) {
00428       d_vc->popto(arg);
00429     }
00430     else {
00431       d_vc->poptoScope(arg);
00432     }
00433     break;
00434   }
00435   case WHERE:
00436   case ASSERTIONS:
00437   case ASSUMPTIONS:
00438   {
00439     vector<Expr> assertions;
00440     ExprMap<bool> skolemAxioms;
00441     ExprMap<bool> visited;
00442 
00443     d_vc->getAssumptions(assertions);
00444 
00445     if (d_vc->getFlags()["printResults"].getBool()) {
00446       cout << "Current stack level is " << d_vc->stackLevel()
00447            << " (scope " << d_vc->scopeLevel() << ")." << endl;
00448       if (assertions.size() == 0) {
00449         cout << "% No active assumptions\n";
00450       } else {
00451         cout << "% Active assumptions:\n";
00452         for (unsigned i = 0; i < assertions.size(); i++) {  
00453           cout << "ASSERT " << assertions[i] << ";" << endl;
00454           findAxioms(assertions[i], skolemAxioms, visited);
00455         }
00456         ExprMap<bool>::iterator it = skolemAxioms.begin();
00457         ExprMap<bool>::iterator end = skolemAxioms.end();
00458         if (it != end) {
00459           cout << "% Skolemization axioms" << endl;
00460           for(; it!=end; ++it)
00461             cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl;
00462         }
00463       }
00464       cout << endl;
00465     }
00466     break;
00467   }
00468   case COUNTEREXAMPLE: {
00469     vector<Expr> assertions;
00470     ExprMap<bool> skolemAxioms;
00471     ExprMap<bool> visited;
00472 
00473     d_vc->getCounterExample(assertions);
00474 
00475     if (d_vc->getFlags()["printResults"].getBool()) {
00476       cout << "Current scope level is " << d_vc->scopeLevel() << "." << endl;
00477       if (assertions.size() == 0) {
00478         cout << "% There are no assertions\n";
00479       } else {
00480 
00481         cout << "% Assertions which make the QUERY invalid:\n";
00482 
00483         for (unsigned i = 0; i < assertions.size(); i++) {
00484           cout << Expr(ASSERT, assertions[i]) << "\n";
00485           findAxioms(assertions[i], skolemAxioms, visited);
00486         }
00487         ExprMap<bool>::iterator end = skolemAxioms.end();
00488         for(ExprMap<bool>::iterator it = skolemAxioms.begin(); it!=end; it++)
00489           cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl;
00490       }
00491       cout << endl;
00492     }
00493     break;
00494   }
00495   case COUNTERMODEL: {
00496     ExprMap<Expr> m;
00497     d_vc->getConcreteModel(m);
00498 
00499     if (d_vc->getFlags()["printResults"].getBool()) {
00500       cout << "Current scope level is " << d_vc->scopeLevel() << "." << endl;
00501       ExprMap<Expr>::iterator it = m.begin(), end = m.end();
00502       if(it == end)
00503         cout << " Did not find concrete model for any vars" << endl;
00504       else {
00505         cout << "%Satisfiable  Variable Assignment: % \n";
00506         for(; it!= end; it++) {
00507           Expr eq;
00508           if(it->first.getType().isBool()) {
00509             DebugAssert((it->second).isBoolConst(),
00510                         "Bad variable assignement: e = "+(it->first).toString()
00511                         +"\n\n val = "+(it->second).toString());
00512             if((it->second).isTrue())
00513               eq = it->first;
00514             else
00515               eq = !(it->first);
00516           }
00517           else
00518             eq = (it->first).eqExpr(it->second);
00519           cout << Expr(ASSERT,  eq) << "\n";
00520         }
00521       }
00522     }
00523     break;
00524   }
00525   case TRACE: { // Set a trace flag
00526 #ifdef DEBUG
00527     if(e.arity() != 2)
00528       throw EvalException("TRACE takes exactly one string argument");
00529     if(!e[1].isString())
00530       throw EvalException("TRACE requires a string argument");
00531     debugger.traceFlag(e[1].getString()) = true;
00532 #endif
00533   }
00534     break;
00535   case UNTRACE: { // Unset a trace flag
00536 #ifdef DEBUG
00537     if(e.arity() != 2)
00538       throw EvalException("UNTRACE takes exactly one string argument");
00539     if(!e[1].isString())
00540       throw EvalException("UNTRACE requires a string argument");
00541     debugger.traceFlag(e[1].getString()) = false;
00542 #endif
00543   }
00544     break;
00545   case OPTION: {
00546     if(e.arity() != 3)
00547       throw EvalException("OPTION takes exactly two arguments "
00548                           "(name and value of a flag)");
00549     if(!e[1].isString())
00550       throw EvalException("OPTION: flag name must be a string");
00551     CLFlags& flags = d_vc->getFlags();
00552     string name(e[1].getString());
00553     vector<string> names;
00554     size_t n = flags.countFlags(name, names);
00555     if(n != 1)
00556       throw EvalException("OPTION: found "+int2string(n)
00557                           +" flags matching "+name
00558                           +".\nThe flag name must uniquely resolve.");
00559     name = names[0];
00560     const CLFlag& flag(flags[name]);
00561     // If the flag is set on the command line, ignore it
00562     if(flag.modified()) break;
00563     switch(flag.getType()) {
00564     case CLFLAG_BOOL:
00565       if(!(e[2].isRational() && e[2].getRational().isInteger()))
00566         throw EvalException("OPTION: flag "+name
00567                             +" expects a boolean value (0 or 1");
00568       flags.setFlag(name, e[2].getRational().getInt() != 0);
00569       break;
00570     case CLFLAG_INT:
00571       if(!(e[2].isRational() && e[2].getRational().isInteger()))
00572         throw EvalException("OPTION: flag "+name+" expects an integer value");
00573       flags.setFlag(name, e[2].getRational().getInt());
00574       break;
00575     case CLFLAG_STRING:
00576       if(!e[2].isString())
00577         throw EvalException("OPTION: flag "+name+" expects a string value");
00578       flags.setFlag(name, e[2].getString());
00579       break;
00580     default:
00581       throw EvalException("OPTION: the type of flag "+name
00582                           +" is not supported by the OPTION commnand");
00583       break;
00584     }
00585     d_vc->reprocessFlags();
00586   }
00587     break;
00588   case DUMP_PROOF: {
00589     Proof p = d_vc->getProof();
00590     if (d_vc->getFlags()["printResults"].getBool()) {
00591       cout << p << endl;
00592       cout << flush;
00593     }
00594     break;
00595   }
00596   case DUMP_ASSUMPTIONS: { // Assumption tracking
00597     vector<Expr> assertions;
00598     d_vc->getAssumptionsUsed(assertions);
00599 
00600     if (d_vc->getFlags()["printResults"].getBool()) {
00601       if(assertions.size() == 0) {
00602         cout << "% No relevant assumptions\n";
00603       } else {
00604         cout << "% Relevant assumptions:\n";
00605         for (unsigned i = 0; i < assertions.size(); i++) {
00606           cout << Expr(ASSERT, assertions[i]) << "\n";
00607         }
00608       }
00609       cout << endl << flush;
00610     }
00611     break;
00612   }
00613   case DUMP_TCC: {
00614     const Expr& tcc = d_vc->getTCC();
00615 
00616     if (d_vc->getFlags()["printResults"].getBool()) {
00617       if(tcc.isNull())
00618         cout << "% No TCC is avaialble" << endl;
00619       else
00620         cout << "% TCC for the last declaration, ASSERT, or QUERY:\n\n"
00621              << tcc << endl;
00622     }
00623     break;
00624   }
00625   case DUMP_TCC_ASSUMPTIONS: {
00626     vector<Expr> assertions;
00627     d_vc->getAssumptionsTCC(assertions);
00628     if (d_vc->getFlags()["printResults"].getBool()) {
00629       if(assertions.size() == 0) {
00630         cout << "% No relevant assumptions\n";
00631       } else {
00632         cout << "% Relevant assumptions for the last TCC:\n";
00633         for (unsigned i = 0; i < assertions.size(); i++) {
00634           cout << Expr(ASSERT, assertions[i]) << "\n";
00635         }
00636       }
00637       cout << endl << flush;
00638     }
00639     break;
00640   }
00641   case DUMP_TCC_PROOF: {
00642     const Proof& tcc = d_vc->getProofTCC();
00643     if (d_vc->getFlags()["printResults"].getBool()) {
00644       if(tcc.isNull())
00645         cout << "% No TCC is avaialble" << endl;
00646       else
00647         cout << "% Proof of TCC for the last declaration, ASSERT, or QUERY:\n\n"
00648              << tcc << endl;
00649     }
00650     break;
00651   }
00652   case DUMP_CLOSURE: {
00653     const Expr& cl = d_vc->getClosure();
00654     if (d_vc->getFlags()["printResults"].getBool()) {
00655       if(cl.isNull())
00656         cout << "% No closure is avaialble" << endl;
00657       else
00658         cout << "% Closure for the last QUERY:\n\n" << cl << endl;
00659     }
00660     break;
00661   }
00662   case DUMP_CLOSURE_PROOF: {
00663     const Proof& cl = d_vc->getProofClosure();
00664     if (d_vc->getFlags()["printResults"].getBool()) {
00665       if(cl.isNull())
00666         cout << "% No closure is avaialble" << endl;
00667       else
00668         cout << "% Proof of closure for the last QUERY:\n\n" << cl << endl;
00669     }
00670     break;
00671   }
00672   case ECHO:
00673     if(e.arity() != 2)
00674       throw EvalException("ECHO: wrong number of arguments: "
00675         + e.toString());
00676     if(!e[1].isString())
00677       throw EvalException("ECHO: the argument must be a string: "
00678         +e.toString());
00679     if (d_vc->getFlags()["printResults"].getBool()) {
00680       cout << e[1].getString();
00681       cout << endl << flush;
00682     }
00683     break;
00684   case SEQ: {
00685     Expr::iterator i=e.begin(), iend=e.end();
00686     ++i; // Skip "SEQ" symbol
00687     bool success = true;
00688     for(; i!=iend; ++i) {
00689       success = success && evaluateCommand(*i);
00690     }
00691     return success;
00692   }
00693   case INCLUDE: { // read in the specified file
00694     if(e.arity() != 2)
00695       throw EvalException("INCLUDE takes exactly one string argument");
00696     if(!e[1].isString())
00697       throw EvalException("INCLUDE requires a string argument");
00698     ifstream fs;
00699     fs.open(e[1].getString().c_str(),ios::in);
00700     if(!fs.is_open()) {
00701       fs.close();
00702       throw EvalException("File "+e[1].getString()+" does not exist");
00703     } 
00704     fs.close();
00705     d_vc->loadFile(e[1].getString(),
00706                    d_vc->getEM()->getInputLang(),
00707                    d_vc->getFlags()["interactive"].getBool());
00708     break;
00709   }
00710   case HELP:
00711     cout << "Use the -help command-line option for help." << endl;
00712     break;
00713   case DUMP_SIG:
00714   case DBG:
00715   case SUBSTITUTE:
00716   case GET_CHILD:
00717   case GET_TYPE:
00718   case CHECK_TYPE:
00719     throw EvalException("Unknown command: " + e.toString());
00720   default:
00721     d_vc->parseExpr(e);
00722     break;
00723   }
00724   TRACE_MSG("commands", "evaluateCommand => true }");
00725   return true;
00726 }
00727 
00728 
00729 void VCCmd::processCommands()
00730 {
00731   bool error(false);
00732   try {
00733     bool success(true);
00734     while(success) {
00735       try {
00736         success = evaluateNext();
00737       } catch(EvalException& e) {
00738         error= true;
00739         cerr << "*** Eval Error:\n  " << e << endl;
00740       }
00741     }
00742   }
00743   catch(Exception& e) { 
00744     cerr << "*** Fatal exception:\n" << e << endl;
00745     error= true;
00746   } catch(...) {
00747     cerr << "*** Unknown fatal exception caught" << endl;
00748     error= true;
00749   }
00750   if (error)
00751   {
00752     d_parser->printLocation(cerr);
00753     cerr << ": this is the location of the error" << endl;
00754   }    
00755 }

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