namespace CVC4 {
-DecisionEngine::DecisionEngine(context::Context *sc,
- context::UserContext *uc) :
- d_enabledStrategies(),
- d_needIteSkolemMap(),
- d_relevancyStrategy(NULL),
- d_assertions(uc),
- d_cnfStream(NULL),
- d_satSolver(NULL),
- d_satContext(sc),
- d_userContext(uc),
- d_result(sc, SAT_VALUE_UNKNOWN),
- d_engineState(0)
+DecisionEngine::DecisionEngine(context::Context* sc,
+ context::UserContext* uc,
+ ResourceManager* rm)
+ : d_enabledITEStrategy(nullptr),
+ d_needIteSkolemMap(),
+ d_relevancyStrategy(nullptr),
+ d_assertions(uc),
+ d_cnfStream(nullptr),
+ d_satSolver(nullptr),
+ d_satContext(sc),
+ d_userContext(uc),
+ d_result(sc, SAT_VALUE_UNKNOWN),
+ d_engineState(0),
+ d_resourceManager(rm)
{
Trace("decision") << "Creating decision engine" << std::endl;
}
if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
{
- ITEDecisionStrategy* ds =
- new decision::JustificationHeuristic(this, d_userContext, d_satContext);
- d_enabledStrategies.push_back(ds);
- d_needIteSkolemMap.push_back(ds);
+ d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
+ this, d_userContext, d_satContext));
+ d_needIteSkolemMap.push_back(d_enabledITEStrategy.get());
}
}
Assert(d_engineState == 1);
d_engineState = 2;
-
- for (DecisionStrategy* s : d_enabledStrategies)
- {
- delete s;
- }
- d_enabledStrategies.clear();
+ d_enabledITEStrategy.reset(nullptr);
d_needIteSkolemMap.clear();
}
+SatLiteral DecisionEngine::getNext(bool& stopSearch)
+{
+ d_resourceManager->spendResource(ResourceManager::Resource::DecisionStep);
+ Assert(d_cnfStream != nullptr)
+ << "Forgot to set cnfStream for decision engine?";
+ Assert(d_satSolver != nullptr)
+ << "Forgot to set satSolver for decision engine?";
+
+ return d_enabledITEStrategy == nullptr
+ ? undefSatLiteral
+ : d_enabledITEStrategy->getNext(stopSearch);
+}
+
bool DecisionEngine::isRelevant(SatVariable var)
{
Debug("decision") << "isRelevant(" << var <<")" << std::endl;
- if(d_relevancyStrategy != NULL) {
+ if (d_relevancyStrategy != nullptr)
+ {
//Assert(d_cnfStream->hasNode(var));
return d_relevancyStrategy->isRelevant( d_cnfStream->getNode(SatLiteral(var)) );
- } else {
+ }
+ else
+ {
return true;
}
}
SatValue DecisionEngine::getPolarity(SatVariable var)
{
Debug("decision") << "getPolarity(" << var <<")" << std::endl;
- if(d_relevancyStrategy != NULL) {
+ if (d_relevancyStrategy != nullptr)
+ {
Assert(isRelevant(var));
return d_relevancyStrategy->getPolarity( d_cnfStream->getNode(SatLiteral(var)) );
- } else {
+ }
+ else
+ {
return SAT_VALUE_UNKNOWN;
}
}