src/main/main.cpp

   1 /*********************                                                        */
   2 /*! \file main.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): barrett, dejan, taking
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Main driver for CVC4 executable
  15  **
  16  ** Main driver for CVC4 executable.
  17  **/
  18
  19 #include <cstdlib>
  20 #include <cstring>
  21 #include <fstream>
  22 #include <iostream>
  23 #include <new>
  24
  25 #include <stdio.h>
  26 #include <unistd.h>
  27
  28 #include "cvc4autoconfig.h"
  29 #include "main/main.h"
  30 #include "main/interactive_shell.h"
  31 #include "parser/parser.h"
  32 #include "parser/parser_builder.h"
  33 #include "parser/parser_exception.h"
  34 #include "expr/expr_manager.h"
  35 #include "smt/smt_engine.h"
  36 #include "expr/command.h"
  37 #include "util/Assert.h"
  38 #include "util/configuration.h"
  39 #include "util/options.h"
  40 #include "util/output.h"
  41 #include "util/result.h"
  42 #include "util/stats.h"
  43
  44 using namespace std;
  45 using namespace CVC4;
  46 using namespace CVC4::parser;
  47 using namespace CVC4::main;
  48
  49 int runCvc4(int argc, char* argv[]);
  50 void doCommand(SmtEngine&, Command*);
  51 void printUsage();
  52
  53 namespace CVC4 {
  54   namespace main {
  55     /** Global options variable */
  56     Options options;
  57
  58     /** Full argv[0] */
  59     const char *progPath;
  60
  61     /** Just the basename component of argv[0] */
  62     const char *progName;
  63
  64     /** A pointer to the StatisticsRegistry (the signal handlers need it) */
  65     CVC4::StatisticsRegistry* pStatistics;
  66   }
  67 }
  68
  69
  70 // no more % chars in here without being escaped; it's used as a
  71 // printf() format string
  72 const string usageMessage = "\
  73 usage: %s [options] [input-file]\n\
  74 \n\
  75 Without an input file, or with `-', CVC4 reads from standard input.\n\
  76 \n\
  77 CVC4 options:\n";
  78
  79 void printUsage() {
  80   stringstream ss;
  81   ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
  82       << endl
  83       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
  84       << endl
  85       << "CVC4 options:" << endl;
  86   Options::printUsage( ss.str(), *options.out );
  87 }
  88
  89 /**
  90  * CVC4's main() routine is just an exception-safe wrapper around CVC4.
  91  * Please don't construct anything here.  Even if the constructor is
  92  * inside the try { }, an exception during destruction can cause
  93  * problems.  That's why main() wraps runCvc4() in the first place.
  94  * Put everything in runCvc4().
  95  */
  96 int main(int argc, char* argv[]) {
  97   try {
  98     return runCvc4(argc, argv);
  99   } catch(OptionException& e) {
 100 #ifdef CVC4_COMPETITION_MODE
 101     *options.out << "unknown" << endl;
 102 #endif
 103     cerr << "CVC4 Error:" << endl << e << endl;
 104     printUsage();
 105     exit(1);
 106   } catch(Exception& e) {
 107 #ifdef CVC4_COMPETITION_MODE
 108     *options.out << "unknown" << endl;
 109 #endif
 110     *options.err << "CVC4 Error:" << endl << e << endl;
 111     if(options.statistics && pStatistics != NULL) {
 112       pStatistics->flushStatistics(*options.err);
 113     }
 114     exit(1);
 115   } catch(bad_alloc&) {
 116 #ifdef CVC4_COMPETITION_MODE
 117     *options.out << "unknown" << endl;
 118 #endif
 119     *options.err << "CVC4 ran out of memory." << endl;
 120     if(options.statistics && pStatistics != NULL) {
 121       pStatistics->flushStatistics(*options.err);
 122     }
 123     exit(1);
 124   } catch(...) {
 125 #ifdef CVC4_COMPETITION_MODE
 126     *options.out << "unknown" << endl;
 127 #endif
 128     *options.err << "CVC4 threw an exception of unknown type." << endl;
 129     exit(1);
 130   }
 131 }
 132
 133
 134 int runCvc4(int argc, char* argv[]) {
 135
 136   // Initialize the signal handlers
 137   cvc4_init();
 138
 139   progPath = argv[0];
 140
 141   // Parse the options
 142   int firstArgIndex = options.parseOptions(argc, argv);
 143
 144   progName = options.binary_name.c_str();
 145
 146   if( options.help ) {
 147     printUsage();
 148     exit(1);
 149   } else if( options.languageHelp ) {
 150     Options::printLanguageHelp(*options.out);
 151     exit(1);
 152   } else if( options.version ) {
 153     *options.out << Configuration::about().c_str() << flush;
 154     exit(0);
 155   }
 156
 157   segvNoSpin = options.segvNoSpin;
 158
 159   // If in competition mode, set output stream option to flush immediately
 160 #ifdef CVC4_COMPETITION_MODE
 161   *options.out << unitbuf;
 162 #endif
 163
 164   // We only accept one input file
 165   if(argc > firstArgIndex + 1) {
 166     throw Exception("Too many input files specified.");
 167   }
 168
 169   // If no file supplied we will read from standard input
 170   const bool inputFromStdin =
 171     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 172
 173   // if we're reading from stdin on a TTY, default to interactive mode
 174   if(!options.interactiveSetByUser) {
 175     options.interactive = inputFromStdin && isatty(fileno(stdin));
 176   }
 177
 178   // Determine which messages to show based on smtcomp_mode and verbosity
 179   if(Configuration::isMuzzledBuild()) {
 180     Debug.setStream(CVC4::null_os);
 181     Trace.setStream(CVC4::null_os);
 182     Notice.setStream(CVC4::null_os);
 183     Chat.setStream(CVC4::null_os);
 184     Message.setStream(CVC4::null_os);
 185     Warning.setStream(CVC4::null_os);
 186     Dump.setStream(CVC4::null_os);
 187   } else {
 188     if(options.verbosity < 2) {
 189       Chat.setStream(CVC4::null_os);
 190     }
 191     if(options.verbosity < 1) {
 192       Notice.setStream(CVC4::null_os);
 193     }
 194     if(options.verbosity < 0) {
 195       Message.setStream(CVC4::null_os);
 196       Warning.setStream(CVC4::null_os);
 197     }
 198   }
 199
 200   // Create the expression manager
 201   ExprManager exprMgr(options);
 202
 203   // Create the SmtEngine
 204   SmtEngine smt(&exprMgr);
 205
 206   // signal handlers need access
 207   pStatistics = smt.getStatisticsRegistry();
 208
 209   // Auto-detect input language by filename extension
 210   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 211
 212   ReferenceStat< const char* > s_statFilename("filename", filename);
 213   RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 214
 215   if(options.inputLanguage == language::input::LANG_AUTO) {
 216     if( inputFromStdin ) {
 217       // We can't do any fancy detection on stdin
 218       options.inputLanguage = language::input::LANG_CVC4;
 219     } else {
 220       unsigned len = strlen(filename);
 221       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 222         options.inputLanguage = language::input::LANG_SMTLIB_V2;
 223       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 224         options.inputLanguage = language::input::LANG_SMTLIB;
 225       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 226                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 227         options.inputLanguage = language::input::LANG_CVC4;
 228       }
 229     }
 230   }
 231
 232   if(options.outputLanguage == language::output::LANG_AUTO) {
 233     options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
 234   }
 235
 236   // Determine which messages to show based on smtcomp_mode and verbosity
 237   if(Configuration::isMuzzledBuild()) {
 238     Debug.setStream(CVC4::null_os);
 239     Trace.setStream(CVC4::null_os);
 240     Notice.setStream(CVC4::null_os);
 241     Chat.setStream(CVC4::null_os);
 242     Message.setStream(CVC4::null_os);
 243     Warning.setStream(CVC4::null_os);
 244     Dump.setStream(CVC4::null_os);
 245   } else {
 246     if(options.verbosity < 2) {
 247       Chat.setStream(CVC4::null_os);
 248     }
 249     if(options.verbosity < 1) {
 250       Notice.setStream(CVC4::null_os);
 251     }
 252     if(options.verbosity < 0) {
 253       Message.setStream(CVC4::null_os);
 254       Warning.setStream(CVC4::null_os);
 255     }
 256
 257     Debug.getStream() << Expr::setlanguage(options.outputLanguage);
 258     Trace.getStream() << Expr::setlanguage(options.outputLanguage);
 259     Notice.getStream() << Expr::setlanguage(options.outputLanguage);
 260     Chat.getStream() << Expr::setlanguage(options.outputLanguage);
 261     Message.getStream() << Expr::setlanguage(options.outputLanguage);
 262     Warning.getStream() << Expr::setlanguage(options.outputLanguage);
 263     Dump.getStream() << Expr::setlanguage(options.outputLanguage)
 264                      << Expr::setdepth(-1)
 265                      << Expr::printtypes(false);
 266   }
 267
 268   Parser* replayParser = NULL;
 269   if( options.replayFilename != "" ) {
 270     ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
 271
 272     if( options.replayFilename == "-") {
 273       if( inputFromStdin ) {
 274         throw OptionException("Replay file and input file can't both be stdin.");
 275       }
 276       replayParserBuilder.withStreamInput(cin);
 277     }
 278     replayParser = replayParserBuilder.build();
 279     options.replayStream = new Parser::ExprStream(replayParser);
 280   }
 281   if( options.replayLog != NULL ) {
 282     *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
 283   }
 284
 285   // Parse and execute commands until we are done
 286   Command* cmd;
 287   if( options.interactive ) {
 288     InteractiveShell shell(exprMgr, options);
 289     Message() << Configuration::getPackageName()
 290               << " " << Configuration::getVersionString();
 291     if(Configuration::isSubversionBuild()) {
 292       Message() << " [" << Configuration::getSubversionId() << "]";
 293     }
 294     Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 295               << " assertions:"
 296               << (Configuration::isAssertionBuild() ? "on" : "off")
 297               << endl;
 298     if(replayParser != NULL) {
 299       // have the replay parser use the declarations input interactively
 300       replayParser->useDeclarationsFrom(shell.getParser());
 301     }
 302     while((cmd = shell.readCommand())) {
 303       doCommand(smt,cmd);
 304       delete cmd;
 305     }
 306   } else {
 307     ParserBuilder parserBuilder(&exprMgr, filename, options);
 308
 309     if( inputFromStdin ) {
 310       parserBuilder.withStreamInput(cin);
 311     }
 312
 313     Parser *parser = parserBuilder.build();
 314     if(replayParser != NULL) {
 315       // have the replay parser use the file's declarations
 316       replayParser->useDeclarationsFrom(parser);
 317     }
 318     while((cmd = parser->nextCommand())) {
 319       doCommand(smt, cmd);
 320       delete cmd;
 321     }
 322     // Remove the parser
 323     delete parser;
 324   }
 325
 326   if( options.replayStream != NULL ) {
 327     // this deletes the expression parser too
 328     delete options.replayStream;
 329     options.replayStream = NULL;
 330   }
 331
 332   string result = smt.getInfo(":status").getValue();
 333   int returnValue;
 334
 335   if(result == "sat") {
 336     returnValue = 10;
 337   } else if(result == "unsat") {
 338     returnValue = 20;
 339   } else {
 340     returnValue = 0;
 341   }
 342
 343 #ifdef CVC4_COMPETITION_MODE
 344   // exit, don't return
 345   // (don't want destructors to run)
 346   exit(returnValue);
 347 #endif
 348
 349   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 350   RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
 351
 352   if(options.statistics) {
 353     smt.getStatisticsRegistry()->flushStatistics(*options.err);
 354   }
 355
 356   return returnValue;
 357 }
 358
 359 /** Executes a command. Deletes the command after execution. */
 360 void doCommand(SmtEngine& smt, Command* cmd) {
 361   if( options.parseOnly ) {
 362     return;
 363   }
 364
 365   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
 366   if(seq != NULL) {
 367     for(CommandSequence::iterator subcmd = seq->begin();
 368         subcmd != seq->end();
 369         ++subcmd) {
 370       doCommand(smt, *subcmd);
 371     }
 372   } else {
 373     if(options.verbosity > 0) {
 374       *options.out << "Invoking: " << *cmd << endl;
 375     }
 376
 377     if(options.verbosity >= 0) {
 378       cmd->invoke(&smt, *options.out);
 379     } else {
 380       cmd->invoke(&smt);
 381     }
 382   }
 383 }