summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/decision/decision_engine.cpp16
-rw-r--r--src/decision/decision_engine.h8
-rw-r--r--src/decision/decision_engine_old.cpp11
-rw-r--r--src/decision/decision_engine_old.h4
-rw-r--r--src/decision/decision_strategy.h28
-rw-r--r--src/decision/justification_heuristic.cpp26
-rw-r--r--src/decision/justification_heuristic.h4
-rw-r--r--src/decision/justification_strategy.cpp21
-rw-r--r--src/decision/justification_strategy.h5
-rw-r--r--src/prop/prop_engine.cpp9
-rw-r--r--src/smt/env.cpp4
-rw-r--r--src/smt/env_obj.cpp9
-rw-r--r--src/smt/env_obj.h9
13 files changed, 69 insertions, 85 deletions
diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp
index 5b65951a6..3011ad6ec 100644
--- a/src/decision/decision_engine.cpp
+++ b/src/decision/decision_engine.cpp
@@ -17,16 +17,14 @@
#include "decision/decision_engine_old.h"
#include "options/decision_options.h"
#include "prop/sat_solver.h"
+#include "smt/env.h"
#include "util/resource_manager.h"
namespace cvc5 {
namespace decision {
-DecisionEngine::DecisionEngine(context::Context* c, ResourceManager* rm)
- : d_context(c),
- d_resourceManager(rm),
- d_cnfStream(nullptr),
- d_satSolver(nullptr)
+DecisionEngine::DecisionEngine(Env& env)
+ : EnvObj(env), d_cnfStream(nullptr), d_satSolver(nullptr)
{
}
@@ -38,15 +36,11 @@ void DecisionEngine::finishInit(CDCLTSatSolverInterface* ss, CnfStream* cs)
prop::SatLiteral DecisionEngine::getNext(bool& stopSearch)
{
- d_resourceManager->spendResource(Resource::DecisionStep);
+ resourceManager()->spendResource(Resource::DecisionStep);
return getNextInternal(stopSearch);
}
-DecisionEngineEmpty::DecisionEngineEmpty(context::Context* sc,
- ResourceManager* rm)
- : DecisionEngine(sc, rm)
-{
-}
+DecisionEngineEmpty::DecisionEngineEmpty(Env& env) : DecisionEngine(env) {}
bool DecisionEngineEmpty::isDone() { return false; }
void DecisionEngineEmpty::addAssertion(TNode assertion) {}
void DecisionEngineEmpty::addSkolemDefinition(TNode lem, TNode skolem) {}
diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h
index aa4c43e89..331d6eaca 100644
--- a/src/decision/decision_engine.h
+++ b/src/decision/decision_engine.h
@@ -22,16 +22,16 @@
#include "prop/cnf_stream.h"
#include "prop/sat_solver.h"
#include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
namespace cvc5 {
namespace decision {
-class DecisionEngine
+class DecisionEngine : protected EnvObj
{
public:
/** Constructor */
- DecisionEngine(context::Context* sc,
- ResourceManager* rm);
+ DecisionEngine(Env& env);
virtual ~DecisionEngine() {}
/** Finish initialize */
@@ -86,7 +86,7 @@ class DecisionEngine
class DecisionEngineEmpty : public DecisionEngine
{
public:
- DecisionEngineEmpty(context::Context* sc, ResourceManager* rm);
+ DecisionEngineEmpty(Env& env);
bool isDone() override;
void addAssertion(TNode assertion) override;
void addSkolemDefinition(TNode lem, TNode skolem) override;
diff --git a/src/decision/decision_engine_old.cpp b/src/decision/decision_engine_old.cpp
index 6bfba35ee..c61069cae 100644
--- a/src/decision/decision_engine_old.cpp
+++ b/src/decision/decision_engine_old.cpp
@@ -25,11 +25,9 @@ using namespace std;
namespace cvc5 {
-DecisionEngineOld::DecisionEngineOld(context::Context* sc,
- context::UserContext* uc,
- ResourceManager* rm)
- : DecisionEngine(sc, rm),
- d_result(sc, SAT_VALUE_UNKNOWN),
+DecisionEngineOld::DecisionEngineOld(Env& env)
+ : DecisionEngine(env),
+ d_result(context(), SAT_VALUE_UNKNOWN),
d_engineState(0),
d_enabledITEStrategy(nullptr),
d_decisionStopOnly(options::decisionMode()
@@ -47,8 +45,7 @@ DecisionEngineOld::DecisionEngineOld(context::Context* sc,
if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
{
- d_enabledITEStrategy.reset(
- new decision::JustificationHeuristic(this, uc, sc));
+ d_enabledITEStrategy.reset(new decision::JustificationHeuristic(env, this));
}
}
diff --git a/src/decision/decision_engine_old.h b/src/decision/decision_engine_old.h
index 93f581143..f1a340ca0 100644
--- a/src/decision/decision_engine_old.h
+++ b/src/decision/decision_engine_old.h
@@ -39,9 +39,7 @@ class DecisionEngineOld : public decision::DecisionEngine
// Necessary functions
/** Constructor */
- DecisionEngineOld(context::Context* sc,
- context::UserContext* uc,
- ResourceManager* rm);
+ DecisionEngineOld(Env& env);
/** Destructor, currently does nothing */
~DecisionEngineOld()
diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h
index 87c463c29..e8f7683fd 100644
--- a/src/decision/decision_strategy.h
+++ b/src/decision/decision_strategy.h
@@ -22,39 +22,35 @@
#include "expr/node.h"
#include "prop/sat_solver_types.h"
+#include "smt/env_obj.h"
#include "smt/term_formula_removal.h"
namespace cvc5 {
class DecisionEngineOld;
-namespace context {
- class Context;
- } // namespace context
-
namespace decision {
-
-class DecisionEngine;
-
-class DecisionStrategy {
-protected:
- DecisionEngineOld* d_decisionEngine;
-public:
- DecisionStrategy(DecisionEngineOld* de, context::Context* c)
- : d_decisionEngine(de)
- {
+class DecisionStrategy : protected EnvObj
+{
+ public:
+ DecisionStrategy(Env& env, DecisionEngineOld* de)
+ : EnvObj(env), d_decisionEngine(de)
+ {
}
virtual ~DecisionStrategy() { }
virtual prop::SatLiteral getNext(bool&) = 0;
+
+ protected:
+ DecisionEngineOld* d_decisionEngine;
};/* class DecisionStrategy */
class ITEDecisionStrategy : public DecisionStrategy {
public:
- ITEDecisionStrategy(DecisionEngineOld* de, context::Context* c)
- : DecisionStrategy(de, c)
+ ITEDecisionStrategy(Env& env, DecisionEngineOld* de)
+ : DecisionStrategy(env, de)
{
}
/**
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp
index dcf8975bb..e04de9ce1 100644
--- a/src/decision/justification_heuristic.cpp
+++ b/src/decision/justification_heuristic.cpp
@@ -34,28 +34,26 @@ using namespace cvc5::prop;
namespace cvc5 {
namespace decision {
-JustificationHeuristic::JustificationHeuristic(DecisionEngineOld* de,
- context::UserContext* uc,
- context::Context* c)
- : ITEDecisionStrategy(de, c),
- d_justified(c),
- d_exploredThreshold(c),
- d_prvsIndex(c, 0),
- d_threshPrvsIndex(c, 0),
+JustificationHeuristic::JustificationHeuristic(Env& env, DecisionEngineOld* de)
+ : ITEDecisionStrategy(env, de),
+ d_justified(context()),
+ d_exploredThreshold(context()),
+ d_prvsIndex(context(), 0),
+ d_threshPrvsIndex(context(), 0),
d_helpfulness(
smtStatisticsRegistry().registerInt("decision::jh::helpfulness")),
d_giveup(smtStatisticsRegistry().registerInt("decision::jh::giveup")),
d_timestat(smtStatisticsRegistry().registerTimer("decision::jh::time")),
- d_assertions(uc),
- d_skolemAssertions(uc),
- d_skolemCache(uc),
+ d_assertions(userContext()),
+ d_skolemAssertions(userContext()),
+ d_skolemCache(userContext()),
d_visited(),
d_visitedComputeSkolems(),
d_curDecision(),
d_curThreshold(0),
- d_childCache(uc),
- d_weightCache(uc),
- d_startIndexCache(c)
+ d_childCache(userContext()),
+ d_weightCache(userContext()),
+ d_startIndexCache(context())
{
Trace("decision") << "Justification heuristic enabled" << std::endl;
}
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h
index 8c713ab06..303f1a63b 100644
--- a/src/decision/justification_heuristic.h
+++ b/src/decision/justification_heuristic.h
@@ -113,9 +113,7 @@ class JustificationHeuristic : public ITEDecisionStrategy {
};
public:
- JustificationHeuristic(DecisionEngineOld* de,
- context::UserContext* uc,
- context::Context* c);
+ JustificationHeuristic(Env& env, DecisionEngineOld* de);
~JustificationHeuristic();
diff --git a/src/decision/justification_strategy.cpp b/src/decision/justification_strategy.cpp
index 56d96b32f..d9e6b43e9 100644
--- a/src/decision/justification_strategy.cpp
+++ b/src/decision/justification_strategy.cpp
@@ -23,20 +23,19 @@ using namespace cvc5::prop;
namespace cvc5 {
namespace decision {
-JustificationStrategy::JustificationStrategy(context::Context* c,
- context::UserContext* u,
- prop::SkolemDefManager* skdm,
- ResourceManager* rm)
- : DecisionEngine(c, rm),
+JustificationStrategy::JustificationStrategy(Env& env,
+ prop::SkolemDefManager* skdm)
+ : DecisionEngine(env),
d_skdm(skdm),
d_assertions(
- u,
- c,
+ userContext(),
+ context(),
options::jhRlvOrder()), // assertions are user-context dependent
- d_skolemAssertions(c, c), // skolem assertions are SAT-context dependent
- d_justified(c),
- d_stack(c),
- d_lastDecisionLit(c),
+ d_skolemAssertions(
+ context(), context()), // skolem assertions are SAT-context dependent
+ d_justified(context()),
+ d_stack(context()),
+ d_lastDecisionLit(context()),
d_currStatusDec(false),
d_useRlvOrder(options::jhRlvOrder()),
d_decisionStopOnly(options::decisionMode()
diff --git a/src/decision/justification_strategy.h b/src/decision/justification_strategy.h
index fc31805dd..26b456cf1 100644
--- a/src/decision/justification_strategy.h
+++ b/src/decision/justification_strategy.h
@@ -122,10 +122,7 @@ class JustificationStrategy : public DecisionEngine
{
public:
/** Constructor */
- JustificationStrategy(context::Context* c,
- context::UserContext* u,
- prop::SkolemDefManager* skdm,
- ResourceManager* rm);
+ JustificationStrategy(Env& env, prop::SkolemDefManager* skdm);
/** Presolve, called at the beginning of each check-sat call */
void presolve() override;
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9060c318c..34dff2ba8 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -79,7 +79,6 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
d_assumptions(d_env.getUserContext())
{
Debug("prop") << "Constructing the PropEngine" << std::endl;
- context::Context* satContext = d_env.getContext();
context::UserContext* userContext = d_env.getUserContext();
ProofNodeManager* pnm = d_env.getProofNodeManager();
ResourceManager* rm = d_env.getResourceManager();
@@ -88,17 +87,17 @@ PropEngine::PropEngine(TheoryEngine* te, Env& env)
if (dmode == options::DecisionMode::JUSTIFICATION
|| dmode == options::DecisionMode::STOPONLY)
{
- d_decisionEngine.reset(new decision::JustificationStrategy(
- satContext, userContext, d_skdm.get(), rm));
+ d_decisionEngine.reset(
+ new decision::JustificationStrategy(env, d_skdm.get()));
}
else if (dmode == options::DecisionMode::JUSTIFICATION_OLD
|| dmode == options::DecisionMode::STOPONLY_OLD)
{
- d_decisionEngine.reset(new DecisionEngineOld(satContext, userContext, rm));
+ d_decisionEngine.reset(new DecisionEngineOld(env));
}
else
{
- d_decisionEngine.reset(new decision::DecisionEngineEmpty(satContext, rm));
+ d_decisionEngine.reset(new decision::DecisionEngineEmpty(env));
}
d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 5c7836fb7..3267702fb 100644
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -77,10 +77,10 @@ void Env::shutdown()
d_resourceManager.reset(nullptr);
}
-context::UserContext* Env::getUserContext() { return d_userContext.get(); }
-
context::Context* Env::getContext() { return d_context.get(); }
+context::UserContext* Env::getUserContext() { return d_userContext.get(); }
+
NodeManager* Env::getNodeManager() const { return d_nodeManager; }
ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
diff --git a/src/smt/env_obj.cpp b/src/smt/env_obj.cpp
index b9aebbe83..926bf61ff 100644
--- a/src/smt/env_obj.cpp
+++ b/src/smt/env_obj.cpp
@@ -49,8 +49,6 @@ Node EnvObj::evaluate(TNode n,
return d_env.evaluate(n, args, vals, visited, useRewriter);
}
-const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
-
const Options& EnvObj::options() const { return d_env.getOptions(); }
context::Context* EnvObj::context() const { return d_env.getContext(); }
@@ -60,6 +58,13 @@ context::UserContext* EnvObj::userContext() const
return d_env.getUserContext();
}
+const LogicInfo& EnvObj::logicInfo() const { return d_env.getLogicInfo(); }
+
+ResourceManager* EnvObj::resourceManager() const
+{
+ return d_env.getResourceManager();
+}
+
StatisticsRegistry& EnvObj::statisticsRegistry() const
{
return d_env.getStatisticsRegistry();
diff --git a/src/smt/env_obj.h b/src/smt/env_obj.h
index 75b97fda9..b240b4852 100644
--- a/src/smt/env_obj.h
+++ b/src/smt/env_obj.h
@@ -70,9 +70,6 @@ class EnvObj
const std::unordered_map<Node, Node>& visited,
bool useRewriter = true) const;
- /** Get the current logic information. */
- const LogicInfo& logicInfo() const;
-
/** Get the options object (const version only) via Env. */
const Options& options() const;
@@ -82,6 +79,12 @@ class EnvObj
/** Get a pointer to the UserContext via Env. */
context::UserContext* userContext() const;
+ /** Get the resource manager owned by this Env. */
+ ResourceManager* resourceManager() const;
+
+ /** Get the current logic information. */
+ const LogicInfo& logicInfo() const;
+
/** Get the statistics registry via Env. */
StatisticsRegistry& statisticsRegistry() const;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback