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 if(options::incrementalSolving()) return;
55 Trace("decision-init") << " * options->decisionMode: "
56 << options::decisionMode() << std:: endl
;
57 Trace("decision-init") << " * options->decisionStopOnly: "
58 << options::decisionStopOnly() << std::endl
;
60 if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
) { }
61 if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION
) {
62 ITEDecisionStrategy
* ds
=
63 new decision::JustificationHeuristic(this, d_satContext
);
65 d_needIteSkolemMap
.push_back(ds
);
67 if(options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY
) {
68 RelevancyStrategy
* ds
=
69 new decision::Relevancy(this, d_satContext
);
71 d_needIteSkolemMap
.push_back(ds
);
72 d_relevancyStrategy
= ds
;
77 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
79 d_enabledStrategies
.push_back(ds
);
83 bool DecisionEngine::isRelevant(SatVariable var
)
85 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
86 if(d_relevancyStrategy
!= NULL
) {
87 //Assert(d_cnfStream->hasNode(var));
88 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
94 SatValue
DecisionEngine::getPolarity(SatVariable var
)
96 Debug("decision") << "getPolariry(" << var
<<")" << std::endl
;
97 if(d_relevancyStrategy
!= NULL
) {
98 Assert(isRelevant(var
));
99 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
101 return SAT_VALUE_UNKNOWN
;
112 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
114 Assert(false); // doing this so that we revisit what to do
115 // here. Currently not being used.
117 // d_result = SAT_VALUE_UNKNOWN;
118 // d_assertions.reserve(assertions.size());
119 // for(unsigned i = 0; i < assertions.size(); ++i)
120 // d_assertions.push_back(assertions[i]);
123 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
,
124 unsigned assertionsEnd
,
125 IteSkolemMap iteSkolemMap
)
127 // new assertions, reset whatever result we knew
128 d_result
= SAT_VALUE_UNKNOWN
;
130 d_assertions
.reserve(assertions
.size());
131 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
132 d_assertions
.push_back(assertions
[i
]);
134 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
135 d_needIteSkolemMap
[i
]->
136 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
139 // void DecisionEngine::addAssertion(Node n)
141 // d_result = SAT_VALUE_UNKNOWN;
142 // if(needIteSkolemMap()) {
143 // d_assertions.push_back(n);
145 // for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
146 // d_needIteSkolemMap[i]->notifyAssertionsAvailable();
150 }/* CVC4 namespace */