1 /********************* */ 2 /*! \file lemma_channels.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Tim King, Andres Noetzli 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS 8 ** in the top-level source directory) and their institutional affiliations. 9 ** All rights reserved. See the file COPYING in the top-level source 10 ** directory for licensing information.\endverbatim 11 ** 12 ** \brief LemmaChannels is a light container for a pair of input and output 13 ** lemma channels. 14 ** 15 ** LemmaChannels is a light container for a pair of input and output 16 ** lemma channels. These contain paramaters for the infrequently 17 ** used Portfolio mode. There should be exactly one of these per SmtEngine 18 ** with the same lifetime as the SmtEngine. The user directly passes these as 19 ** pointers and is resonsible for cleaning up the memory. 20 ** 21 ** Basically, the problem this class is solving is that previously these were 22 ** using smt_options.h and the Options class as globals for these same 23 ** datastructures. 24 **/ 25 26 #include "cvc4_public.h" 27 28 #ifndef __CVC4__SMT_UTIL__LEMMA_CHANNELS_H 29 #define __CVC4__SMT_UTIL__LEMMA_CHANNELS_H 30 31 #include <iosfwd> 32 #include <string> 33 #include <utility> 34 35 #include "options/option_exception.h" 36 #include "smt_util/lemma_input_channel.h" 37 #include "smt_util/lemma_output_channel.h" 38 39 namespace CVC4 { 40 41 /** 42 * LemmaChannels is a wrapper around two pointers: 43 * - getLemmaInputChannel() 44 * - getLemmaOutputChannel() 45 * 46 * The user can directly set these and is responsible for handling the 47 * memory for these. These datastructures are used for Portfolio mode. 48 */ 49 class CVC4_PUBLIC LemmaChannels { 50 public: 51 /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */ 52 LemmaChannels(); 53 ~LemmaChannels(); 54 55 void setLemmaInputChannel(LemmaInputChannel* in); getLemmaInputChannel()56 LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; } 57 58 void setLemmaOutputChannel(LemmaOutputChannel* out); getLemmaOutputChannel()59 LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; } 60 61 private: 62 // Disable copy constructor. 63 LemmaChannels(const LemmaChannels&) = delete; 64 65 // Disable assignment operator. 66 LemmaChannels& operator=(const LemmaChannels&) = delete; 67 68 /** This captures the old options::lemmaInputChannel .*/ 69 LemmaInputChannel* d_lemmaInputChannel; 70 71 /** This captures the old options::lemmaOutputChannel .*/ 72 LemmaOutputChannel* d_lemmaOutputChannel; 73 }; /* class LemmaChannels */ 74 75 } /* namespace CVC4 */ 76 77 #endif /* __CVC4__SMT_UTIL__LEMMA_CHANNELS_H */ 78