CVC3 2.2
|
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, bool calledFromParser) 00033 : d_vc(vc), d_parser(parser), d_name_of_cur_ctxt("DEFAULT"), 00034 d_calledFromParser(calledFromParser) 00035 { 00036 d_map[d_name_of_cur_ctxt.c_str()] = d_vc->getCurrentContext(); 00037 } 00038 00039 VCCmd::~VCCmd() { } 00040 00041 void VCCmd::findAxioms(const Expr& e, ExprMap<bool>& skolemAxioms, 00042 ExprMap<bool>& visited) { 00043 if(visited.count(e)>0) 00044 return; 00045 else visited[e] = true; 00046 if(e.isSkolem()) { 00047 skolemAxioms.insert(e.getExistential(), true); 00048 return; 00049 } 00050 if(e.isClosure()) { 00051 findAxioms(e.getBody(), skolemAxioms, visited); 00052 } 00053 if(e.arity()>0) { 00054 Expr::iterator end = e.end(); 00055 for(Expr::iterator i = e.begin(); i!=end; ++i) 00056 findAxioms(*i, skolemAxioms, visited); 00057 } 00058 00059 } 00060 00061 Expr VCCmd::skolemizeAx(const Expr& e) 00062 { 00063 vector<Expr>vars; 00064 const vector<Expr>boundVars = e.getVars(); 00065 for(unsigned int i=0; i<boundVars.size(); i++) { 00066 Expr skolV(e.skolemExpr(i)); 00067 vars.push_back(skolV); 00068 } 00069 Expr sub = e.getBody().substExpr(boundVars, vars); 00070 return e.iffExpr(sub); 00071 } 00072 00073 bool VCCmd::evaluateNext() 00074 { 00075 readAgain: 00076 if(d_parser->done()) return false; // No more commands 00077 Expr e; 00078 try { 00079 TRACE_MSG("commands", "** [commands] Parsing command..."); 00080 e = d_parser->next(); 00081 TRACE("commands verbose", "evaluateNext(", e, ")"); 00082 } 00083 catch(Exception& e) { 00084 cerr << "*** " << e << endl; 00085 IF_DEBUG(++(debugger.counter("parse errors"));) 00086 } 00087 // The parser may return a Null Expr in case of parse errors or end 00088 // of file. The right thing to do is to ignore it and repeat 00089 // reading. 00090 if(e.isNull()) { 00091 TRACE_MSG("commands", "** [commands] Null command; read again"); 00092 goto readAgain; 00093 } 00094 00095 return evaluateCommand(e); 00096 } 00097 00098 void VCCmd::reportResult(QueryResult qres, bool checkingValidity) 00099 { 00100 if (d_vc->getFlags()["printResults"].getBool()) { 00101 if (d_vc->getEM()->getOutputLang() == SMTLIB_LANG) { 00102 switch (qres) { 00103 case VALID: 00104 cout << "unsat" << endl; 00105 break; 00106 case INVALID: 00107 cout << "sat" << endl; 00108 break; 00109 case ABORT: 00110 case UNKNOWN: 00111 cout << "unknown" << endl; 00112 break; 00113 default: 00114 FatalAssert(false, "Unexpected case"); 00115 } 00116 } 00117 else { 00118 switch (qres) { 00119 case VALID: 00120 cout << (checkingValidity ? "Valid." : "Unsatisfiable.") << endl; 00121 break; 00122 case INVALID: 00123 cout << (checkingValidity ? "Invalid." : "Satisfiable.") << endl; 00124 break; 00125 case ABORT: 00126 cout << "Unknown: resource limit exhausted." << endl; 00127 break; 00128 case UNKNOWN: { 00129 // Vector of reasons in case of incomplete result 00130 vector<string> reasons; 00131 IF_DEBUG(bool b =) d_vc->incomplete(reasons); 00132 DebugAssert(b, "Expected incompleteness"); 00133 cout << "Unknown.\n\n"; 00134 cout << "CVC3 was incomplete in this example due to:"; 00135 for(vector<string>::iterator i=reasons.begin(), iend=reasons.end(); 00136 i!=iend; ++i) 00137 cout << "\n * " << (*i); 00138 cout << endl << endl; 00139 break; 00140 } 00141 default: 00142 FatalAssert(false, "Unexpected case"); 00143 } 00144 } 00145 cout << flush; 00146 } 00147 //d_vc->printStatistics(); 00148 // exit(0); 00149 } 00150 00151 00152 void VCCmd::printModel() 00153 { 00154 ExprMap<Expr> m; 00155 d_vc->getConcreteModel(m); 00156 00157 cout << "Current scope level is " << d_vc->scopeLevel() << "." << endl; 00158 ExprMap<Expr>::iterator it = m.begin(), end = m.end(); 00159 if(it == end) 00160 cout << " Did not find concrete model for any vars" << endl; 00161 else { 00162 cout << "%Satisfiable Variable Assignment: % \n"; 00163 for(; it!= end; it++) { 00164 Expr eq; 00165 if(it->first.getType().isBool()) { 00166 DebugAssert((it->second).isBoolConst(), 00167 "Bad variable assignement: e = "+(it->first).toString() 00168 +"\n\n val = "+(it->second).toString()); 00169 if((it->second).isTrue()) 00170 eq = it->first; 00171 else 00172 eq = !(it->first); 00173 } 00174 else 00175 eq = (it->first).eqExpr(it->second); 00176 cout << Expr(ASSERT, eq) << "\n"; 00177 } 00178 } 00179 } 00180 00181 00182 // For debugging: there are missing cases: user-defined types, symbols inside of quantifiers, etc. 00183 void VCCmd::printSymbols(Expr e, ExprMap<bool>& cache) 00184 { 00185 if (cache.find(e) != cache.end()) return; 00186 switch (e.getKind()) { 00187 case SKOLEM_VAR: 00188 case UCONST: { 00189 cout << e << " : "; 00190 ExprStream os(d_vc->getEM()); 00191 os.dagFlag(false); 00192 os << e.getType().getExpr(); 00193 cout << ";" << endl; 00194 break; 00195 } 00196 case APPLY: { 00197 Expr op = e.getOpExpr(); 00198 if ((op.getKind() == UFUNC) && (cache.find(op) == cache.end())) { 00199 cout << op << " : "; 00200 ExprStream os(d_vc->getEM()); 00201 os.dagFlag(false); 00202 os << op.getType().getExpr(); 00203 cout << ";" << endl; 00204 cache[op] = true; 00205 } 00206 // fall through 00207 } 00208 default: { 00209 Expr::iterator i = e.begin(), iend = e.end(); 00210 for (; i != iend; ++i) { 00211 printSymbols(*i, cache); 00212 } 00213 break; 00214 } 00215 } 00216 cache[e] = true; 00217 } 00218 00219 00220 bool debug_skolem = false; 00221 00222 00223 void VCCmd::printCounterExample() 00224 { 00225 vector<Expr> assertions; 00226 ExprMap<bool> skolemAxioms; 00227 ExprMap<bool> visited; 00228 00229 d_vc->getCounterExample(assertions); 00230 00231 // get variable information 00232 ExprMap<bool> cache; 00233 unsigned i; 00234 for (i = 0; i < assertions.size(); i++) { 00235 printSymbols(assertions[i], cache); 00236 } 00237 00238 cout << "% Current scope level is " << d_vc->scopeLevel() << "." << endl; 00239 if (assertions.size() == 0) { 00240 cout << "% There are no assertions\n"; 00241 } else { 00242 00243 cout << "% Assertions which make the QUERY invalid:\n"; 00244 00245 for (i = 0; i < assertions.size(); i++) { 00246 cout << Expr(ASSERT, assertions[i]) << "\n"; 00247 findAxioms(assertions[i], skolemAxioms, visited); 00248 } 00249 00250 if (debug_skolem) { 00251 cout << "% Including skolemization axioms:\n"; 00252 00253 ExprMap<bool>::iterator end = skolemAxioms.end(); 00254 for(ExprMap<bool>::iterator it = skolemAxioms.begin(); it!=end; it++) 00255 cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl; 00256 } 00257 } 00258 cout << endl; 00259 } 00260 00261 00262 bool VCCmd::evaluateCommand(const Expr& e0) 00263 { 00264 TRACE("commands", "evaluateCommand(", e0.toString(PRESENTATION_LANG), ") {"); 00265 Expr e(e0); 00266 if(e.getKind() != RAW_LIST || e.arity() == 0 || e[0].getKind() != ID) 00267 throw EvalException("Invalid command: "+e.toString()); 00268 const string& kindName = e[0][0].getString(); 00269 int kind = d_vc->getEM()->getKind(kindName); 00270 if(kind == NULL_KIND) 00271 throw EvalException("Unknown command: "+e.toString()); 00272 switch(kind) { 00273 case CONST: { // (CONST (id_1 ... id_n) type) or (CONST id type) 00274 if(e.arity() == 3) { 00275 Type t(d_vc->parseExpr(e[2])); 00276 vector<Expr> vars; 00277 if(e[1].getKind() == RAW_LIST) 00278 vars = e[1].getKids(); 00279 else 00280 vars.push_back(e[1]); 00281 for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); i!=iend; ++i) { 00282 if((*i).getKind() != ID) 00283 throw EvalException("Constant name must be an identifier: " 00284 +i->toString()); 00285 } 00286 if (t.isFunction()) { 00287 for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); 00288 i!=iend; ++i) { 00289 Op op = d_vc->createOp((*i)[0].getString(), t); 00290 TRACE("commands", "evaluateNext: declare new uninterpreted function: ", 00291 op, ""); 00292 } 00293 } 00294 else { 00295 for(vector<Expr>::iterator i=vars.begin(), iend=vars.end(); 00296 i!=iend; ++i) { 00297 // Add to variable list 00298 Expr v = d_vc->varExpr((*i)[0].getString(), t); 00299 TRACE_MSG("commands", "** [commands] Declare new variable"); 00300 TRACE("commands verbose", "evaluateNext: declare new UCONST: ", 00301 v, ""); 00302 } 00303 } 00304 } else if(e.arity() == 4) { // Constant definition (CONST id type def) 00305 TRACE_MSG("commands", "** [commands] Define new constant"); 00306 // Set the type for later typechecking 00307 DebugAssert(e[1].getKind() == ID, "Expected ID kind"); 00308 Type t(d_vc->parseExpr(e[2])); 00309 Expr def(d_vc->parseExpr(e[3])); 00310 00311 if(t.isFunction()) { 00312 d_vc->createOp(e[1][0].getString(), t, def); 00313 TRACE("commands verbose", "evaluateNext: define new function: ", 00314 e[1][0].getString(), ""); 00315 } else { 00316 d_vc->varExpr(e[1][0].getString(), t, def); 00317 TRACE("commands verbose", "evaluateNext: define new variable: ", 00318 e[1][0].getString(), ""); 00319 } 00320 } else 00321 throw EvalException("Wrong number of arguments in CONST: "+e.toString()); 00322 break; 00323 } 00324 case DEFUN: { // (DEFUN name ((x y z type1) ... ) resType [ body ]) 00325 if(e.arity() != 5 && e.arity() != 4) 00326 throw EvalException 00327 ("DEFUN requires 3 or 4 arguments:" 00328 " (DEFUN f (args) type [ body ]):\n\n " 00329 +e.toString()); 00330 if(e[2].getKind() != RAW_LIST) 00331 throw EvalException 00332 ("2nd argument of DEFUN must be a list of arguments:\n\n " 00333 +e.toString()); 00334 00335 // Build a CONST declaration and parse it recursively 00336 00337 // Build the function type 00338 vector<Expr> argTps; 00339 for(Expr::iterator i=e[2].begin(), iend=e[2].end(); i!=iend; ++i) { 00340 if(i->getKind() != RAW_LIST || i->arity() < 2) 00341 throw EvalException 00342 ("DEFUN: bad argument declaration:\n\n "+i->toString() 00343 +"\n\nIn the following statement:\n\n " 00344 +e.toString()); 00345 Expr tp((*i)[i->arity()-1]); 00346 for(int j=0, jend=i->arity()-1; j<jend; ++j) 00347 argTps.push_back(tp); 00348 } 00349 argTps.push_back(e[3]); 00350 Expr fnType = d_vc->listExpr("ARROW", argTps); 00351 Expr newDecl; // The resulting transformed declaration 00352 if(e.arity() == 5) { 00353 // Build the LAMBDA expression 00354 Expr lambda(d_vc->listExpr("LAMBDA", e[2], e[4])); 00355 // Construct the (CONST name fnType lambda) declaration 00356 newDecl = d_vc->listExpr("CONST", e[1], fnType, lambda); 00357 } else { 00358 newDecl = d_vc->listExpr("CONST", e[1], fnType); 00359 } 00360 // Parse the new declaration 00361 return evaluateCommand(newDecl); 00362 break; 00363 } 00364 case TYPEDEF: { 00365 if (e.arity() == 2) { 00366 // Datatype command 00367 DebugAssert(e.arity() == 2, "Bad TYPEDEF"); 00368 Expr res = d_vc->parseExpr(e[1]); 00369 // convert res to vectors 00370 00371 Expr eNames = res[0]; 00372 Expr eCons = res[1]; 00373 Expr eSel = res[2]; 00374 Expr eTypes = res[3]; 00375 00376 vector<string> names; 00377 vector<vector<string> > constructors(eNames.arity()); 00378 vector<vector<vector<string> > > selectors(eNames.arity()); 00379 vector<vector<vector<Expr> > > types(eNames.arity()); 00380 00381 int i, j, k; 00382 for (i = 0; i < eNames.arity(); ++i) { 00383 names.push_back(eNames[i].getString()); 00384 selectors[i].resize(eSel[i].arity()); 00385 types[i].resize(eTypes[i].arity()); 00386 for (j = 0; j < eCons[i].arity(); ++j) { 00387 constructors[i].push_back(eCons[i][j].getString()); 00388 for (k = 0; k < eSel[i][j].arity(); ++k) { 00389 selectors[i][j].push_back(eSel[i][j][k].getString()); 00390 types[i][j].push_back(eTypes[i][j][k]); 00391 } 00392 } 00393 } 00394 00395 vector<Type> returnTypes; 00396 d_vc->dataType(names, constructors, selectors, types, returnTypes); 00397 break; 00398 } 00399 DebugAssert(e.arity() == 3, "Bad TYPEDEF"); 00400 Expr def(d_vc->parseExpr(e[2])); 00401 Type t = d_vc->createType(e[1][0].getString(), def); 00402 TRACE("commands", "evaluateNext: declare new TYPEDEF: ", t, ""); 00403 } 00404 break; 00405 case TYPE: { 00406 if(e.arity() < 2) 00407 throw EvalException("Bad TYPE declaration: "+e.toString()); 00408 Expr::iterator i=e.begin(), iend=e.end(); 00409 ++i; // Skip "TYPE" symbol 00410 for(; i!=iend; ++i) { 00411 if(i->getKind() != ID) 00412 throw EvalException("Type name must be an identifier: "+i->toString()); 00413 Type t = d_vc->createType((*i)[0].getString()); 00414 TRACE("commands", "evaluateNext: declare new TYPEDECL: ", t, ""); 00415 } 00416 } 00417 break; 00418 case ASSERT: { 00419 if(e.arity() != 2) 00420 throw EvalException("ASSERT requires exactly one argument, but is given " 00421 +int2string(e.arity()-1)+":\n "+e.toString()); 00422 TRACE_MSG("commands", "** [commands] Asserting formula"); 00423 d_vc->assertFormula(d_vc->parseExpr(e[1])); 00424 break; 00425 } 00426 case QUERY: { 00427 if(e.arity() != 2) 00428 throw EvalException("QUERY requires exactly one argument, but is given " 00429 +int2string(e.arity()-1)+":\n "+e.toString()); 00430 TRACE_MSG("commands", "** [commands] Query formula"); 00431 QueryResult qres = d_vc->query(d_vc->parseExpr(e[1])); 00432 if (qres == UNKNOWN && d_vc->getFlags()["unknown-check-model"].getBool()) 00433 qres = d_vc->tryModelGeneration(); 00434 reportResult(qres); 00435 if (qres == INVALID) { 00436 if (d_vc->getFlags()["counterexample"].getBool()) { 00437 printCounterExample(); 00438 } 00439 if (d_vc->getFlags()["model"].getBool()) { 00440 printModel(); 00441 } 00442 } 00443 break; 00444 } 00445 case CHECKSAT: { 00446 QueryResult qres; 00447 TRACE_MSG("commands", "** [commands] CheckSat"); 00448 if (e.arity() == 1) { 00449 qres = d_vc->checkUnsat(d_vc->trueExpr()); 00450 } 00451 else if (e.arity() == 2) { 00452 qres = d_vc->checkUnsat(d_vc->parseExpr(e[1])); 00453 } 00454 else { 00455 throw EvalException("CHECKSAT requires no more than one argument, but is given " 00456 +int2string(e.arity()-1)+":\n "+e.toString()); 00457 } 00458 if (qres == UNKNOWN && !d_vc->getFlags()["translate"].getBool() && d_vc->getFlags()["unknown-check-model"].getBool()) 00459 qres = d_vc->tryModelGeneration(); 00460 reportResult(qres, false); 00461 if (qres == SATISFIABLE) { 00462 if (d_vc->getFlags()["counterexample"].getBool()) { 00463 printCounterExample(); 00464 } 00465 if (d_vc->getFlags()["model"].getBool()) { 00466 printModel(); 00467 } 00468 } 00469 // {//for debug only by yeting 00470 // Proof p = d_vc->getProof(); 00471 // if (d_vc->getFlags()["printResults"].getBool()) { 00472 // cout << p << endl; 00473 // cout << flush; 00474 // } 00475 // } 00476 00477 00478 break; 00479 } 00480 case CONTINUE: { 00481 if (e.arity() != 1) { 00482 throw EvalException("CONTINUE takes no arguments"); 00483 } 00484 TRACE_MSG("commands", "** [commands] Continue"); 00485 QueryResult qres = d_vc->checkContinue(); 00486 if (d_vc->getFlags()["printResults"].getBool()) { 00487 switch (qres) { 00488 case VALID: 00489 cout << "No more models found." << endl; 00490 break; 00491 case INVALID: 00492 cout << "Model found" << endl; 00493 break; 00494 case ABORT: 00495 cout << "Unknown: resource limit exhausted." << endl; 00496 break; 00497 case UNKNOWN: { 00498 // Vector of reasons in case of incomplete result 00499 vector<string> reasons; 00500 IF_DEBUG(bool b =) d_vc->incomplete(reasons); 00501 DebugAssert(b, "Expected incompleteness"); 00502 cout << "Unknown.\n\n"; 00503 cout << "CVC3 was incomplete in this example due to:"; 00504 for(vector<string>::iterator i=reasons.begin(), iend=reasons.end(); 00505 i!=iend; ++i) 00506 cout << "\n * " << (*i); 00507 cout << endl << endl; 00508 break; 00509 } 00510 default: 00511 FatalAssert(false, "Unexpected case"); 00512 } 00513 cout << flush; 00514 } 00515 break; 00516 } 00517 case RESTART: { 00518 if(e.arity() != 2) 00519 throw EvalException("RESTART requires exactly one argument, but is given " 00520 +int2string(e.arity()-1)+":\n "+e.toString()); 00521 TRACE_MSG("commands", "** [commands] Restart formula"); 00522 QueryResult qres = d_vc->restart(d_vc->parseExpr(e[1])); 00523 reportResult(qres); 00524 if (qres == INVALID) { 00525 if (d_vc->getFlags()["counterexample"].getBool()) { 00526 printCounterExample(); 00527 } 00528 if (d_vc->getFlags()["model"].getBool()) { 00529 printModel(); 00530 } 00531 } 00532 break; 00533 } 00534 case TRANSFORM: { 00535 if(e.arity() != 2) 00536 throw EvalException 00537 ("TRANSFORM requires exactly one argument, but is given " 00538 +int2string(e.arity()-1)+":\n "+e.toString()); 00539 TRACE_MSG("commands", "** [commands] Transforming expression"); 00540 Expr ee = d_vc->parseExpr(e[1]); 00541 e = d_vc->simplify(ee); 00542 if (d_vc->getFlags()["printResults"].getBool()) d_vc->printExpr(e); 00543 break; 00544 } 00545 case PRINT: 00546 if(e.arity() != 2) 00547 throw EvalException 00548 ("PRINT requires exactly one argument, but is given " 00549 +int2string(e.arity()-1)+":\n "+e.toString()); 00550 d_vc->printExpr(d_vc->parseExpr(e[1])); 00551 break; 00552 case PUSH: 00553 case POP: 00554 case PUSH_SCOPE: 00555 case POP_SCOPE: { 00556 int arg; 00557 if (e.arity() == 1) arg = 1; 00558 else { 00559 DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR, 00560 "Bad argument to "+kindName); 00561 arg = e[1].getRational().getInt(); 00562 if(arg <= 0) 00563 throw EvalException("Argument to PUSH or POP is <= 0"); 00564 } 00565 if (kind == PUSH) { 00566 for (int i = 0; i < arg; i++) { 00567 d_vc->push(); 00568 } 00569 } 00570 else if (kind == POP) { 00571 if(arg > d_vc->stackLevel()) 00572 throw EvalException("Argument to POP is out of range:\n" 00573 " current stack level = " 00574 +int2string(d_vc->stackLevel()) 00575 +"\n argument = " 00576 +int2string(arg)); 00577 for (int i = 0; i < arg; i++) { 00578 d_vc->pop(); 00579 } 00580 } 00581 else if (kind == PUSH_SCOPE) { 00582 for (int i = 0; i < arg; i++) { 00583 d_vc->pushScope(); 00584 } 00585 } 00586 else if (kind == POP_SCOPE) { 00587 if(arg >= d_vc->scopeLevel()) 00588 throw EvalException("Argument to POP_SCOPE is out of range:\n" 00589 " current scope = " 00590 +int2string(d_vc->scopeLevel()) 00591 +"\n argument = " 00592 +int2string(arg)); 00593 for (int i = 0; i < arg; i++) { 00594 d_vc->popScope(); 00595 } 00596 } 00597 break; 00598 } 00599 case POPTO: 00600 case POPTO_SCOPE: { 00601 int arg; 00602 if (e.arity() == 1) arg = 0; 00603 else { 00604 DebugAssert(e.arity() == 2 && e[1].getKind() == RATIONAL_EXPR, 00605 "Bad argument to "+kindName); 00606 arg = e[1].getRational().getInt(); 00607 } 00608 if (kind == POPTO) { 00609 d_vc->popto(arg); 00610 } 00611 else { 00612 d_vc->poptoScope(arg); 00613 } 00614 break; 00615 } 00616 case RESET: { 00617 throw ResetException(); 00618 break; 00619 } 00620 case WHERE: 00621 case ASSERTIONS: 00622 case ASSUMPTIONS: 00623 { 00624 vector<Expr> assertions; 00625 ExprMap<bool> skolemAxioms; 00626 ExprMap<bool> visited; 00627 00628 d_vc->getAssumptions(assertions); 00629 00630 if (d_vc->getFlags()["printResults"].getBool()) { 00631 cout << "Current stack level is " << d_vc->stackLevel() 00632 << " (scope " << d_vc->scopeLevel() << ")." << endl; 00633 if (assertions.size() == 0) { 00634 cout << "% No active assumptions\n"; 00635 } else { 00636 cout << "% Active assumptions:\n"; 00637 for (unsigned i = 0; i < assertions.size(); i++) { 00638 cout << "ASSERT " << assertions[i] << ";" << endl; 00639 findAxioms(assertions[i], skolemAxioms, visited); 00640 } 00641 ExprMap<bool>::iterator it = skolemAxioms.begin(); 00642 ExprMap<bool>::iterator end = skolemAxioms.end(); 00643 if (it != end) { 00644 cout << "% Skolemization axioms" << endl; 00645 for(; it!=end; ++it) 00646 cout << "ASSERT " << skolemizeAx((*it).first) << ";" << endl; 00647 } 00648 } 00649 cout << endl; 00650 } 00651 break; 00652 } 00653 case COUNTEREXAMPLE: { 00654 if (d_vc->getFlags()["printResults"].getBool()) { 00655 printCounterExample(); 00656 } 00657 break; 00658 } 00659 case COUNTERMODEL: { 00660 if (d_vc->getFlags()["printResults"].getBool()) { 00661 try { 00662 printModel(); 00663 } catch (Exception& e) { 00664 throw EvalException(e.toString()); 00665 } 00666 } 00667 break; 00668 } 00669 case TRACE: { // Set a trace flag 00670 #ifdef _CVC3_DEBUG_MODE 00671 if(e.arity() != 2) 00672 throw EvalException("TRACE takes exactly one string argument"); 00673 if(!e[1].isString()) 00674 throw EvalException("TRACE requires a string argument"); 00675 debugger.traceFlag(e[1].getString()) = true; 00676 #endif 00677 } 00678 break; 00679 case UNTRACE: { // Unset a trace flag 00680 #ifdef _CVC3_DEBUG_MODE 00681 if(e.arity() != 2) 00682 throw EvalException("UNTRACE takes exactly one string argument"); 00683 if(!e[1].isString()) 00684 throw EvalException("UNTRACE requires a string argument"); 00685 debugger.traceFlag(e[1].getString()) = false; 00686 #endif 00687 } 00688 break; 00689 case OPTION: { 00690 if(e.arity() != 3) 00691 throw EvalException("OPTION takes exactly two arguments " 00692 "(name and value of a flag)"); 00693 if(!e[1].isString()) 00694 throw EvalException("OPTION: flag name must be a string"); 00695 CLFlags& flags = d_vc->getFlags(); 00696 string name(e[1].getString()); 00697 vector<string> names; 00698 size_t n = flags.countFlags(name, names); 00699 if(n != 1) 00700 throw EvalException("OPTION: found "+int2string(n) 00701 +" flags matching "+name 00702 +".\nThe flag name must uniquely resolve."); 00703 name = names[0]; 00704 const CLFlag& flag(flags[name]); 00705 // If the flag is set on the command line, ignore it 00706 if(flag.modified()) break; 00707 switch(flag.getType()) { 00708 case CLFLAG_BOOL: 00709 if(!(e[2].isRational() && e[2].getRational().isInteger())) 00710 throw EvalException("OPTION: flag "+name 00711 +" expects a boolean value (0 or 1"); 00712 flags.setFlag(name, e[2].getRational().getInt() != 0); 00713 break; 00714 case CLFLAG_INT: 00715 if(!(e[2].isRational() && e[2].getRational().isInteger())) 00716 throw EvalException("OPTION: flag "+name+" expects an integer value"); 00717 flags.setFlag(name, e[2].getRational().getInt()); 00718 break; 00719 case CLFLAG_STRING: 00720 if(!e[2].isString()) 00721 throw EvalException("OPTION: flag "+name+" expects a string value"); 00722 flags.setFlag(name, e[2].getString()); 00723 break; 00724 default: 00725 throw EvalException("OPTION: the type of flag "+name 00726 +" is not supported by the OPTION commnand"); 00727 break; 00728 } 00729 d_vc->reprocessFlags(); 00730 } 00731 break; 00732 case DUMP_PROOF: { 00733 Proof p = d_vc->getProof(); 00734 if (d_vc->getFlags()["printResults"].getBool()) { 00735 cout << p << endl; 00736 cout << flush; 00737 } 00738 break; 00739 } 00740 case DUMP_ASSUMPTIONS: { // Assumption tracking 00741 vector<Expr> assertions; 00742 d_vc->getAssumptionsUsed(assertions); 00743 00744 if (d_vc->getFlags()["printResults"].getBool()) { 00745 if(assertions.size() == 0) { 00746 cout << "% No relevant assumptions\n"; 00747 } else { 00748 cout << "% Relevant assumptions:\n"; 00749 for (unsigned i = 0; i < assertions.size(); i++) { 00750 cout << Expr(ASSERT, assertions[i]) << "\n"; 00751 } 00752 } 00753 cout << endl << flush; 00754 } 00755 break; 00756 } 00757 case DUMP_TCC: { 00758 const Expr& tcc = d_vc->getTCC(); 00759 00760 if (d_vc->getFlags()["printResults"].getBool()) { 00761 if(tcc.isNull()) 00762 cout << "% No TCC is avaialble" << endl; 00763 else 00764 cout << "% TCC for the last declaration, ASSERT, or QUERY:\n\n" 00765 << tcc << endl; 00766 } 00767 break; 00768 } 00769 case DUMP_TCC_ASSUMPTIONS: { 00770 vector<Expr> assertions; 00771 d_vc->getAssumptionsTCC(assertions); 00772 if (d_vc->getFlags()["printResults"].getBool()) { 00773 if(assertions.size() == 0) { 00774 cout << "% No relevant assumptions\n"; 00775 } else { 00776 cout << "% Relevant assumptions for the last TCC:\n"; 00777 for (unsigned i = 0; i < assertions.size(); i++) { 00778 cout << Expr(ASSERT, assertions[i]) << "\n"; 00779 } 00780 } 00781 cout << endl << flush; 00782 } 00783 break; 00784 } 00785 case DUMP_TCC_PROOF: { 00786 const Proof& tcc = d_vc->getProofTCC(); 00787 if (d_vc->getFlags()["printResults"].getBool()) { 00788 if(tcc.isNull()) 00789 cout << "% No TCC is avaialble" << endl; 00790 else 00791 cout << "% Proof of TCC for the last declaration, ASSERT, or QUERY:\n\n" 00792 << tcc << endl; 00793 } 00794 break; 00795 } 00796 case DUMP_CLOSURE: { 00797 const Expr& cl = d_vc->getClosure(); 00798 if (d_vc->getFlags()["printResults"].getBool()) { 00799 if(cl.isNull()) 00800 cout << "% No closure is avaialble" << endl; 00801 else 00802 cout << "% Closure for the last QUERY:\n\n" << cl << endl; 00803 } 00804 break; 00805 } 00806 case DUMP_CLOSURE_PROOF: { 00807 const Proof& cl = d_vc->getProofClosure(); 00808 if (d_vc->getFlags()["printResults"].getBool()) { 00809 if(cl.isNull()) 00810 cout << "% No closure is avaialble" << endl; 00811 else 00812 cout << "% Proof of closure for the last QUERY:\n\n" << cl << endl; 00813 } 00814 break; 00815 } 00816 case ECHO: 00817 if(e.arity() != 2) 00818 throw EvalException("ECHO: wrong number of arguments: " 00819 + e.toString()); 00820 if(!e[1].isString()) 00821 throw EvalException("ECHO: the argument must be a string: " 00822 +e.toString()); 00823 if (d_vc->getFlags()["printResults"].getBool()) { 00824 cout << e[1].getString(); 00825 cout << endl << flush; 00826 } 00827 break; 00828 case SEQ: { 00829 Expr::iterator i=e.begin(), iend=e.end(); 00830 ++i; // Skip "SEQ" symbol 00831 bool success = true; 00832 for(; i!=iend; ++i) { 00833 try { 00834 success = success && evaluateCommand(*i); 00835 } catch(ResetException& e) { 00836 if (++i == iend) throw e; 00837 throw EvalException("RESET can only be the last command in a sequence"); 00838 } 00839 } 00840 return success; 00841 } 00842 case ARITH_VAR_ORDER: { 00843 if (e.arity() <= 2) 00844 throw EvalException("ARITH_VAR_ORDER takes at least two arguments"); 00845 Expr smaller; 00846 Expr bigger = d_vc->parseExpr(e[1]); 00847 for (int i = 2; i < e.arity(); i ++) { 00848 smaller = bigger; 00849 bigger = d_vc->parseExpr(e[i]); 00850 if (!d_vc->addPairToArithOrder(smaller, bigger)) 00851 throw EvalException("ARITH_VAR_ORDER only takes arithmetic terms"); 00852 } 00853 return true; 00854 } 00855 case INCLUDE: { // read in the specified file 00856 if(e.arity() != 2) 00857 throw EvalException("INCLUDE takes exactly one string argument"); 00858 if(!e[1].isString()) 00859 throw EvalException("INCLUDE requires a string argument"); 00860 ifstream fs; 00861 fs.open(e[1].getString().c_str(),ios::in); 00862 if(!fs.is_open()) { 00863 fs.close(); 00864 throw EvalException("File "+e[1].getString()+" does not exist"); 00865 } 00866 fs.close(); 00867 d_vc->loadFile(e[1].getString(), 00868 d_vc->getEM()->getInputLang(), 00869 d_vc->getFlags()["interactive"].getBool(), 00870 true /* nested call */); 00871 break; 00872 } 00873 case HELP: 00874 cout << "Use the -help command-line option for help." << endl; 00875 break; 00876 case DUMP_SIG: 00877 case DBG: 00878 case SUBSTITUTE: 00879 case GET_CHILD: 00880 case GET_TYPE: 00881 case CHECK_TYPE: 00882 case FORGET: 00883 case CALL: 00884 default: 00885 throw EvalException("Unknown command: " + e.toString()); 00886 break; 00887 } 00888 TRACE_MSG("commands", "evaluateCommand => true }"); 00889 return true; 00890 } 00891 00892 00893 void VCCmd::processCommands() 00894 { 00895 bool error(false); 00896 try { 00897 bool success(true); 00898 while(success) { 00899 try { 00900 success = evaluateNext(); 00901 } catch (ResetException& e) { 00902 if (d_calledFromParser) { 00903 throw EvalException("RESET not supported within INCLUDEd file"); 00904 } 00905 d_parser->reset(); 00906 d_vc->reset(); 00907 success = true; 00908 } catch (EvalException& e) { 00909 error= true; 00910 cerr << "*** Eval Error:\n " << e << endl; 00911 } 00912 } 00913 00914 } 00915 00916 catch(Exception& e) { 00917 cerr << "*** Fatal exception:\n" << e << endl; 00918 error= true; 00919 } catch(...) { 00920 cerr << "*** Unknown fatal exception caught" << endl; 00921 error= true; 00922 } 00923 00924 if (error) 00925 { 00926 d_parser->printLocation(cerr); 00927 cerr << ": this is the location of the error" << endl; 00928 } 00929 }