This is work towards eliminating singletons.
Also, TheoryModel should use the same substitution map as the preprocessor. This is work towards unifying these things, which will be done in a future PR.
#include "prop/sat_solver.h"
#include "prop/sat_solver_factory.h"
#include "prop/theory_proxy.h"
+#include "smt/env.h"
#include "smt/smt_statistics_registry.h"
#include "theory/output_channel.h"
#include "theory/theory_engine.h"
};
PropEngine::PropEngine(TheoryEngine* te,
- context::Context* satContext,
- context::UserContext* userContext,
- ResourceManager* rm,
+ Env& env,
OutputManager& outMgr,
ProofNodeManager* pnm)
: d_inCheckSat(false),
d_theoryEngine(te),
- d_context(satContext),
- d_skdm(new SkolemDefManager(satContext, userContext)),
+ d_env(env),
+ d_skdm(new SkolemDefManager(d_env.getContext(), d_env.getUserContext())),
d_theoryProxy(nullptr),
d_satSolver(nullptr),
d_pnm(pnm),
d_pfCnfStream(nullptr),
d_ppm(nullptr),
d_interrupted(false),
- d_resourceManager(rm),
d_outMgr(outMgr),
- d_assumptions(userContext)
+ d_assumptions(d_env.getUserContext())
{
Debug("prop") << "Constructing the PropEngine" << std::endl;
+ context::Context* satContext = d_env.getContext();
+ context::UserContext* userContext = d_env.getUserContext();
+ ResourceManager* rm = d_env.getResourceManager();
d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
d_decisionEngine->init(); // enable appropriate strategies
d_theoryProxy->finishInit(d_cnfStream);
// connect SAT solver
d_satSolver->initialize(
- d_context,
+ d_env.getContext(),
d_theoryProxy,
- userContext,
+ d_env.getUserContext(),
options::unsatCoresMode() != options::UnsatCoresMode::ASSUMPTIONS
? pnm
: nullptr);
}
if( result == SAT_VALUE_UNKNOWN ) {
-
+ ResourceManager* rm = d_env.getResourceManager();
Result::UnknownExplanation why = Result::INTERRUPTED;
- if (d_resourceManager->outOfTime())
+ if (rm->outOfTime())
+ {
why = Result::TIMEOUT;
- if (d_resourceManager->outOfResources())
+ }
+ if (rm->outOfResources())
+ {
why = Result::RESOURCEOUT;
-
+ }
return Result(Result::SAT_UNKNOWN, why);
}
void PropEngine::spendResource(Resource r)
{
- d_resourceManager->spendResource(r);
+ d_env.getResourceManager()->spendResource(r);
}
bool PropEngine::properExplanation(TNode node, TNode expl) const
namespace cvc5 {
+class Env;
class ResourceManager;
class OutputManager;
class ProofNodeManager;
/**
* Create a PropEngine with a particular decision and theory engine.
*/
- PropEngine(TheoryEngine*,
- context::Context* satContext,
- context::UserContext* userContext,
- ResourceManager* rm,
+ PropEngine(TheoryEngine* te,
+ Env& env,
OutputManager& outMgr,
ProofNodeManager* pnm);
/** The theory engine we will be using */
TheoryEngine* d_theoryEngine;
+ /** Reference to the environment */
+ Env& d_env;
+
/** The decision engine we will be using */
std::unique_ptr<decision::DecisionEngine> d_decisionEngine;
- /** The context */
- context::Context* d_context;
-
/** The skolem definition manager */
std::unique_ptr<SkolemDefManager> d_skdm;
/** Whether we were just interrupted (or not) */
bool d_interrupted;
- /** Pointer to resource manager for associated SmtEngine */
- ResourceManager* d_resourceManager;
/** Reference to the output manager of the smt engine */
OutputManager& d_outMgr;
new smt::Preprocessor(*this, *d_env.get(), *d_absValues.get(), *d_stats));
// make the SMT solver
d_smtSolver.reset(
- new SmtSolver(*this, *d_state, getResourceManager(), *d_pp, *d_stats));
+ new SmtSolver(*this, *d_env.get(), *d_state, *d_pp, *d_stats));
// make the SyGuS solver
d_sygusSolver.reset(
new SygusSolver(*d_smtSolver, *d_pp, getUserContext(), d_outMgr));
#include "options/smt_options.h"
#include "prop/prop_engine.h"
#include "smt/assertions.h"
+#include "smt/env.h"
#include "smt/preprocessor.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_state.h"
namespace smt {
SmtSolver::SmtSolver(SmtEngine& smt,
+ Env& env,
SmtEngineState& state,
- ResourceManager* rm,
Preprocessor& pp,
SmtEngineStatistics& stats)
: d_smt(smt),
+ d_env(env),
d_state(state),
- d_rm(rm),
d_pp(pp),
d_stats(stats),
d_pnm(nullptr),
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
d_theoryEngine.reset(new TheoryEngine(
- d_smt.getContext(),
- d_smt.getUserContext(),
- d_rm,
- logicInfo,
+ d_env,
d_smt.getOutputManager(),
// Other than whether d_pm is set, theory engine proofs are conditioned on
// the relationshup between proofs and unsat cores: the unsat cores are in
* are unregistered by the obsolete PropEngine object before registered
* again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
- d_smt.getContext(),
- d_smt.getUserContext(),
- d_rm,
- d_smt.getOutputManager(),
- d_pnm));
+ d_propEngine.reset(new prop::PropEngine(
+ d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));
Trace("smt-debug") << "Setting up theory engine..." << std::endl;
d_theoryEngine->setPropEngine(getPropEngine());
* statistics are unregistered by the obsolete PropEngine object before
* registered again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new prop::PropEngine(d_theoryEngine.get(),
- d_smt.getContext(),
- d_smt.getUserContext(),
- d_rm,
- d_smt.getOutputManager(),
- d_pnm));
+ d_propEngine.reset(new prop::PropEngine(
+ d_theoryEngine.get(), d_env, d_smt.getOutputManager(), d_pnm));
d_theoryEngine->setPropEngine(getPropEngine());
// Notice that we do not reset TheoryEngine, nor does it require calling
// finishInit again. In particular, TheoryEngine::finishInit does not
Trace("smt") << "SmtSolver::check()" << endl;
const std::string& filename = d_state.getFilename();
- if (d_rm->out())
+ ResourceManager* rm = d_env.getResourceManager();
+ if (rm->out())
{
Result::UnknownExplanation why =
- d_rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
+ rm->outOfResources() ? Result::RESOURCEOUT : Result::TIMEOUT;
return Result(Result::ENTAILMENT_UNKNOWN, why, filename);
}
- d_rm->beginCall();
+ rm->beginCall();
// Make sure the prop layer has all of the assertions
Trace("smt") << "SmtSolver::check(): processing assertions" << endl;
Trace("smt") << "SmtSolver::check(): running check" << endl;
Result result = d_propEngine->checkSat();
- d_rm->endCall();
+ rm->endCall();
Trace("limit") << "SmtSolver::check(): cumulative millis "
- << d_rm->getTimeUsage() << ", resources "
- << d_rm->getResourceUsage() << endl;
+ << rm->getTimeUsage() << ", resources "
+ << rm->getResourceUsage() << endl;
if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
&& result.asSatisfiabilityResult().isSat() == Result::UNSAT)
// includes linear arithmetic and bitvectors, which are the primary
// targets for the global negate option. Other logics are possible here
// but not considered.
- LogicInfo logic = d_smt.getLogicInfo();
+ LogicInfo logic = d_env.getLogicInfo();
if ((logic.isPure(theory::THEORY_ARITH) && logic.isLinear()) ||
logic.isPure(theory::THEORY_BV))
{
void SmtSolver::processAssertions(Assertions& as)
{
TimerStat::CodeTimer paTimer(d_stats.d_processAssertionsTime);
- d_rm->spendResource(Resource::PreprocessStep);
+ d_env.getResourceManager()->spendResource(Resource::PreprocessStep);
Assert(d_state.isFullyReady());
preprocessing::AssertionPipeline& ap = as.getAssertionPipeline();
namespace cvc5 {
class SmtEngine;
+class Env;
class TheoryEngine;
class ResourceManager;
class ProofNodeManager;
{
public:
SmtSolver(SmtEngine& smt,
+ Env& env,
SmtEngineState& state,
- ResourceManager* rm,
Preprocessor& pp,
SmtEngineStatistics& stats);
~SmtSolver();
private:
/** Reference to the parent SMT engine */
SmtEngine& d_smt;
+ /** Reference to the environment */
+ Env& d_env;
/** Reference to the state of the SmtEngine */
SmtEngineState& d_state;
- /** Pointer to a resource manager (owned by SmtEngine) */
- ResourceManager* d_rm;
/** Reference to the preprocessor of SmtEngine */
Preprocessor& d_pp;
/** Reference to the statistics of SmtEngine */
#include "printer/printer.h"
#include "prop/prop_engine.h"
#include "smt/dump.h"
+#include "smt/env.h"
#include "smt/logic_exception.h"
#include "smt/output_manager.h"
#include "theory/combination_care_graph.h"
if (options::relevanceFilter())
{
d_relManager.reset(
- new RelevanceManager(d_userContext, theory::Valuation(this)));
+ new RelevanceManager(d_env.getUserContext(), theory::Valuation(this)));
}
// initialize the quantifiers engine
ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
-TheoryEngine::TheoryEngine(context::Context* context,
- context::UserContext* userContext,
- ResourceManager* rm,
- const LogicInfo& logicInfo,
+context::Context* TheoryEngine::getSatContext() const
+{
+ return d_env.getContext();
+}
+
+context::UserContext* TheoryEngine::getUserContext() const
+{
+ return d_env.getUserContext();
+}
+
+TheoryEngine::TheoryEngine(Env& env,
OutputManager& outMgr,
ProofNodeManager* pnm)
: d_propEngine(nullptr),
- d_context(context),
- d_userContext(userContext),
- d_logicInfo(logicInfo),
+ d_env(env),
+ d_logicInfo(env.getLogicInfo()),
d_outMgr(outMgr),
d_pnm(pnm),
- d_lazyProof(
- d_pnm != nullptr ? new LazyCDProof(
- d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
- : nullptr),
- d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
+ d_lazyProof(d_pnm != nullptr
+ ? new LazyCDProof(d_pnm,
+ nullptr,
+ d_env.getUserContext(),
+ "TheoryEngine::LazyCDProof")
+ : nullptr),
+ d_tepg(new TheoryEngineProofGenerator(d_pnm, d_env.getUserContext())),
d_tc(nullptr),
d_sharedSolver(nullptr),
d_quantEngine(nullptr),
- d_decManager(new DecisionManager(userContext)),
+ d_decManager(new DecisionManager(d_env.getUserContext())),
d_relManager(nullptr),
d_eager_model_building(false),
- d_inConflict(context, false),
+ d_inConflict(d_env.getContext(), false),
d_inSatMode(false),
d_hasShutDown(false),
- d_incomplete(context, false),
- d_incompleteTheory(context, THEORY_BUILTIN),
- d_incompleteId(context, IncompleteId::UNKNOWN),
- d_propagationMap(context),
- d_propagationMapTimestamp(context, 0),
- d_propagatedLiterals(context),
- d_propagatedLiteralsIndex(context, 0),
- d_atomRequests(context),
+ d_incomplete(d_env.getContext(), false),
+ d_incompleteTheory(d_env.getContext(), THEORY_BUILTIN),
+ d_incompleteId(d_env.getContext(), IncompleteId::UNKNOWN),
+ d_propagationMap(d_env.getContext()),
+ d_propagationMapTimestamp(d_env.getContext(), 0),
+ d_propagatedLiterals(d_env.getContext()),
+ d_propagatedLiteralsIndex(d_env.getContext(), 0),
+ d_atomRequests(d_env.getContext()),
d_combineTheoriesTime(smtStatisticsRegistry().registerTimer(
"TheoryEngine::combineTheoriesTime")),
d_true(),
d_false(),
d_interrupted(false),
- d_resourceManager(rm),
d_inPreregister(false),
- d_factsAsserted(context, false),
+ d_factsAsserted(d_env.getContext(), false),
d_attr_handle()
{
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
- Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
+ Trace("dtview::prop") << std::string(d_env.getContext()->getLevel(), ' ')
<< ":THEORY-PROP: " << literal << endl;
// spendResource();
void TheoryEngine::spendResource(Resource r)
{
- d_resourceManager->spendResource(r);
+ d_env.getResourceManager()->spendResource(r);
}
void TheoryEngine::initializeProofChecker(ProofChecker* pc)
namespace cvc5 {
+class Env;
class ResourceManager;
class OutputManager;
class TheoryEngineProofGenerator;
/** Associated PropEngine engine */
prop::PropEngine* d_propEngine;
- /** Our context */
- context::Context* d_context;
-
- /** Our user context */
- context::UserContext* d_userContext;
+ /**
+ * Reference to the environment.
+ */
+ Env& d_env;
/**
* A table of from theory IDs to theory pointers. Never use this table
* the cost of walking the DAG on registration, etc.
*/
const LogicInfo& d_logicInfo;
+
/** The separation logic location and data types */
TypeNode d_sepLocType;
TypeNode d_sepDataType;
/** Whether we were just interrupted (or not) */
bool d_interrupted;
- ResourceManager* d_resourceManager;
public:
/** Constructs a theory engine */
- TheoryEngine(context::Context* context,
- context::UserContext* userContext,
- ResourceManager* rm,
- const LogicInfo& logic,
- OutputManager& outMgr,
- ProofNodeManager* pnm);
+ TheoryEngine(Env& env, OutputManager& outMgr, ProofNodeManager* pnm);
/** Destroys a theory engine */
~TheoryEngine();
{
Assert(d_theoryTable[theoryId] == NULL && d_theoryOut[theoryId] == NULL);
d_theoryOut[theoryId] = new theory::EngineOutputChannel(this, theoryId);
- d_theoryTable[theoryId] = new TheoryClass(d_context,
- d_userContext,
+ d_theoryTable[theoryId] = new TheoryClass(getSatContext(),
+ getUserContext(),
*d_theoryOut[theoryId],
theory::Valuation(this),
d_logicInfo,
/**
* Get a pointer to the underlying sat context.
*/
- context::Context* getSatContext() const { return d_context; }
+ context::Context* getSatContext() const;
/**
* Get a pointer to the underlying user context.
*/
- context::UserContext* getUserContext() const { return d_userContext; }
+ context::UserContext* getUserContext() const;
/**
* Get a pointer to the underlying quantifiers engine.
projects / cvc5.git / commitdiff