summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/CMakeLists.txt10
-rw-r--r--src/bindings/java/CMakeLists.txt1
-rw-r--r--src/main/command_executor.h1
-rw-r--r--src/options/main_options.toml28
-rw-r--r--src/options/options.h3
-rw-r--r--src/options/options_public_functions.cpp12
-rw-r--r--src/prop/cnf_stream.h1
-rw-r--r--src/prop/prop_engine.cpp39
-rw-r--r--src/prop/prop_engine.h24
-rw-r--r--src/prop/theory_proxy.cpp67
-rw-r--r--src/prop/theory_proxy.h26
-rw-r--r--src/smt/smt_engine.cpp18
-rw-r--r--src/smt/smt_engine.h6
-rw-r--r--src/smt_util/lemma_channels.cpp54
-rw-r--r--src/smt_util/lemma_channels.h77
-rw-r--r--src/smt_util/lemma_input_channel.h38
-rw-r--r--src/smt_util/lemma_output_channel.h45
-rw-r--r--src/theory/theory_engine.cpp10
-rw-r--r--src/theory/theory_engine.h25
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) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback