1 /********************* */
2 /*! \file decision_engine.cpp
4 ** Original author: kshitij
5 ** Major contributors: none
6 ** Minor contributors (to current version): taking, mdeters
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief Decision engine
17 #include "decision/decision_engine.h"
18 #include "decision/justification_heuristic.h"
19 #include "decision/relevancy.h"
21 #include "expr/node.h"
22 #include "decision/options.h"
23 #include "decision/decision_mode.h"
25 #include "smt/options.h"
31 DecisionEngine::DecisionEngine(context::Context
*sc
,
32 context::Context
*uc
) :
33 d_enabledStrategies(),
35 d_relevancyStrategy(NULL
),
41 d_result(sc
, SAT_VALUE_UNKNOWN
),
44 Trace("decision") << "Creating decision engine" << std::endl
;
47 void DecisionEngine::init()
49 Assert(d_engineState
== 0);
52 Trace("decision-init") << "DecisionEngine::init()" << std::endl
;
53 Trace("decision-init") << " * options->decisionMode: "
54 << options::decisionMode() << std:: endl
;
55 Trace("decision-init") << " * options->decisionStopOnly: "
56 << options::decisionStopOnly() << std::endl
;
58 if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
) { }
59 if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION
) {
60 ITEDecisionStrategy
* ds
=
61 new decision::JustificationHeuristic(this, d_userContext
, d_satContext
);
63 d_needIteSkolemMap
.push_back(ds
);
65 if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
) {
66 if(options::incrementalSolving()) {
67 Warning() << "Relevancy decision heuristic and incremental not supported together"
69 return; // Currently not supported with incremental
71 RelevancyStrategy
* ds
=
72 new decision::Relevancy(this, d_satContext
);
74 d_needIteSkolemMap
.push_back(ds
);
75 d_relevancyStrategy
= ds
;
80 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
82 d_enabledStrategies
.push_back(ds
);
86 bool DecisionEngine::isRelevant(SatVariable var
)
88 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
89 if(d_relevancyStrategy
!= NULL
) {
90 //Assert(d_cnfStream->hasNode(var));
91 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
97 SatValue
DecisionEngine::getPolarity(SatVariable var
)
99 Debug("decision") << "getPolarity(" << var
<<")" << std::endl
;
100 if(d_relevancyStrategy
!= NULL
) {
101 Assert(isRelevant(var
));
102 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
104 return SAT_VALUE_UNKNOWN
;
115 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
117 Assert(false); // doing this so that we revisit what to do
118 // here. Currently not being used.
120 // d_result = SAT_VALUE_UNKNOWN;
121 // d_assertions.reserve(assertions.size());
122 // for(unsigned i = 0; i < assertions.size(); ++i)
123 // d_assertions.push_back(assertions[i]);
126 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
,
127 unsigned assertionsEnd
,
128 IteSkolemMap iteSkolemMap
)
130 // new assertions, reset whatever result we knew
131 d_result
= SAT_VALUE_UNKNOWN
;
133 // d_assertions.reserve(assertions.size());
134 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
135 d_assertions
.push_back(assertions
[i
]);
137 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
138 d_needIteSkolemMap
[i
]->
139 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
142 // void DecisionEngine::addAssertion(Node n)
144 // d_result = SAT_VALUE_UNKNOWN;
145 // if(needIteSkolemMap()) {
146 // d_assertions.push_back(n);
148 // for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
149 // d_needIteSkolemMap[i]->notifyAssertionsAvailable();
153 }/* CVC4 namespace */