diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-02-26 00:08:20 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-26 00:08:20 -0800 |
commit | 50c31e61ab240ccd551a0aea732f8b9a88d7fb32 (patch) | |
tree | 30531d1f4813ed399209d198ca1eb75ac6f9dc30 /src/smt_util | |
parent | b28ff31b6713791f27b4860f439aaa3f63aab9d7 (diff) |
Remove portfolio leftovers (#3821)
Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.
Diffstat (limited to 'src/smt_util')
-rw-r--r-- | src/smt_util/lemma_channels.cpp | 54 | ||||
-rw-r--r-- | src/smt_util/lemma_channels.h | 77 | ||||
-rw-r--r-- | src/smt_util/lemma_input_channel.h | 38 | ||||
-rw-r--r-- | src/smt_util/lemma_output_channel.h | 45 |
4 files changed, 0 insertions, 214 deletions
diff --git a/src/smt_util/lemma_channels.cpp b/src/smt_util/lemma_channels.cpp deleted file mode 100644 index d65a2596e..000000000 --- a/src/smt_util/lemma_channels.cpp +++ /dev/null @@ -1,54 +0,0 @@ -/********************* */ -/*! \file lemma_channels.cpp - ** \verbatim - ** Top contributors (to current version): - ** Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief This class is a light container for globals that used to live - ** in options. This is NOT a good long term solution, but is a reasonable - ** stop gap. - ** - ** This class is a light container for globals that used to live - ** in options. This is NOT a good long term solution, but is a reasonable - ** stop gap. - **/ - -#include "smt_util/lemma_channels.h" - -#include <cerrno> -#include <iostream> -#include <string> -#include <utility> - -#include "cvc4autoconfig.h" // Needed for CVC4_REPLAY -#include "expr/expr_stream.h" -#include "options/open_ostream.h" -#include "options/option_exception.h" -#include "options/parser_options.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" - -namespace CVC4 { - -LemmaChannels::LemmaChannels() - : d_lemmaInputChannel(NULL) - , d_lemmaOutputChannel(NULL) -{} - -LemmaChannels::~LemmaChannels(){} - -void LemmaChannels::setLemmaInputChannel(LemmaInputChannel* in) { - d_lemmaInputChannel = in; -} - -void LemmaChannels::setLemmaOutputChannel(LemmaOutputChannel* out) { - d_lemmaOutputChannel = out; -} - - -} /* namespace CVC4 */ diff --git a/src/smt_util/lemma_channels.h b/src/smt_util/lemma_channels.h deleted file mode 100644 index 40c58dd24..000000000 --- a/src/smt_util/lemma_channels.h +++ /dev/null @@ -1,77 +0,0 @@ -/********************* */ -/*! \file lemma_channels.h - ** \verbatim - ** Top contributors (to current version): - ** Tim King, Andres Noetzli - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief LemmaChannels is a light container for a pair of input and output - ** lemma channels. - ** - ** LemmaChannels is a light container for a pair of input and output - ** lemma channels. These contain paramaters for the infrequently - ** used Portfolio mode. There should be exactly one of these per SmtEngine - ** with the same lifetime as the SmtEngine. The 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. - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__SMT_UTIL__LEMMA_CHANNELS_H -#define CVC4__SMT_UTIL__LEMMA_CHANNELS_H - -#include <iosfwd> -#include <string> -#include <utility> - -#include "options/option_exception.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" - -namespace CVC4 { - -/** - * LemmaChannels is a wrapper around two pointers: - * - getLemmaInputChannel() - * - getLemmaOutputChannel() - * - * The user can directly set these and is responsible for handling the - * memory for these. These datastructures are used for Portfolio mode. - */ -class CVC4_PUBLIC LemmaChannels { - public: - /** Creates an empty LemmaChannels with all 4 pointers initially NULL. */ - LemmaChannels(); - ~LemmaChannels(); - - void setLemmaInputChannel(LemmaInputChannel* in); - LemmaInputChannel* getLemmaInputChannel() { return d_lemmaInputChannel; } - - void setLemmaOutputChannel(LemmaOutputChannel* out); - LemmaOutputChannel* getLemmaOutputChannel() { return d_lemmaOutputChannel; } - - private: - // Disable copy constructor. - LemmaChannels(const LemmaChannels&) = delete; - - // Disable assignment operator. - LemmaChannels& operator=(const LemmaChannels&) = delete; - - /** This captures the old options::lemmaInputChannel .*/ - LemmaInputChannel* d_lemmaInputChannel; - - /** This captures the old options::lemmaOutputChannel .*/ - LemmaOutputChannel* d_lemmaOutputChannel; -}; /* class LemmaChannels */ - -} /* namespace CVC4 */ - -#endif /* CVC4__SMT_UTIL__LEMMA_CHANNELS_H */ diff --git a/src/smt_util/lemma_input_channel.h b/src/smt_util/lemma_input_channel.h deleted file mode 100644 index 16bb457c8..000000000 --- a/src/smt_util/lemma_input_channel.h +++ /dev/null @@ -1,38 +0,0 @@ -/********************* */ -/*! \file lemma_input_channel.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__LEMMA_INPUT_CHANNEL_H -#define CVC4__LEMMA_INPUT_CHANNEL_H - -#include "expr/expr.h" - -namespace CVC4 { - -class CVC4_PUBLIC LemmaInputChannel { -public: - virtual ~LemmaInputChannel() {} - - virtual bool hasNewLemma() = 0; - virtual Expr getNewLemma() = 0; - -};/* class LemmaOutputChannel */ - -}/* CVC4 namespace */ - -#endif /* CVC4__LEMMA_INPUT_CHANNEL_H */ diff --git a/src/smt_util/lemma_output_channel.h b/src/smt_util/lemma_output_channel.h deleted file mode 100644 index e5c5cffe2..000000000 --- a/src/smt_util/lemma_output_channel.h +++ /dev/null @@ -1,45 +0,0 @@ -/********************* */ -/*! \file lemma_output_channel.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King - ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS - ** in the top-level source directory) and their institutional affiliations. - ** All rights reserved. See the file COPYING in the top-level source - ** directory for licensing information.\endverbatim - ** - ** \brief Mechanism for communication about new lemmas - ** - ** This file defines an interface for use by the theory and propositional - ** engines to communicate new lemmas to the "outside world". - **/ - -#include "cvc4_public.h" - -#ifndef CVC4__LEMMA_OUTPUT_CHANNEL_H -#define CVC4__LEMMA_OUTPUT_CHANNEL_H - -#include "expr/expr.h" - -namespace CVC4 { - -/** - * This interface describes a mechanism for the propositional and theory - * engines to communicate with the "outside world" about new lemmas being - * discovered. - */ -class CVC4_PUBLIC LemmaOutputChannel { -public: - virtual ~LemmaOutputChannel() {} - - /** - * Notifies this output channel that there's a new lemma. - * The lemma may or may not be in CNF. - */ - virtual void notifyNewLemma(Expr lemma) = 0; -};/* class LemmaOutputChannel */ - -}/* CVC4 namespace */ - -#endif /* CVC4__LEMMA_OUTPUT_CHANNEL_H */ |