d_listenerRegistrations(new ListenerRegistrationList()),
d_propagator(true, true),
d_assertions(),
- d_assertionsProcessed(smt.d_userContext, false),
+ d_assertionsProcessed(smt.getUserContext(), false),
d_fakeContext(),
d_abstractValueMap(&d_fakeContext),
d_abstractValues(),
d_simplifyAssertionsDepth(0),
// d_needsExpandDefs(true), //TODO?
- d_exprNames(smt.d_userContext),
- d_iteRemover(smt.d_userContext),
- d_sygusConjectureStale(smt.d_userContext, true)
+ d_exprNames(smt.getUserContext()),
+ d_iteRemover(smt.getUserContext()),
+ d_sygusConjectureStale(smt.getUserContext(), true)
{
d_smt.d_nodeManager->subscribeEvents(this);
d_true = NodeManager::currentNM()->mkConst(true);
d_nodeManager(d_exprManager->getNodeManager()),
d_theoryEngine(nullptr),
d_propEngine(nullptr),
- d_proofManager(NULL),
- d_definedFunctions(NULL),
- d_fmfRecFunctionsDefined(NULL),
- d_assertionList(NULL),
- d_assignments(NULL),
+ d_proofManager(nullptr),
+ d_definedFunctions(nullptr),
+ d_fmfRecFunctionsDefined(nullptr),
+ d_assertionList(nullptr),
+ d_assignments(nullptr),
d_modelGlobalCommands(),
- d_modelCommands(NULL),
+ d_modelCommands(nullptr),
d_dumpCommands(),
d_defineCommands(),
d_logic(),
d_status(),
d_expectedStatus(),
d_smtMode(SMT_MODE_START),
- d_replayStream(NULL),
- d_private(NULL),
- d_statisticsRegistry(NULL),
- d_stats(NULL)
+ d_replayStream(nullptr),
+ d_private(nullptr),
+ d_statisticsRegistry(nullptr),
+ d_stats(nullptr)
{
SmtScope smts(this);
d_originalOptions.copyValues(em->getOptions());
- d_private = new smt::SmtEnginePrivate(*this);
- d_statisticsRegistry = new StatisticsRegistry();
- d_stats = new SmtEngineStatistics();
+ d_private.reset(new smt::SmtEnginePrivate(*this));
+ d_statisticsRegistry.reset(new StatisticsRegistry());
+ d_stats.reset(new SmtEngineStatistics());
d_stats->d_resourceUnitsUsed.setData(
d_private->getResourceManager()->getResourceUsage());
// The ProofManager is constructed before any other proof objects such as
// SatProof and TheoryProofs. The TheoryProofEngine and the SatProof are
// initialized in TheoryEngine and PropEngine respectively.
- Assert(d_proofManager == NULL);
+ Assert(d_proofManager == nullptr);
// d_proofManager must be created before Options has been finished
// being parsed from the input file. Because of this, we cannot trust
// that options::proof() is set correctly yet.
#ifdef CVC4_PROOF
- d_proofManager = new ProofManager(d_userContext);
+ d_proofManager.reset(new ProofManager(getUserContext()));
#endif
- d_definedFunctions = new (true) DefinedFunctionMap(d_userContext);
- d_fmfRecFunctionsDefined = new (true) NodeList(d_userContext);
- d_modelCommands = new (true) smt::CommandList(d_userContext);
+ d_definedFunctions = new (true) DefinedFunctionMap(getUserContext());
+ d_fmfRecFunctionsDefined = new (true) NodeList(getUserContext());
+ d_modelCommands = new (true) smt::CommandList(getUserContext());
}
void SmtEngine::finishInit()
Trace("smt-debug") << "SmtEngine::finishInit" << std::endl;
// We have mutual dependency here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_context,
- d_userContext,
- d_private->d_iteRemover,
- const_cast<const LogicInfo&>(d_logic));
+ d_theoryEngine.reset(new TheoryEngine(getContext(),
+ getUserContext(),
+ d_private->d_iteRemover,
+ const_cast<const LogicInfo&>(d_logic)));
// Add the theories
for(TheoryId id = theory::THEORY_FIRST; id < theory::THEORY_LAST; ++id) {
- TheoryConstructor::addTheory(d_theoryEngine, id);
+ TheoryConstructor::addTheory(getTheoryEngine(), id);
//register with proof engine if applicable
#ifdef CVC4_PROOF
ProofManager::currentPM()->getTheoryProofEngine()->registerTheory(d_theoryEngine->theoryOf(id));
#endif
}
- d_private->addUseTheoryListListener(d_theoryEngine);
+ d_private->addUseTheoryListListener(getTheoryEngine());
// ensure that our heuristics are properly set up
setDefaults();
* are unregistered by the obsolete PropEngine object before registered
* again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(d_theoryEngine,
- d_context,
- d_userContext,
+ d_propEngine.reset(new PropEngine(getTheoryEngine(),
+ getContext(),
+ getUserContext(),
d_private->getReplayLog(),
d_replayStream));
options::incrementalSolving()) {
// In the case of incremental solving, we appear to need these to
// ensure the relevant Nodes remain live.
- d_assertionList = new(true) AssertionList(d_userContext);
+ d_assertionList = new (true) AssertionList(getUserContext());
}
// dump out a set-logic command only when raw-benchmark is disabled to avoid
// Because the destruction of the proofs depends on contexts owned be the
// theory solvers.
#ifdef CVC4_PROOF
- delete d_proofManager;
- d_proofManager = NULL;
+ d_proofManager.reset(nullptr);
#endif
- delete d_theoryEngine;
- d_theoryEngine = NULL;
+ d_theoryEngine.reset(nullptr);
d_propEngine.reset(nullptr);
- delete d_stats;
- d_stats = NULL;
- delete d_statisticsRegistry;
- d_statisticsRegistry = NULL;
+ d_stats.reset(nullptr);
+ d_statisticsRegistry.reset(nullptr);
- delete d_private;
- d_private = NULL;
-
- delete d_userContext;
- d_userContext = NULL;
- delete d_context;
- d_context = NULL;
+ d_private.reset(nullptr);
+ d_userContext.reset(nullptr);
+ d_context.reset(nullptr);
} catch(Exception& e) {
Warning() << "CVC4 threw an exception during cleanup." << endl
<< e << endl;
return false;
}
if(d_assignments == NULL) {
- d_assignments = new(true) AssignmentSet(d_context);
+ d_assignments = new (true) AssignmentSet(getContext());
}
d_assignments->insert(n);
* statistics are unregistered by the obsolete PropEngine object before
* registered again by the new PropEngine object */
d_propEngine.reset(nullptr);
- d_propEngine.reset(new PropEngine(d_theoryEngine,
- d_context,
- d_userContext,
+ d_propEngine.reset(new PropEngine(getTheoryEngine(),
+ getContext(),
+ getUserContext(),
d_private->getReplayLog(),
d_replayStream));
d_theoryEngine->setPropEngine(getPropEngine());
SmtEngine(const SmtEngine&) = delete;
SmtEngine& operator=(const SmtEngine&) = delete;
+ /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
+ TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
+
/** Get a pointer to the PropEngine owned by this SmtEngine. */
prop::PropEngine* getPropEngine() { return d_propEngine.get(); }
+ /** Get a pointer to the UserContext owned by this SmtEngine. */
+ context::UserContext* getUserContext() { return d_userContext.get(); };
+
+ /** Get a pointer to the Context owned by this SmtEngine. */
+ context::Context* getContext() { return d_context.get(); };
+
+ /** Get a pointer to the ProofManager owned by this SmtEngine. */
+ ProofManager* getProofManager() { return d_proofManager.get(); };
+
+ /** Get a pointer to the StatisticsRegistry owned by this SmtEngine. */
+ StatisticsRegistry* getStatisticsRegistry()
+ {
+ return d_statisticsRegistry.get();
+ };
+
/**
* Check that a generated proof (via getProof()) checks.
*/
/* Members -------------------------------------------------------------- */
/** Expr manager context */
- context::Context* d_context;
+ std::unique_ptr<context::Context> d_context;
/** User level context */
- context::UserContext* d_userContext;
+ std::unique_ptr<context::UserContext> d_userContext;
/** The context levels of user pushes */
std::vector<int> d_userLevels;
NodeManager* d_nodeManager;
/** The theory engine */
- TheoryEngine* d_theoryEngine;
+ std::unique_ptr<TheoryEngine> d_theoryEngine;
/** The propositional engine */
std::unique_ptr<prop::PropEngine> d_propEngine;
/** The proof manager */
- ProofManager* d_proofManager;
+ std::unique_ptr<ProofManager> d_proofManager;
/** An index of our defined functions */
DefinedFunctionMap* d_definedFunctions;
/**
* A private utility class to SmtEngine.
*/
- smt::SmtEnginePrivate* d_private;
+ std::unique_ptr<smt::SmtEnginePrivate> d_private;
- StatisticsRegistry* d_statisticsRegistry;
+ std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
- smt::SmtEngineStatistics* d_stats;
+ std::unique_ptr<smt::SmtEngineStatistics> d_stats;
/*---------------------------- sygus commands ---------------------------*/
projects / cvc5.git / commitdiff