/********************* */
/*! \file decision_engine.cpp
** \verbatim
- ** Original author: kshitij
- ** Major contributors: none
- ** Minor contributors (to current version): taking, mdeters
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009-2012 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Top contributors (to current version):
+ ** Kshitij Bansal, Tim King, Andres Noetzli
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Decision engine
**
** Decision engine
**/
-
#include "decision/decision_engine.h"
-#include "decision/justification_heuristic.h"
-#include "decision/relevancy.h"
+#include "decision/decision_attributes.h"
+#include "decision/justification_heuristic.h"
#include "expr/node.h"
-#include "decision/options.h"
-#include "decision/decision_mode.h"
-
-#include "smt/options.h"
+#include "options/decision_options.h"
+#include "options/smt_options.h"
using namespace std;
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;
}
d_engineState = 1;
Trace("decision-init") << "DecisionEngine::init()" << std::endl;
- Trace("decision-init") << " * options->decisionMode: "
+ Trace("decision-init") << " * options->decisionMode: "
<< options::decisionMode() << std:: endl;
Trace("decision-init") << " * options->decisionStopOnly: "
<< options::decisionStopOnly() << std::endl;
- if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL) { }
- if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION) {
- ITEDecisionStrategy* ds =
- new decision::JustificationHeuristic(this, d_userContext, d_satContext);
- enableStrategy(ds);
- d_needIteSkolemMap.push_back(ds);
- }
- if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY) {
- if(options::incrementalSolving()) {
- Warning() << "Relevancy decision heuristic and incremental not supported together"
- << std::endl;
- return; // Currently not supported with incremental
- }
- RelevancyStrategy* ds =
- new decision::Relevancy(this, d_satContext);
- enableStrategy(ds);
- d_needIteSkolemMap.push_back(ds);
- d_relevancyStrategy = ds;
+ if (options::decisionMode() == options::DecisionMode::JUSTIFICATION)
+ {
+ d_enabledITEStrategy.reset(new decision::JustificationHeuristic(
+ this, d_userContext, d_satContext));
+ d_needIteSkolemMap.push_back(d_enabledITEStrategy.get());
}
}
-
-void DecisionEngine::enableStrategy(DecisionStrategy* ds)
+void DecisionEngine::shutdown()
{
- d_enabledStrategies.push_back(ds);
+ Trace("decision") << "Shutting down decision engine" << std::endl;
+
+ Assert(d_engineState == 1);
+ d_engineState = 2;
+ 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;
}
}
-
-
-
-
-
-
-
-void DecisionEngine::addAssertions(const vector<Node> &assertions)
-{
- Assert(false); // doing this so that we revisit what to do
- // here. Currently not being used.
-
- // d_result = SAT_VALUE_UNKNOWN;
- // d_assertions.reserve(assertions.size());
- // for(unsigned i = 0; i < assertions.size(); ++i)
- // d_assertions.push_back(assertions[i]);
-}
-
-void DecisionEngine::addAssertions(const vector<Node> &assertions,
- unsigned assertionsEnd,
- IteSkolemMap iteSkolemMap)
+void DecisionEngine::addAssertions(
+ const preprocessing::AssertionPipeline& assertions)
{
// new assertions, reset whatever result we knew
d_result = SAT_VALUE_UNKNOWN;
-
- // d_assertions.reserve(assertions.size());
- for(unsigned i = 0; i < assertions.size(); ++i)
- d_assertions.push_back(assertions[i]);
-
+
+ for (const Node& assertion : assertions)
+ {
+ d_assertions.push_back(assertion);
+ }
+
for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
- d_needIteSkolemMap[i]->
- addAssertions(assertions, assertionsEnd, iteSkolemMap);
+ {
+ d_needIteSkolemMap[i]->addAssertions(assertions);
+ }
}
-// void DecisionEngine::addAssertion(Node n)
-// {
-// d_result = SAT_VALUE_UNKNOWN;
-// if(needIteSkolemMap()) {
-// d_assertions.push_back(n);
-// }
-// for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
-// d_needIteSkolemMap[i]->notifyAssertionsAvailable();
-// }
-
-
}/* CVC4 namespace */