Add symbol manager (#5380)
[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-2020 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 class SymbolManager;
37 }/* CVC4::parser namespace */
38
39 class CVC4_PUBLIC InteractiveShell
40 {
41 const Options& d_options;
42 std::istream& d_in;
43 std::ostream& d_out;
44 parser::Parser* d_parser;
45 bool d_quit;
46 bool d_usingEditline;
47
48 std::string d_historyFilename;
49
50 static const std::string INPUT_FILENAME;
51 static const unsigned s_historyLimit = 500;
52
53 public:
54 InteractiveShell(api::Solver* solver, parser::SymbolManager* sm);
55
56 /**
57 * Close out the interactive session.
58 */
59 ~InteractiveShell();
60
61 /**
62 * Read a command from the interactive shell. This will read as
63 * many lines as necessary to parse a well-formed command.
64 */
65 Command* readCommand();
66
67 /**
68 * Return the internal parser being used.
69 */
70 parser::Parser* getParser() { return d_parser; }
71
72 };/* class InteractiveShell */
73
74 }/* CVC4 namespace */
75
76 #endif /* CVC4__INTERACTIVE_SHELL_H */