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/options.h" |
37 |
|
#include "options/set_language.h" |
38 |
|
#include "parser/parser.h" |
39 |
|
#include "parser/parser_builder.h" |
40 |
|
#include "smt/command.h" |
41 |
|
#include "smt/smt_engine.h" |
42 |
|
#include "util/result.h" |
43 |
|
|
44 |
|
using namespace std; |
45 |
|
using namespace cvc5; |
46 |
|
using namespace cvc5::parser; |
47 |
|
using namespace cvc5::main; |
48 |
|
|
49 |
|
namespace cvc5 { |
50 |
|
namespace main { |
51 |
|
/** Global options variable */ |
52 |
|
thread_local Options* pOptions; |
53 |
|
|
54 |
|
/** Full argv[0] */ |
55 |
|
const char* progPath; |
56 |
|
|
57 |
|
/** Just the basename component of argv[0] */ |
58 |
|
const std::string* progName; |
59 |
|
|
60 |
|
/** A pointer to the CommandExecutor (the signal handlers need it) */ |
61 |
9392 |
std::unique_ptr<cvc5::main::CommandExecutor> pExecutor; |
62 |
|
|
63 |
|
/** The time point the binary started, accessible to signal handlers */ |
64 |
9392 |
std::unique_ptr<TotalTimer> totalTime; |
65 |
|
|
66 |
16770 |
TotalTimer::~TotalTimer() |
67 |
|
{ |
68 |
8385 |
if (pExecutor != nullptr) |
69 |
|
{ |
70 |
5880 |
auto duration = std::chrono::steady_clock::now() - d_start; |
71 |
11760 |
pExecutor->getSmtEngine()->setTotalTimeStatistic( |
72 |
11760 |
std::chrono::duration<double>(duration).count()); |
73 |
|
} |
74 |
8385 |
} |
75 |
|
|
76 |
|
} // namespace main |
77 |
|
} // namespace cvc5 |
78 |
|
|
79 |
|
void printUsage(Options& opts, bool full) { |
80 |
|
stringstream ss; |
81 |
|
ss << "usage: " << opts.getBinaryName() << " [options] [input-file]" << endl |
82 |
|
<< endl |
83 |
|
<< "Without an input file, or with `-', cvc5 reads from standard input." |
84 |
|
<< endl |
85 |
|
<< endl |
86 |
|
<< "cvc5 options:" << endl; |
87 |
|
if(full) { |
88 |
|
Options::printUsage( ss.str(), *(opts.getOut()) ); |
89 |
|
} else { |
90 |
|
Options::printShortUsage( ss.str(), *(opts.getOut()) ); |
91 |
|
} |
92 |
|
} |
93 |
|
|
94 |
8385 |
int runCvc5(int argc, char* argv[], Options& opts) |
95 |
|
{ |
96 |
8385 |
main::totalTime = std::make_unique<TotalTimer>(); |
97 |
|
// For the signal handlers' benefit |
98 |
8385 |
pOptions = &opts; |
99 |
|
|
100 |
|
// Initialize the signal handlers |
101 |
8385 |
signal_handlers::install(); |
102 |
|
|
103 |
8385 |
progPath = argv[0]; |
104 |
|
|
105 |
|
// Parse the options |
106 |
14266 |
vector<string> filenames = Options::parseOptions(&opts, argc, argv); |
107 |
|
|
108 |
11762 |
auto limit = install_time_limit(opts); |
109 |
|
|
110 |
11762 |
string progNameStr = opts.getBinaryName(); |
111 |
5881 |
progName = &progNameStr; |
112 |
|
|
113 |
5881 |
if( opts.getHelp() ) { |
114 |
|
printUsage(opts, true); |
115 |
|
exit(1); |
116 |
5881 |
} else if( opts.getLanguageHelp() ) { |
117 |
|
Options::printLanguageHelp(*(opts.getOut())); |
118 |
|
exit(1); |
119 |
5881 |
} else if( opts.getVersion() ) { |
120 |
|
*(opts.getOut()) << Configuration::about().c_str() << flush; |
121 |
|
exit(0); |
122 |
|
} |
123 |
|
|
124 |
5881 |
segvSpin = opts.getSegvSpin(); |
125 |
|
|
126 |
|
// If in competition mode, set output stream option to flush immediately |
127 |
|
#ifdef CVC5_COMPETITION_MODE |
128 |
|
*(opts.getOut()) << unitbuf; |
129 |
|
#endif /* CVC5_COMPETITION_MODE */ |
130 |
|
|
131 |
|
// We only accept one input file |
132 |
5881 |
if(filenames.size() > 1) { |
133 |
|
throw Exception("Too many input files specified."); |
134 |
|
} |
135 |
|
|
136 |
|
// If no file supplied we will read from standard input |
137 |
5881 |
const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; |
138 |
|
|
139 |
|
// if we're reading from stdin on a TTY, default to interactive mode |
140 |
5881 |
if(!opts.wasSetByUserInteractive()) { |
141 |
5881 |
opts.setInteractive(inputFromStdin && isatty(fileno(stdin))); |
142 |
|
} |
143 |
|
|
144 |
|
// Auto-detect input language by filename extension |
145 |
11762 |
std::string filenameStr("<stdin>"); |
146 |
5881 |
if (!inputFromStdin) { |
147 |
|
// Use swap to avoid copying the string |
148 |
|
// TODO: use std::move() when switching to c++11 |
149 |
5881 |
filenameStr.swap(filenames[0]); |
150 |
|
} |
151 |
5881 |
const char* filename = filenameStr.c_str(); |
152 |
|
|
153 |
5881 |
if(opts.getInputLanguage() == language::input::LANG_AUTO) { |
154 |
5657 |
if( inputFromStdin ) { |
155 |
|
// We can't do any fancy detection on stdin |
156 |
|
opts.setInputLanguage(language::input::LANG_CVC); |
157 |
|
} else { |
158 |
5657 |
unsigned len = filenameStr.size(); |
159 |
5657 |
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { |
160 |
4799 |
opts.setInputLanguage(language::input::LANG_SMTLIB_V2_6); |
161 |
858 |
} else if((len >= 2 && !strcmp(".p", filename + len - 2)) |
162 |
815 |
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) { |
163 |
43 |
opts.setInputLanguage(language::input::LANG_TPTP); |
164 |
815 |
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) |
165 |
11 |
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { |
166 |
804 |
opts.setInputLanguage(language::input::LANG_CVC); |
167 |
11 |
} else if((len >= 3 && !strcmp(".sy", filename + len - 3)) |
168 |
|
|| (len >= 3 && !strcmp(".sl", filename + len - 3))) { |
169 |
|
// version 2 sygus is the default |
170 |
11 |
opts.setInputLanguage(language::input::LANG_SYGUS_V2); |
171 |
|
} |
172 |
|
} |
173 |
|
} |
174 |
|
|
175 |
5881 |
if(opts.getOutputLanguage() == language::output::LANG_AUTO) { |
176 |
5881 |
opts.setOutputLanguage(language::toOutputLanguage(opts.getInputLanguage())); |
177 |
|
} |
178 |
|
|
179 |
|
// Determine which messages to show based on smtcomp_mode and verbosity |
180 |
5881 |
if(Configuration::isMuzzledBuild()) { |
181 |
|
DebugChannel.setStream(&cvc5::null_os); |
182 |
|
TraceChannel.setStream(&cvc5::null_os); |
183 |
|
NoticeChannel.setStream(&cvc5::null_os); |
184 |
|
ChatChannel.setStream(&cvc5::null_os); |
185 |
|
MessageChannel.setStream(&cvc5::null_os); |
186 |
|
WarningChannel.setStream(&cvc5::null_os); |
187 |
|
} |
188 |
|
|
189 |
|
// important even for muzzled builds (to get result output right) |
190 |
5881 |
(*(opts.getOut())) << language::SetLanguage(opts.getOutputLanguage()); |
191 |
|
|
192 |
|
// Create the command executor to execute the parsed commands |
193 |
5881 |
pExecutor = std::make_unique<CommandExecutor>(opts); |
194 |
|
|
195 |
5880 |
int returnValue = 0; |
196 |
|
{ |
197 |
|
// notify SmtEngine that we are starting to parse |
198 |
5880 |
pExecutor->getSmtEngine()->notifyStartParsing(filenameStr); |
199 |
|
|
200 |
|
// Parse and execute commands until we are done |
201 |
11760 |
std::unique_ptr<Command> cmd; |
202 |
5880 |
bool status = true; |
203 |
5880 |
if(opts.getInteractive() && inputFromStdin) { |
204 |
|
if(opts.getTearDownIncremental() > 0) { |
205 |
|
throw Exception( |
206 |
|
"--tear-down-incremental doesn't work in interactive mode"); |
207 |
|
} |
208 |
|
if(!opts.wasSetByUserIncrementalSolving()) { |
209 |
|
cmd.reset(new SetOptionCommand("incremental", "true")); |
210 |
|
cmd->setMuted(true); |
211 |
|
pExecutor->doCommand(cmd); |
212 |
|
} |
213 |
|
InteractiveShell shell(pExecutor->getSolver(), |
214 |
|
pExecutor->getSymbolManager()); |
215 |
|
if(opts.getInteractivePrompt()) { |
216 |
|
CVC5Message() << Configuration::getPackageName() << " " |
217 |
|
<< Configuration::getVersionString(); |
218 |
|
if(Configuration::isGitBuild()) { |
219 |
|
CVC5Message() << " [" << Configuration::getGitId() << "]"; |
220 |
|
} |
221 |
|
CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") |
222 |
|
<< " assertions:" |
223 |
|
<< (Configuration::isAssertionBuild() ? "on" : "off") |
224 |
|
<< endl |
225 |
|
<< endl; |
226 |
|
CVC5Message() << Configuration::copyright() << endl; |
227 |
|
} |
228 |
|
|
229 |
|
while(true) { |
230 |
|
try { |
231 |
|
cmd.reset(shell.readCommand()); |
232 |
|
} catch(UnsafeInterruptException& e) { |
233 |
|
(*opts.getOut()) << CommandInterrupted(); |
234 |
|
break; |
235 |
|
} |
236 |
|
if (cmd == nullptr) |
237 |
|
break; |
238 |
|
status = pExecutor->doCommand(cmd) && status; |
239 |
|
if (cmd->interrupted()) { |
240 |
|
break; |
241 |
|
} |
242 |
|
} |
243 |
5880 |
} else if( opts.getTearDownIncremental() > 0) { |
244 |
|
if(!opts.getIncrementalSolving() && opts.getTearDownIncremental() > 1) { |
245 |
|
// For tear-down-incremental values greater than 1, need incremental |
246 |
|
// on too. |
247 |
|
cmd.reset(new SetOptionCommand("incremental", "true")); |
248 |
|
cmd->setMuted(true); |
249 |
|
pExecutor->doCommand(cmd); |
250 |
|
// if(opts.wasSetByUserIncrementalSolving()) { |
251 |
|
// throw OptionException( |
252 |
|
// "--tear-down-incremental incompatible with --incremental"); |
253 |
|
// } |
254 |
|
|
255 |
|
// cmd.reset(new SetOptionCommand("incremental", "false")); |
256 |
|
// cmd->setMuted(true); |
257 |
|
// pExecutor->doCommand(cmd); |
258 |
|
} |
259 |
|
|
260 |
|
ParserBuilder parserBuilder(pExecutor->getSolver(), |
261 |
|
pExecutor->getSymbolManager(), |
262 |
|
opts); |
263 |
|
std::unique_ptr<Parser> parser(parserBuilder.build()); |
264 |
|
if( inputFromStdin ) { |
265 |
|
parser->setInput( |
266 |
|
Input::newStreamInput(opts.getInputLanguage(), cin, filename)); |
267 |
|
} |
268 |
|
else |
269 |
|
{ |
270 |
|
parser->setInput(Input::newFileInput( |
271 |
|
opts.getInputLanguage(), filename, opts.getMemoryMap())); |
272 |
|
} |
273 |
|
|
274 |
|
vector< vector<Command*> > allCommands; |
275 |
|
allCommands.push_back(vector<Command*>()); |
276 |
|
int needReset = 0; |
277 |
|
// true if one of the commands was interrupted |
278 |
|
bool interrupted = false; |
279 |
|
while (status) |
280 |
|
{ |
281 |
|
if (interrupted) { |
282 |
|
(*opts.getOut()) << CommandInterrupted(); |
283 |
|
break; |
284 |
|
} |
285 |
|
|
286 |
|
try { |
287 |
|
cmd.reset(parser->nextCommand()); |
288 |
|
if (cmd == nullptr) break; |
289 |
|
} catch (UnsafeInterruptException& e) { |
290 |
|
interrupted = true; |
291 |
|
continue; |
292 |
|
} |
293 |
|
|
294 |
|
if(dynamic_cast<PushCommand*>(cmd.get()) != nullptr) { |
295 |
|
if(needReset >= opts.getTearDownIncremental()) { |
296 |
|
pExecutor->reset(); |
297 |
|
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { |
298 |
|
if (interrupted) break; |
299 |
|
for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) |
300 |
|
{ |
301 |
|
Command* ccmd = allCommands[i][j]->clone(); |
302 |
|
ccmd->setMuted(true); |
303 |
|
pExecutor->doCommand(ccmd); |
304 |
|
if (ccmd->interrupted()) |
305 |
|
{ |
306 |
|
interrupted = true; |
307 |
|
} |
308 |
|
delete ccmd; |
309 |
|
} |
310 |
|
} |
311 |
|
needReset = 0; |
312 |
|
} |
313 |
|
allCommands.push_back(vector<Command*>()); |
314 |
|
Command* copy = cmd->clone(); |
315 |
|
allCommands.back().push_back(copy); |
316 |
|
status = pExecutor->doCommand(cmd); |
317 |
|
if(cmd->interrupted()) { |
318 |
|
interrupted = true; |
319 |
|
continue; |
320 |
|
} |
321 |
|
} else if(dynamic_cast<PopCommand*>(cmd.get()) != nullptr) { |
322 |
|
allCommands.pop_back(); // fixme leaks cmds here |
323 |
|
if (needReset >= opts.getTearDownIncremental()) { |
324 |
|
pExecutor->reset(); |
325 |
|
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { |
326 |
|
for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) |
327 |
|
{ |
328 |
|
std::unique_ptr<Command> ccmd(allCommands[i][j]->clone()); |
329 |
|
ccmd->setMuted(true); |
330 |
|
pExecutor->doCommand(ccmd); |
331 |
|
if (ccmd->interrupted()) |
332 |
|
{ |
333 |
|
interrupted = true; |
334 |
|
} |
335 |
|
} |
336 |
|
} |
337 |
|
if (interrupted) continue; |
338 |
|
(*opts.getOut()) << CommandSuccess(); |
339 |
|
needReset = 0; |
340 |
|
} else { |
341 |
|
status = pExecutor->doCommand(cmd); |
342 |
|
if(cmd->interrupted()) { |
343 |
|
interrupted = true; |
344 |
|
continue; |
345 |
|
} |
346 |
|
} |
347 |
|
} else if(dynamic_cast<CheckSatCommand*>(cmd.get()) != nullptr || |
348 |
|
dynamic_cast<QueryCommand*>(cmd.get()) != nullptr) { |
349 |
|
if(needReset >= opts.getTearDownIncremental()) { |
350 |
|
pExecutor->reset(); |
351 |
|
for(size_t i = 0; i < allCommands.size() && !interrupted; ++i) { |
352 |
|
for(size_t j = 0; j < allCommands[i].size() && !interrupted; ++j) |
353 |
|
{ |
354 |
|
Command* ccmd = allCommands[i][j]->clone(); |
355 |
|
ccmd->setMuted(true); |
356 |
|
pExecutor->doCommand(ccmd); |
357 |
|
if (ccmd->interrupted()) |
358 |
|
{ |
359 |
|
interrupted = true; |
360 |
|
} |
361 |
|
delete ccmd; |
362 |
|
} |
363 |
|
} |
364 |
|
needReset = 0; |
365 |
|
} else { |
366 |
|
++needReset; |
367 |
|
} |
368 |
|
if (interrupted) { |
369 |
|
continue; |
370 |
|
} |
371 |
|
|
372 |
|
status = pExecutor->doCommand(cmd); |
373 |
|
if(cmd->interrupted()) { |
374 |
|
interrupted = true; |
375 |
|
continue; |
376 |
|
} |
377 |
|
} else if(dynamic_cast<ResetCommand*>(cmd.get()) != nullptr) { |
378 |
|
pExecutor->doCommand(cmd); |
379 |
|
allCommands.clear(); |
380 |
|
allCommands.push_back(vector<Command*>()); |
381 |
|
} else { |
382 |
|
// We shouldn't copy certain commands, because they can cause |
383 |
|
// an error on replay since there's no associated sat/unsat check |
384 |
|
// preceding them. |
385 |
|
if(dynamic_cast<GetUnsatCoreCommand*>(cmd.get()) == nullptr && |
386 |
|
dynamic_cast<GetProofCommand*>(cmd.get()) == nullptr && |
387 |
|
dynamic_cast<GetValueCommand*>(cmd.get()) == nullptr && |
388 |
|
dynamic_cast<GetModelCommand*>(cmd.get()) == nullptr && |
389 |
|
dynamic_cast<GetAssignmentCommand*>(cmd.get()) == nullptr && |
390 |
|
dynamic_cast<GetInstantiationsCommand*>(cmd.get()) == nullptr && |
391 |
|
dynamic_cast<GetAssertionsCommand*>(cmd.get()) == nullptr && |
392 |
|
dynamic_cast<GetInfoCommand*>(cmd.get()) == nullptr && |
393 |
|
dynamic_cast<GetOptionCommand*>(cmd.get()) == nullptr && |
394 |
|
dynamic_cast<EchoCommand*>(cmd.get()) == nullptr) { |
395 |
|
Command* copy = cmd->clone(); |
396 |
|
allCommands.back().push_back(copy); |
397 |
|
} |
398 |
|
status = pExecutor->doCommand(cmd); |
399 |
|
if(cmd->interrupted()) { |
400 |
|
interrupted = true; |
401 |
|
continue; |
402 |
|
} |
403 |
|
|
404 |
|
if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) { |
405 |
|
break; |
406 |
|
} |
407 |
|
} |
408 |
|
} |
409 |
|
} else { |
410 |
5880 |
if(!opts.wasSetByUserIncrementalSolving()) { |
411 |
5258 |
cmd.reset(new SetOptionCommand("incremental", "false")); |
412 |
5258 |
cmd->setMuted(true); |
413 |
5258 |
pExecutor->doCommand(cmd); |
414 |
|
} |
415 |
|
|
416 |
|
ParserBuilder parserBuilder(pExecutor->getSolver(), |
417 |
|
pExecutor->getSymbolManager(), |
418 |
11760 |
opts); |
419 |
11760 |
std::unique_ptr<Parser> parser(parserBuilder.build()); |
420 |
5880 |
if( inputFromStdin ) { |
421 |
|
parser->setInput( |
422 |
|
Input::newStreamInput(opts.getInputLanguage(), cin, filename)); |
423 |
|
} |
424 |
|
else |
425 |
|
{ |
426 |
11760 |
parser->setInput(Input::newFileInput( |
427 |
5880 |
opts.getInputLanguage(), filename, opts.getMemoryMap())); |
428 |
|
} |
429 |
|
|
430 |
5880 |
bool interrupted = false; |
431 |
590714 |
while (status) |
432 |
|
{ |
433 |
298262 |
if (interrupted) { |
434 |
|
(*opts.getOut()) << CommandInterrupted(); |
435 |
|
pExecutor->reset(); |
436 |
|
break; |
437 |
|
} |
438 |
|
try { |
439 |
298262 |
cmd.reset(parser->nextCommand()); |
440 |
298242 |
if (cmd == nullptr) break; |
441 |
|
} catch (UnsafeInterruptException& e) { |
442 |
|
interrupted = true; |
443 |
|
continue; |
444 |
|
} |
445 |
|
|
446 |
293154 |
status = pExecutor->doCommand(cmd); |
447 |
293154 |
if (cmd->interrupted() && status == 0) { |
448 |
|
interrupted = true; |
449 |
|
break; |
450 |
|
} |
451 |
|
|
452 |
293154 |
if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) { |
453 |
737 |
break; |
454 |
|
} |
455 |
|
} |
456 |
|
} |
457 |
|
|
458 |
11720 |
api::Result result; |
459 |
5860 |
if(status) { |
460 |
5825 |
result = pExecutor->getResult(); |
461 |
5825 |
returnValue = 0; |
462 |
|
} else { |
463 |
|
// there was some kind of error |
464 |
35 |
returnValue = 1; |
465 |
|
} |
466 |
|
|
467 |
|
#ifdef CVC5_COMPETITION_MODE |
468 |
|
opts.flushOut(); |
469 |
|
// exit, don't return (don't want destructors to run) |
470 |
|
// _exit() from unistd.h doesn't run global destructors |
471 |
|
// or other on_exit/atexit stuff. |
472 |
|
_exit(returnValue); |
473 |
|
#endif /* CVC5_COMPETITION_MODE */ |
474 |
|
|
475 |
5860 |
totalTime.reset(); |
476 |
5860 |
pExecutor->flushOutputStreams(); |
477 |
|
|
478 |
|
#ifdef CVC5_DEBUG |
479 |
5860 |
if(opts.getEarlyExit() && opts.wasSetByUserEarlyExit()) { |
480 |
|
_exit(returnValue); |
481 |
|
} |
482 |
|
#else /* CVC5_DEBUG */ |
483 |
|
if(opts.getEarlyExit()) { |
484 |
|
_exit(returnValue); |
485 |
|
} |
486 |
|
#endif /* CVC5_DEBUG */ |
487 |
|
} |
488 |
|
|
489 |
5860 |
pExecutor.reset(); |
490 |
|
|
491 |
5860 |
signal_handlers::cleanup(); |
492 |
|
|
493 |
11720 |
return returnValue; |
494 |
28176 |
} |