d_engineState = 1;
Trace("decision-init") << "DecisionEngine::init()" << std::endl;
- if(options::incrementalSolving()) return;
-
+ if(options::incrementalSolving()) {
+ if(options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL) {
+ if(options::decisionMode.wasSetByUser()) {
+ Warning() << "Ignorning decision option since using incremental mode (currently not supported together)"
+ << std::endl;
+ } else {
+ Notice() << "Using internal decision heuristic since using incremental mode (not supported currently)"
+ << std::endl;
+ }
+ }
+ return;
+ }
Trace("decision-init") << " * options->decisionMode: "
<< options::decisionMode() << std:: endl;
Trace("decision-init") << " * options->decisionStopOnly: "
**
** \brief Justification heuristic for decision making
**
- ** A ATGP-inspired justification-based decision heuristic. See
- ** [insert reference] for more details. This code is, or not, based
+ ** A ATGP-inspired justification-based decision heuristic. This code is based
** on the CVC3 implementation of the same heuristic -- note below.
**
** It needs access to the simplified but non-clausal formula.
#include "theory/rewriter.h"
#include "util/ite_removal.h"
-/***
-Here's the main idea
-
- Given a boolean formula "node", the goal is to try to make it
-evaluate to "desiredVal" (true/false). for instance if "node" is a AND
-formula we want to make it evaluate to true, we'd like one of the
-children to be true. this is done recursively.
-
-***/
-
-/*
-
-CVC3 code <----> this code
-
- value desiredVal
- getValue(lit) litVal
-
-***/
-
-
-// Local helper functions for just this file
-
-
-
// JustificationHeuristic stuff
void JustificationHeuristic::setJustified(TNode n)
Trace("decision") << "jh: Nothing to split on " << std::endl;
-#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
+#if defined CVC4_DEBUG
bool alljustified = true;
for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
TNode curass = d_assertions[i];
}
}
- /* Compute justified */
- /*bool computeJustified() {
-
- }*/
private:
SatLiteral findSplitter(TNode node, SatValue desiredVal)
{
ret = findSplitterRec(node, desiredVal, &litDecision);
if(ret == true) {
Debug("decision") << "Yippee!!" << std::endl;
- //d_prvsIndex = i;
++d_helfulness;
return litDecision;
} else {
/**
* Do all the hard work.
- * @param findFirst returns
*/
bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
\n\
justification-stoponly\n\
+ Use the justification heuristic only to stop early, not for decisions\n\
+";
+/** Under-development options, commenting out from help for the release */
+/*
\n\
relevancy\n\
+ Under development may-relevancy\n\
justification-must\n\
+ Start deciding on literals close to root instead of those\n\
+ near leaves (don't expect it to work well) [Unimplemented]\n\
-";
+";*/
inline DecisionMode stringToDecisionMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
options::decisionRelevancyLeaves.set(false);