CVC3

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