00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
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;
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
00087
00088
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
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
00147
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: {
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
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) {
00194 TRACE_MSG("commands", "** [commands] Define new constant");
00195
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: {
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
00225
00226
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;
00241 if(e.arity() == 5) {
00242
00243 Expr lambda(d_vc->listExpr("LAMBDA", e[2], e[4]));
00244
00245 newDecl = d_vc->listExpr("CONST", e[1], fnType, lambda);
00246 } else {
00247 newDecl = d_vc->listExpr("CONST", e[1], fnType);
00248 }
00249
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;
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
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: {
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: {
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
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: {
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;
00687 bool success = true;
00688 for(; i!=iend; ++i) {
00689 success = success && evaluateCommand(*i);
00690 }
00691 return success;
00692 }
00693 case INCLUDE: {
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 }