1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Morgan Deters, Liana Hadarean, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
12 |
|
* |
13 |
|
* Driver for cvc5 executable (cvc5). |
14 |
|
*/ |
15 |
|
|
16 |
|
#include <stdio.h> |
17 |
|
#include <unistd.h> |
18 |
|
|
19 |
|
#include <chrono> |
20 |
|
#include <cstdlib> |
21 |
|
#include <cstring> |
22 |
|
#include <fstream> |
23 |
|
#include <iostream> |
24 |
|
#include <memory> |
25 |
|
#include <new> |
26 |
|
|
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" |
47 |
|
|
48 |
|
using namespace std; |
49 |
|
using namespace cvc5; |
50 |
|
using namespace cvc5::parser; |
51 |
|
using namespace cvc5::main; |
52 |
|
|
53 |
|
namespace cvc5 { |
54 |
|
namespace main { |
55 |
|
|
56 |
|
/** Full argv[0] */ |
57 |
|
const char* progPath; |
58 |
|
|
59 |
|
/** Just the basename component of argv[0] */ |
60 |
9773 |
std::string progName; |
61 |
|
|
62 |
|
/** A pointer to the CommandExecutor (the signal handlers need it) */ |
63 |
9773 |
std::unique_ptr<cvc5::main::CommandExecutor> pExecutor; |
64 |
|
|
65 |
|
/** The time point the binary started, accessible to signal handlers */ |
66 |
9773 |
std::unique_ptr<TotalTimer> totalTime; |
67 |
|
|
68 |
17480 |
TotalTimer::~TotalTimer() |
69 |
|
{ |
70 |
8740 |
if (pExecutor != nullptr) |
71 |
|
{ |
72 |
6131 |
auto duration = std::chrono::steady_clock::now() - d_start; |
73 |
12262 |
pExecutor->getSmtEngine()->setTotalTimeStatistic( |
74 |
12262 |
std::chrono::duration<double>(duration).count()); |
75 |
|
} |
76 |
8740 |
} |
77 |
|
|
78 |
|
} // namespace main |
79 |
|
} // namespace cvc5 |
80 |
|
|
81 |
|
void printUsage(const Options& opts, bool full) { |
82 |
|
stringstream ss; |
83 |
|
ss << "usage: " << progName << " [options] [input-file]" |
84 |
|
<< endl |
85 |
|
<< endl |
86 |
|
<< "Without an input file, or with `-', cvc5 reads from standard input." |
87 |
|
<< endl |
88 |
|
<< endl |
89 |
|
<< "cvc5 options:" << endl; |
90 |
|
if(full) { |
91 |
|
options::printUsage(ss.str(), *opts.base.out); |
92 |
|
} else { |
93 |
|
options::printShortUsage(ss.str(), *opts.base.out); |
94 |
|
} |
95 |
|
} |
96 |
|
|
97 |
8740 |
int runCvc5(int argc, char* argv[], Options& opts) |
98 |
|
{ |
99 |
8740 |
main::totalTime = std::make_unique<TotalTimer>(); |
100 |
|
|
101 |
|
// Initialize the signal handlers |
102 |
8740 |
signal_handlers::install(); |
103 |
|
|
104 |
8740 |
progPath = argv[0]; |
105 |
|
|
106 |
|
// Parse the options |
107 |
14871 |
std::vector<string> filenames = options::parse(opts, argc, argv, progName); |
108 |
|
|
109 |
12262 |
auto limit = install_time_limit(opts); |
110 |
|
|
111 |
6131 |
if (opts.driver.help) |
112 |
|
{ |
113 |
|
printUsage(opts, true); |
114 |
|
exit(1); |
115 |
|
} |
116 |
6131 |
else if (opts.base.languageHelp) |
117 |
|
{ |
118 |
|
options::printLanguageHelp(*opts.base.out); |
119 |
|
exit(1); |
120 |
|
} |
121 |
6131 |
else if (opts.driver.version) |
122 |
|
{ |
123 |
|
*opts.base.out << Configuration::about().c_str() << flush; |
124 |
|
exit(0); |
125 |
|
} |
126 |
|
|
127 |
6131 |
segvSpin = opts.driver.segvSpin; |
128 |
|
|
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 */ |
133 |
|
|
134 |
|
// We only accept one input file |
135 |
6131 |
if(filenames.size() > 1) { |
136 |
|
throw Exception("Too many input files specified."); |
137 |
|
} |
138 |
|
|
139 |
|
// If no file supplied we will read from standard input |
140 |
6131 |
const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; |
141 |
|
|
142 |
|
// if we're reading from stdin on a TTY, default to interactive mode |
143 |
6131 |
if (!opts.driver.interactiveWasSetByUser) |
144 |
|
{ |
145 |
6131 |
opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); |
146 |
|
} |
147 |
|
|
148 |
|
// Auto-detect input language by filename extension |
149 |
12262 |
std::string filenameStr("<stdin>"); |
150 |
6131 |
if (!inputFromStdin) { |
151 |
|
// Use swap to avoid copying the string |
152 |
|
// TODO: use std::move() when switching to c++11 |
153 |
6131 |
filenameStr.swap(filenames[0]); |
154 |
|
} |
155 |
6131 |
const char* filename = filenameStr.c_str(); |
156 |
|
|
157 |
6131 |
if (opts.base.inputLanguage == language::input::LANG_AUTO) |
158 |
|
{ |
159 |
5904 |
if( inputFromStdin ) { |
160 |
|
// We can't do any fancy detection on stdin |
161 |
|
opts.base.inputLanguage = language::input::LANG_CVC; |
162 |
|
} else { |
163 |
5904 |
size_t len = filenameStr.size(); |
164 |
5904 |
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { |
165 |
5050 |
opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; |
166 |
854 |
} else if((len >= 2 && !strcmp(".p", filename + len - 2)) |
167 |
813 |
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) { |
168 |
41 |
opts.base.inputLanguage = language::input::LANG_TPTP; |
169 |
813 |
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) |
170 |
11 |
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { |
171 |
802 |
opts.base.inputLanguage = language::input::LANG_CVC; |
172 |
11 |
} 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 |
11 |
opts.base.inputLanguage = language::input::LANG_SYGUS_V2; |
176 |
|
} |
177 |
|
} |
178 |
|
} |
179 |
|
|
180 |
6131 |
if (opts.base.outputLanguage == language::output::LANG_AUTO) |
181 |
|
{ |
182 |
6131 |
opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); |
183 |
|
} |
184 |
|
|
185 |
|
// Determine which messages to show based on smtcomp_mode and verbosity |
186 |
6131 |
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); |
193 |
|
} |
194 |
|
|
195 |
|
// important even for muzzled builds (to get result output right) |
196 |
6131 |
(*opts.base.out) |
197 |
6131 |
<< language::SetLanguage(opts.base.outputLanguage); |
198 |
|
|
199 |
|
// Create the command executor to execute the parsed commands |
200 |
6131 |
pExecutor = std::make_unique<CommandExecutor>(opts); |
201 |
|
|
202 |
6131 |
int returnValue = 0; |
203 |
|
{ |
204 |
|
// notify SmtEngine that we are starting to parse |
205 |
6131 |
pExecutor->getSmtEngine()->notifyStartParsing(filenameStr); |
206 |
|
|
207 |
|
// Parse and execute commands until we are done |
208 |
12262 |
std::unique_ptr<Command> cmd; |
209 |
6131 |
bool status = true; |
210 |
6131 |
if (opts.driver.interactive && inputFromStdin) |
211 |
|
{ |
212 |
|
if (!opts.base.incrementalSolvingWasSetByUser) |
213 |
|
{ |
214 |
|
cmd.reset(new SetOptionCommand("incremental", "true")); |
215 |
|
cmd->setMuted(true); |
216 |
|
pExecutor->doCommand(cmd); |
217 |
|
} |
218 |
|
InteractiveShell shell(pExecutor->getSolver(), |
219 |
|
pExecutor->getSymbolManager()); |
220 |
|
if (opts.driver.interactivePrompt) |
221 |
|
{ |
222 |
|
CVC5Message() << Configuration::getPackageName() << " " |
223 |
|
<< Configuration::getVersionString(); |
224 |
|
if(Configuration::isGitBuild()) { |
225 |
|
CVC5Message() << " [" << Configuration::getGitId() << "]"; |
226 |
|
} |
227 |
|
CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") |
228 |
|
<< " assertions:" |
229 |
|
<< (Configuration::isAssertionBuild() ? "on" : "off") |
230 |
|
<< endl |
231 |
|
<< endl; |
232 |
|
CVC5Message() << Configuration::copyright() << endl; |
233 |
|
} |
234 |
|
|
235 |
|
while(true) { |
236 |
|
try { |
237 |
|
cmd.reset(shell.readCommand()); |
238 |
|
} catch(UnsafeInterruptException& e) { |
239 |
|
*opts.base.out << CommandInterrupted(); |
240 |
|
break; |
241 |
|
} |
242 |
|
if (cmd == nullptr) |
243 |
|
break; |
244 |
|
status = pExecutor->doCommand(cmd) && status; |
245 |
|
if (cmd->interrupted()) { |
246 |
|
break; |
247 |
|
} |
248 |
|
} |
249 |
|
} |
250 |
|
else |
251 |
|
{ |
252 |
6131 |
if (!opts.base.incrementalSolvingWasSetByUser) |
253 |
|
{ |
254 |
5467 |
cmd.reset(new SetOptionCommand("incremental", "false")); |
255 |
5467 |
cmd->setMuted(true); |
256 |
5467 |
pExecutor->doCommand(cmd); |
257 |
|
} |
258 |
|
|
259 |
|
ParserBuilder parserBuilder(pExecutor->getSolver(), |
260 |
|
pExecutor->getSymbolManager(), |
261 |
12262 |
opts); |
262 |
12262 |
std::unique_ptr<Parser> parser(parserBuilder.build()); |
263 |
6131 |
if( inputFromStdin ) { |
264 |
|
parser->setInput(Input::newStreamInput( |
265 |
|
opts.base.inputLanguage, cin, filename)); |
266 |
|
} |
267 |
|
else |
268 |
|
{ |
269 |
12262 |
parser->setInput(Input::newFileInput(opts.base.inputLanguage, |
270 |
|
filename, |
271 |
6131 |
opts.parser.memoryMap)); |
272 |
|
} |
273 |
|
|
274 |
6131 |
bool interrupted = false; |
275 |
585903 |
while (status) |
276 |
|
{ |
277 |
295979 |
if (interrupted) { |
278 |
|
*opts.base.out << CommandInterrupted(); |
279 |
|
pExecutor->reset(); |
280 |
|
break; |
281 |
|
} |
282 |
|
try { |
283 |
295979 |
cmd.reset(parser->nextCommand()); |
284 |
295959 |
if (cmd == nullptr) break; |
285 |
|
} catch (UnsafeInterruptException& e) { |
286 |
|
interrupted = true; |
287 |
|
continue; |
288 |
|
} |
289 |
|
|
290 |
290620 |
status = pExecutor->doCommand(cmd); |
291 |
290620 |
if (cmd->interrupted() && status == 0) { |
292 |
|
interrupted = true; |
293 |
|
break; |
294 |
|
} |
295 |
|
|
296 |
290620 |
if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) { |
297 |
734 |
break; |
298 |
|
} |
299 |
|
} |
300 |
|
} |
301 |
|
|
302 |
12222 |
api::Result result; |
303 |
6111 |
if(status) { |
304 |
6073 |
result = pExecutor->getResult(); |
305 |
6073 |
returnValue = 0; |
306 |
|
} else { |
307 |
|
// there was some kind of error |
308 |
38 |
returnValue = 1; |
309 |
|
} |
310 |
|
|
311 |
|
#ifdef CVC5_COMPETITION_MODE |
312 |
|
if (opts.base.out != nullptr) |
313 |
|
{ |
314 |
|
*opts.base.out << std::flush; |
315 |
|
} |
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. |
319 |
|
_exit(returnValue); |
320 |
|
#endif /* CVC5_COMPETITION_MODE */ |
321 |
|
|
322 |
6111 |
totalTime.reset(); |
323 |
6111 |
pExecutor->flushOutputStreams(); |
324 |
|
|
325 |
|
#ifdef CVC5_DEBUG |
326 |
6111 |
if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) |
327 |
|
{ |
328 |
|
_exit(returnValue); |
329 |
|
} |
330 |
|
#else /* CVC5_DEBUG */ |
331 |
|
if (opts.driver.earlyExit) |
332 |
|
{ |
333 |
|
_exit(returnValue); |
334 |
|
} |
335 |
|
#endif /* CVC5_DEBUG */ |
336 |
|
} |
337 |
|
|
338 |
6111 |
pExecutor.reset(); |
339 |
|
|
340 |
6111 |
signal_handlers::cleanup(); |
341 |
|
|
342 |
12222 |
return returnValue; |
343 |
29319 |
} |