Update copyright headers.
[cvc5.git] / src / main / interactive_shell.h
1 /********************* */
2 /*! \file interactive_shell.h
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Morgan Deters, Christopher L. Conway, Aina Niemetz
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
15 #ifndef __CVC4__INTERACTIVE_SHELL_H
16 #define __CVC4__INTERACTIVE_SHELL_H
17
18 #include <iosfwd>
19 #include <string>
20
21 #include "options/language.h"
22 #include "options/options.h"
23 #include "util/unsafe_interrupt_exception.h"
24
25 namespace CVC4 {
26
27 class Command;
28 class Options;
29
30 namespace api {
31 class Solver;
32 }
33
34 namespace parser {
35 class Parser;
36 }/* CVC4::parser namespace */
37
38 class CVC4_PUBLIC InteractiveShell
39 {
40 const Options& d_options;
41 std::istream& d_in;
42 std::ostream& d_out;
43 parser::Parser* d_parser;
44 bool d_quit;
45 bool d_usingReadline;
46
47 std::string d_historyFilename;
48
49 static const std::string INPUT_FILENAME;
50 static const unsigned s_historyLimit = 500;
51
52 public:
53 InteractiveShell(api::Solver* solver);
54
55 /**
56 * Close out the interactive session.
57 */
58 ~InteractiveShell();
59
60 /**
61 * Read a command from the interactive shell. This will read as
62 * many lines as necessary to parse a well-formed command.
63 */
64 Command* readCommand();
65
66 /**
67 * Return the internal parser being used.
68 */
69 parser::Parser* getParser() { return d_parser; }
70
71 };/* class InteractiveShell */
72
73 }/* CVC4 namespace */
74
75 #endif /* __CVC4__INTERACTIVE_SHELL_H */