1 /********************* */
2 /*! \file driver_unified.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Tim King, Liana Hadarean
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Driver for CVC4 executable (cvc4) unified for both
13 ** sequential and portfolio versions
25 // This must come before PORTFOLIO_BUILD.
26 #include "cvc4autoconfig.h"
28 #include "base/configuration.h"
29 #include "base/output.h"
30 #include "base/ptr_closer.h"
31 #include "expr/expr_iomanip.h"
32 #include "expr/expr_manager.h"
33 #include "main/command_executor.h"
35 #ifdef PORTFOLIO_BUILD
36 # include "main/command_executor_portfolio.h"
39 #include "main/interactive_shell.h"
40 #include "main/main.h"
41 #include "options/options.h"
42 #include "options/set_language.h"
43 #include "parser/parser.h"
44 #include "parser/parser_builder.h"
45 #include "parser/parser_exception.h"
46 #include "smt/command.h"
47 #include "util/result.h"
48 #include "util/statistics_registry.h"
52 using namespace CVC4::parser
;
53 using namespace CVC4::main
;
57 /** Global options variable */
58 CVC4_THREADLOCAL(Options
*) pOptions
;
63 /** Just the basename component of argv[0] */
64 const std::string
*progName
;
66 /** A pointer to the CommandExecutor (the signal handlers need it) */
67 CVC4::main::CommandExecutor
* pExecutor
= NULL
;
69 /** A pointer to the totalTime driver stat (the signal handlers need it) */
70 CVC4::TimerStat
* pTotalTime
= NULL
;
72 }/* CVC4::main namespace */
76 void printUsage(Options
& opts
, bool full
) {
78 ss
<< "usage: " << opts
.getBinaryName() << " [options] [input-file]"
80 << "Without an input file, or with `-', CVC4 reads from standard input."
82 << "CVC4 options:" << endl
;
84 Options::printUsage( ss
.str(), *(opts
.getOut()) );
86 Options::printShortUsage( ss
.str(), *(opts
.getOut()) );
90 int runCvc4(int argc
, char* argv
[], Options
& opts
) {
93 pTotalTime
= new TimerStat("totalTime");
96 // For the signal handlers' benefit
99 // Initialize the signal handlers
105 vector
<string
> filenames
= Options::parseOptions(&opts
, argc
, argv
);
107 # ifndef PORTFOLIO_BUILD
108 if( opts
.wasSetByUserThreads() ||
109 opts
.wasSetByUserThreadStackSize() ||
110 (! opts
.getThreadArgv().empty()) ) {
111 throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'.");
115 string progNameStr
= opts
.getBinaryName();
116 progName
= &progNameStr
;
118 if( opts
.getHelp() ) {
119 printUsage(opts
, true);
121 } else if( opts
.getLanguageHelp() ) {
122 Options::printLanguageHelp(*(opts
.getOut()));
124 } else if( opts
.getVersion() ) {
125 *(opts
.getOut()) << Configuration::about().c_str() << flush
;
129 segvSpin
= opts
.getSegvSpin();
131 // If in competition mode, set output stream option to flush immediately
132 #ifdef CVC4_COMPETITION_MODE
133 *(opts
.getOut()) << unitbuf
;
134 #endif /* CVC4_COMPETITION_MODE */
136 // We only accept one input file
137 if(filenames
.size() > 1) {
138 throw Exception("Too many input files specified.");
141 // If no file supplied we will read from standard input
142 const bool inputFromStdin
= filenames
.empty() || filenames
[0] == "-";
144 // if we're reading from stdin on a TTY, default to interactive mode
145 if(!opts
.wasSetByUserInteractive()) {
146 opts
.setInteractive(inputFromStdin
&& isatty(fileno(stdin
)));
149 // Auto-detect input language by filename extension
150 std::string
filenameStr("<stdin>");
151 if (!inputFromStdin
) {
152 // Use swap to avoid copying the string
153 // TODO: use std::move() when switching to c++11
154 filenameStr
.swap(filenames
[0]);
156 const char* filename
= filenameStr
.c_str();
158 if(opts
.getInputLanguage() == language::input::LANG_AUTO
) {
159 if( inputFromStdin
) {
160 // We can't do any fancy detection on stdin
161 opts
.setInputLanguage(language::input::LANG_CVC4
);
163 unsigned len
= filenameStr
.size();
164 if(len
>= 5 && !strcmp(".smt2", filename
+ len
- 5)) {
165 opts
.setInputLanguage(language::input::LANG_SMTLIB_V2_5
);
166 } else if(len
>= 4 && !strcmp(".smt", filename
+ len
- 4)) {
167 opts
.setInputLanguage(language::input::LANG_SMTLIB_V1
);
168 } else if(len
>= 5 && !strcmp(".smt1", filename
+ len
- 5)) {
169 opts
.setInputLanguage(language::input::LANG_SMTLIB_V1
);
170 } else if((len
>= 2 && !strcmp(".p", filename
+ len
- 2))
171 || (len
>= 5 && !strcmp(".tptp", filename
+ len
- 5))) {
172 opts
.setInputLanguage(language::input::LANG_TPTP
);
173 } else if(( len
>= 4 && !strcmp(".cvc", filename
+ len
- 4) )
174 || ( len
>= 5 && !strcmp(".cvc4", filename
+ len
- 5) )) {
175 opts
.setInputLanguage(language::input::LANG_CVC4
);
176 } else if((len
>= 3 && !strcmp(".sy", filename
+ len
- 3))
177 || (len
>= 3 && !strcmp(".sl", filename
+ len
- 3))) {
178 opts
.setInputLanguage(language::input::LANG_SYGUS
);
179 //since there is no sygus output language, set this to SMT lib 2
180 //opts.setOutputLanguage(language::output::LANG_SMTLIB_V2_0);
185 if(opts
.getOutputLanguage() == language::output::LANG_AUTO
) {
186 opts
.setOutputLanguage(language::toOutputLanguage(opts
.getInputLanguage()));
189 // if doing sygus, turn on CEGQI by default
190 if(opts
.getInputLanguage() == language::input::LANG_SYGUS
){
191 if( !opts
.wasSetByUserCeGuidedInst()) {
192 opts
.setCeGuidedInst(true);
194 if( !opts
.wasSetByUserDumpSynth()) {
195 opts
.setDumpSynth(true);
199 // Determine which messages to show based on smtcomp_mode and verbosity
200 if(Configuration::isMuzzledBuild()) {
201 DebugChannel
.setStream(&CVC4::null_os
);
202 TraceChannel
.setStream(&CVC4::null_os
);
203 NoticeChannel
.setStream(&CVC4::null_os
);
204 ChatChannel
.setStream(&CVC4::null_os
);
205 MessageChannel
.setStream(&CVC4::null_os
);
206 WarningChannel
.setStream(&CVC4::null_os
);
209 // important even for muzzled builds (to get result output right)
210 (*(opts
.getOut())) << language::SetLanguage(opts
.getOutputLanguage());
212 // Create the expression manager using appropriate options
213 ExprManager
* exprMgr
;
214 # ifndef PORTFOLIO_BUILD
215 exprMgr
= new ExprManager(opts
);
216 pExecutor
= new CommandExecutor(*exprMgr
, opts
);
218 OptionsList threadOpts
;
219 parseThreadSpecificOptions(threadOpts
, opts
);
221 bool useParallelExecutor
= true;
223 if(opts
.wasSetByUserIncrementalSolving() &&
224 opts
.getIncrementalSolving() &&
225 (! opts
.getIncrementalParallel()) ) {
226 Notice() << "Notice: In --incremental mode, using the sequential solver"
227 << " unless forced by...\n"
228 << "Notice: ...the experimental --incremental-parallel option.\n";
229 useParallelExecutor
= false;
232 if(opts
.getCheckProofs()) {
233 if(opts
.getFallbackSequential()) {
234 Warning() << "Warning: Falling back to sequential mode, as cannot run"
235 << " portfolio in check-proofs mode.\n";
236 useParallelExecutor
= false;
239 throw OptionException("Cannot run portfolio in check-proofs mode.");
242 // pick appropriate one
243 if(useParallelExecutor
) {
244 exprMgr
= new ExprManager(threadOpts
[0]);
245 pExecutor
= new CommandExecutorPortfolio(*exprMgr
, opts
, threadOpts
);
247 exprMgr
= new ExprManager(opts
);
248 pExecutor
= new CommandExecutor(*exprMgr
, opts
);
252 PtrCloser
<Parser
> replayParser
;
253 if( opts
.getReplayInputFilename() != "" ) {
254 std::string replayFilename
= opts
.getReplayInputFilename();
255 ParserBuilder
replayParserBuilder(exprMgr
, replayFilename
, opts
);
257 if( replayFilename
== "-") {
258 if( inputFromStdin
) {
259 throw OptionException("Replay file and input file can't both be stdin.");
261 replayParserBuilder
.withStreamInput(cin
);
263 replayParser
.reset(replayParserBuilder
.build());
264 pExecutor
->setReplayStream(new Parser::ExprStream(replayParser
.get()));
270 RegisterStatistic
statTotalTime(&pExecutor
->getStatisticsRegistry(),
273 // Filename statistics
274 ReferenceStat
<std::string
> s_statFilename("filename", filenameStr
);
275 RegisterStatistic
statFilenameReg(&pExecutor
->getStatisticsRegistry(),
278 // Parse and execute commands until we are done
281 if(opts
.getInteractive() && inputFromStdin
) {
282 if(opts
.getTearDownIncremental() > 0) {
283 throw OptionException(
284 "--tear-down-incremental doesn't work in interactive mode");
286 #ifndef PORTFOLIO_BUILD
287 if(!opts
.wasSetByUserIncrementalSolving()) {
288 cmd
= new SetOptionCommand("incremental", SExpr(true));
290 pExecutor
->doCommand(cmd
);
293 #endif /* PORTFOLIO_BUILD */
294 InteractiveShell
shell(*exprMgr
, opts
);
295 if(opts
.getInteractivePrompt()) {
296 Message() << Configuration::getPackageName()
297 << " " << Configuration::getVersionString();
298 if(Configuration::isGitBuild()) {
299 Message() << " [" << Configuration::getGitId() << "]";
300 } else if(Configuration::isSubversionBuild()) {
301 Message() << " [" << Configuration::getSubversionId() << "]";
303 Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
305 << (Configuration::isAssertionBuild() ? "on" : "off")
309 // have the replay parser use the declarations input interactively
310 replayParser
->useDeclarationsFrom(shell
.getParser());
315 cmd
= shell
.readCommand();
316 } catch(UnsafeInterruptException
& e
) {
317 (*opts
.getOut()) << CommandInterrupted();
322 status
= pExecutor
->doCommand(cmd
) && status
;
323 if (cmd
->interrupted()) {
329 } else if( opts
.getTearDownIncremental() > 0) {
330 if(!opts
.getIncrementalSolving() && opts
.getTearDownIncremental() > 1) {
331 // For tear-down-incremental values greater than 1, need incremental
333 cmd
= new SetOptionCommand("incremental", SExpr(true));
335 pExecutor
->doCommand(cmd
);
337 // if(opts.wasSetByUserIncrementalSolving()) {
338 // throw OptionException(
339 // "--tear-down-incremental incompatible with --incremental");
342 // cmd = new SetOptionCommand("incremental", SExpr(false));
343 // cmd->setMuted(true);
344 // pExecutor->doCommand(cmd);
348 ParserBuilder
parserBuilder(exprMgr
, filename
, opts
);
350 if( inputFromStdin
) {
351 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
352 parserBuilder
.withStreamInput(cin
);
353 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
354 parserBuilder
.withLineBufferedStreamInput(cin
);
355 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
358 vector
< vector
<Command
*> > allCommands
;
359 allCommands
.push_back(vector
<Command
*>());
360 PtrCloser
<Parser
> parser(parserBuilder
.build());
362 // have the replay parser use the file's declarations
363 replayParser
->useDeclarationsFrom(parser
.get());
366 // true if one of the commands was interrupted
367 bool interrupted
= false;
368 while (status
|| opts
.getContinuedExecution()) {
370 (*opts
.getOut()) << CommandInterrupted();
375 cmd
= parser
->nextCommand();
376 if (cmd
== NULL
) break;
377 } catch (UnsafeInterruptException
& e
) {
382 if(dynamic_cast<PushCommand
*>(cmd
) != NULL
) {
383 if(needReset
>= opts
.getTearDownIncremental()) {
385 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
386 if (interrupted
) break;
387 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
389 Command
* cmd
= allCommands
[i
][j
]->clone();
391 pExecutor
->doCommand(cmd
);
392 if(cmd
->interrupted()) {
400 allCommands
.push_back(vector
<Command
*>());
401 Command
* copy
= cmd
->clone();
402 allCommands
.back().push_back(copy
);
403 status
= pExecutor
->doCommand(cmd
);
404 if(cmd
->interrupted()) {
408 } else if(dynamic_cast<PopCommand
*>(cmd
) != NULL
) {
409 allCommands
.pop_back(); // fixme leaks cmds here
410 if (needReset
>= opts
.getTearDownIncremental()) {
412 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
413 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
415 Command
* cmd
= allCommands
[i
][j
]->clone();
417 pExecutor
->doCommand(cmd
);
418 if(cmd
->interrupted()) {
424 if (interrupted
) continue;
425 (*opts
.getOut()) << CommandSuccess();
428 status
= pExecutor
->doCommand(cmd
);
429 if(cmd
->interrupted()) {
434 } else if(dynamic_cast<CheckSatCommand
*>(cmd
) != NULL
||
435 dynamic_cast<QueryCommand
*>(cmd
) != NULL
) {
436 if(needReset
>= opts
.getTearDownIncremental()) {
438 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
439 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
441 Command
* cmd
= allCommands
[i
][j
]->clone();
443 pExecutor
->doCommand(cmd
);
444 if(cmd
->interrupted()) {
458 status
= pExecutor
->doCommand(cmd
);
459 if(cmd
->interrupted()) {
463 } else if(dynamic_cast<ResetCommand
*>(cmd
) != NULL
) {
464 pExecutor
->doCommand(cmd
);
466 allCommands
.push_back(vector
<Command
*>());
468 // We shouldn't copy certain commands, because they can cause
469 // an error on replay since there's no associated sat/unsat check
471 if(dynamic_cast<GetUnsatCoreCommand
*>(cmd
) == NULL
&&
472 dynamic_cast<GetProofCommand
*>(cmd
) == NULL
&&
473 dynamic_cast<GetValueCommand
*>(cmd
) == NULL
&&
474 dynamic_cast<GetModelCommand
*>(cmd
) == NULL
&&
475 dynamic_cast<GetAssignmentCommand
*>(cmd
) == NULL
&&
476 dynamic_cast<GetInstantiationsCommand
*>(cmd
) == NULL
&&
477 dynamic_cast<GetAssertionsCommand
*>(cmd
) == NULL
&&
478 dynamic_cast<GetInfoCommand
*>(cmd
) == NULL
&&
479 dynamic_cast<GetOptionCommand
*>(cmd
) == NULL
&&
480 dynamic_cast<EchoCommand
*>(cmd
) == NULL
) {
481 Command
* copy
= cmd
->clone();
482 allCommands
.back().push_back(copy
);
484 status
= pExecutor
->doCommand(cmd
);
485 if(cmd
->interrupted()) {
490 if(dynamic_cast<QuitCommand
*>(cmd
) != NULL
) {
498 if(!opts
.wasSetByUserIncrementalSolving()) {
499 cmd
= new SetOptionCommand("incremental", SExpr(false));
501 pExecutor
->doCommand(cmd
);
505 ParserBuilder
parserBuilder(exprMgr
, filename
, opts
);
507 if( inputFromStdin
) {
508 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
509 parserBuilder
.withStreamInput(cin
);
510 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
511 parserBuilder
.withLineBufferedStreamInput(cin
);
512 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
515 PtrCloser
<Parser
> parser(parserBuilder
.build());
517 // have the replay parser use the file's declarations
518 replayParser
->useDeclarationsFrom(parser
.get());
520 bool interrupted
= false;
521 while(status
|| opts
.getContinuedExecution()) {
523 (*opts
.getOut()) << CommandInterrupted();
528 cmd
= parser
->nextCommand();
529 if (cmd
== NULL
) break;
530 } catch (UnsafeInterruptException
& e
) {
535 status
= pExecutor
->doCommand(cmd
);
536 if (cmd
->interrupted() && status
== 0) {
541 if(dynamic_cast<QuitCommand
*>(cmd
) != NULL
) {
551 result
= pExecutor
->getResult();
554 // there was some kind of error
558 #ifdef CVC4_COMPETITION_MODE
560 // exit, don't return (don't want destructors to run)
561 // _exit() from unistd.h doesn't run global destructors
562 // or other on_exit/atexit stuff.
564 #endif /* CVC4_COMPETITION_MODE */
566 ReferenceStat
< Result
> s_statSatResult("sat/unsat", result
);
567 RegisterStatistic
statSatResultReg(&pExecutor
->getStatisticsRegistry(),
572 // Tim: I think that following comment is out of date?
573 // Set the global executor pointer to NULL first. If we get a
574 // signal while dumping statistics, we don't want to try again.
575 pExecutor
->flushOutputStreams();
578 if(opts
.getEarlyExit() && opts
.wasSetByUserEarlyExit()) {
581 #else /* CVC4_DEBUG */
582 if(opts
.getEarlyExit()) {
585 #endif /* CVC4_DEBUG */
588 // On exceptional exit, these are leaked, but that's okay... they
589 // need to be around in that case for main() to print statistics.