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() :
30 d_needSimplifiedPreITEAssertions(),
34 const Options
* options
= Options::current();
35 Trace("decision") << "Creating decision engine" << std::endl
;
36 if(options
->decisionMode
== Options::DECISION_STRATEGY_INTERNAL
) { }
37 if(options
->decisionMode
== Options::DECISION_STRATEGY_JUSTIFICATION
) {
38 DecisionStrategy
* ds
= new decision::JustificationHeuristic(this);
43 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
45 d_enabledStrategies
.push_back(ds
);
46 if( ds
->needSimplifiedPreITEAssertions() )
47 d_needSimplifiedPreITEAssertions
.push_back(ds
);
50 void DecisionEngine::informSimplifiedPreITEAssertions(const vector
<Node
> &assertions
)
52 d_assertions
.reserve(assertions
.size());
53 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
54 d_assertions
.push_back(assertions
[i
]);
55 for(unsigned i
= 0; i
< d_needSimplifiedPreITEAssertions
.size(); ++i
)
56 d_needSimplifiedPreITEAssertions
[i
]->notifyAssertionsAvailable();