Merge branch 'master' of github.com:tiliang/CVC4
[cvc5.git] / src / main / interactive_shell.h
1 /********************* */
2 /*! \file interactive_shell.h
3 ** \verbatim
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** 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 <iostream>
19 #include <string>
20
21 #include "util/language.h"
22 #include "util/unsafe_interrupt_exception.h"
23 #include "options/options.h"
24
25 namespace CVC4 {
26
27 class Command;
28 class ExprManager;
29 class Options;
30
31 namespace parser {
32 class Parser;
33 }/* CVC4::parser namespace */
34
35 class CVC4_PUBLIC InteractiveShell {
36 std::istream& d_in;
37 std::ostream& d_out;
38 parser::Parser* d_parser;
39 const Options& d_options;
40 bool d_quit;
41 bool d_usingReadline;
42
43 std::string d_historyFilename;
44
45 static const std::string INPUT_FILENAME;
46 static const unsigned s_historyLimit = 500;
47
48 public:
49 InteractiveShell(ExprManager& exprManager, const Options& options);
50
51 /**
52 * Close out the interactive session.
53 */
54 ~InteractiveShell();
55
56 /**
57 * Read a command from the interactive shell. This will read as
58 * many lines as necessary to parse a well-formed command.
59 */
60 Command* readCommand() throw (UnsafeInterruptException);
61
62 /**
63 * Return the internal parser being used.
64 */
65 parser::Parser* getParser() {
66 return d_parser;
67 }
68
69 };/* class InteractiveShell */
70
71 }/* CVC4 namespace */
72
73 #endif /* __CVC4__INTERACTIVE_SHELL_H */