1 /********************* */
2 /*! \file driver_unified.cpp
4 ** Original author: Kshitij Bansal
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Francois Bobot
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Driver for CVC4 executable (cvc4) unified for both
13 ** sequential and portfolio versions
26 #include "cvc4autoconfig.h"
27 #include "main/main.h"
28 #include "main/interactive_shell.h"
29 #include "main/options.h"
30 #include "parser/parser.h"
31 #include "parser/parser_builder.h"
32 #include "parser/parser_exception.h"
33 #include "expr/expr_manager.h"
34 #include "expr/command.h"
35 #include "util/configuration.h"
36 #include "options/options.h"
37 #include "main/command_executor.h"
38 # ifdef PORTFOLIO_BUILD
39 # include "main/command_executor_portfolio.h"
41 #include "main/options.h"
42 #include "smt/options.h"
43 #include "theory/uf/options.h"
44 #include "util/output.h"
45 #include "util/result.h"
46 #include "util/statistics_registry.h"
50 using namespace CVC4::parser
;
51 using namespace CVC4::main
;
55 /** Global options variable */
56 CVC4_THREADLOCAL(Options
*) pOptions
;
61 /** Just the basename component of argv[0] */
64 /** A pointer to the CommandExecutor (the signal handlers need it) */
65 CVC4::main::CommandExecutor
* pExecutor
= NULL
;
67 /** A pointer to the totalTime driver stat (the signal handlers need it) */
68 CVC4::TimerStat
* pTotalTime
= NULL
;
70 }/* CVC4::main namespace */
74 void printUsage(Options
& opts
, bool full
) {
76 ss
<< "usage: " << opts
[options::binary_name
] << " [options] [input-file]" << endl
78 << "Without an input file, or with `-', CVC4 reads from standard input." << endl
80 << "CVC4 options:" << endl
;
82 Options::printUsage( ss
.str(), *opts
[options::out
] );
84 Options::printShortUsage( ss
.str(), *opts
[options::out
] );
88 void printStatsFilterZeros(std::ostream
& out
, const std::string
& statsString
) {
89 // read each line, if a number, check zero and skip if so
90 // Stat are assumed to one-per line: "<statName>, <statValue>"
92 std::istringstream
iss(statsString
);
93 std::string statName
, statValue
;
95 std::getline(iss
, statName
, ',');
99 std::getline(iss
, statValue
, '\n');
102 bool isFloat
= (std::istringstream(statValue
) >> curFloat
);
104 if( (isFloat
&& curFloat
== 0) ||
105 statValue
== " \"0\"" ||
106 statValue
== " \"[]\"") {
109 out
<< statName
<< "," << statValue
<< std::endl
;
112 std::getline(iss
, statName
, ',');
117 int runCvc4(int argc
, char* argv
[], Options
& opts
) {
120 pTotalTime
= new TimerStat("totalTime");
123 // For the signal handlers' benefit
126 // Initialize the signal handlers
132 vector
<string
> filenames
= opts
.parseOptions(argc
, argv
);
134 # ifndef PORTFOLIO_BUILD
135 if( opts
.wasSetByUser(options::threads
) ||
136 ! opts
[options::threadArgv
].empty() ) {
137 throw OptionException("Thread options cannot be used with sequential CVC4. Please build and use the portfolio binary `pcvc4'.");
140 if( opts
[options::checkProofs
] ) {
141 throw OptionException("Cannot run portfolio in check-proofs mode.");
145 progName
= opts
[options::binary_name
].c_str();
147 if( opts
[options::help
] ) {
148 printUsage(opts
, true);
150 } else if( opts
[options::languageHelp
] ) {
151 Options::printLanguageHelp(*opts
[options::out
]);
153 } else if( opts
[options::version
] ) {
154 *opts
[options::out
] << Configuration::about().c_str() << flush
;
158 segvSpin
= opts
[options::segvSpin
];
160 // If in competition mode, set output stream option to flush immediately
161 #ifdef CVC4_COMPETITION_MODE
162 *opts
[options::out
] << unitbuf
;
163 #endif /* CVC4_COMPETITION_MODE */
165 // We only accept one input file
166 if(filenames
.size() > 1) {
167 throw Exception("Too many input files specified.");
170 // If no file supplied we will read from standard input
171 const bool inputFromStdin
= filenames
.empty() || filenames
[0] == "-";
173 // if we're reading from stdin on a TTY, default to interactive mode
174 if(!opts
.wasSetByUser(options::interactive
)) {
175 opts
.set(options::interactive
, inputFromStdin
&& isatty(fileno(stdin
)));
178 // Auto-detect input language by filename extension
179 const char* filename
= inputFromStdin
? "<stdin>" : filenames
[0].c_str();
181 if(opts
[options::inputLanguage
] == language::input::LANG_AUTO
) {
182 if( inputFromStdin
) {
183 // We can't do any fancy detection on stdin
184 opts
.set(options::inputLanguage
, language::input::LANG_CVC4
);
186 unsigned len
= strlen(filename
);
187 if(len
>= 5 && !strcmp(".smt2", filename
+ len
- 5)) {
188 opts
.set(options::inputLanguage
, language::input::LANG_SMTLIB_V2
);
189 } else if(len
>= 4 && !strcmp(".smt", filename
+ len
- 4)) {
190 opts
.set(options::inputLanguage
, language::input::LANG_SMTLIB_V1
);
191 } else if(len
>= 5 && !strcmp(".smt1", filename
+ len
- 5)) {
192 opts
.set(options::inputLanguage
, language::input::LANG_SMTLIB_V1
);
193 } else if((len
>= 2 && !strcmp(".p", filename
+ len
- 2))
194 || (len
>= 5 && !strcmp(".tptp", filename
+ len
- 5))) {
195 opts
.set(options::inputLanguage
, language::input::LANG_TPTP
);
196 } else if(( len
>= 4 && !strcmp(".cvc", filename
+ len
- 4) )
197 || ( len
>= 5 && !strcmp(".cvc4", filename
+ len
- 5) )) {
198 opts
.set(options::inputLanguage
, language::input::LANG_CVC4
);
203 if(opts
[options::outputLanguage
] == language::output::LANG_AUTO
) {
204 opts
.set(options::outputLanguage
, language::toOutputLanguage(opts
[options::inputLanguage
]));
207 // Determine which messages to show based on smtcomp_mode and verbosity
208 if(Configuration::isMuzzledBuild()) {
209 DebugChannel
.setStream(CVC4::null_os
);
210 TraceChannel
.setStream(CVC4::null_os
);
211 NoticeChannel
.setStream(CVC4::null_os
);
212 ChatChannel
.setStream(CVC4::null_os
);
213 MessageChannel
.setStream(CVC4::null_os
);
214 WarningChannel
.setStream(CVC4::null_os
);
217 // important even for muzzled builds (to get result output right)
218 *opts
[options::out
] << Expr::setlanguage(opts
[options::outputLanguage
]);
220 // Create the expression manager using appropriate options
221 ExprManager
* exprMgr
;
222 # ifndef PORTFOLIO_BUILD
223 exprMgr
= new ExprManager(opts
);
224 pExecutor
= new CommandExecutor(*exprMgr
, opts
);
226 vector
<Options
> threadOpts
= parseThreadSpecificOptions(opts
);
227 if(opts
.wasSetByUser(options::incrementalSolving
) &&
228 opts
[options::incrementalSolving
] &&
229 !opts
[options::incrementalParallel
]) {
230 Notice() << "Notice: In --incremental mode, using the sequential solver unless forced by...\n"
231 << "Notice: ...the experimental --incremental-parallel option.\n";
232 exprMgr
= new ExprManager(opts
);
233 pExecutor
= new CommandExecutor(*exprMgr
, opts
);
235 exprMgr
= new ExprManager(threadOpts
[0]);
236 pExecutor
= new CommandExecutorPortfolio(*exprMgr
, opts
, threadOpts
);
240 Parser
* replayParser
= NULL
;
241 if( opts
[options::replayFilename
] != "" ) {
242 ParserBuilder
replayParserBuilder(exprMgr
, opts
[options::replayFilename
], opts
);
244 if( opts
[options::replayFilename
] == "-") {
245 if( inputFromStdin
) {
246 throw OptionException("Replay file and input file can't both be stdin.");
248 replayParserBuilder
.withStreamInput(cin
);
250 replayParser
= replayParserBuilder
.build();
251 opts
.set(options::replayStream
, new Parser::ExprStream(replayParser
));
253 if( opts
[options::replayLog
] != NULL
) {
254 *opts
[options::replayLog
] << Expr::setlanguage(opts
[options::outputLanguage
]) << Expr::setdepth(-1);
260 RegisterStatistic
statTotalTime(&pExecutor
->getStatisticsRegistry(), pTotalTime
);
262 // Filename statistics
263 ReferenceStat
< const char* > s_statFilename("filename", filename
);
264 RegisterStatistic
statFilenameReg(&pExecutor
->getStatisticsRegistry(), &s_statFilename
);
266 // Parse and execute commands until we are done
269 if(opts
[options::interactive
] && inputFromStdin
) {
270 if(opts
[options::tearDownIncremental
] && opts
[options::incrementalSolving
]) {
271 if(opts
.wasSetByUser(options::incrementalSolving
)) {
272 throw OptionException("--tear-down-incremental incompatible with --incremental");
275 cmd
= new SetOptionCommand("incremental", false);
277 pExecutor
->doCommand(cmd
);
280 #ifndef PORTFOLIO_BUILD
281 if(!opts
.wasSetByUser(options::incrementalSolving
)) {
282 cmd
= new SetOptionCommand("incremental", true);
284 pExecutor
->doCommand(cmd
);
287 #endif /* PORTFOLIO_BUILD */
288 InteractiveShell
shell(*exprMgr
, opts
);
289 if(opts
[options::interactivePrompt
]) {
290 Message() << Configuration::getPackageName()
291 << " " << Configuration::getVersionString();
292 if(Configuration::isGitBuild()) {
293 Message() << " [" << Configuration::getGitId() << "]";
294 } else if(Configuration::isSubversionBuild()) {
295 Message() << " [" << Configuration::getSubversionId() << "]";
297 Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
299 << (Configuration::isAssertionBuild() ? "on" : "off")
302 if(replayParser
!= NULL
) {
303 // have the replay parser use the declarations input interactively
304 replayParser
->useDeclarationsFrom(shell
.getParser());
306 while((cmd
= shell
.readCommand())) {
307 status
= pExecutor
->doCommand(cmd
) && status
;
310 } else if(opts
[options::tearDownIncremental
]) {
311 if(opts
[options::incrementalSolving
]) {
312 if(opts
.wasSetByUser(options::incrementalSolving
)) {
313 throw OptionException("--tear-down-incremental incompatible with --incremental");
316 cmd
= new SetOptionCommand("incremental", false);
318 pExecutor
->doCommand(cmd
);
322 ParserBuilder
parserBuilder(exprMgr
, filename
, opts
);
324 if( inputFromStdin
) {
325 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
326 parserBuilder
.withStreamInput(cin
);
327 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
328 parserBuilder
.withLineBufferedStreamInput(cin
);
329 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
332 vector
< vector
<Command
*> > allCommands
;
333 allCommands
.push_back(vector
<Command
*>());
334 Parser
*parser
= parserBuilder
.build();
335 if(replayParser
!= NULL
) {
336 // have the replay parser use the file's declarations
337 replayParser
->useDeclarationsFrom(parser
);
339 bool needReset
= false;
340 while(status
&& (cmd
= parser
->nextCommand())) {
341 if(dynamic_cast<PushCommand
*>(cmd
) != NULL
) {
344 for(size_t i
= 0; i
< allCommands
.size(); ++i
) {
345 for(size_t j
= 0; j
< allCommands
[i
].size(); ++j
) {
346 Command
* cmd
= allCommands
[i
][j
]->clone();
348 pExecutor
->doCommand(cmd
);
354 *opts
[options::out
] << CommandSuccess();
355 allCommands
.push_back(vector
<Command
*>());
356 } else if(dynamic_cast<PopCommand
*>(cmd
) != NULL
) {
357 allCommands
.pop_back(); // fixme leaks cmds here
359 for(size_t i
= 0; i
< allCommands
.size(); ++i
) {
360 for(size_t j
= 0; j
< allCommands
[i
].size(); ++j
) {
361 Command
* cmd
= allCommands
[i
][j
]->clone();
363 pExecutor
->doCommand(cmd
);
367 *opts
[options::out
] << CommandSuccess();
368 } else if(dynamic_cast<CheckSatCommand
*>(cmd
) != NULL
||
369 dynamic_cast<QueryCommand
*>(cmd
) != NULL
) {
372 for(size_t i
= 0; i
< allCommands
.size(); ++i
) {
373 for(size_t j
= 0; j
< allCommands
[i
].size(); ++j
) {
374 Command
* cmd
= allCommands
[i
][j
]->clone();
376 pExecutor
->doCommand(cmd
);
381 status
= pExecutor
->doCommand(cmd
);
384 Command
* copy
= cmd
->clone();
385 allCommands
.back().push_back(copy
);
386 if(dynamic_cast<QuitCommand
*>(cmd
) != NULL
) {
390 status
= pExecutor
->doCommand(cmd
);
397 if(!opts
.wasSetByUser(options::incrementalSolving
)) {
398 cmd
= new SetOptionCommand("incremental", false);
400 pExecutor
->doCommand(cmd
);
404 ParserBuilder
parserBuilder(exprMgr
, filename
, opts
);
406 if( inputFromStdin
) {
407 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
408 parserBuilder
.withStreamInput(cin
);
409 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
410 parserBuilder
.withLineBufferedStreamInput(cin
);
411 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
414 Parser
*parser
= parserBuilder
.build();
415 if(replayParser
!= NULL
) {
416 // have the replay parser use the file's declarations
417 replayParser
->useDeclarationsFrom(parser
);
419 while(status
&& (cmd
= parser
->nextCommand())) {
420 if(dynamic_cast<QuitCommand
*>(cmd
) != NULL
) {
424 status
= pExecutor
->doCommand(cmd
);
431 if( opts
[options::replayStream
] != NULL
) {
432 // this deletes the expression parser too
433 delete opts
[options::replayStream
];
434 opts
.set(options::replayStream
, NULL
);
439 result
= pExecutor
->getResult();
442 // there was some kind of error
446 #ifdef CVC4_COMPETITION_MODE
447 // exit, don't return (don't want destructors to run)
448 // _exit() from unistd.h doesn't run global destructors
449 // or other on_exit/atexit stuff.
451 #endif /* CVC4_COMPETITION_MODE */
453 ReferenceStat
< Result
> s_statSatResult("sat/unsat", result
);
454 RegisterStatistic
statSatResultReg(&pExecutor
->getStatisticsRegistry(), &s_statSatResult
);
458 // Set the global executor pointer to NULL first. If we get a
459 // signal while dumping statistics, we don't want to try again.
460 if(opts
[options::statistics
]) {
461 if(opts
[options::statsHideZeros
] == false) {
462 pExecutor
->flushStatistics(*opts
[options::err
]);
464 std::ostringstream ossStats
;
465 pExecutor
->flushStatistics(ossStats
);
466 printStatsFilterZeros(*opts
[options::err
], ossStats
.str());
470 // make sure to flush replay output log before early-exit
471 if( opts
[options::replayLog
] != NULL
) {
472 *opts
[options::replayLog
] << flush
;
475 // make sure out and err streams are flushed too
476 *opts
[options::out
] << flush
;
477 *opts
[options::err
] << flush
;
480 if(opts
[options::earlyExit
] && opts
.wasSetByUser(options::earlyExit
)) {
483 #else /* CVC4_DEBUG */
484 if(opts
[options::earlyExit
]) {
487 #endif /* CVC4_DEBUG */
490 // On exceptional exit, these are leaked, but that's okay... they
491 // need to be around in that case for main() to print statistics.