Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/main/interactive_shell.cpp	Lines:	60	89	67.4 %
Date:	2021-08-15	Branches:	100	283	35.3 %


/******************************************************************************
 * Top contributors (to current version):
 *   Morgan Deters, Christopher L. Conway, Andrew V. Jones
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Interactive shell for cvc5.
 *
 * This file is the implementation for the cvc5 interactive shell.
 * The shell supports the editline library.
 */
#include "main/interactive_shell.h"

#include <cstring>
#include <unistd.h>

#include <algorithm>
#include <cstdlib>
#include <iostream>
#include <set>
#include <string>
#include <utility>
#include <vector>

// This must go before HAVE_LIBEDITLINE.
#include "base/cvc5config.h"

#if HAVE_LIBEDITLINE
#include <editline/readline.h>
#  if HAVE_EXT_STDIO_FILEBUF_H
#    include <ext/stdio_filebuf.h>
#  endif /* HAVE_EXT_STDIO_FILEBUF_H */
#endif   /* HAVE_LIBEDITLINE */

#include "api/cpp/cvc5.h"
#include "base/check.h"
#include "base/output.h"
#include "expr/symbol_manager.h"
#include "options/base_options.h"
#include "options/language.h"
#include "options/main_options.h"
#include "options/options.h"
#include "options/parser_options.h"
#include "parser/input.h"
#include "parser/parser.h"
#include "parser/parser_builder.h"
#include "smt/command.h"
#include "theory/logic_info.h"

using namespace std;

