src/main/interactive_shell.cpp

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