summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/cnf_stream.cpp30
-rw-r--r--src/prop/cnf_stream.h17
-rw-r--r--src/prop/prop_engine.cpp34
-rw-r--r--src/prop/prop_engine.h24
4 files changed, 70 insertions, 35 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 7df5fb492..1d622cd1b 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -42,10 +42,14 @@ using namespace CVC4::kind;
namespace CVC4 {
namespace prop {
-CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
- context::Context* context, bool fullLitToNodeMap,
+CnfStream::CnfStream(Environment* env,
+ SatSolver* satSolver,
+ Registrar* registrar,
+ context::Context* context,
+ bool fullLitToNodeMap,
std::string name)
- : d_satSolver(satSolver),
+ : d_env(env),
+ d_satSolver(satSolver),
d_booleanVariables(context),
d_nodeToLiteralMap(context),
d_literalToNodeMap(context),
@@ -54,13 +58,17 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
d_registrar(registrar),
d_name(name),
d_cnfProof(NULL),
- d_removable(false) {
+ d_removable(false)
+{
}
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
+TseitinCnfStream::TseitinCnfStream(Environment* env,
+ SatSolver* satSolver,
+ Registrar* registrar,
context::Context* context,
- bool fullLitToNodeMap, std::string name)
- : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name)
+ bool fullLitToNodeMap,
+ std::string name)
+ : CnfStream(env, satSolver, registrar, context, fullLitToNodeMap, name)
{}
void CnfStream::assertClause(TNode node, SatClause& c) {
@@ -155,8 +163,8 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
n = n[0];
}
- if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
- !n.isVar() ) {
+ if (d_env->theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
+ {
// If we were called with something other than a theory atom (or
// Boolean variable), we get a SatLiteral that is definitionally
// equal to it.
@@ -166,7 +174,9 @@ void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
// These may already exist
d_literalToNodeMap.insert_safe(lit, n);
d_literalToNodeMap.insert_safe(~lit, n.notNode());
- } else {
+ }
+ else
+ {
// We have a theory atom or variable.
lit = convertAtom(n, noPreregistration);
}
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a9b786615..3a4cfe209 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -31,6 +31,7 @@
#include "proof/proof_manager.h"
#include "prop/registrar.h"
#include "prop/theory_proxy.h"
+#include "smt/environment.h"
#include "smt_util/lemma_channels.h"
namespace CVC4 {
@@ -54,6 +55,8 @@ class CnfStream {
NodeToLiteralMap;
protected:
+ Environment* d_env;
+
/** The SAT solver we will be using */
SatSolver* d_satSolver;
@@ -171,8 +174,11 @@ class CnfStream {
* @param name string identifier to distinguish between different instances
* even for non-theory literals.
*/
- CnfStream(SatSolver* satSolver, Registrar* registrar,
- context::Context* context, bool fullLitToNodeMap = false,
+ CnfStream(Environment* env,
+ SatSolver* satSolver,
+ Registrar* registrar,
+ context::Context* context,
+ bool fullLitToNodeMap = false,
std::string name = "");
/**
@@ -257,8 +263,11 @@ class TseitinCnfStream : public CnfStream {
* @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
* even for non-theory literals
*/
- TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
- context::Context* context, bool fullLitToNodeMap = false,
+ TseitinCnfStream(Environment* env,
+ SatSolver* satSolver,
+ Registrar* registrar,
+ context::Context* context,
+ bool fullLitToNodeMap = false,
std::string name = "");
/**
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 8a0cc9f15..abb90e569 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -74,19 +74,25 @@ 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(Environment* env,
+ TheoryEngine* te,
+ DecisionEngine* de,
+ Context* satContext,
+ Context* userContext,
+ std::ostream* replayLog,
+ ExprStream* replayStream,
+ LemmaChannels* channels)
+ : d_env(env),
+ 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;
@@ -95,7 +101,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
d_registrar = new theory::TheoryRegistrar(d_theoryEngine);
d_cnfStream = new CVC4::prop::TseitinCnfStream(
- d_satSolver, d_registrar, userContext, true);
+ d_env, d_satSolver, d_registrar, userContext, true);
d_theoryProxy = new TheoryProxy(
this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, replayLog,
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index aaa65b85a..735c82bde 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -28,6 +28,7 @@
#include "expr/node.h"
#include "options/options.h"
#include "proof/proof_manager.h"
+#include "smt/environment.h"
#include "smt_util/lemma_channels.h"
#include "util/result.h"
#include "util/unsafe_interrupt_exception.h"
@@ -54,6 +55,7 @@ class PropEngine;
* solving the SAT problem and conversion to CNF (via the CnfStream).
*/
class PropEngine {
+ Environment* d_env;
/**
* Indicates that the SAT solver is currently solving something and we should
@@ -93,14 +95,18 @@ 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(Environment* env,
+ TheoryEngine*,
+ DecisionEngine*,
+ context::Context* satContext,
+ context::Context* userContext,
+ std::ostream* replayLog,
+ ExprStream* replayStream,
+ LemmaChannels* channels);
/**
* Destructor.
@@ -114,7 +120,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.
@@ -134,7 +140,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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback