diff options
Diffstat (limited to 'src/smt/smt_globals.h')
-rw-r--r-- | src/smt/smt_globals.h | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/src/smt/smt_globals.h b/src/smt/smt_globals.h new file mode 100644 index 000000000..00b90a703 --- /dev/null +++ b/src/smt/smt_globals.h @@ -0,0 +1,106 @@ +/********************* */ +/*! \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 */ |