Remove public option wrappers (#6716)

[cvc5.git] / src / main / interactive_shell.h

diff --git a/src/main/interactive_shell.h b/src/main/interactive_shell.h
index a60278ebad4fdd8999cb609131fa59416ff1e9b4..cf5f22b51753bfc18538d4f81635c227a80c772f 100644 (file)
--- a/src/main/interactive_shell.h
+++ b/src/main/interactive_shell.h
@@ -1,59 +1,78 @@
-/*********************                                                        */
-/*! \file interactive_shell.h
- ** \verbatim
- ** Original author: cconway
- ** Major contributors: 
- ** Minor contributors (to current version): 
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Interactive shell for CVC4
- **/
-
-#ifndef __CVC4__INTERACTIVE_SHELL_H
-#define __CVC4__INTERACTIVE_SHELL_H
-
-#include <iostream>
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Morgan Deters, Christopher L. Conway, Mathias Preiner
+ *
+ * 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.
+ */
+
+#ifndef CVC5__INTERACTIVE_SHELL_H
+#define CVC5__INTERACTIVE_SHELL_H
+
+#include <iosfwd>
 #include <string>
 
-#include "parser/parser_builder.h"
-#include "util/language.h"
-#include "util/options.h"
+#include "options/language.h"
+#include "options/options.h"
+#include "util/unsafe_interrupt_exception.h"
+
+namespace cvc5 {
 
-namespace CVC4 {
+class Command;
+class Options;
 
-  class Command;
+namespace api {
+class Solver;
+}
 
-  using namespace parser;
+namespace parser {
+  class Parser;
+  }  // namespace parser
 
-class CVC4_PUBLIC InteractiveShell {
+class SymbolManager;
+
+class InteractiveShell
+{
+  const Options& d_options;
   std::istream& d_in;
   std::ostream& d_out;
-  Parser* d_parser;
-  const InputLanguage d_language;
+  parser::Parser* d_parser;
+  bool d_quit;
+  bool d_usingEditline;
+
+  std::string d_historyFilename;
 
   static const std::string INPUT_FILENAME;
+  static const unsigned s_historyLimit = 500;
 
 public:
-  InteractiveShell(ExprManager& exprManager,
-                  const Options& options) : 
-    d_in(*options.in),
-    d_out(*options.out),
-    d_language(options.inputLanguage) {
-    ParserBuilder parserBuilder(exprManager,INPUT_FILENAME,options);
-    /* Create parser with bogus input. */
-    d_parser = parserBuilder.withStringInput("").build();
-  }
-
-  /** Read a command from the interactive shell. This will read as
-      many lines as necessary to parse a well-formed command. */
-  Command *readCommand();
-};
-
-} // CVC4 namespace
-
-#endif // __CVC4__INTERACTIVE_SHELL_H
+ InteractiveShell(api::Solver* solver, SymbolManager* sm);
+
+ /**
+  * Close out the interactive session.
+  */
+ ~InteractiveShell();
+
+ /**
+  * Read a command from the interactive shell. This will read as
+  * many lines as necessary to parse a well-formed command.
+  */
+ Command* readCommand();
+
+ /**
+  * Return the internal parser being used.
+  */
+ parser::Parser* getParser() { return d_parser; }
+
+};/* class InteractiveShell */
+
+}  // namespace cvc5
+
+#endif /* CVC5__INTERACTIVE_SHELL_H */