Fix ufho issues (#3551)

[cvc5.git] / src / options / options.h

diff --git a/src/options/options.h b/src/options/options.h
index 8ca713642975f400eb40db9873f142c56ec37258..c321b349921f761c21d0a73f646da054628fe611 100644 (file)
--- a/src/options/options.h
+++ b/src/options/options.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Morgan Deters, Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 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
@@ -16,8 +16,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__OPTIONS__OPTIONS_H
-#define __CVC4__OPTIONS__OPTIONS_H
+#ifndef CVC4__OPTIONS__OPTIONS_H
+#define CVC4__OPTIONS__OPTIONS_H
 
 #include <fstream>
 #include <ostream>
@@ -26,7 +26,6 @@
 
 #include "base/listener.h"
 #include "base/modal_exception.h"
-#include "base/tls.h"
 #include "options/argument_extender.h"
 #include "options/language.h"
 #include "options/option_exception.h"
@@ -34,12 +33,16 @@
 
 namespace CVC4 {
 
+namespace api {
+class Solver;
+}
 namespace options {
   struct OptionsHolder;
   class OptionsHandler;
 }/* CVC4::options namespace */
 
 class CVC4_PUBLIC Options {
+  friend api::Solver;
   /** The struct that holds all option values. */
   options::OptionsHolder* d_holder;
 
@@ -47,10 +50,7 @@ class CVC4_PUBLIC Options {
   options::OptionsHandler* d_handler;
 
   /** The current Options in effect */
-  static CVC4_THREAD_LOCAL Options* s_current;
-
-  /** Listeners for options::forceLogicString being set. */
-  ListenerCollection d_forceLogicListeners;
+  static thread_local Options* s_current;
 
   /** Listeners for notifyBeforeSearch. */
   ListenerCollection d_beforeSearchListeners;
@@ -114,13 +114,13 @@ class CVC4_PUBLIC Options {
    * Options cannot be copied as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options(const Options& options) CVC4_UNDEFINED;
+  Options(const Options& options) = delete;
 
   /**
    * Options cannot be assigned as they are given an explicit list of
    * Listeners to respond to.
    */
-  Options& operator=(const Options& options) CVC4_UNDEFINED;
+  Options& operator=(const Options& options) = delete;
 
   static std::string formatThreadOptionException(const std::string& option);
 
@@ -197,8 +197,8 @@ public:
   InputLanguage getInputLanguage() const;
   InstFormatMode getInstFormatMode() const;
   OutputLanguage getOutputLanguage() const;
+  bool getUfHo() const;
   bool getCheckProofs() const;
-  bool getContinuedExecution() const;
   bool getDumpInstantiations() const;
   bool getDumpModels() const;
   bool getDumpProofs() const;
@@ -228,9 +228,6 @@ public:
   bool getVersion() const;
   bool getWaitToJoin() const;
   const std::string& getForceLogicString() const;
-  const std::vector<std::string>& getThreadArgv() const;
-  int getSharingFilterByLength() const;
-  int getThreadId() const;
   int getVerbosity() const;
   std::istream* getIn() const;
   std::ostream* getErr();
@@ -239,17 +236,12 @@ public:
   std::string getBinaryName() const;
   std::string getReplayInputFilename() const;
   unsigned getParseStep() const;
-  unsigned getThreadStackSize() const;
-  unsigned getThreads() const;
-
 
   // TODO: Document these.
   void setInputLanguage(InputLanguage);
   void setInteractive(bool);
   void setOut(std::ostream*);
   void setOutputLanguage(OutputLanguage);
-  void setSharingFilterByLength(int length);
-  void setThreadId(int);
 
   bool wasSetByUserCeGuidedInst() const;
   bool wasSetByUserDumpSynth() const;
@@ -257,13 +249,9 @@ public:
   bool wasSetByUserForceLogicString() const;
   bool wasSetByUserIncrementalSolving() const;
   bool wasSetByUserInteractive() const;
-  bool wasSetByUserThreadStackSize() const;
-  bool wasSetByUserThreads() const;
 
   // Static accessor functions.
   // TODO: Document these.
-  static int currentGetSharingFilterByLength();
-  static int currentGetThreadId();
   static std::ostream* currentGetOut();
 
   /**
@@ -348,19 +336,6 @@ public:
   ListenerCollection::Registration* registerBeforeSearchListener(
       Listener* listener);
 
-
-  /**
-   * Registers a listener for options::forceLogic being set.
-   *
-   * If notifyIfSet is true, this calls notify on the listener
-   * if the option was set by the user.
-   *
-   * The memory for the Registration is controlled by the user and must
-   * be destroyed before the Options object is.
-   */
-  ListenerCollection::Registration* registerForceLogicListener(
-      Listener* listener, bool notifyIfSet);
-
   /**
    * Registers a listener for options::tlimit being set.
    *
@@ -557,4 +532,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__OPTIONS__OPTIONS_H */
+#endif /* CVC4__OPTIONS__OPTIONS_H */