1 /********************* */
2 /*! \file driver_unified.cpp
4 ** Top contributors (to current version):
5 ** Morgan Deters, Liana Hadarean, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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)
25 #include "cvc4autoconfig.h"
27 #include "api/cvc4cpp.h"
28 #include "base/configuration.h"
29 #include "base/output.h"
30 #include "expr/expr_iomanip.h"
31 #include "expr/expr_manager.h"
32 #include "main/command_executor.h"
33 #include "main/interactive_shell.h"
34 #include "main/main.h"
35 #include "main/signal_handlers.h"
36 #include "main/time_limit.h"
37 #include "options/options.h"
38 #include "options/set_language.h"
39 #include "parser/parser.h"
40 #include "parser/parser_builder.h"
41 #include "parser/parser_exception.h"
42 #include "smt/command.h"
43 #include "util/result.h"
44 #include "util/statistics_registry.h"
48 using namespace CVC4::parser
;
49 using namespace CVC4::main
;
53 /** Global options variable */
54 thread_local Options
* pOptions
;
59 /** Just the basename component of argv[0] */
60 const std::string
*progName
;
62 /** A pointer to the CommandExecutor (the signal handlers need it) */
63 CVC4::main::CommandExecutor
* pExecutor
= nullptr;
65 /** A pointer to the totalTime driver stat (the signal handlers need it) */
66 CVC4::TimerStat
* pTotalTime
= nullptr;
68 }/* CVC4::main namespace */
72 void printUsage(Options
& opts
, bool full
) {
74 ss
<< "usage: " << opts
.getBinaryName() << " [options] [input-file]"
76 << "Without an input file, or with `-', CVC4 reads from standard input."
78 << "CVC4 options:" << endl
;
80 Options::printUsage( ss
.str(), *(opts
.getOut()) );
82 Options::printShortUsage( ss
.str(), *(opts
.getOut()) );
86 int runCvc4(int argc
, char* argv
[], Options
& opts
) {
89 pTotalTime
= new TimerStat("totalTime");
92 // For the signal handlers' benefit
95 // Initialize the signal handlers
96 signal_handlers::install();
101 vector
<string
> filenames
= Options::parseOptions(&opts
, argc
, argv
);
103 install_time_limit(opts
);
105 string progNameStr
= opts
.getBinaryName();
106 progName
= &progNameStr
;
108 if( opts
.getHelp() ) {
109 printUsage(opts
, true);
111 } else if( opts
.getLanguageHelp() ) {
112 Options::printLanguageHelp(*(opts
.getOut()));
114 } else if( opts
.getVersion() ) {
115 *(opts
.getOut()) << Configuration::about().c_str() << flush
;
119 segvSpin
= opts
.getSegvSpin();
121 // If in competition mode, set output stream option to flush immediately
122 #ifdef CVC4_COMPETITION_MODE
123 *(opts
.getOut()) << unitbuf
;
124 #endif /* CVC4_COMPETITION_MODE */
126 // We only accept one input file
127 if(filenames
.size() > 1) {
128 throw Exception("Too many input files specified.");
131 // If no file supplied we will read from standard input
132 const bool inputFromStdin
= filenames
.empty() || filenames
[0] == "-";
134 // if we're reading from stdin on a TTY, default to interactive mode
135 if(!opts
.wasSetByUserInteractive()) {
136 opts
.setInteractive(inputFromStdin
&& isatty(fileno(stdin
)));
139 // Auto-detect input language by filename extension
140 std::string
filenameStr("<stdin>");
141 if (!inputFromStdin
) {
142 // Use swap to avoid copying the string
143 // TODO: use std::move() when switching to c++11
144 filenameStr
.swap(filenames
[0]);
146 const char* filename
= filenameStr
.c_str();
148 if(opts
.getInputLanguage() == language::input::LANG_AUTO
) {
149 if( inputFromStdin
) {
150 // We can't do any fancy detection on stdin
151 opts
.setInputLanguage(language::input::LANG_CVC4
);
153 unsigned len
= filenameStr
.size();
154 if(len
>= 5 && !strcmp(".smt2", filename
+ len
- 5)) {
155 opts
.setInputLanguage(language::input::LANG_SMTLIB_V2_6
);
156 } else if((len
>= 2 && !strcmp(".p", filename
+ len
- 2))
157 || (len
>= 5 && !strcmp(".tptp", filename
+ len
- 5))) {
158 opts
.setInputLanguage(language::input::LANG_TPTP
);
159 } else if(( len
>= 4 && !strcmp(".cvc", filename
+ len
- 4) )
160 || ( len
>= 5 && !strcmp(".cvc4", filename
+ len
- 5) )) {
161 opts
.setInputLanguage(language::input::LANG_CVC4
);
162 } else if((len
>= 3 && !strcmp(".sy", filename
+ len
- 3))
163 || (len
>= 3 && !strcmp(".sl", filename
+ len
- 3))) {
164 // version 2 sygus is the default
165 opts
.setInputLanguage(language::input::LANG_SYGUS_V2
);
170 if(opts
.getOutputLanguage() == language::output::LANG_AUTO
) {
171 opts
.setOutputLanguage(language::toOutputLanguage(opts
.getInputLanguage()));
174 // Determine which messages to show based on smtcomp_mode and verbosity
175 if(Configuration::isMuzzledBuild()) {
176 DebugChannel
.setStream(&CVC4::null_os
);
177 TraceChannel
.setStream(&CVC4::null_os
);
178 NoticeChannel
.setStream(&CVC4::null_os
);
179 ChatChannel
.setStream(&CVC4::null_os
);
180 MessageChannel
.setStream(&CVC4::null_os
);
181 WarningChannel
.setStream(&CVC4::null_os
);
184 // important even for muzzled builds (to get result output right)
185 (*(opts
.getOut())) << language::SetLanguage(opts
.getOutputLanguage());
187 // Create the command executor to execute the parsed commands
188 pExecutor
= new CommandExecutor(opts
);
193 RegisterStatistic
statTotalTime(&pExecutor
->getStatisticsRegistry(),
196 // Filename statistics
197 ReferenceStat
<std::string
> s_statFilename("filename", filenameStr
);
198 RegisterStatistic
statFilenameReg(&pExecutor
->getStatisticsRegistry(),
200 // notify SmtEngine that we are starting to parse
201 pExecutor
->getSmtEngine()->notifyStartParsing(filenameStr
);
203 // Parse and execute commands until we are done
204 std::unique_ptr
<Command
> cmd
;
206 if(opts
.getInteractive() && inputFromStdin
) {
207 if(opts
.getTearDownIncremental() > 0) {
208 throw OptionException(
209 "--tear-down-incremental doesn't work in interactive mode");
211 if(!opts
.wasSetByUserIncrementalSolving()) {
212 cmd
.reset(new SetOptionCommand("incremental", "true"));
214 pExecutor
->doCommand(cmd
);
216 InteractiveShell
shell(pExecutor
->getSolver(),
217 pExecutor
->getSymbolManager());
218 if(opts
.getInteractivePrompt()) {
219 CVC4Message() << Configuration::getPackageName() << " "
220 << Configuration::getVersionString();
221 if(Configuration::isGitBuild()) {
222 CVC4Message() << " [" << Configuration::getGitId() << "]";
224 CVC4Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
226 << (Configuration::isAssertionBuild() ? "on" : "off")
229 CVC4Message() << Configuration::copyright() << endl
;
234 cmd
.reset(shell
.readCommand());
235 } catch(UnsafeInterruptException
& e
) {
236 (*opts
.getOut()) << CommandInterrupted();
241 status
= pExecutor
->doCommand(cmd
) && status
;
242 if (cmd
->interrupted()) {
246 } else if( opts
.getTearDownIncremental() > 0) {
247 if(!opts
.getIncrementalSolving() && opts
.getTearDownIncremental() > 1) {
248 // For tear-down-incremental values greater than 1, need incremental
250 cmd
.reset(new SetOptionCommand("incremental", "true"));
252 pExecutor
->doCommand(cmd
);
253 // if(opts.wasSetByUserIncrementalSolving()) {
254 // throw OptionException(
255 // "--tear-down-incremental incompatible with --incremental");
258 // cmd.reset(new SetOptionCommand("incremental", SExpr(false)));
259 // cmd->setMuted(true);
260 // pExecutor->doCommand(cmd);
263 ParserBuilder
parserBuilder(pExecutor
->getSolver(),
264 pExecutor
->getSymbolManager(),
268 if( inputFromStdin
) {
269 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
270 parserBuilder
.withStreamInput(cin
);
271 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
272 parserBuilder
.withLineBufferedStreamInput(cin
);
273 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
276 vector
< vector
<Command
*> > allCommands
;
277 allCommands
.push_back(vector
<Command
*>());
278 std::unique_ptr
<Parser
> parser(parserBuilder
.build());
280 // true if one of the commands was interrupted
281 bool interrupted
= false;
285 (*opts
.getOut()) << CommandInterrupted();
290 cmd
.reset(parser
->nextCommand());
291 if (cmd
== nullptr) break;
292 } catch (UnsafeInterruptException
& e
) {
297 if(dynamic_cast<PushCommand
*>(cmd
.get()) != nullptr) {
298 if(needReset
>= opts
.getTearDownIncremental()) {
300 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
301 if (interrupted
) break;
302 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
304 Command
* ccmd
= allCommands
[i
][j
]->clone();
305 ccmd
->setMuted(true);
306 pExecutor
->doCommand(ccmd
);
307 if (ccmd
->interrupted())
316 allCommands
.push_back(vector
<Command
*>());
317 Command
* copy
= cmd
->clone();
318 allCommands
.back().push_back(copy
);
319 status
= pExecutor
->doCommand(cmd
);
320 if(cmd
->interrupted()) {
324 } else if(dynamic_cast<PopCommand
*>(cmd
.get()) != nullptr) {
325 allCommands
.pop_back(); // fixme leaks cmds here
326 if (needReset
>= opts
.getTearDownIncremental()) {
328 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
329 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
331 std::unique_ptr
<Command
> ccmd(allCommands
[i
][j
]->clone());
332 ccmd
->setMuted(true);
333 pExecutor
->doCommand(ccmd
);
334 if (ccmd
->interrupted())
340 if (interrupted
) continue;
341 (*opts
.getOut()) << CommandSuccess();
344 status
= pExecutor
->doCommand(cmd
);
345 if(cmd
->interrupted()) {
350 } else if(dynamic_cast<CheckSatCommand
*>(cmd
.get()) != nullptr ||
351 dynamic_cast<QueryCommand
*>(cmd
.get()) != nullptr) {
352 if(needReset
>= opts
.getTearDownIncremental()) {
354 for(size_t i
= 0; i
< allCommands
.size() && !interrupted
; ++i
) {
355 for(size_t j
= 0; j
< allCommands
[i
].size() && !interrupted
; ++j
)
357 Command
* ccmd
= allCommands
[i
][j
]->clone();
358 ccmd
->setMuted(true);
359 pExecutor
->doCommand(ccmd
);
360 if (ccmd
->interrupted())
375 status
= pExecutor
->doCommand(cmd
);
376 if(cmd
->interrupted()) {
380 } else if(dynamic_cast<ResetCommand
*>(cmd
.get()) != nullptr) {
381 pExecutor
->doCommand(cmd
);
383 allCommands
.push_back(vector
<Command
*>());
385 // We shouldn't copy certain commands, because they can cause
386 // an error on replay since there's no associated sat/unsat check
388 if(dynamic_cast<GetUnsatCoreCommand
*>(cmd
.get()) == nullptr &&
389 dynamic_cast<GetProofCommand
*>(cmd
.get()) == nullptr &&
390 dynamic_cast<GetValueCommand
*>(cmd
.get()) == nullptr &&
391 dynamic_cast<GetModelCommand
*>(cmd
.get()) == nullptr &&
392 dynamic_cast<GetAssignmentCommand
*>(cmd
.get()) == nullptr &&
393 dynamic_cast<GetInstantiationsCommand
*>(cmd
.get()) == nullptr &&
394 dynamic_cast<GetAssertionsCommand
*>(cmd
.get()) == nullptr &&
395 dynamic_cast<GetInfoCommand
*>(cmd
.get()) == nullptr &&
396 dynamic_cast<GetOptionCommand
*>(cmd
.get()) == nullptr &&
397 dynamic_cast<EchoCommand
*>(cmd
.get()) == nullptr) {
398 Command
* copy
= cmd
->clone();
399 allCommands
.back().push_back(copy
);
401 status
= pExecutor
->doCommand(cmd
);
402 if(cmd
->interrupted()) {
407 if(dynamic_cast<QuitCommand
*>(cmd
.get()) != nullptr) {
413 if(!opts
.wasSetByUserIncrementalSolving()) {
414 cmd
.reset(new SetOptionCommand("incremental", "false"));
416 pExecutor
->doCommand(cmd
);
419 ParserBuilder
parserBuilder(pExecutor
->getSolver(),
420 pExecutor
->getSymbolManager(),
424 if( inputFromStdin
) {
425 #if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
426 parserBuilder
.withStreamInput(cin
);
427 #else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
428 parserBuilder
.withLineBufferedStreamInput(cin
);
429 #endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
432 std::unique_ptr
<Parser
> parser(parserBuilder
.build());
433 bool interrupted
= false;
437 (*opts
.getOut()) << CommandInterrupted();
442 cmd
.reset(parser
->nextCommand());
443 if (cmd
== nullptr) break;
444 } catch (UnsafeInterruptException
& e
) {
449 status
= pExecutor
->doCommand(cmd
);
450 if (cmd
->interrupted() && status
== 0) {
455 if(dynamic_cast<QuitCommand
*>(cmd
.get()) != nullptr) {
463 result
= pExecutor
->getResult();
466 // there was some kind of error
470 #ifdef CVC4_COMPETITION_MODE
472 // exit, don't return (don't want destructors to run)
473 // _exit() from unistd.h doesn't run global destructors
474 // or other on_exit/atexit stuff.
476 #endif /* CVC4_COMPETITION_MODE */
478 ReferenceStat
<api::Result
> s_statSatResult("sat/unsat", result
);
479 RegisterStatistic
statSatResultReg(&pExecutor
->getStatisticsRegistry(),
484 // Tim: I think that following comment is out of date?
485 // Set the global executor pointer to nullptr first. If we get a
486 // signal while dumping statistics, we don't want to try again.
487 pExecutor
->flushOutputStreams();
490 if(opts
.getEarlyExit() && opts
.wasSetByUserEarlyExit()) {
493 #else /* CVC4_DEBUG */
494 if(opts
.getEarlyExit()) {
497 #endif /* CVC4_DEBUG */
500 // On exceptional exit, these are leaked, but that's okay... they
501 // need to be around in that case for main() to print statistics.
505 pTotalTime
= nullptr;
508 signal_handlers::cleanup();