1 /******************************************************************************
2 * Top contributors (to current version):
3 * Morgan Deters, Liana Hadarean, Tim King
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 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.
11 * ****************************************************************************
13 * Driver for cvc5 executable (cvc5).
27 #include "api/cpp/cvc5.h"
28 #include "base/configuration.h"
29 #include "base/cvc5config.h"
30 #include "base/output.h"
31 #include "main/command_executor.h"
32 #include "main/interactive_shell.h"
33 #include "main/main.h"
34 #include "main/signal_handlers.h"
35 #include "main/time_limit.h"
36 #include "options/base_options.h"
37 #include "options/options.h"
38 #include "options/options_public.h"
39 #include "options/parser_options.h"
40 #include "options/main_options.h"
41 #include "options/set_language.h"
42 #include "parser/parser.h"
43 #include "parser/parser_builder.h"
44 #include "smt/command.h"
45 #include "smt/smt_engine.h"
46 #include "util/result.h"
50 using namespace cvc5::parser
;
51 using namespace cvc5::main
;
59 /** Just the basename component of argv[0] */
62 /** A pointer to the CommandExecutor (the signal handlers need it) */
63 std::unique_ptr
<cvc5::main::CommandExecutor
> pExecutor
;
65 /** The time point the binary started, accessible to signal handlers */
66 std::unique_ptr
<TotalTimer
> totalTime
;
68 TotalTimer::~TotalTimer()
70 if (pExecutor
!= nullptr)
72 auto duration
= std::chrono::steady_clock::now() - d_start
;
73 pExecutor
->getSmtEngine()->setTotalTimeStatistic(
74 std::chrono::duration
<double>(duration
).count());
81 void printUsage(const Options
& opts
, bool full
) {
83 ss
<< "usage: " << progName
<< " [options] [input-file]"
86 << "Without an input file, or with `-', cvc5 reads from standard input."
89 << "cvc5 options:" << endl
;
91 options::printUsage(ss
.str(), *opts
.base
.out
);
93 options::printShortUsage(ss
.str(), *opts
.base
.out
);
97 int runCvc5(int argc
, char* argv
[], Options
& opts
)
99 main::totalTime
= std::make_unique
<TotalTimer
>();
101 // Initialize the signal handlers
102 signal_handlers::install();
107 std::vector
<string
> filenames
= options::parse(opts
, argc
, argv
, progName
);
109 auto limit
= install_time_limit(opts
);
111 if (opts
.driver
.help
)
113 printUsage(opts
, true);
116 else if (opts
.base
.languageHelp
)
118 options::printLanguageHelp(*opts
.base
.out
);
121 else if (opts
.driver
.version
)
123 *opts
.base
.out
<< Configuration::about().c_str() << flush
;
127 segvSpin
= opts
.driver
.segvSpin
;
129 // If in competition mode, set output stream option to flush immediately
130 #ifdef CVC5_COMPETITION_MODE
131 *opts
.base
.out
<< unitbuf
;
132 #endif /* CVC5_COMPETITION_MODE */
134 // We only accept one input file
135 if(filenames
.size() > 1) {
136 throw Exception("Too many input files specified.");
139 // If no file supplied we will read from standard input
140 const bool inputFromStdin
= filenames
.empty() || filenames
[0] == "-";
142 // if we're reading from stdin on a TTY, default to interactive mode
143 if (!opts
.driver
.interactiveWasSetByUser
)
145 opts
.driver
.interactive
= inputFromStdin
&& isatty(fileno(stdin
));
148 // Auto-detect input language by filename extension
149 std::string
filenameStr("<stdin>");
150 if (!inputFromStdin
) {
151 // Use swap to avoid copying the string
152 // TODO: use std::move() when switching to c++11
153 filenameStr
.swap(filenames
[0]);
155 const char* filename
= filenameStr
.c_str();
157 if (opts
.base
.inputLanguage
== language::input::LANG_AUTO
)
159 if( inputFromStdin
) {
160 // We can't do any fancy detection on stdin
161 opts
.base
.inputLanguage
= language::input::LANG_CVC
;
163 size_t len
= filenameStr
.size();
164 if(len
>= 5 && !strcmp(".smt2", filename
+ len
- 5)) {
165 opts
.base
.inputLanguage
= language::input::LANG_SMTLIB_V2_6
;
166 } else if((len
>= 2 && !strcmp(".p", filename
+ len
- 2))
167 || (len
>= 5 && !strcmp(".tptp", filename
+ len
- 5))) {
168 opts
.base
.inputLanguage
= language::input::LANG_TPTP
;
169 } else if(( len
>= 4 && !strcmp(".cvc", filename
+ len
- 4) )
170 || ( len
>= 5 && !strcmp(".cvc4", filename
+ len
- 5) )) {
171 opts
.base
.inputLanguage
= language::input::LANG_CVC
;
172 } else if((len
>= 3 && !strcmp(".sy", filename
+ len
- 3))
173 || (len
>= 3 && !strcmp(".sl", filename
+ len
- 3))) {
174 // version 2 sygus is the default
175 opts
.base
.inputLanguage
= language::input::LANG_SYGUS_V2
;
180 if (opts
.base
.outputLanguage
== language::output::LANG_AUTO
)
182 opts
.base
.outputLanguage
= language::toOutputLanguage(opts
.base
.inputLanguage
);
185 // Determine which messages to show based on smtcomp_mode and verbosity
186 if(Configuration::isMuzzledBuild()) {
187 DebugChannel
.setStream(&cvc5::null_os
);
188 TraceChannel
.setStream(&cvc5::null_os
);
189 NoticeChannel
.setStream(&cvc5::null_os
);
190 ChatChannel
.setStream(&cvc5::null_os
);
191 MessageChannel
.setStream(&cvc5::null_os
);
192 WarningChannel
.setStream(&cvc5::null_os
);
195 // important even for muzzled builds (to get result output right)
197 << language::SetLanguage(opts
.base
.outputLanguage
);
199 // Create the command executor to execute the parsed commands
200 pExecutor
= std::make_unique
<CommandExecutor
>(opts
);
204 // notify SmtEngine that we are starting to parse
205 pExecutor
->getSmtEngine()->notifyStartParsing(filenameStr
);
207 // Parse and execute commands until we are done
208 std::unique_ptr
<Command
> cmd
;
210 if (opts
.driver
.interactive
&& inputFromStdin
)
212 if (!opts
.base
.incrementalSolvingWasSetByUser
)
214 cmd
.reset(new SetOptionCommand("incremental", "true"));
216 pExecutor
->doCommand(cmd
);
218 InteractiveShell
shell(pExecutor
->getSolver(),
219 pExecutor
->getSymbolManager());
220 if (opts
.driver
.interactivePrompt
)
222 CVC5Message() << Configuration::getPackageName() << " "
223 << Configuration::getVersionString();
224 if(Configuration::isGitBuild()) {
225 CVC5Message() << " [" << Configuration::getGitId() << "]";
227 CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "")
229 << (Configuration::isAssertionBuild() ? "on" : "off")
232 CVC5Message() << Configuration::copyright() << endl
;
237 cmd
.reset(shell
.readCommand());
238 } catch(UnsafeInterruptException
& e
) {
239 *opts
.base
.out
<< CommandInterrupted();
244 status
= pExecutor
->doCommand(cmd
) && status
;
245 if (cmd
->interrupted()) {
252 if (!opts
.base
.incrementalSolvingWasSetByUser
)
254 cmd
.reset(new SetOptionCommand("incremental", "false"));
256 pExecutor
->doCommand(cmd
);
259 ParserBuilder
parserBuilder(pExecutor
->getSolver(),
260 pExecutor
->getSymbolManager(),
262 std::unique_ptr
<Parser
> parser(parserBuilder
.build());
263 if( inputFromStdin
) {
264 parser
->setInput(Input::newStreamInput(
265 opts
.base
.inputLanguage
, cin
, filename
));
269 parser
->setInput(Input::newFileInput(opts
.base
.inputLanguage
,
271 opts
.parser
.memoryMap
));
274 bool interrupted
= false;
278 *opts
.base
.out
<< CommandInterrupted();
283 cmd
.reset(parser
->nextCommand());
284 if (cmd
== nullptr) break;
285 } catch (UnsafeInterruptException
& e
) {
290 status
= pExecutor
->doCommand(cmd
);
291 if (cmd
->interrupted() && status
== 0) {
296 if(dynamic_cast<QuitCommand
*>(cmd
.get()) != nullptr) {
304 result
= pExecutor
->getResult();
307 // there was some kind of error
311 #ifdef CVC5_COMPETITION_MODE
312 if (opts
.base
.out
!= nullptr)
314 *opts
.base
.out
<< std::flush
;
316 // exit, don't return (don't want destructors to run)
317 // _exit() from unistd.h doesn't run global destructors
318 // or other on_exit/atexit stuff.
320 #endif /* CVC5_COMPETITION_MODE */
323 pExecutor
->flushOutputStreams();
326 if (opts
.driver
.earlyExit
&& opts
.driver
.earlyExitWasSetByUser
)
330 #else /* CVC5_DEBUG */
331 if (opts
.driver
.earlyExit
)
335 #endif /* CVC5_DEBUG */
340 signal_handlers::cleanup();