src/smt/smt_globals.h

   1 /*********************                                                        */
   2 /*! \file smt_globals.h
   3  ** \verbatim
   4  ** Original author: Tim King
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2015  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** \brief SmtGlobals is a light container for psuedo-global datastructures
  13  ** that are set by the user.
  14  **
  15  ** SmtGlobals is a light container for psuedo-global datastructures
  16  ** that are set by the user. These contain paramaters for infrequently
  17  ** used modes: Portfolio and Replay. There should be exactly one of these
  18  ** per SmtEngine with the same lifetime as the SmtEngine.
  19  ** A user directly passes these as pointers and is resonsible for cleaning up
  20  ** the memory.
  21  **
  22  ** Basically, the problem this class is solving is that previously these were
  23  ** using smt_options.h and the Options class as globals for these same
  24  ** datastructures.
  25  **
  26  ** This class is NOT a good long term solution, but is a reasonable stop gap.
  27  **/
  28
  29 #include "cvc4_public.h"
  30
  31 #ifndef __CVC4__SMT__SMT_GLOBALS_H
  32 #define __CVC4__SMT__SMT_GLOBALS_H
  33
  34 #include <iosfwd>
  35 #include <string>
  36 #include <utility>
  37
  38 #include "expr/expr_stream.h"
  39 #include "options/option_exception.h"
  40 #include "smt_util/lemma_input_channel.h"
  41 #include "smt_util/lemma_output_channel.h"
  42
  43 namespace CVC4 {
  44
  45 /**
  46  * SmtGlobals is a wrapper around 4 pointers:
  47  * - getReplayLog()
  48  * - getReplayStream()
  49  * - getLemmaInputChannel()
  50  * - getLemmaOutputChannel()
  51  *
  52  * The user can directly set these and is responsible for handling the
  53  * memory for these. These datastructures are used for the Replay and Portfolio
  54  * modes.
  55  */
  56 class CVC4_PUBLIC SmtGlobals {
  57  public:
  58   /** Creates an empty SmtGlobals with all 4 pointers initially NULL. */
  59   SmtGlobals();
  60   ~SmtGlobals();
  61
  62   /** This setsReplayLog based on --replay-log */
  63   void parseReplayLog(std::string optarg) throw (OptionException);
  64   void setReplayLog(std::ostream*);
  65   std::ostream* getReplayLog() { return d_replayLog; }
  66
  67   void setReplayStream(ExprStream* stream);
  68   ExprStream* getReplayStream() { return d_replayStream; }
  69
  70   void setLemmaInputChannel(LemmaInputChannel* in);
  71   LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; }
  72
  73   void setLemmaOutputChannel(LemmaOutputChannel* out);
  74   LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; }
  75
  76  private:
  77   // Disable copy constructor.
  78   SmtGlobals(const SmtGlobals&) CVC4_UNDEFINED;
  79
  80   // Disable assignment operator.
  81   SmtGlobals& operator=(const SmtGlobals&) CVC4_UNDEFINED;
  82
  83   static std::pair<bool, std::ostream*>
  84       checkReplayLogFilename(std::string optarg) throw (OptionException);
  85
  86   /**
  87    * d_gcReplayLog is true iff d_replayLog was allocated by parseReplayLog.
  88    */
  89   bool d_gcReplayLog;
  90
  91   /** This captures the old options::replayLog .*/
  92   std::ostream* d_replayLog;
  93
  94   /** This captures the old options::replayStream .*/
  95   ExprStream* d_replayStream;
  96
  97   /** This captures the old options::lemmaInputChannel .*/
  98   LemmaInputChannel* d_lemmaInputChannel;
  99
 100   /** This captures the old options::lemmaOutputChannel .*/
 101   LemmaOutputChannel* d_lemmaOutputChannel;
 102 }; /* class SmtGlobals */
 103
 104 } /* namespace CVC4 */
 105
 106 #endif /* __CVC4__SMT__SMT_GLOBALS_H */