namespace cvc5 {

using namespace parser;
using namespace language;

const string InteractiveShell::INPUT_FILENAME = "<shell>";

#if HAVE_LIBEDITLINE

#if HAVE_EXT_STDIO_FILEBUF_H
using __gnu_cxx::stdio_filebuf;
#endif /* HAVE_EXT_STDIO_FILEBUF_H */

char** commandCompletion(const char* text, int start, int end);
char* commandGenerator(const char* text, int state);

static const std::string cvc_commands[] = {
#include "main/cvc_tokens.h"
};/* cvc_commands */

static const std::string smt2_commands[] = {
#include "main/smt2_tokens.h"
};/* smt2_commands */

static const std::string tptp_commands[] = {
#include "main/tptp_tokens.h"
};/* tptp_commands */

static const std::string* commandsBegin;
static const std::string* commandsEnd;

static set<string> s_declarations;

#endif /* HAVE_LIBEDITLINE */

InteractiveShell::InteractiveShell(api::Solver* solver, SymbolManager* sm)
    : d_options(solver->getOptions()),
      d_in(*d_options.base.in),
      d_out(*d_options.base.out),
      d_quit(false)
{
  ParserBuilder parserBuilder(solver, sm, d_options);
  /* Create parser with bogus input. */
  d_parser = parserBuilder.build();
  if (d_options.parser.forceLogicStringWasSetByUser)
  {
    LogicInfo tmp(d_options.parser.forceLogicString);
    d_parser->forceLogic(tmp.getLogicString());
  }

#if HAVE_LIBEDITLINE
  if (&d_in == &std::cin && isatty(fileno(stdin)))
  {
    ::rl_readline_name = const_cast<char*>("cvc5");
#if EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP
    ::rl_completion_entry_function = commandGenerator;
#else /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
    ::rl_completion_entry_function = (int (*)(const char*, int)) commandGenerator;
#endif /* EDITLINE_COMPENTRY_FUNC_RETURNS_CHARP */
    ::using_history();

    OutputLanguage lang =
        toOutputLanguage(d_options.base.inputLanguage);
    switch(lang) {
      case output::LANG_CVC:
        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history";
        commandsBegin = cvc_commands;
        commandsEnd =
            cvc_commands + sizeof(cvc_commands) / sizeof(*cvc_commands);
        break;
      case output::LANG_TPTP:
        d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_tptp";
        commandsBegin = tptp_commands;
        commandsEnd =
            tptp_commands + sizeof(tptp_commands) / sizeof(*tptp_commands);
        break;
      default:
        if (language::isOutputLang_smt2(lang))
        {
          d_historyFilename = string(getenv("HOME")) + "/.cvc5_history_smtlib2";
          commandsBegin = smt2_commands;
          commandsEnd =
              smt2_commands + sizeof(smt2_commands) / sizeof(*smt2_commands);
        }
        else
        {
          std::stringstream ss;
          ss << "internal error: unhandled language " << lang;
          throw Exception(ss.str());
        }
    }
    d_usingEditline = true;
    int err = ::read_history(d_historyFilename.c_str());
    ::stifle_history(s_historyLimit);
    if(Notice.isOn()) {
      if(err == 0) {
        Notice() << "Read " << ::history_length << " lines of history from "
                 << d_historyFilename << std::endl;
      } else {
        Notice() << "Could not read history from " << d_historyFilename
                 << ": " << strerror(err) << std::endl;
      }
    }
  }
  else
  {
    d_usingEditline = false;
  }
#else  /* HAVE_LIBEDITLINE */
  d_usingEditline = false;
#endif /* HAVE_LIBEDITLINE */
}/* InteractiveShell::InteractiveShell() */

InteractiveShell::~InteractiveShell() {
#if HAVE_LIBEDITLINE
  int err = ::write_history(d_historyFilename.c_str());
  if(err == 0) {
    Notice() << "Wrote " << ::history_length << " lines of history to "
             << d_historyFilename << std::endl;
  } else {
    Notice() << "Could not write history to " << d_historyFilename
             << ": " << strerror(err) << std::endl;
  }
#endif /* HAVE_LIBEDITLINE */
  delete d_parser;
}

Command* InteractiveShell::readCommand()
{
  char* lineBuf = NULL;
  string line = "";

restart:

  /* Don't do anything if the input is closed or if we've seen a
   * QuitCommand. */
  if(d_in.eof() || d_quit) {
    d_out << endl;
    return NULL;
  }

  /* If something's wrong with the input, there's nothing we can do. */
  if( !d_in.good() ) {
    throw ParserException("Interactive input broken.");
  }

  /* Prompt the user for input. */
  if (d_usingEditline)
  {
#if HAVE_LIBEDITLINE
    lineBuf = ::readline(d_options.driver.interactivePrompt
                             ? (line == "" ? "cvc5> " : "... > ")
                             : "");
    if(lineBuf != NULL && lineBuf[0] != '\0') {
      ::add_history(lineBuf);
    }
    line += lineBuf == NULL ? "" : lineBuf;
    free(lineBuf);
#endif /* HAVE_LIBEDITLINE */
  }
  else
  {
    if (d_options.driver.interactivePrompt)
    {
      if(line == "") {
        d_out << "cvc5> " << flush;
      } else {
        d_out << "... > " << flush;
      }
    }

    /* Read a line */
    stringbuf sb;
    d_in.get(sb);
    line += sb.str();
  }

  string input = "";
  while(true) {
    Debug("interactive") << "Input now '" << input << line << "'" << endl
                         << flush;

    Assert(!(d_in.fail() && !d_in.eof()) || line.empty());

    /* Check for failure. */
    if(d_in.fail() && !d_in.eof()) {
      /* This should only happen if the input line was empty. */
      Assert(line.empty());
      d_in.clear();
    }

    /* Strip trailing whitespace. */
    int n = line.length() - 1;
    while( !line.empty() && isspace(line[n]) ) {
      line.erase(n,1);
      n--;
    }

    /* If we hit EOF, we're done. */
    if ((!d_usingEditline && d_in.eof())
        || (d_usingEditline && lineBuf == NULL))
    {
      input += line;

      if(input.empty()) {
        /* Nothing left to parse. */
        d_out << endl;
        return NULL;
      }

      /* Some input left to parse, but nothing left to read.
         Jump out of input loop. */
      d_out << endl;
      input = line = "";
      d_in.clear();
      goto restart;
    }

    if (!d_usingEditline)
    {
      /* Extract the newline delimiter from the stream too */
      int c CVC5_UNUSED = d_in.get();
      Assert(c == '\n');
      Debug("interactive") << "Next char is '" << (char)c << "'" << endl
                           << flush;
    }

    input += line;

    /* If the last char was a backslash, continue on the next line. */
    n = input.length() - 1;
    if( !line.empty() && input[n] == '\\' ) {
      input[n] = '\n';
      if (d_usingEditline)
      {
#if HAVE_LIBEDITLINE
        lineBuf = ::readline(d_options.driver.interactivePrompt ? "... > "
                                                                      : "");
        if(lineBuf != NULL && lineBuf[0] != '\0') {
          ::add_history(lineBuf);
        }
        line = lineBuf == NULL ? "" : lineBuf;
        free(lineBuf);
#endif /* HAVE_LIBEDITLINE */
      }
      else
      {
        if (d_options.driver.interactivePrompt)
        {
          d_out << "... > " << flush;
        }

        /* Read a line */
        stringbuf sb;
        d_in.get(sb);
        line = sb.str();
      }
    } else {
      /* No continuation, we're done. */
      Debug("interactive") << "Leaving input loop." << endl << flush;
      break;
    }
  }

  d_parser->setInput(Input::newStringInput(
      d_options.base.inputLanguage, input, INPUT_FILENAME));

  /* There may be more than one command in the input. Build up a
     sequence. */
  CommandSequence *cmd_seq = new CommandSequence();
  Command *cmd;

  try
  {
    while ((cmd = d_parser->nextCommand()))
    {
      cmd_seq->addCommand(cmd);
      if (dynamic_cast<QuitCommand*>(cmd) != NULL)
      {
        d_quit = true;
        break;
      }
      else
      {
#if HAVE_LIBEDITLINE
        if (dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL)
        {
          s_declarations.insert(
              dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
        }
        else if (dynamic_cast<DefineFunctionCommand*>(cmd) != NULL)
        {
          s_declarations.insert(
              dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
        }
        else if (dynamic_cast<DeclareSortCommand*>(cmd) != NULL)
        {
          s_declarations.insert(
              dynamic_cast<DeclareSortCommand*>(cmd)->getSymbol());
        }
        else if (dynamic_cast<DefineSortCommand*>(cmd) != NULL)
        {
          s_declarations.insert(
              dynamic_cast<DefineSortCommand*>(cmd)->getSymbol());
        }
#endif /* HAVE_LIBEDITLINE */
      }
    }
  }
  catch (ParserEndOfFileException& pe)
  {
    line += "\n";
    goto restart;
  }
  catch (ParserException& pe)
  {
    if (language::isOutputLang_smt2(d_options.base.outputLanguage))
    {
      d_out << "(error \"" << pe << "\")" << endl;
    }
    else
    {
      d_out << pe << endl;
    }
    // We can't really clear out the sequence and abort the current line,
    // because the parse error might be for the second command on the
    // line.  The first ones haven't yet been executed by the SmtEngine,
    // but the parser state has already made the variables and the mappings
    // in the symbol table.  So unfortunately, either we exit cvc5 entirely,
    // or we commit to the current line up to the command with the parse
    // error.
    //
    // FIXME: does that mean e.g. that a pushed LET scope might not yet have
    // been popped?!
    //
    // delete cmd_seq;
    // cmd_seq = new CommandSequence();
  }

  return cmd_seq;
}/* InteractiveShell::readCommand() */

#if HAVE_LIBEDITLINE

char** commandCompletion(const char* text, int start, int end) {
  Debug("rl") << "text: " << text << endl;
  Debug("rl") << "start: " << start << " end: " << end << endl;
  return rl_completion_matches(text, commandGenerator);
}

// Our peculiar versions of "less than" for strings
struct StringPrefix1Less {
  bool operator()(const std::string& s1, const std::string& s2) {
    size_t l1 = s1.length(), l2 = s2.length();
    size_t l = l1 <= l2 ? l1 : l2;
    return s1.compare(0, l1, s2, 0, l) < 0;
  }
};/* struct StringPrefix1Less */
struct StringPrefix2Less {
  bool operator()(const std::string& s1, const std::string& s2) {
    size_t l1 = s1.length(), l2 = s2.length();
    size_t l = l1 <= l2 ? l1 : l2;
    return s1.compare(0, l, s2, 0, l2) < 0;
  }
};/* struct StringPrefix2Less */

char* commandGenerator(const char* text, int state) {
  static thread_local const std::string* rlCommand;
  static thread_local set<string>::const_iterator* rlDeclaration;

  const std::string* i = lower_bound(commandsBegin, commandsEnd, text, StringPrefix2Less());
  const std::string* j = upper_bound(commandsBegin, commandsEnd, text, StringPrefix1Less());

  set<string>::const_iterator ii = lower_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix2Less());
  set<string>::const_iterator jj = upper_bound(s_declarations.begin(), s_declarations.end(), text, StringPrefix1Less());

  if(rlDeclaration == NULL) {
    rlDeclaration = new set<string>::const_iterator();
  }

  if(state == 0) {
    rlCommand = i;
    *rlDeclaration = ii;
  }

  if(rlCommand != j) {
    return strdup((*rlCommand++).c_str());
  }

  return *rlDeclaration == jj ? NULL : strdup((*(*rlDeclaration)++).c_str());
}

#endif /* HAVE_LIBEDITLINE */

}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

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