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/main_options.h" |
38 |
|
#include "options/option_exception.h" |
39 |
|
#include "options/options.h" |
40 |
|
#include "options/options_public.h" |
41 |
|
#include "options/parser_options.h" |
42 |
|
#include "options/set_language.h" |
43 |
|
#include "parser/parser.h" |
44 |
|
#include "parser/parser_builder.h" |
45 |
|
#include "smt/command.h" |
46 |
|
#include "smt/smt_engine.h" |
47 |
|
#include "util/result.h" |
48 |
|
|
49 |
|
using namespace std; |
50 |
|
using namespace cvc5; |
51 |
|
using namespace cvc5::parser; |
52 |
|
using namespace cvc5::main; |
53 |
|
|
54 |
|
namespace cvc5 { |
55 |
|
namespace main { |
56 |
|
|
57 |
|
/** Full argv[0] */ |
58 |
|
const char* progPath; |
59 |
|
|
60 |
|
/** Just the basename component of argv[0] */ |
61 |
9779 |
std::string progName; |
62 |
|
|
63 |
|
/** A pointer to the CommandExecutor (the signal handlers need it) */ |
64 |
9779 |
std::unique_ptr<cvc5::main::CommandExecutor> pExecutor; |
65 |
|
|
66 |
|
/** The time point the binary started, accessible to signal handlers */ |
67 |
9779 |
std::unique_ptr<TotalTimer> totalTime; |
68 |
|
|
69 |
17492 |
TotalTimer::~TotalTimer() |
70 |
|
{ |
71 |
8746 |
if (pExecutor != nullptr) |
72 |
|
{ |
73 |
6135 |
auto duration = std::chrono::steady_clock::now() - d_start; |
74 |
12270 |
pExecutor->getSmtEngine()->setTotalTimeStatistic( |
75 |
12270 |
std::chrono::duration<double>(duration).count()); |
76 |
|
} |
77 |
8746 |
} |
78 |
|
|
79 |
|
} // namespace main |
80 |
|
} // namespace cvc5 |
81 |
|
|
82 |
|
void printUsage(const Options& opts, bool full) { |
83 |
|
stringstream ss; |
84 |
|
ss << "usage: " << progName << " [options] [input-file]" |
85 |
|
<< endl |
86 |
|
<< endl |
87 |
|
<< "Without an input file, or with `-', cvc5 reads from standard input." |
88 |
|
<< endl |
89 |
|
<< endl |
90 |
|
<< "cvc5 options:" << endl; |
91 |
|
if(full) { |
92 |
|
options::printUsage(ss.str(), *opts.base.out); |
93 |
|
} else { |
94 |
|
options::printShortUsage(ss.str(), *opts.base.out); |
95 |
|
} |
96 |
|
} |
97 |
|
|
98 |
8746 |
int runCvc5(int argc, char* argv[], Options& opts) |
99 |
|
{ |
100 |
8746 |
main::totalTime = std::make_unique<TotalTimer>(); |
101 |
|
|
102 |
|
// Initialize the signal handlers |
103 |
8746 |
signal_handlers::install(); |
104 |
|
|
105 |
8746 |
progPath = argv[0]; |
106 |
|
|
107 |
|
// Parse the options |
108 |
14881 |
std::vector<string> filenames = options::parse(opts, argc, argv, progName); |
109 |
|
|
110 |
12270 |
auto limit = install_time_limit(opts); |
111 |
|
|
112 |
6135 |
if (opts.driver.help) |
113 |
|
{ |
114 |
|
printUsage(opts, true); |
115 |
|
exit(1); |
116 |
|
} |
117 |
6135 |
else if (opts.base.languageHelp) |
118 |
|
{ |
119 |
|
options::printLanguageHelp(*opts.base.out); |
120 |
|
exit(1); |
121 |
|
} |
122 |
6135 |
else if (opts.driver.version) |
123 |
|
{ |
124 |
|
*opts.base.out << Configuration::about().c_str() << flush; |
125 |
|
exit(0); |
126 |
|
} |
127 |
|
|
128 |
6135 |
segvSpin = opts.driver.segvSpin; |
129 |
|
|
130 |
|
// If in competition mode, set output stream option to flush immediately |
131 |
|
#ifdef CVC5_COMPETITION_MODE |
132 |
|
*opts.base.out << unitbuf; |
133 |
|
#endif /* CVC5_COMPETITION_MODE */ |
134 |
|
|
135 |
|
// We only accept one input file |
136 |
6135 |
if(filenames.size() > 1) { |
137 |
|
throw Exception("Too many input files specified."); |
138 |
|
} |
139 |
|
|
140 |
|
// If no file supplied we will read from standard input |
141 |
6135 |
const bool inputFromStdin = filenames.empty() || filenames[0] == "-"; |
142 |
|
|
143 |
|
// if we're reading from stdin on a TTY, default to interactive mode |
144 |
6135 |
if (!opts.driver.interactiveWasSetByUser) |
145 |
|
{ |
146 |
6135 |
opts.driver.interactive = inputFromStdin && isatty(fileno(stdin)); |
147 |
|
} |
148 |
|
|
149 |
|
// Auto-detect input language by filename extension |
150 |
12270 |
std::string filenameStr("<stdin>"); |
151 |
6135 |
if (!inputFromStdin) { |
152 |
6135 |
filenameStr = std::move(filenames[0]); |
153 |
|
} |
154 |
6135 |
const char* filename = filenameStr.c_str(); |
155 |
|
|
156 |
6135 |
if (opts.base.inputLanguage == language::input::LANG_AUTO) |
157 |
|
{ |
158 |
5908 |
if( inputFromStdin ) { |
159 |
|
// We can't do any fancy detection on stdin |
160 |
|
opts.base.inputLanguage = language::input::LANG_CVC; |
161 |
|
} else { |
162 |
5908 |
size_t len = filenameStr.size(); |
163 |
5908 |
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { |
164 |
5053 |
opts.base.inputLanguage = language::input::LANG_SMTLIB_V2_6; |
165 |
855 |
} else if((len >= 2 && !strcmp(".p", filename + len - 2)) |
166 |
814 |
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) { |
167 |
41 |
opts.base.inputLanguage = language::input::LANG_TPTP; |
168 |
814 |
} else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) |
169 |
12 |
|| ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { |
170 |
802 |
opts.base.inputLanguage = language::input::LANG_CVC; |
171 |
12 |
} else if((len >= 3 && !strcmp(".sy", filename + len - 3)) |
172 |
|
|| (len >= 3 && !strcmp(".sl", filename + len - 3))) { |
173 |
|
// version 2 sygus is the default |
174 |
12 |
opts.base.inputLanguage = language::input::LANG_SYGUS_V2; |
175 |
|
} |
176 |
|
} |
177 |
|
} |
178 |
|
|
179 |
6135 |
if (opts.base.outputLanguage == language::output::LANG_AUTO) |
180 |
|
{ |
181 |
6135 |
opts.base.outputLanguage = language::toOutputLanguage(opts.base.inputLanguage); |
182 |
|
} |
183 |
|
|
184 |
|
// Determine which messages to show based on smtcomp_mode and verbosity |
185 |
6135 |
if(Configuration::isMuzzledBuild()) { |
186 |
|
DebugChannel.setStream(&cvc5::null_os); |
187 |
|
TraceChannel.setStream(&cvc5::null_os); |
188 |
|
NoticeChannel.setStream(&cvc5::null_os); |
189 |
|
ChatChannel.setStream(&cvc5::null_os); |
190 |
|
MessageChannel.setStream(&cvc5::null_os); |
191 |
|
WarningChannel.setStream(&cvc5::null_os); |
192 |
|
} |
193 |
|
|
194 |
|
// important even for muzzled builds (to get result output right) |
195 |
6135 |
(*opts.base.out) |
196 |
6135 |
<< language::SetLanguage(opts.base.outputLanguage); |
197 |
|
|
198 |
|
// Create the command executor to execute the parsed commands |
199 |
6135 |
pExecutor = std::make_unique<CommandExecutor>(opts); |
200 |
|
|
201 |
6135 |
int returnValue = 0; |
202 |
|
{ |
203 |
|
// notify SmtEngine that we are starting to parse |
204 |
6135 |
pExecutor->getSmtEngine()->notifyStartParsing(filenameStr); |
205 |
|
|
206 |
|
// Parse and execute commands until we are done |
207 |
12270 |
std::unique_ptr<Command> cmd; |
208 |
6135 |
bool status = true; |
209 |
6135 |
if (opts.driver.interactive && inputFromStdin) |
210 |
|
{ |
211 |
|
if (!opts.base.incrementalSolvingWasSetByUser) |
212 |
|
{ |
213 |
|
cmd.reset(new SetOptionCommand("incremental", "true")); |
214 |
|
cmd->setMuted(true); |
215 |
|
pExecutor->doCommand(cmd); |
216 |
|
} |
217 |
|
InteractiveShell shell(pExecutor->getSolver(), |
218 |
|
pExecutor->getSymbolManager()); |
219 |
|
|
220 |
|
CVC5Message() << Configuration::getPackageName() << " " |
221 |
|
<< Configuration::getVersionString(); |
222 |
|
if (Configuration::isGitBuild()) |
223 |
|
{ |
224 |
|
CVC5Message() << " [" << Configuration::getGitId() << "]"; |
225 |
|
} |
226 |
|
CVC5Message() << (Configuration::isDebugBuild() ? " DEBUG" : "") |
227 |
|
<< " assertions:" |
228 |
|
<< (Configuration::isAssertionBuild() ? "on" : "off") |
229 |
|
<< endl |
230 |
|
<< endl; |
231 |
|
CVC5Message() << Configuration::copyright() << endl; |
232 |
|
|
233 |
|
while(true) { |
234 |
|
try { |
235 |
|
cmd.reset(shell.readCommand()); |
236 |
|
} catch(UnsafeInterruptException& e) { |
237 |
|
*opts.base.out << CommandInterrupted(); |
238 |
|
break; |
239 |
|
} |
240 |
|
if (cmd == nullptr) |
241 |
|
break; |
242 |
|
status = pExecutor->doCommand(cmd) && status; |
243 |
|
if (cmd->interrupted()) { |
244 |
|
break; |
245 |
|
} |
246 |
|
} |
247 |
|
} |
248 |
|
else |
249 |
|
{ |
250 |
6135 |
if (!opts.base.incrementalSolvingWasSetByUser) |
251 |
|
{ |
252 |
5471 |
cmd.reset(new SetOptionCommand("incremental", "false")); |
253 |
5471 |
cmd->setMuted(true); |
254 |
5471 |
pExecutor->doCommand(cmd); |
255 |
|
} |
256 |
|
|
257 |
|
ParserBuilder parserBuilder(pExecutor->getSolver(), |
258 |
|
pExecutor->getSymbolManager(), |
259 |
12270 |
opts); |
260 |
12270 |
std::unique_ptr<Parser> parser(parserBuilder.build()); |
261 |
6135 |
if( inputFromStdin ) { |
262 |
|
parser->setInput(Input::newStreamInput( |
263 |
|
opts.base.inputLanguage, cin, filename)); |
264 |
|
} |
265 |
|
else |
266 |
|
{ |
267 |
12270 |
parser->setInput(Input::newFileInput(opts.base.inputLanguage, |
268 |
|
filename, |
269 |
6135 |
opts.parser.memoryMap)); |
270 |
|
} |
271 |
|
|
272 |
6135 |
bool interrupted = false; |
273 |
585955 |
while (status) |
274 |
|
{ |
275 |
296007 |
if (interrupted) { |
276 |
|
*opts.base.out << CommandInterrupted(); |
277 |
|
pExecutor->reset(); |
278 |
|
break; |
279 |
|
} |
280 |
|
try { |
281 |
296007 |
cmd.reset(parser->nextCommand()); |
282 |
295987 |
if (cmd == nullptr) break; |
283 |
|
} catch (UnsafeInterruptException& e) { |
284 |
|
interrupted = true; |
285 |
|
continue; |
286 |
|
} |
287 |
|
|
288 |
290644 |
status = pExecutor->doCommand(cmd); |
289 |
290644 |
if (cmd->interrupted() && status == 0) { |
290 |
|
interrupted = true; |
291 |
|
break; |
292 |
|
} |
293 |
|
|
294 |
290644 |
if(dynamic_cast<QuitCommand*>(cmd.get()) != nullptr) { |
295 |
734 |
break; |
296 |
|
} |
297 |
|
} |
298 |
|
} |
299 |
|
|
300 |
12230 |
api::Result result; |
301 |
6115 |
if(status) { |
302 |
6077 |
result = pExecutor->getResult(); |
303 |
6077 |
returnValue = 0; |
304 |
|
} else { |
305 |
|
// there was some kind of error |
306 |
38 |
returnValue = 1; |
307 |
|
} |
308 |
|
|
309 |
|
#ifdef CVC5_COMPETITION_MODE |
310 |
|
if (opts.base.out != nullptr) |
311 |
|
{ |
312 |
|
*opts.base.out << std::flush; |
313 |
|
} |
314 |
|
// exit, don't return (don't want destructors to run) |
315 |
|
// _exit() from unistd.h doesn't run global destructors |
316 |
|
// or other on_exit/atexit stuff. |
317 |
|
_exit(returnValue); |
318 |
|
#endif /* CVC5_COMPETITION_MODE */ |
319 |
|
|
320 |
6115 |
totalTime.reset(); |
321 |
6115 |
pExecutor->flushOutputStreams(); |
322 |
|
|
323 |
|
#ifdef CVC5_DEBUG |
324 |
6115 |
if (opts.driver.earlyExit && opts.driver.earlyExitWasSetByUser) |
325 |
|
{ |
326 |
|
_exit(returnValue); |
327 |
|
} |
328 |
|
#else /* CVC5_DEBUG */ |
329 |
|
if (opts.driver.earlyExit) |
330 |
|
{ |
331 |
|
_exit(returnValue); |
332 |
|
} |
333 |
|
#endif /* CVC5_DEBUG */ |
334 |
|
} |
335 |
|
|
336 |
6115 |
pExecutor.reset(); |
337 |
|
|
338 |
6115 |
signal_handlers::cleanup(); |
339 |
|
|
340 |
12230 |
return returnValue; |
341 |
29337 |
} |