Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Morgan Deters, Andrew Reynolds, Christopher L. Conway
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Interactive shell for cvc5.
14 : : *
15 : : * This file is the implementation for the cvc5 interactive shell.
16 : : * The shell supports the editline library.
17 : : */
18 : : #include "main/interactive_shell.h"
19 : :
20 : : #include <unistd.h>
21 : :
22 : : #include <algorithm>
23 : : #include <cstdlib>
24 : : #include <cstring>
25 : : #include <iostream>
26 : : #include <optional>
27 : : #include <set>
28 : : #include <string>
29 : : #include <utility>
30 : : #include <vector>
31 : :
32 : : // This must go before HAVE_LIBEDITLINE.
33 : : #include "base/cvc5config.h"
34 : :
35 : : #if HAVE_LIBEDITLINE
36 : : #include <editline/readline.h>
37 : : # if HAVE_EXT_STDIO_FILEBUF_H
38 : : # include <ext/stdio_filebuf.h>
39 : : # endif /* HAVE_EXT_STDIO_FILEBUF_H */
40 : : #endif /* HAVE_LIBEDITLINE */
41 : :
42 : : #include <cvc5/cvc5.h>
43 : : #include <cvc5/cvc5_parser.h>
44 : :
45 : : #include "base/check.h"
46 : : #include "base/output.h"
47 : : #include "main/command_executor.h"
48 : : #include "parser/commands.h"
49 : : #include "parser/sym_manager.h"
50 : : #include "theory/logic_info.h"
51 : :
52 : : using namespace std;
53 : : using namespace cvc5::parser;
54 : :
55 : : namespace cvc5::internal {
56 : :
57 : : using namespace language;
58 : :
59 : : const string InteractiveShell::INPUT_FILENAME = "<shell>";
60 : :
61 : : #if HAVE_LIBEDITLINE
62 : :
63 : : #if HAVE_EXT_STDIO_FILEBUF_H
64 : : using __gnu_cxx::stdio_filebuf;
65 : : #endif /* HAVE_EXT_STDIO_FILEBUF_H */
66 : :
67 : : char** commandCompletion(const char* text, int start, int end);
68 : : char* commandGenerator(const char* text, int state);
69 : :
70 : : static const std::string smt2_commands[] = {
71 : : #include "main/smt2_tokens.h"
72 : : };/* smt2_commands */
73 : :
74 : : static const std::string* commandsBegin;
75 : : static const std::string* commandsEnd;
76 : :
77 : : static set<string> s_declarations;
78 : :
79 : : #endif /* HAVE_LIBEDITLINE */
80 : :
81 : 7 : InteractiveShell::InteractiveShell(main::CommandExecutor* cexec,
82 : : std::istream& in,
83 : : std::ostream& out,
84 : 7 : bool isInteractive)
85 : : : d_cexec(cexec),
86 : 7 : d_solver(cexec->getSolver()),
87 : 7 : d_symman(cexec->getSymbolManager()->toSymManager()),
88 : : d_in(in),
89 : : d_out(out),
90 : : d_isInteractive(isInteractive),
91 : 14 : d_quit(false)
92 : : {
93 : : /* Create parser with bogus input. */
94 : 7 : d_parser.reset(
95 : 7 : new cvc5::parser::InputParser(d_solver, cexec->getSymbolManager()));
96 : 14 : std::string langs = d_solver->getOption("input-language");
97 [ + + ]: 7 : if (langs == "LANG_SMTLIB_V2_6")
98 : : {
99 : 6 : d_lang = modes::InputLanguage::SMT_LIB_2_6;
100 : : }
101 [ + - ]: 1 : else if (langs == "LANG_SYGUS_V2")
102 : : {
103 : 1 : d_lang = modes::InputLanguage::SYGUS_2_1;
104 : : }
105 : : else
106 : : {
107 : 0 : throw Exception("internal error: unhandled language " + langs);
108 : : }
109 : :
110 : : // initialize for incremental string input
111 : 7 : d_parser->setStringInput(d_lang, "", INPUT_FILENAME);
112 : 7 : d_usingEditline = false;
113 : : #if HAVE_LIBEDITLINE
114 : : if (&d_in == &std::cin && isatty(fileno(stdin)))
115 : : {
116 : : ::rl_readline_name = const_cast<char*>("cvc5");
117 : : #if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP
118 : : ::rl_completion_entry_function = commandGenerator;
119 : : #else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
120 : : ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator;
121 : : #endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
122 : : ::using_history();
123 : :
124 : : if (d_lang == modes::InputLanguage::SMT_LIB_2_6)
125 : : {
126 : : d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
127 : : commandsBegin = smt2_commands;
128 : : commandsEnd =
129 : : smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
130 : : d_usingEditline = true;
131 : : int err = ::read_history(d_historyFilename.c_str());
132 : : ::stifle_history(s_historyLimit);
133 : : if (d_solver->getOptionInfo("verbosity").intValue() >= 1)
134 : : {
135 : : if(err == 0) {
136 : : d_solver->getDriverOptions().err()
137 : : << "Read " << ::history_length << " lines of history from "
138 : : << d_historyFilename << std::endl;
139 : : } else {
140 : : d_solver->getDriverOptions().err()
141 : : << "Could not read history from " << d_historyFilename << ": "
142 : : << strerror(err) << std::endl;
143 : : }
144 : : }
145 : : }
146 : : }
147 : : #endif /* HAVE_LIBEDITLINE */
148 : 7 : } /* InteractiveShell::InteractiveShell() */
149 : :
150 : 7 : InteractiveShell::~InteractiveShell() {
151 : : #if HAVE_LIBEDITLINE
152 : : int err = ::write_history(d_historyFilename.c_str());
153 : : if (d_solver->getOptionInfo("verbosity").intValue() >= 1)
154 : : {
155 : : if (err == 0)
156 : : {
157 : : d_solver->getDriverOptions().err()
158 : : << "Wrote " << ::history_length << " lines of history to "
159 : : << d_historyFilename << std::endl;
160 : : } else {
161 : : d_solver->getDriverOptions().err()
162 : : << "Could not write history to " << d_historyFilename << ": "
163 : : << strerror(err) << std::endl;
164 : : }
165 : : }
166 : : #endif /* HAVE_LIBEDITLINE */
167 : 7 : }
168 : :
169 : 17 : bool InteractiveShell::readAndExecCommands()
170 : : {
171 : 17 : char* lineBuf = NULL;
172 : 51 : string line = "";
173 : 17 : restart:
174 : :
175 : : /* Don't do anything if the input is closed or if we've seen a
176 : : * QuitCommand. */
177 [ + - ][ - + ]: 17 : if(d_in.eof() || d_quit) {
[ - + ]
178 [ - - ]: 0 : if (d_isInteractive)
179 : : {
180 : 0 : d_out << endl;
181 : : }
182 : 0 : return false;
183 : : }
184 : :
185 : : /* If something's wrong with the input, there's nothing we can do. */
186 [ - + ]: 17 : if( !d_in.good() ) {
187 : 0 : throw ParserException("Interactive input broken.");
188 : : }
189 : :
190 : : /* Prompt the user for input. */
191 [ + - ]: 17 : if (d_usingEditline)
192 : : {
193 : : #if HAVE_LIBEDITLINE
194 : : Assert(d_isInteractive);
195 : : lineBuf = ::readline(line == "" ? "cvc5> " : "... > ");
196 : : if(lineBuf != NULL && lineBuf[0] != '\0') {
197 : : ::add_history(lineBuf);
198 : : }
199 : : line += lineBuf == NULL ? "" : lineBuf;
200 : : free(lineBuf);
201 : : #endif /* HAVE_LIBEDITLINE */
202 : : }
203 : : else
204 : : {
205 [ + - ]: 17 : if (d_isInteractive)
206 : : {
207 [ + - ]: 17 : if (line == "")
208 : : {
209 : 17 : d_out << "cvc5> " << flush;
210 : : }
211 : : else
212 : : {
213 : 0 : d_out << "... > " << flush;
214 : : }
215 : : }
216 : :
217 : : /* Read a line */
218 : 17 : stringbuf sb;
219 : 17 : d_in.get(sb);
220 : 17 : line += sb.str();
221 : : }
222 : :
223 : 34 : string input = "";
224 : : while(true) {
225 [ + - ]: 34 : Trace("interactive") << "Input now '" << input << line << "'" << endl
226 : 17 : << flush;
227 : :
228 [ + + ][ + + ]: 17 : Assert(!(d_in.fail() && !d_in.eof()) || line.empty() || !d_isInteractive);
[ - + ][ - - ]
[ - + ][ - - ]
229 : :
230 : : /* Check for failure. */
231 [ + + ][ + + ]: 17 : if(d_in.fail() && !d_in.eof()) {
[ + + ]
232 : : /* This should only happen if the input line was empty. */
233 [ - + ][ - - ]: 4 : Assert(line.empty() || !d_isInteractive);
[ - + ][ - - ]
234 : 4 : d_in.clear();
235 : : }
236 : :
237 : : /* Strip trailing whitespace. */
238 : 17 : int n = line.length() - 1;
239 [ + + ][ - + ]: 17 : while( !line.empty() && isspace(line[n]) ) {
[ - + ]
240 : 0 : line.erase(n,1);
241 : 0 : n--;
242 : : }
243 : :
244 : : /* If we hit EOF, we're done. */
245 [ + + ]: 17 : if ((!d_usingEditline && d_in.eof())
246 [ + - ][ - + ]: 34 : || (d_usingEditline && lineBuf == NULL))
[ - - ][ + + ]
247 : : {
248 : 7 : input += line;
249 : :
250 [ + - ]: 7 : if (input.empty())
251 : : {
252 : : /* Nothing left to parse. */
253 [ + - ]: 7 : if (d_isInteractive)
254 : : {
255 : 7 : d_out << endl;
256 : : }
257 : 7 : return false;
258 : : }
259 : :
260 : : /* Some input left to parse, but nothing left to read.
261 : : Jump out of input loop. */
262 : 0 : d_out << endl;
263 : 0 : input = line = "";
264 : 0 : d_in.clear();
265 : 0 : goto restart;
266 : : }
267 : :
268 [ + - ]: 10 : if (!d_usingEditline)
269 : : {
270 : : /* Extract the newline delimiter from the stream too */
271 : 10 : int c CVC5_UNUSED = d_in.get();
272 [ - + ][ - + ]: 10 : Assert(c == '\n');
[ - - ]
273 [ + - ]: 20 : Trace("interactive") << "Next char is '" << (char)c << "'" << endl
274 : 10 : << flush;
275 : : }
276 : :
277 : 10 : input += line;
278 : :
279 : : /* If the last char was a backslash, continue on the next line. */
280 : 10 : n = input.length() - 1;
281 [ + + ][ - + ]: 10 : if( !line.empty() && input[n] == '\\' ) {
[ - + ]
282 : 0 : input[n] = '\n';
283 [ - - ]: 0 : if (d_usingEditline)
284 : : {
285 : : #if HAVE_LIBEDITLINE
286 : : lineBuf = ::readline("... > ");
287 : : if(lineBuf != NULL && lineBuf[0] != '\0') {
288 : : ::add_history(lineBuf);
289 : : }
290 : : line = lineBuf == NULL ? "" : lineBuf;
291 : : free(lineBuf);
292 : : #endif /* HAVE_LIBEDITLINE */
293 : : }
294 : : else
295 : : {
296 [ - - ]: 0 : if (d_isInteractive)
297 : : {
298 : 0 : d_out << "... > " << flush;
299 : : }
300 : :
301 : : /* Read a line */
302 : 0 : stringbuf sb;
303 : 0 : d_in.get(sb);
304 : 0 : line = sb.str();
305 : : }
306 : : } else {
307 : : /* No continuation, we're done. */
308 [ + - ]: 10 : Trace("interactive") << "Leaving input loop." << endl << flush;
309 : 10 : break;
310 : : }
311 : 0 : }
312 : :
313 : : // set new string input, without a new parser
314 : 10 : d_parser->setStringInputInternal(input, INPUT_FILENAME);
315 : :
316 : : /* There may be more than one command in the input. Build up a
317 : : sequence. */
318 : 10 : std::vector<Command> cmdSeq;
319 : 10 : Command cmdp;
320 : : // remember the scope level of the symbol manager, in case we hit an end of
321 : : // line (when catching ParserEndOfFileException).
322 : 10 : size_t lastScopeLevel = d_symman->scopeLevel();
323 : :
324 : : try
325 : : {
326 : : while (true)
327 : : {
328 : 16 : cmdp = d_parser->nextCommand();
329 [ + + ]: 15 : if (cmdp.isNull())
330 : : {
331 : 9 : break;
332 : : }
333 : 6 : Cmd* cmd = cmdp.d_cmd.get();
334 : : // execute the command immediately
335 : 6 : d_cexec->doCommand(&cmdp);
336 [ - + ]: 6 : if (cmd->interrupted())
337 : : {
338 : 0 : d_quit = true;
339 : 0 : return false;
340 : : }
341 : 6 : cmdSeq.emplace_back(std::move(cmdp));
342 [ + - ][ - + ]: 6 : if (dynamic_cast<QuitCommand*>(cmd) != NULL)
343 : : {
344 : 0 : d_quit = true;
345 : 0 : break;
346 : : }
347 : : else
348 : : {
349 : : #if HAVE_LIBEDITLINE
350 : : if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL)
351 : : {
352 : : s_declarations.insert(
353 : : dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
354 : : }
355 : : else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL)
356 : : {
357 : : s_declarations.insert(
358 : : dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
359 : : }
360 : : else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL)
361 : : {
362 : : s_declarations.insert(
363 : : dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol());
364 : : }
365 : : else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL)
366 : : {
367 : : s_declarations.insert(
368 : : dynamic_cast<DefineSortCommand*>(cmd)->getSymbol());
369 : : }
370 : : #endif /* HAVE_LIBEDITLINE */
371 : : }
372 : 6 : lastScopeLevel = d_symman->scopeLevel();
373 : 6 : }
374 : : }
375 : 0 : catch (ParserEndOfFileException& pe)
376 : : {
377 : : // pop back to the scope we were at prior to reading the last command
378 [ - - ]: 0 : while (d_symman->scopeLevel() > lastScopeLevel)
379 : : {
380 : 0 : d_symman->popScope();
381 : : }
382 : 0 : line += "\n";
383 : 0 : goto restart;
384 : : }
385 [ + - ]: 2 : catch (ParserException& pe)
386 : : {
387 [ - + ]: 1 : if (d_solver->getOption("output-language") == "LANG_SMTLIB_V2_6")
388 : : {
389 : 0 : d_out << "(error \"" << pe << "\")" << endl;
390 : : }
391 : : else
392 : : {
393 : 1 : d_out << pe << endl;
394 : : }
395 : : // if not interactive, we quit when we encounter a parse error
396 [ - + ]: 1 : if (!d_isInteractive)
397 : : {
398 : 0 : d_quit = true;
399 : 0 : return false;
400 : : }
401 : : // We can't really clear out the sequence and abort the current line,
402 : : // because the parse error might be for the second command on the
403 : : // line. The first ones haven't yet been executed by the SolverEngine,
404 : : // but the parser state has already made the variables and the mappings
405 : : // in the symbol table. So unfortunately, either we exit cvc5 entirely,
406 : : // or we commit to the current line up to the command with the parse
407 : : // error.
408 : : //
409 : : // FIXME: does that mean e.g. that a pushed LET scope might not yet have
410 : : // been popped?!
411 : : //
412 : : // delete cmd_seq;
413 : : // cmd_seq = new CommandSequence();
414 : : }
415 : :
416 : 10 : return true;
417 : : }/* InteractiveShell::readCommand() */
418 : :
419 : : #if HAVE_LIBEDITLINE
420 : :
421 : : char** commandCompletion(const char* text, int start, int end) {
422 : : Trace("rl") << "text: " << text << endl;
423 : : Trace("rl") << "start: " << start << " end: " << end << endl;
424 : : return rl_completion_matches(text, commandGenerator);
425 : : }
426 : :
427 : : // Our peculiar versions of "less than" for strings
428 : : struct StringPrefix1Less {
429 : : bool operator()(const std::string& s1, const std::string& s2) {
430 : : size_t l1 = s1.length(), l2 = s2.length();
431 : : size_t l = l1 <= l2 ? l1 : l2;
432 : : return s1.compare(0, l1, s2, 0, l) < 0;
433 : : }
434 : : };/* struct StringPrefix1Less */
435 : : struct StringPrefix2Less {
436 : : bool operator()(const std::string& s1, const std::string& s2) {
437 : : size_t l1 = s1.length(), l2 = s2.length();
438 : : size_t l = l1 <= l2 ? l1 : l2;
439 : : return s1.compare(0, l, s2, 0, l2) < 0;
440 : : }
441 : : };/* struct StringPrefix2Less */
442 : :
443 : : char* commandGenerator(const char* text, int state) {
444 : : static thread_local const std::string* rlCommand;
445 : : static thread_local set<string>::const_iterator* rlDeclaration;
446 : :
447 : : const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less());
448 : : const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less());
449 : :
450 : : set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix2Less());
451 : : set<string>::const_iterator jj = upper_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix1Less());
452 : :
453 : : if(rlDeclaration == NULL) {
454 : : rlDeclaration = new set<string>::const_iterator();
455 : : }
456 : :
457 : : if(state == 0) {
458 : : rlCommand = i;
459 : : *rlDeclaration = ii;
460 : : }
461 : :
462 : : if(rlCommand != j) {
463 : : return strdup((*rlCommand++).c_str());
464 : : }
465 : :
466 : : return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
467 : : }
468 : :
469 : : #endif /* HAVE_LIBEDITLINE */
470 : :
471 : : } // namespace cvc5::internal
|
