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"
22 #include "expr/node.h"
23 #include "util/options.h"
29 DecisionEngine::DecisionEngine(context::Context
*sc
,
30 context::Context
*uc
) :
31 d_enabledStrategies(),
38 d_result(SAT_VALUE_UNKNOWN
)
40 const Options
* options
= Options::current();
41 Trace("decision") << "Creating decision engine" << std::endl
;
43 if(options
->incrementalSolving
) return;
45 if(options
->decisionMode
== Options::DECISION_STRATEGY_INTERNAL
) { }
46 if(options
->decisionMode
== Options::DECISION_STRATEGY_JUSTIFICATION
) {
47 ITEDecisionStrategy
* ds
=
48 new decision::JustificationHeuristic(this, d_satContext
);
50 d_needIteSkolemMap
.push_back(ds
);
54 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
56 d_enabledStrategies
.push_back(ds
);
60 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
62 Assert(false); // doing this so that we revisit what to do
63 // here. Currently not being used.
65 // d_result = SAT_VALUE_UNKNOWN;
66 // d_assertions.reserve(assertions.size());
67 // for(unsigned i = 0; i < assertions.size(); ++i)
68 // d_assertions.push_back(assertions[i]);
71 void DecisionEngine::addAssertions
72 (const vector
<Node
> &assertions
,
73 unsigned assertionsEnd
,
74 IteSkolemMap iteSkolemMap
)
76 // new assertions, reset whatever result we knew
77 d_result
= SAT_VALUE_UNKNOWN
;
79 d_assertions
.reserve(assertions
.size());
80 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
81 d_assertions
.push_back(assertions
[i
]);
83 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
84 d_needIteSkolemMap
[i
]->
85 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
88 // void DecisionEngine::addAssertion(Node n)
90 // d_result = SAT_VALUE_UNKNOWN;
91 // if(needIteSkolemMap()) {
92 // d_assertions.push_back(n);
94 // for(unsigned i = 0; i < d_needIteSkolemMap.size(); ++i)
95 // d_needIteSkolemMap[i]->notifyAssertionsAvailable();