1 /********************* */
2 /*! \file interactive_shell.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Christopher L. Conway, Tim King
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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.\endverbatim
11 **
12 ** \brief Interactive shell for CVC4
13 **
14 ** This file is the implementation for the CVC4 interactive shell.
15 ** The shell supports the readline library.
16 **/
17 #include "main/interactive_shell.h"
18
19 #include <algorithm>
20 #include <cassert>
21 #include <cstdlib>
22 #include <iostream>
23 #include <set>
24 #include <string.h>
25 #include <string>
26 #include <utility>
27 #include <vector>
28
29 //This must go before HAVE_LIBREADLINE.
30 #include "cvc4autoconfig.h"
31
32 #if HAVE_LIBREADLINE
33 # include <readline/readline.h>
34 # include <readline/history.h>
35 # if HAVE_EXT_STDIO_FILEBUF_H
36 # include <ext/stdio_filebuf.h>
37 # endif /* HAVE_EXT_STDIO_FILEBUF_H */
38 #endif /* HAVE_LIBREADLINE */
39
40 #include "api/cvc4cpp.h"
41 #include "base/output.h"
42 #include "options/language.h"
43 #include "options/options.h"
44 #include "parser/input.h"
45 #include "parser/parser.h"
46 #include "parser/parser_builder.h"
47 #include "smt/command.h"
48 #include "theory/logic_info.h"
49
50 using namespace std;
51
52 namespace CVC4 {
53
54 using namespace parser;
55 using namespace language;
56
57 const string InteractiveShell::INPUT_FILENAME = "<shell>";
58
59 #if HAVE_LIBREADLINE
60
61 #if HAVE_EXT_STDIO_FILEBUF_H
62 using __gnu_cxx::stdio_filebuf;
63 #endif /* HAVE_EXT_STDIO_FILEBUF_H */
64
65 char** commandCompletion(const char* text, int start, int end);
66 char* commandGenerator(const char* text, int state);
67
68 static const std::string cvc_commands[] = {
69 #include "main/cvc_tokens.h"
70 };/* cvc_commands */
71
72 static const std::string smt1_commands[] = {
73 #include "main/smt1_tokens.h"
74 };/* smt1_commands */
75
76 static const std::string smt2_commands[] = {
77 #include "main/smt2_tokens.h"
78 };/* smt2_commands */
79
80 static const std::string tptp_commands[] = {
81 #include "main/tptp_tokens.h"
82 };/* tptp_commands */
83
84 static const std::string* commandsBegin;
85 static const std::string* commandsEnd;
86
87 static set<string> s_declarations;
88
89 #endif /* HAVE_LIBREADLINE */
90
InteractiveShell(api::Solver * solver)91 InteractiveShell::InteractiveShell(api::Solver* solver)
92 : d_options(solver->getExprManager()->getOptions()),
93 d_in(*d_options.getIn()),
94 d_out(*d_options.getOutConst()),
95 d_quit(false)
96 {
97 ParserBuilder parserBuilder(solver, INPUT_FILENAME, d_options);
98 /* Create parser with bogus input. */
99 d_parser = parserBuilder.withStringInput("").build();
100 if(d_options.wasSetByUserForceLogicString()) {
101 LogicInfo tmp(d_options.getForceLogicString());
102 d_parser->forceLogic(tmp.getLogicString());
103 }
104
105 #if HAVE_LIBREADLINE
106 if(&d_in == &cin) {
107 ::rl_readline_name = const_cast<char*>("CVC4");
108 #if READLINE_COMPENTRY_FUNC_RETURNS_CHARP
109 ::rl_completion_entry_function = commandGenerator;
110 #else /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
111 ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator;
112 #endif /* READLINE_COMPENTRY_FUNC_RETURNS_CHARP */
113 ::using_history();
114
115 OutputLanguage lang = toOutputLanguage(d_options.getInputLanguage());
116 switch(lang) {
117 case output::LANG_CVC4:
118 d_historyFilename = string(getenv("HOME")) + "/.cvc4_history";
119 commandsBegin = cvc_commands;
120 commandsEnd = cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
121 break;
122 case output::LANG_SMTLIB_V1:
123 d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib1";
124 commandsBegin = smt1_commands;
125 commandsEnd = smt1_commands + sizeof(smt1_commands) / sizeof(*smt1_commands);
126 break;
127 case output::LANG_TPTP:
128 d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_tptp";
129 commandsBegin = tptp_commands;
130 commandsEnd = tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
131 break;
132 default:
133 if (language::isOutputLang_smt2(lang))
134 {
135 d_historyFilename = string(getenv("HOME")) + "/.cvc4_history_smtlib2";
136 commandsBegin = smt2_commands;
137 commandsEnd =
138 smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
139 }
140 else
141 {
142 std::stringstream ss;
143 ss << "internal error: unhandled language " << lang;
144 throw Exception(ss.str());
145 }
146 }
147 d_usingReadline = true;
148 int err = ::read_history(d_historyFilename.c_str());
149 ::stifle_history(s_historyLimit);
150 if(Notice.isOn()) {
151 if(err == 0) {
152 Notice() << "Read " << ::history_length << " lines of history from "
153 << d_historyFilename << std::endl;
154 } else {
155 Notice() << "Could not read history from " << d_historyFilename
156 << ": " << strerror(err) << std::endl;
157 }
158 }
159 } else {
160 d_usingReadline = false;
161 }
162 #else /* HAVE_LIBREADLINE */
163 d_usingReadline = false;
164 #endif /* HAVE_LIBREADLINE */
165 }/* InteractiveShell::InteractiveShell() */
166
~InteractiveShell()167 InteractiveShell::~InteractiveShell() {
168 #if HAVE_LIBREADLINE
169 int err = ::write_history(d_historyFilename.c_str());
170 if(err == 0) {
171 Notice() << "Wrote " << ::history_length << " lines of history to "
172 << d_historyFilename << std::endl;
173 } else {
174 Notice() << "Could not write history to " << d_historyFilename
175 << ": " << strerror(err) << std::endl;
176 }
177 #endif /* HAVE_LIBREADLINE */
178 delete d_parser;
179 }
180
readCommand()181 Command* InteractiveShell::readCommand()
182 {
183 char* lineBuf = NULL;
184 string line = "";
185
186 restart:
187
188 /* Don't do anything if the input is closed or if we've seen a
189 * QuitCommand. */
190 if(d_in.eof() || d_quit) {
191 d_out << endl;
192 return NULL;
193 }
194
195 /* If something's wrong with the input, there's nothing we can do. */
196 if( !d_in.good() ) {
197 throw ParserException("Interactive input broken.");
198 }
199
200 /* Prompt the user for input. */
201 if(d_usingReadline) {
202 #if HAVE_LIBREADLINE
203 lineBuf = ::readline(d_options.getInteractivePrompt()
204 ? (line == "" ? "CVC4> " : "... > ") : "");
205 if(lineBuf != NULL && lineBuf[0] != '\0') {
206 ::add_history(lineBuf);
207 }
208 line += lineBuf == NULL ? "" : lineBuf;
209 free(lineBuf);
210 #endif /* HAVE_LIBREADLINE */
211 } else {
212 if(d_options.getInteractivePrompt()) {
213 if(line == "") {
214 d_out << "CVC4> " << flush;
215 } else {
216 d_out << "... > " << flush;
217 }
218 }
219
220 /* Read a line */
221 stringbuf sb;
222 d_in.get(sb);
223 line += sb.str();
224 }
225
226 string input = "";
227 while(true) {
228 Debug("interactive") << "Input now '" << input << line << "'" << endl
229 << flush;
230
231 assert( !(d_in.fail() && !d_in.eof()) || line.empty() );
232
233 /* Check for failure. */
234 if(d_in.fail() && !d_in.eof()) {
235 /* This should only happen if the input line was empty. */
236 assert( line.empty() );
237 d_in.clear();
238 }
239
240 /* Strip trailing whitespace. */
241 int n = line.length() - 1;
242 while( !line.empty() && isspace(line[n]) ) {
243 line.erase(n,1);
244 n--;
245 }
246
247 /* If we hit EOF, we're done. */
248 if( (!d_usingReadline && d_in.eof()) ||
249 (d_usingReadline && lineBuf == NULL) ) {
250 input += line;
251
252 if(input.empty()) {
253 /* Nothing left to parse. */
254 d_out << endl;
255 return NULL;
256 }
257
258 /* Some input left to parse, but nothing left to read.
259 Jump out of input loop. */
260 d_out << endl;
261 input = line = "";
262 d_in.clear();
263 goto restart;
264 }
265
266 if(!d_usingReadline) {
267 /* Extract the newline delimiter from the stream too */
268 int c CVC4_UNUSED = d_in.get();
269 assert(c == '\n');
270 Debug("interactive") << "Next char is '" << (char)c << "'" << endl
271 << flush;
272 }
273
274 input += line;
275
276 /* If the last char was a backslash, continue on the next line. */
277 n = input.length() - 1;
278 if( !line.empty() && input[n] == '\\' ) {
279 input[n] = '\n';
280 if(d_usingReadline) {
281 #if HAVE_LIBREADLINE
282 lineBuf = ::readline(d_options.getInteractivePrompt() ? "... > " : "");
283 if(lineBuf != NULL && lineBuf[0] != '\0') {
284 ::add_history(lineBuf);
285 }
286 line = lineBuf == NULL ? "" : lineBuf;
287 free(lineBuf);
288 #endif /* HAVE_LIBREADLINE */
289 } else {
290 if(d_options.getInteractivePrompt()) {
291 d_out << "... > " << flush;
292 }
293
294 /* Read a line */
295 stringbuf sb;
296 d_in.get(sb);
297 line = sb.str();
298 }
299 } else {
300 /* No continuation, we're done. */
301 Debug("interactive") << "Leaving input loop." << endl << flush;
302 break;
303 }
304 }
305
306 d_parser->setInput(Input::newStringInput(d_options.getInputLanguage(),
307 input, INPUT_FILENAME));
308
309 /* There may be more than one command in the input. Build up a
310 sequence. */
311 CommandSequence *cmd_seq = new CommandSequence();
312 Command *cmd;
313
314 try {
315 while( (cmd = d_parser->nextCommand()) ) {
316 cmd_seq->addCommand(cmd);
317 if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
318 d_quit = true;
319 break;
320 } else {
321 #if HAVE_LIBREADLINE
322 if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
323 s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
324 } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
325 s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
326 } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) {
327 s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol());
328 } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
329 s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
330 }
331 #endif /* HAVE_LIBREADLINE */
332 }
333 }
334 } catch(ParserEndOfFileException& pe) {
335 line += "\n";
336 goto restart;
337 } catch(ParserException& pe) {
338 if (language::isOutputLang_smt2(d_options.getOutputLanguage()))
339 {
340 d_out << "(error \"" << pe << "\")" << endl;
341 } else {
342 d_out << pe << endl;
343 }
344 // We can't really clear out the sequence and abort the current line,
345 // because the parse error might be for the second command on the
346 // line. The first ones haven't yet been executed by the SmtEngine,
347 // but the parser state has already made the variables and the mappings
348 // in the symbol table. So unfortunately, either we exit CVC4 entirely,
349 // or we commit to the current line up to the command with the parse
350 // error.
351 //
352 // FIXME: does that mean e.g. that a pushed LET scope might not yet have
353 // been popped?!
354 //
355 //delete cmd_seq;
356 //cmd_seq = new CommandSequence();
357 }
358
359 return cmd_seq;
360 }/* InteractiveShell::readCommand() */
361
362 #if HAVE_LIBREADLINE
363
commandCompletion(const char * text,int start,int end)364 char** commandCompletion(const char* text, int start, int end) {
365 Debug("rl") << "text: " << text << endl;
366 Debug("rl") << "start: " << start << " end: " << end << endl;
367 return rl_completion_matches(text, commandGenerator);
368 }
369
370 // Our peculiar versions of "less than" for strings
371 struct StringPrefix1Less {
operator ()CVC4::StringPrefix1Less372 bool operator()(const std::string& s1, const std::string& s2) {
373 size_t l1 = s1.length(), l2 = s2.length();
374 size_t l = l1 <= l2 ? l1 : l2;
375 return s1.compare(0, l1, s2, 0, l) < 0;
376 }
377 };/* struct StringPrefix1Less */
378 struct StringPrefix2Less {
operator ()CVC4::StringPrefix2Less379 bool operator()(const std::string& s1, const std::string& s2) {
380 size_t l1 = s1.length(), l2 = s2.length();
381 size_t l = l1 <= l2 ? l1 : l2;
382 return s1.compare(0, l, s2, 0, l2) < 0;
383 }
384 };/* struct StringPrefix2Less */
385
commandGenerator(const char * text,int state)386 char* commandGenerator(const char* text, int state) {
387 static thread_local const std::string* rlCommand;
388 static thread_local set<string>::const_iterator* rlDeclaration;
389
390 const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less());
391 const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less());
392
393 set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix2Less());
394 set<string>::const_iterator jj = upper_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix1Less());
395
396 if(rlDeclaration == NULL) {
397 rlDeclaration = new set<string>::const_iterator();
398 }
399
400 if(state == 0) {
401 rlCommand = i;
402 *rlDeclaration = ii;
403 }
404
405 if(rlCommand != j) {
406 return strdup((*rlCommand++).c_str());
407 }
408
409 return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
410 }
411
412 #endif /* HAVE_LIBREADLINE */
413
414 }/* CVC4 namespace */
415