diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/CMakeLists.txt | 10 | ||||
-rw-r--r-- | src/bindings/java/CMakeLists.txt | 1 | ||||
-rw-r--r-- | src/main/command_executor.h | 1 | ||||
-rw-r--r-- | src/options/main_options.toml | 28 | ||||
-rw-r--r-- | src/options/options.h | 3 | ||||
-rw-r--r-- | src/options/options_public_functions.cpp | 12 | ||||
-rw-r--r-- | src/prop/cnf_stream.h | 1 | ||||
-rw-r--r-- | src/prop/prop_engine.cpp | 39 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 24 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 67 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 26 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 18 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 6 | ||||
-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 | ||||
-rw-r--r-- | src/theory/theory_engine.cpp | 10 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 25 |
19 files changed, 64 insertions, 421 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4567f45be..e8c38f39d 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -253,10 +253,6 @@ libcvc4_add_sources( smt/update_ostream.h smt_util/boolean_simplification.cpp smt_util/boolean_simplification.h - smt_util/lemma_channels.cpp - smt_util/lemma_channels.h - smt_util/lemma_input_channel.h - smt_util/lemma_output_channel.h smt_util/nary_builder.cpp smt_util/nary_builder.h smt_util/node_visitor.h @@ -945,12 +941,6 @@ install(FILES DESTINATION ${INCLUDE_INSTALL_DIR}/cvc4/smt) install(FILES - smt_util/lemma_channels.h - smt_util/lemma_input_channel.h - smt_util/lemma_output_channel.h - DESTINATION - ${INCLUDE_INSTALL_DIR}/cvc4/smt_util) -install(FILES theory/logic_info.h theory/theory_id.h DESTINATION diff --git a/src/bindings/java/CMakeLists.txt b/src/bindings/java/CMakeLists.txt index b8452d1aa..344387ed9 100644 --- a/src/bindings/java/CMakeLists.txt +++ b/src/bindings/java/CMakeLists.txt @@ -122,7 +122,6 @@ set(gen_java_files ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Model.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__Printer.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_CVC4__options__InstFormatMode.java - ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_LemmaChannels.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_Listener.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_ListenerCollection__Registration.java ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_MaybeT_CVC4__Rational_t.java diff --git a/src/main/command_executor.h b/src/main/command_executor.h index c71f4d7a5..3688f592f 100644 --- a/src/main/command_executor.h +++ b/src/main/command_executor.h @@ -85,7 +85,6 @@ public: static void printStatsFilterZeros(std::ostream& out, const std::string& statsString); - LemmaChannels* channels() { return d_smtEngine->channels(); } void flushOutputStreams(); void setReplayStream(ExprStream* replayStream); diff --git a/src/options/main_options.toml b/src/options/main_options.toml index 84ac7d955..f373e9836 100644 --- a/src/options/main_options.toml +++ b/src/options/main_options.toml @@ -79,25 +79,6 @@ header = "options/main_options.h" help = "do not run destructors at exit; default on except in debug builds" [[option]] - name = "fallbackSequential" - category = "regular" - long = "fallback-sequential" - type = "bool" - default = "false" - read_only = true - help = "Switch to sequential mode (instead of printing an error) if it can't be solved in portfolio mode" - -[[option]] - name = "incrementalParallel" - category = "regular" - long = "incremental-parallel" - type = "bool" - default = "false" - links = ["--incremental"] - read_only = true - help = "Use parallel solver even in incremental mode (may print 'unknown's at times)" - -[[option]] name = "interactive" category = "regular" long = "interactive" @@ -135,12 +116,3 @@ header = "options/main_options.h" default = "0" read_only = true help = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries" - -[[option]] - name = "waitToJoin" - category = "expert" - long = "wait-to-join" - type = "bool" - default = "true" - read_only = true - help = "wait for other threads to join before quitting" diff --git a/src/options/options.h b/src/options/options.h index 1493ceac9..fcf99134d 100644 --- a/src/options/options.h +++ b/src/options/options.h @@ -205,11 +205,9 @@ public: bool getDumpSynth() const; bool getDumpUnsatCores() const; bool getEarlyExit() const; - bool getFallbackSequential() const; bool getFilesystemAccess() const; bool getForceNoLimitCpuWhileDump() const; bool getHelp() const; - bool getIncrementalParallel() const; bool getIncrementalSolving() const; bool getInteractive() const; bool getInteractivePrompt() const; @@ -226,7 +224,6 @@ public: bool getStrictParsing() const; int getTearDownIncremental() const; bool getVersion() const; - bool getWaitToJoin() const; const std::string& getForceLogicString() const; int getVerbosity() const; std::istream* getIn() const; diff --git a/src/options/options_public_functions.cpp b/src/options/options_public_functions.cpp index 6548150aa..a556f2152 100644 --- a/src/options/options_public_functions.cpp +++ b/src/options/options_public_functions.cpp @@ -82,10 +82,6 @@ bool Options::getEarlyExit() const{ return (*this)[options::earlyExit]; } -bool Options::getFallbackSequential() const{ - return (*this)[options::fallbackSequential]; -} - bool Options::getFilesystemAccess() const{ return (*this)[options::filesystemAccess]; } @@ -98,10 +94,6 @@ bool Options::getHelp() const{ return (*this)[options::help]; } -bool Options::getIncrementalParallel() const{ - return (*this)[options::incrementalParallel]; -} - bool Options::getIncrementalSolving() const{ return (*this)[options::incrementalSolving]; } @@ -166,10 +158,6 @@ bool Options::getVersion() const{ return (*this)[options::version]; } -bool Options::getWaitToJoin() const{ - return (*this)[options::waitToJoin]; -} - const std::string& Options::getForceLogicString() const{ return (*this)[options::forceLogicString]; } diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index a9b786615..6b528bb81 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -31,7 +31,6 @@ #include "proof/proof_manager.h" #include "prop/registrar.h" #include "prop/theory_proxy.h" -#include "smt_util/lemma_channels.h" namespace CVC4 { diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index bac584236..05704c0fa 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -74,19 +74,22 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, - Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels) : - d_inCheckSat(false), - d_theoryEngine(te), - d_decisionEngine(de), - d_context(satContext), - d_theoryProxy(NULL), - d_satSolver(NULL), - d_registrar(NULL), - d_cnfStream(NULL), - d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) +PropEngine::PropEngine(TheoryEngine* te, + DecisionEngine* de, + Context* satContext, + Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream) + : d_inCheckSat(false), + d_theoryEngine(te), + d_decisionEngine(de), + d_context(satContext), + d_theoryProxy(NULL), + d_satSolver(NULL), + d_registrar(NULL), + d_cnfStream(NULL), + d_interrupted(false), + d_resourceManager(NodeManager::currentResourceManager()) { Debug("prop") << "Constructing the PropEngine" << endl; @@ -97,9 +100,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_cnfStream = new CVC4::prop::TseitinCnfStream( d_satSolver, d_registrar, userContext, true); - d_theoryProxy = new TheoryProxy( - this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog, - replayStream, channels); + d_theoryProxy = new TheoryProxy(this, + d_theoryEngine, + d_decisionEngine, + d_context, + d_cnfStream, + replayLog, + replayStream); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index efbd82947..42b3ce65f 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -28,7 +28,6 @@ #include "expr/node.h" #include "options/options.h" #include "proof/proof_manager.h" -#include "smt_util/lemma_channels.h" #include "util/resource_manager.h" #include "util/result.h" #include "util/unsafe_interrupt_exception.h" @@ -94,14 +93,16 @@ class PropEngine { /** Dump out the satisfying assignment (after SAT result) */ void printSatisfyingAssignment(); -public: - + public: /** * Create a PropEngine with a particular decision and theory engine. */ - PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, - context::Context* userContext, std::ostream* replayLog, - ExprStream* replayStream, LemmaChannels* channels); + PropEngine(TheoryEngine*, + DecisionEngine*, + context::Context* satContext, + context::Context* userContext, + std::ostream* replayLog, + ExprStream* replayStream); /** * Destructor. @@ -115,7 +116,7 @@ public: * PropEngine and Theory). For now, there's nothing to do here in * the PropEngine. */ - void shutdown() { } + void shutdown() {} /** * Converts the given formula to CNF and assert the CNF to the SAT solver. @@ -135,7 +136,11 @@ public: * @param removable whether this lemma can be quietly removed based * on an activity heuristic (or not) */ - void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null()); + void assertLemma(TNode node, + bool negated, + bool removable, + ProofRule rule, + TNode from = TNode::null()); /** * If ever n is decided upon, it must be in the given phase. This @@ -243,8 +248,7 @@ public: */ bool properExplanation(TNode node, TNode expl) const; -};/* class PropEngine */ - +}; /* class PropEngine */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index cf7c9f0d9..557dcc413 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -25,8 +25,6 @@ #include "proof/cnf_proof.h" #include "smt/command.h" #include "smt/smt_statistics_registry.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" #include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/statistics_registry.h" @@ -41,13 +39,11 @@ TheoryProxy::TheoryProxy(PropEngine* propEngine, context::Context* context, CnfStream* cnfStream, std::ostream* replayLog, - ExprStream* replayStream, - LemmaChannels* channels) + ExprStream* replayStream) : d_propEngine(propEngine), d_cnfStream(cnfStream), d_decisionEngine(decisionEngine), d_theoryEngine(theoryEngine), - d_channels(channels), d_replayLog(replayLog), d_replayStream(replayStream), d_queue(context), @@ -61,17 +57,6 @@ TheoryProxy::~TheoryProxy() { smtStatisticsRegistry()->unregisterStat(&d_replayedDecisions); } -/** The lemma input channel we are using. */ -LemmaInputChannel* TheoryProxy::inputChannel() { - return d_channels->getLemmaInputChannel(); -} - -/** The lemma output channel we are using. */ -LemmaOutputChannel* TheoryProxy::outputChannel() { - return d_channels->getLemmaOutputChannel(); -} - - void TheoryProxy::variableNotify(SatVariable var) { d_theoryEngine->preRegister(getNode(SatLiteral(var))); } @@ -163,56 +148,6 @@ TNode TheoryProxy::getNode(SatLiteral lit) { void TheoryProxy::notifyRestart() { d_propEngine->spendResource(ResourceManager::Resource::RestartStep); d_theoryEngine->notifyRestart(); - - static uint32_t lemmaCount = 0; - - if(inputChannel() != NULL) { - while(inputChannel()->hasNewLemma()) { - Debug("shared") << "shared" << std::endl; - Expr lemma = inputChannel()->getNewLemma(); - Node asNode = lemma.getNode(); - asNode = theory::Rewriter::rewrite(asNode); - - if(d_shared.find(asNode) == d_shared.end()) { - d_shared.insert(asNode); - if(asNode.getKind() == kind::OR) { - ++lemmaCount; - if(lemmaCount % 1 == 0) { - Debug("shared") << "=) " << asNode << std::endl; - } - - d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID); - } else { - Debug("shared") << "=(" << asNode << std::endl; - } - } else { - Debug("shared") <<"drop shared " << asNode << std::endl; - } - } - } -} - -void TheoryProxy::notifyNewLemma(SatClause& lemma) { - Assert(lemma.size() > 0); - if(outputChannel() != NULL) { - if(lemma.size() == 1) { - // cannot share units yet - //options::lemmaOutputChannel()->notifyNewLemma(d_cnfStream->getNode(lemma[0]).toExpr()); - } else { - NodeBuilder<> b(kind::OR); - for(unsigned i = 0, i_end = lemma.size(); i < i_end; ++i) { - b << d_cnfStream->getNode(lemma[i]); - } - Node n = b; - - if(d_shared.find(n) == d_shared.end()) { - d_shared.insert(n); - outputChannel()->notifyNewLemma(n.toExpr()); - } else { - Debug("shared") <<"drop new " << n << std::endl; - } - } - } } SatLiteral TheoryProxy::getNextReplayDecision() { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index 61c556f34..0d76b473f 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -30,9 +30,6 @@ #include "expr/expr_stream.h" #include "expr/node.h" #include "prop/sat_solver.h" -#include "smt_util/lemma_channels.h" -#include "smt_util/lemma_input_channel.h" -#include "smt_util/lemma_output_channel.h" #include "theory/theory.h" #include "util/resource_manager.h" #include "util/statistics_registry.h" @@ -50,20 +47,19 @@ class CnfStream; /** * The proxy class that allows the SatSolver to communicate with the theories */ -class TheoryProxy { -public: +class TheoryProxy +{ + public: TheoryProxy(PropEngine* propEngine, TheoryEngine* theoryEngine, DecisionEngine* decisionEngine, context::Context* context, CnfStream* cnfStream, std::ostream* replayLog, - ExprStream* replayStream, - LemmaChannels* globals); + ExprStream* replayStream); ~TheoryProxy(); - void theoryCheck(theory::Theory::Effort effort); void explainPropagation(SatLiteral l, SatClause& explanation); @@ -87,8 +83,6 @@ public: void notifyRestart(); - void notifyNewLemma(SatClause& lemma); - SatLiteral getNextReplayDecision(); void logDecision(SatLiteral lit); @@ -117,22 +111,12 @@ public: /** The theory engine we are using. */ TheoryEngine* d_theoryEngine; - - /** Container for inputChannel() and outputChannel(). */ - LemmaChannels* d_channels; - /** Stream on which to log replay events. */ std::ostream* d_replayLog; /** Stream for replaying decisions. */ ExprStream* d_replayStream; - /** The lemma input channel we are using. */ - LemmaInputChannel* inputChannel(); - - /** The lemma output channel we are using. */ - LemmaOutputChannel* outputChannel(); - /** Queue of asserted facts */ context::CDQueue<TNode> d_queue; @@ -147,7 +131,7 @@ public: */ IntStat d_replayedDecisions; -};/* class SatSolver */ +}; /* class SatSolver */ }/* CVC4::prop namespace */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2bfb8353f..081e36953 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -877,8 +877,7 @@ SmtEngine::SmtEngine(ExprManager* em) d_replayStream(NULL), d_private(NULL), d_statisticsRegistry(NULL), - d_stats(NULL), - d_channels(new LemmaChannels()) + d_stats(NULL) { SmtScope smts(this); d_originalOptions.copyValues(em->getOptions()); @@ -913,8 +912,7 @@ void SmtEngine::finishInit() d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, - const_cast<const LogicInfo&>(d_logic), - d_channels); + const_cast<const LogicInfo&>(d_logic)); // Add the theories for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) { @@ -941,9 +939,12 @@ void SmtEngine::finishInit() d_decisionEngine->init(); // enable appropriate strategies Trace("smt-debug") << "Making prop engine..." << std::endl; - d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, - d_userContext, d_private->getReplayLog(), - d_replayStream, d_channels); + d_propEngine = new PropEngine(d_theoryEngine, + d_decisionEngine, + d_context, + d_userContext, + d_private->getReplayLog(), + d_replayStream); Trace("smt-debug") << "Setting up theory engine..." << std::endl; d_theoryEngine->setPropEngine(d_propEngine); @@ -1107,9 +1108,6 @@ SmtEngine::~SmtEngine() delete d_context; d_context = NULL; - delete d_channels; - d_channels = NULL; - } catch(Exception& e) { Warning() << "CVC4 threw an exception during cleanup." << endl << e << endl; diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index a91a3a201..0ef22f353 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -32,7 +32,6 @@ #include "options/options.h" #include "proof/unsat_core.h" #include "smt/logic_exception.h" -#include "smt_util/lemma_channels.h" #include "theory/logic_info.h" #include "util/hash.h" #include "util/proof.h" @@ -798,8 +797,6 @@ class CVC4_PUBLIC SmtEngine */ void beforeSearch(); - LemmaChannels* channels() { return d_channels; } - /** * Expermintal feature: Sets the sequence of decisions. * This currently requires very fine grained knowledge about literal @@ -1243,9 +1240,6 @@ class CVC4_PUBLIC SmtEngine smt::SmtEngineStatistics* d_stats; - /** Container for the lemma input and output channels for this SmtEngine.*/ - LemmaChannels* d_channels; - /*---------------------------- sygus commands ---------------------------*/ /** 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 */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 9ef228865..dec648688 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -37,7 +37,6 @@ #include "proof/theory_proof.h" #include "smt/logic_exception.h" #include "smt/term_formula_removal.h" -#include "smt_util/lemma_output_channel.h" #include "smt_util/node_visitor.h" #include "theory/arith/arith_ite_utils.h" #include "theory/bv/theory_bv_utils.h" @@ -314,8 +313,7 @@ void TheoryEngine::eqNotifyNewClass(TNode t){ TheoryEngine::TheoryEngine(context::Context* context, context::UserContext* userContext, RemoveTermFormulas& iteRemover, - const LogicInfo& logicInfo, - LemmaChannels* channels) + const LogicInfo& logicInfo) : d_propEngine(nullptr), d_decisionEngine(nullptr), d_context(context), @@ -349,7 +347,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_false(), d_interrupted(false), d_resourceManager(NodeManager::currentResourceManager()), - d_channels(channels), d_inPreregister(false), d_factsAsserted(context, false), d_preRegistrationVisitor(this, context), @@ -1867,11 +1864,6 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, << CheckSatCommand(n.toExpr()); } - // Share with other portfolio threads - if(d_channels->getLemmaOutputChannel() != NULL) { - d_channels->getLemmaOutputChannel()->notifyNewLemma(node.toExpr()); - } - AssertionPipeline additionalLemmas; // Run theory preprocessing, maybe diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 0770efc7b..a5631059f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -34,7 +34,6 @@ #include "options/theory_options.h" #include "prop/prop_engine.h" #include "smt/command.h" -#include "smt_util/lemma_channels.h" #include "theory/atom_requests.h" #include "theory/decision_manager.h" #include "theory/interrupted.h" @@ -468,15 +467,12 @@ class TheoryEngine { bool d_interrupted; ResourceManager* d_resourceManager; - /** Container for lemma input and output channels. */ - LemmaChannels* d_channels; - -public: - + public: /** Constructs a theory engine */ - TheoryEngine(context::Context* context, context::UserContext* userContext, - RemoveTermFormulas& iteRemover, const LogicInfo& logic, - LemmaChannels* channels); + TheoryEngine(context::Context* context, + context::UserContext* userContext, + RemoveTermFormulas& iteRemover, + const LogicInfo& logic); /** Destroys a theory engine */ ~TheoryEngine(); @@ -491,12 +487,15 @@ public: * there is another theory it will be deleted. */ template <class TheoryClass> - inline void addTheory(theory::TheoryId theoryId) { + inline void addTheory(theory::TheoryId theoryId) + { Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL); d_theoryOut[theoryId] = new EngineOutputChannel(this, theoryId); - d_theoryTable[theoryId] = - new TheoryClass(d_context, d_userContext, *d_theoryOut[theoryId], - theory::Valuation(this), d_logicInfo); + d_theoryTable[theoryId] = new TheoryClass(d_context, + d_userContext, + *d_theoryOut[theoryId], + theory::Valuation(this), + d_logicInfo); } inline void setPropEngine(prop::PropEngine* propEngine) { |