1 /********************* */
2 /*! \file decision_engine.cpp
4 ** Original author: kshitij
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Decision engine
19 #include "decision/decision_engine.h"
20 #include "decision/justification_heuristic.h"
21 #include "decision/relevancy.h"
23 #include "expr/node.h"
24 #include "util/options.h"
30 DecisionEngine::DecisionEngine(context::Context
*sc
,
31 context::Context
*uc
) :
32 d_enabledStrategies(),
34 d_relevancyStrategy(NULL
),
40 d_result(SAT_VALUE_UNKNOWN
)
42 const Options
* options
= Options::current();
43 Trace("decision") << "Creating decision engine" << std::endl
;
45 if(options
->incrementalSolving
) return;
47 if(options
->decisionMode
== Options::DECISION_STRATEGY_INTERNAL
) { }
48 if(options
->decisionMode
== Options::DECISION_STRATEGY_JUSTIFICATION
) {
49 ITEDecisionStrategy
* ds
=
50 new decision::JustificationHeuristic(this, d_satContext
);
52 d_needIteSkolemMap
.push_back(ds
);
54 if(options
->decisionMode
== Options::DECISION_STRATEGY_RELEVANCY
) {
55 RelevancyStrategy
* ds
=
56 new decision::Relevancy(this, d_satContext
, options
->decisionOptions
);
58 d_needIteSkolemMap
.push_back(ds
);
59 d_relevancyStrategy
= ds
;
63 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
65 d_enabledStrategies
.push_back(ds
);
69 bool DecisionEngine::isRelevant(SatVariable var
)
71 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
72 if(d_relevancyStrategy
!= NULL
) {
73 //Assert(d_cnfStream->hasNode(var));
74 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
80 SatValue
DecisionEngine::getPolarity(SatVariable var
)
82 Debug("decision") << "getPolariry(" << var
<<")" << std::endl
;
83 if(d_relevancyStrategy
!= NULL
) {
84 Assert(isRelevant(var
));
85 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
87 return SAT_VALUE_UNKNOWN
;
98 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
100 Assert(false); // doing this so that we revisit what to do
101 // here. Currently not being used.
103 // d_result = SAT_VALUE_UNKNOWN;
104 // d_assertions.reserve(assertions.size());
105 // for(unsigned i = 0; i < assertions.size(); ++i)
106 // d_assertions.push_back(assertions[i]);
109 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
,
110 unsigned assertionsEnd
,
111 IteSkolemMap iteSkolemMap
)
113 // new assertions, reset whatever result we knew
114 d_result
= SAT_VALUE_UNKNOWN
;
116 d_assertions
.reserve(assertions
.size());
117 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
118 d_assertions
.push_back(assertions
[i
]);
120 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
121 d_needIteSkolemMap
[i
]->
122 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
125 // void DecisionEngine::addAssertion(Node n)
127 // d_result = SAT_VALUE_UNKNOWN;
128 // if(needIteSkolemMap()) {
129 // d_assertions.push_back(n);
131 // for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
132 // d_needIteSkolemMap[i]->notifyAssertionsAvailable();
136 }/* CVC4 namespace */