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