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