diff options
Diffstat (limited to 'src/smt/smt_globals.h')
-rw-r--r-- | src/smt/smt_globals.h | 106 |
1 files changed, 0 insertions, 106 deletions
diff --git a/src/smt/smt_globals.h b/src/smt/smt_globals.h deleted file mode 100644 index 00b90a703..000000000 --- a/src/smt/smt_globals.h +++ /dev/null @@ -1,106 +0,0 @@ -/********************* */ -/*! \file smt_globals.h - ** \verbatim - ** Original author: Tim King - ** Major contributors: none - ** Minor contributors (to current version): none - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2015 New York University and The University of Iowa - ** See the file COPYING in the top-level source directory for licensing - ** information.\endverbatim - ** - ** \brief SmtGlobals is a light container for psuedo-global datastructures - ** that are set by the user. - ** - ** SmtGlobals is a light container for psuedo-global datastructures - ** that are set by the user. These contain paramaters for infrequently - ** used modes: Portfolio and Replay. There should be exactly one of these - ** per SmtEngine with the same lifetime as the SmtEngine. - ** A user directly passes these as pointers and is resonsible for cleaning up - ** the memory. - ** - ** Basically, the problem this class is solving is that previously these were - ** using smt_options.h and the Options class as globals for these same - ** datastructures. - ** - ** This class is NOT a good long term solution, but is a reasonable stop gap. - **/ - -#include "cvc4_public.h" - -#ifndef __CVC4__SMT__SMT_GLOBALS_H -#define __CVC4__SMT__SMT_GLOBALS_H - -#include <iosfwd> -#include <string> -#include <utility> - -#include "expr/expr_stream.h" -#include "options/option_exception.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" - -namespace CVC4 { - -/** - * SmtGlobals is a wrapper around 4 pointers: - * - getReplayLog() - * - getReplayStream() - * - getLemmaInputChannel() - * - getLemmaOutputChannel() - * - * The user can directly set these and is responsible for handling the - * memory for these. These datastructures are used for the Replay and Portfolio - * modes. - */ -class CVC4_PUBLIC SmtGlobals { - public: - /** Creates an empty SmtGlobals with all 4 pointers initially NULL. */ - SmtGlobals(); - ~SmtGlobals(); - - /** This setsReplayLog based on --replay-log */ - void parseReplayLog(std::string optarg) throw (OptionException); - void setReplayLog(std::ostream*); - std::ostream* getReplayLog() { return d_replayLog; } - - void setReplayStream(ExprStream* stream); - ExprStream* getReplayStream() { return d_replayStream; } - - void setLemmaInputChannel(LemmaInputChannel* in); - LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; } - - void setLemmaOutputChannel(LemmaOutputChannel* out); - LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; } - - private: - // Disable copy constructor. - SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED; - - // Disable assignment operator. - SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED; - - static std::pair<bool, std::ostream*> - checkReplayLogFilename(std::string optarg) throw (OptionException); - - /** - * d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog. - */ - bool d_gcReplayLog; - - /** This captures the old options::replayLog .*/ - std::ostream* d_replayLog; - - /** This captures the old options::replayStream .*/ - ExprStream* d_replayStream; - - /** This captures the old options::lemmaInputChannel .*/ - LemmaInputChannel* d_lemmaInputChannel; - - /** This captures the old options::lemmaOutputChannel .*/ - LemmaOutputChannel* d_lemmaOutputChannel; -}; /* class SmtGlobals */ - -} /* namespace CVC4 */ - -#endif /* __CVC4__SMT__SMT_GLOBALS_H */ |