Remove public option wrappers (#6716)
[cvc5.git] / src / main / interactive_shell.h
index 18e42f1e5f2e27baab3acbba4c362bf9074b221e..cf5f22b51753bfc18538d4f81635c227a80c772f 100644 (file)
@@ -1,19 +1,20 @@
-/*********************                                                        */
-/*! \file interactive_shell.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Morgan Deters, Christopher L. Conway, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2016 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.\endverbatim
- **
- ** \brief Interactive shell for CVC4
- **/
-
-#ifndef __CVC4__INTERACTIVE_SHELL_H
-#define __CVC4__INTERACTIVE_SHELL_H
+/******************************************************************************
+ * 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 "options/options.h"
 #include "util/unsafe_interrupt_exception.h"
 
-namespace CVC4 {
+namespace cvc5 {
 
 class Command;
-class ExprManager;
 class Options;
 
+namespace api {
+class Solver;
+}
+
 namespace parser {
   class Parser;
-}/* CVC4::parser namespace */
+  }  // namespace parser
+
+class SymbolManager;
 
-class CVC4_PUBLIC InteractiveShell {
+class InteractiveShell
+{
+  const Options& d_options;
   std::istream& d_in;
   std::ostream& d_out;
   parser::Parser* d_parser;
-  const Options& d_options;
   bool d_quit;
-  bool d_usingReadline;
+  bool d_usingEditline;
 
   std::string d_historyFilename;
 
@@ -46,28 +53,26 @@ class CVC4_PUBLIC InteractiveShell {
   static const unsigned s_historyLimit = 500;
 
 public:
-  InteractiveShell(ExprManager& exprManager, const Options& options);
-
-  /**
-   * 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() throw (UnsafeInterruptException);
-
-  /**
-   * Return the internal parser being used.
-   */
-  parser::Parser* getParser() {
-    return d_parser;
-  }
+ 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 */
 
-}/* CVC4 namespace */
+}  // namespace cvc5
 
-#endif /* __CVC4__INTERACTIVE_SHELL_H */
+#endif /* CVC5__INTERACTIVE_SHELL_H */