src/main/driver_unified.cpp

   1 /*********************                                                        */
   2 /*! \file driver_unified.cpp
   3  ** \verbatim
   4  ** Original author: mdeters
   5  ** Major contributors: cconway
   6  ** Minor contributors (to current version): barrett, dejan, taking, kshitij
   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 CVC4 executable (cvc4) unified for both
  15  ** sequential and portfolio versions
  16  **/
  17
  18 #include <cstdlib>
  19 #include <cstring>
  20 #include <fstream>
  21 #include <iostream>
  22 #include <new>
  23 #include <unistd.h>
  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 "expr/command.h"
  36 #include "util/Assert.h"
  37 #include "util/configuration.h"
  38 #include "options/options.h"
  39 #include "main/command_executor.h"
  40 # ifdef PORTFOLIO_BUILD
  41 #    include "main/command_executor_portfolio.h"
  42 # endif
  43 #include "main/options.h"
  44 #include "smt/options.h"
  45 #include "theory/uf/options.h"
  46 #include "util/output.h"
  47 #include "util/dump.h"
  48 #include "util/result.h"
  49
  50 using namespace std;
  51 using namespace CVC4;
  52 using namespace CVC4::parser;
  53 using namespace CVC4::main;
  54
  55 namespace CVC4 {
  56   namespace main {
  57     /** Global options variable */
  58     CVC4_THREADLOCAL(Options*) pOptions;
  59
  60     /** Full argv[0] */
  61     const char *progPath;
  62
  63     /** Just the basename component of argv[0] */
  64     const char *progName;
  65
  66     /** A pointer to the CommandExecutor (the signal handlers need it) */
  67     CVC4::main::CommandExecutor* pExecutor;
  68
  69   }/* CVC4::main namespace */
  70 }/* CVC4 namespace */
  71
  72
  73 void printUsage(Options& opts, bool full) {
  74   stringstream ss;
  75   ss << "usage: " << opts[options::binary_name] << " [options] [input-file]" << endl
  76       << endl
  77       << "Without an input file, or with `-', CVC4 reads from standard input." << endl
  78       << endl
  79       << "CVC4 options:" << endl;
  80   if(full) {
  81     Options::printUsage( ss.str(), *opts[options::out] );
  82   } else {
  83     Options::printShortUsage( ss.str(), *opts[options::out] );
  84   }
  85 }
  86
  87 int runCvc4(int argc, char* argv[], Options& opts) {
  88
  89   // Timer statistic
  90   TimerStat s_totalTime("totalTime");
  91   s_totalTime.start();
  92
  93   // For the signal handlers' benefit
  94   pOptions = &opts;
  95
  96   // Initialize the signal handlers
  97   cvc4_init();
  98
  99   progPath = argv[0];
 100
 101   // Parse the options
 102   vector<string> filenames = opts.parseOptions(argc, argv);
 103
 104 # ifndef PORTFOLIO_BUILD
 105   if( opts.wasSetByUser(options::threads) ||
 106       ! opts[options::threadArgv].empty() ) {
 107     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
 108   }
 109 # endif
 110
 111   progName = opts[options::binary_name].c_str();
 112
 113   if( opts[options::help] ) {
 114     printUsage(opts, true);
 115     exit(1);
 116   } else if( opts[options::languageHelp] ) {
 117     Options::printLanguageHelp(*opts[options::out]);
 118     exit(1);
 119   } else if( opts[options::version] ) {
 120     *opts[options::out] << Configuration::about().c_str() << flush;
 121     exit(0);
 122   }
 123
 124   segvNoSpin = opts[options::segvNoSpin];
 125
 126   // If in competition mode, set output stream option to flush immediately
 127 #ifdef CVC4_COMPETITION_MODE
 128   *opts[options::out] << unitbuf;
 129 #endif /* CVC4_COMPETITION_MODE */
 130
 131   // We only accept one input file
 132   if(filenames.size() > 1) {
 133     throw Exception("Too many input files specified.");
 134   }
 135
 136   // If no file supplied we will read from standard input
 137   const bool inputFromStdin = filenames.empty() || filenames[0] == "-";
 138
 139   // if we're reading from stdin on a TTY, default to interactive mode
 140   if(!opts.wasSetByUser(options::interactive)) {
 141     opts.set(options::interactive, inputFromStdin && isatty(fileno(stdin)));
 142   }
 143
 144   // Auto-detect input language by filename extension
 145   const char* filename = inputFromStdin ? "<stdin>" : filenames[0].c_str();
 146
 147   if(opts[options::inputLanguage] == language::input::LANG_AUTO) {
 148     if( inputFromStdin ) {
 149       // We can't do any fancy detection on stdin
 150       opts.set(options::inputLanguage, language::input::LANG_CVC4);
 151     } else {
 152       unsigned len = strlen(filename);
 153       if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
 154         opts.set(options::inputLanguage, language::input::LANG_SMTLIB_V2);
 155       } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) {
 156         opts.set(options::inputLanguage, language::input::LANG_SMTLIB);
 157       } else if((len >= 2 && !strcmp(".p", filename + len - 2))
 158                 || (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
 159         opts.set(options::inputLanguage, language::input::LANG_TPTP);
 160       } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
 161                 || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
 162         opts.set(options::inputLanguage, language::input::LANG_CVC4);
 163       }
 164     }
 165   }
 166
 167   if(opts[options::outputLanguage] == language::output::LANG_AUTO) {
 168     opts.set(options::outputLanguage, language::toOutputLanguage(opts[options::inputLanguage]));
 169   }
 170
 171   // Determine which messages to show based on smtcomp_mode and verbosity
 172   if(Configuration::isMuzzledBuild()) {
 173     DebugChannel.setStream(CVC4::null_os);
 174     TraceChannel.setStream(CVC4::null_os);
 175     NoticeChannel.setStream(CVC4::null_os);
 176     ChatChannel.setStream(CVC4::null_os);
 177     MessageChannel.setStream(CVC4::null_os);
 178     WarningChannel.setStream(CVC4::null_os);
 179     DumpChannel.setStream(CVC4::null_os);
 180   }
 181
 182   // important even for muzzled builds (to get result output right)
 183   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
 184
 185   // Create the expression manager using appropriate options
 186 # ifndef PORTFOLIO_BUILD
 187   ExprManager exprMgr(opts);
 188 # else
 189   vector<Options> threadOpts = parseThreadSpecificOptions(opts);
 190   ExprManager exprMgr(threadOpts[0]);
 191 # endif
 192
 193 # ifndef PORTFOLIO_BUILD
 194   CommandExecutor cmdExecutor(exprMgr, opts);
 195 # else
 196   CommandExecutorPortfolio cmdExecutor(exprMgr, opts, threadOpts);
 197 # endif
 198
 199   // give access to the signal handlers for stats output
 200   pExecutor = &cmdExecutor;
 201
 202   Parser* replayParser = NULL;
 203   if( opts[options::replayFilename] != "" ) {
 204     ParserBuilder replayParserBuilder(&exprMgr, opts[options::replayFilename], opts);
 205
 206     if( opts[options::replayFilename] == "-") {
 207       if( inputFromStdin ) {
 208         throw OptionException("Replay file and input file can't both be stdin.");
 209       }
 210       replayParserBuilder.withStreamInput(cin);
 211     }
 212     replayParser = replayParserBuilder.build();
 213     opts.set(options::replayStream, new Parser::ExprStream(replayParser));
 214   }
 215   if( opts[options::replayLog] != NULL ) {
 216     *opts[options::replayLog] << Expr::setlanguage(opts[options::outputLanguage]) << Expr::setdepth(-1);
 217   }
 218
 219   // Timer statistic
 220   RegisterStatistic statTotalTime(&cmdExecutor.getStatisticsRegistry(), &s_totalTime);
 221
 222   // Filename statistics
 223   ReferenceStat< const char* > s_statFilename("filename", filename);
 224   RegisterStatistic statFilenameReg(&cmdExecutor.getStatisticsRegistry(), &s_statFilename);
 225
 226   // Parse and execute commands until we are done
 227   Command* cmd;
 228   bool status = true;
 229   if( opts[options::interactive] ) {
 230     InteractiveShell shell(exprMgr, opts);
 231     Message() << Configuration::getPackageName()
 232               << " " << Configuration::getVersionString();
 233     if(Configuration::isSubversionBuild()) {
 234       Message() << " [" << Configuration::getSubversionId() << "]";
 235     }
 236     Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
 237               << " assertions:"
 238               << (Configuration::isAssertionBuild() ? "on" : "off")
 239               << endl;
 240     if(replayParser != NULL) {
 241       // have the replay parser use the declarations input interactively
 242       replayParser->useDeclarationsFrom(shell.getParser());
 243     }
 244     while((cmd = shell.readCommand())) {
 245       status = cmdExecutor.doCommand(cmd) && status;
 246       delete cmd;
 247     }
 248   } else {
 249     ParserBuilder parserBuilder(&exprMgr, filename, opts);
 250
 251     if( inputFromStdin ) {
 252 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
 253       parserBuilder.withStreamInput(cin);
 254 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 255       parserBuilder.withLineBufferedStreamInput(cin);
 256 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
 257     }
 258
 259     Parser *parser = parserBuilder.build();
 260     if(replayParser != NULL) {
 261       // have the replay parser use the file's declarations
 262       replayParser->useDeclarationsFrom(parser);
 263     }
 264     while(status && (cmd = parser->nextCommand())) {
 265       if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
 266         delete cmd;
 267         break;
 268       }
 269       status = cmdExecutor.doCommand(cmd);
 270       delete cmd;
 271     }
 272     // Remove the parser
 273     delete parser;
 274   }
 275
 276   if( opts[options::replayStream] != NULL ) {
 277     // this deletes the expression parser too
 278     delete opts[options::replayStream];
 279     opts.set(options::replayStream, NULL);
 280   }
 281
 282   int returnValue;
 283   string result = "unknown";
 284   if(status) {
 285     result = cmdExecutor.getSmtEngineStatus();
 286
 287     if(result == "sat") {
 288       returnValue = 10;
 289     } else if(result == "unsat") {
 290       returnValue = 20;
 291     } else {
 292       returnValue = 0;
 293     }
 294   } else {
 295     // there was some kind of error
 296     returnValue = 1;
 297   }
 298
 299 #ifdef CVC4_COMPETITION_MODE
 300   // exit, don't return (don't want destructors to run)
 301   // _exit() from unistd.h doesn't run global destructors
 302   // or other on_exit/atexit stuff.
 303   _exit(returnValue);
 304 #endif /* CVC4_COMPETITION_MODE */
 305
 306   ReferenceStat< Result > s_statSatResult("sat/unsat", result);
 307   RegisterStatistic statSatResultReg(&cmdExecutor.getStatisticsRegistry(), &s_statSatResult);
 308
 309   s_totalTime.stop();
 310
 311   // Set the global executor pointer to NULL first.  If we get a
 312   // signal while dumping statistics, we don't want to try again.
 313   pExecutor = NULL;
 314   if(opts[options::statistics]) {
 315     cmdExecutor.flushStatistics(*opts[options::err]);
 316   }
 317
 318 #ifdef CVC4_DEBUG
 319   if(opts[options::earlyExit] && opts.wasSetByUser(options::earlyExit)) {
 320     _exit(returnValue);
 321   }
 322 #else /* CVC4_DEBUG */
 323   if(opts[options::earlyExit]) {
 324     _exit(returnValue);
 325   }
 326 #endif /* CVC4_DEBUG */
 327
 328   return returnValue;
 329 }