src/main/driver.cpp

   1 /*********************                                                        */
   2 /*! \file driver.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, 2012  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 Driver for (sequential) CVC4 executable
  15  **
  16  ** Driver for (sequential) 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/dump.h"
  42 #include "util/result.h"
  43 #include "util/stats.h"
  44
  45 using namespace std;
  46 using namespace CVC4;
  47 using namespace CVC4::parser;
  48 using namespace CVC4::main;
  49
  50 static bool doCommand(SmtEngine&, Command*, Options&);
  51
  52 namespace CVC4 {
  53   namespace main {
  54     /** Global options variable */
  55     CVC4_THREADLOCAL(Options*) pOptions;
  56
  57     /** Full argv[0] */
  58     const char *progPath;
  59
  60     /** Just the basename component of argv[0] */
  61     const char *progName;
  62
  63     /** A pointer to the StatisticsRegistry (the signal handlers need it) */
  64     CVC4::StatisticsRegistry* pStatistics;
  65   }
  66 }
  67
  68
  69 void printUsage(Options& options, bool full) {
  70   stringstream ss;
  71   ss << "usage: " << options.binary_name << " [options] [input-file]" << endl
  72       << endl
  73       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
  74       << endl
  75       << "CVC4 options:" << endl;
  76   if(full) {
  77     Options::printUsage( ss.str(), *options.out );
  78   } else {
  79     Options::printShortUsage( ss.str(), *options.out );
  80   }
  81 }
  82
  83 int runCvc4(int argc, char* argv[], Options& options) {
  84
  85   // For the signal handlers' benefit
  86   pOptions = &options;
  87
  88   // Initialize the signal handlers
  89   cvc4_init();
  90
  91   progPath = argv[0];
  92
  93   // Parse the options
  94   int firstArgIndex = options.parseOptions(argc, argv);
  95
  96   progName = options.binary_name.c_str();
  97
  98   if( options.help ) {
  99     printUsage(options, true);
 100     exit(1);
 101   } else if( options.languageHelp ) {
 102     Options::printLanguageHelp(*options.out);
 103     exit(1);
 104   } else if( options.version ) {
 105     *options.out << Configuration::about().c_str() << flush;
 106     exit(0);
 107   }
 108
 109   segvNoSpin = options.segvNoSpin;
 110
 111   // If in competition mode, set output stream option to flush immediately
 112 #ifdef CVC4_COMPETITION_MODE
 113   *options.out << unitbuf;
 114 #endif
 115
 116   // We only accept one input file
 117   if(argc > firstArgIndex + 1) {
 118     throw Exception("Too many input files specified.");
 119   }
 120
 121   // If no file supplied we will read from standard input
 122   const bool inputFromStdin =
 123     firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]);
 124
 125   // if we're reading from stdin on a TTY, default to interactive mode
 126   if(!options.interactiveSetByUser) {
 127     options.interactive = inputFromStdin && isatty(fileno(stdin));
 128   }
 129
 130   // Determine which messages to show based on smtcomp_mode and verbosity
 131   if(Configuration::isMuzzledBuild()) {
 132     Debug.setStream(CVC4::null_os);
 133     Trace.setStream(CVC4::null_os);
 134     Notice.setStream(CVC4::null_os);
 135     Chat.setStream(CVC4::null_os);
 136     Message.setStream(CVC4::null_os);
 137     Warning.setStream(CVC4::null_os);
 138     Dump.setStream(CVC4::null_os);
 139   } else {
 140     if(options.verbosity < 2) {
 141       Chat.setStream(CVC4::null_os);
 142     }
 143     if(options.verbosity < 1) {
 144       Notice.setStream(CVC4::null_os);
 145     }
 146     if(options.verbosity < 0) {
 147       Message.setStream(CVC4::null_os);
 148       Warning.setStream(CVC4::null_os);
 149     }
 150   }
 151
 152   // Create the expression manager
 153   ExprManager exprMgr(options);
 154
 155   // Create the SmtEngine
 156   SmtEngine smt(&exprMgr);
 157
 158   // signal handlers need access
 159   pStatistics = smt.getStatisticsRegistry();
 160
 161   // Auto-detect input language by filename extension
 162   const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex];
 163
 164   ReferenceStat< const char* > s_statFilename("filename", filename);
 165   RegisterStatistic statFilenameReg(exprMgr, &s_statFilename);
 166
 167   if(options.inputLanguage == language::input::LANG_AUTO) {
 168     if( inputFromStdin ) {
 169       // We can't do any fancy detection on stdin
 170       options.inputLanguage = language::input::LANG_CVC4;
 171     } else {
 172       unsigned len = strlen(filename);
 173       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 174         options.inputLanguage = language::input::LANG_SMTLIB_V2;
 175       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 176         options.inputLanguage = language::input::LANG_SMTLIB;
 177       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 178                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 179         options.inputLanguage = language::input::LANG_CVC4;
 180       }
 181     }
 182   }
 183
 184   if(options.outputLanguage == language::output::LANG_AUTO) {
 185     options.outputLanguage = language::toOutputLanguage(options.inputLanguage);
 186   }
 187
 188   // Determine which messages to show based on smtcomp_mode and verbosity
 189   if(Configuration::isMuzzledBuild()) {
 190     Debug.setStream(CVC4::null_os);
 191     Trace.setStream(CVC4::null_os);
 192     Notice.setStream(CVC4::null_os);
 193     Chat.setStream(CVC4::null_os);
 194     Message.setStream(CVC4::null_os);
 195     Warning.setStream(CVC4::null_os);
 196     Dump.setStream(CVC4::null_os);
 197   } else {
 198     if(options.verbosity < 2) {
 199       Chat.setStream(CVC4::null_os);
 200     }
 201     if(options.verbosity < 1) {
 202       Notice.setStream(CVC4::null_os);
 203     }
 204     if(options.verbosity < 0) {
 205       Message.setStream(CVC4::null_os);
 206       Warning.setStream(CVC4::null_os);
 207     }
 208
 209     Debug.getStream() << Expr::setlanguage(options.outputLanguage);
 210     Trace.getStream() << Expr::setlanguage(options.outputLanguage);
 211     Notice.getStream() << Expr::setlanguage(options.outputLanguage);
 212     Chat.getStream() << Expr::setlanguage(options.outputLanguage);
 213     Message.getStream() << Expr::setlanguage(options.outputLanguage);
 214     Warning.getStream() << Expr::setlanguage(options.outputLanguage);
 215     Dump.getStream() << Expr::setlanguage(options.outputLanguage)
 216                      << Expr::setdepth(-1)
 217                      << Expr::printtypes(false);
 218   }
 219
 220   Parser* replayParser = NULL;
 221   if( options.replayFilename != "" ) {
 222     ParserBuilder replayParserBuilder(&exprMgr, options.replayFilename, options);
 223
 224     if( options.replayFilename == "-") {
 225       if( inputFromStdin ) {
 226         throw OptionException("Replay file and input file can't both be stdin.");
 227       }
 228       replayParserBuilder.withStreamInput(cin);
 229     }
 230     replayParser = replayParserBuilder.build();
 231     options.replayStream = new Parser::ExprStream(replayParser);
 232   }
 233   if( options.replayLog != NULL ) {
 234     *options.replayLog << Expr::setlanguage(options.outputLanguage) << Expr::setdepth(-1);
 235   }
 236
 237   // Parse and execute commands until we are done
 238   Command* cmd;
 239   bool status = true;
 240   if( options.interactive ) {
 241     InteractiveShell shell(exprMgr, options);
 242     Message() << Configuration::getPackageName()
 243               << " " << Configuration::getVersionString();
 244     if(Configuration::isSubversionBuild()) {
 245       Message() << " [" << Configuration::getSubversionId() << "]";
 246     }
 247     Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 248               << " assertions:"
 249               << (Configuration::isAssertionBuild() ? "on" : "off")
 250               << endl;
 251     if(replayParser != NULL) {
 252       // have the replay parser use the declarations input interactively
 253       replayParser->useDeclarationsFrom(shell.getParser());
 254     }
 255     while((cmd = shell.readCommand())) {
 256       status = doCommand(smt,cmd, options) && status;
 257       delete cmd;
 258     }
 259   } else {
 260     ParserBuilder parserBuilder(&exprMgr, filename, options);
 261
 262     if( inputFromStdin ) {
 263       parserBuilder.withLineBufferedStreamInput(cin);
 264     }
 265
 266     Parser *parser = parserBuilder.build();
 267     if(replayParser != NULL) {
 268       // have the replay parser use the file's declarations
 269       replayParser->useDeclarationsFrom(parser);
 270     }
 271     while((cmd = parser->nextCommand())) {
 272       status = doCommand(smt, cmd, options) && status;
 273       delete cmd;
 274     }
 275     // Remove the parser
 276     delete parser;
 277   }
 278
 279   if( options.replayStream != NULL ) {
 280     // this deletes the expression parser too
 281     delete options.replayStream;
 282     options.replayStream = NULL;
 283   }
 284
 285   int returnValue;
 286   string result = "unknown";
 287   if(status) {
 288     result = smt.getInfo(":status").getValue();
 289
 290     if(result == "sat") {
 291       returnValue = 10;
 292     } else if(result == "unsat") {
 293       returnValue = 20;
 294     } else {
 295       returnValue = 0;
 296     }
 297   } else {
 298     // there was some kind of error
 299     returnValue = 1;
 300   }
 301
 302 #ifdef CVC4_COMPETITION_MODE
 303   // exit, don't return
 304   // (don't want destructors to run)
 305   exit(returnValue);
 306 #endif
 307
 308   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 309   RegisterStatistic statSatResultReg(exprMgr, &s_statSatResult);
 310
 311   if(options.statistics) {
 312     pStatistics->flushInformation(*options.err);
 313   }
 314
 315   return returnValue;
 316 }
 317
 318 /** Executes a command. Deletes the command after execution. */
 319 static bool doCommand(SmtEngine& smt, Command* cmd, Options& options) {
 320   if( options.parseOnly ) {
 321     return true;
 322   }
 323
 324   // assume no error
 325   bool status = true;
 326
 327   CommandSequence *seq = dynamic_cast<CommandSequence*>(cmd);
 328   if(seq != NULL) {
 329     for(CommandSequence::iterator subcmd = seq->begin();
 330         subcmd != seq->end();
 331         ++subcmd) {
 332       status = doCommand(smt, *subcmd, options) && status;
 333     }
 334   } else {
 335     if(options.verbosity > 0) {
 336       *options.out << "Invoking: " << *cmd << endl;
 337     }
 338
 339     if(options.verbosity >= 0) {
 340       cmd->invoke(&smt, *options.out);
 341     } else {
 342       cmd->invoke(&smt);
 343     }
 344     status = status && cmd->ok();
 345   }
 346
 347   return status;
 348 }