summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-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
5 files changed, 43 insertions, 114 deletions
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback