1 /********************* */
2 /*! \file decision_engine.cpp
4 ** Original author: Kshitij Bansal
5 ** Major contributors: none
6 ** Minor contributors (to current version): Tim King, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 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"
20 #include "expr/node.h"
21 #include "decision/options.h"
22 #include "decision/decision_mode.h"
24 #include "smt/options.h"
30 DecisionEngine::DecisionEngine(context::Context
*sc
,
31 context::UserContext
*uc
) :
32 d_enabledStrategies(),
34 d_relevancyStrategy(NULL
),
40 d_result(sc
, SAT_VALUE_UNKNOWN
),
43 Trace("decision") << "Creating decision engine" << std::endl
;
46 void DecisionEngine::init()
48 Assert(d_engineState
== 0);
51 Trace("decision-init") << "DecisionEngine::init()" << std::endl
;
52 Trace("decision-init") << " * options->decisionMode: "
53 << options::decisionMode() << std:: endl
;
54 Trace("decision-init") << " * options->decisionStopOnly: "
55 << options::decisionStopOnly() << std::endl
;
57 if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
) { }
58 if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION
) {
59 ITEDecisionStrategy
* ds
=
60 new decision::JustificationHeuristic(this, d_userContext
, d_satContext
);
62 d_needIteSkolemMap
.push_back(ds
);
67 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
69 d_enabledStrategies
.push_back(ds
);
72 void DecisionEngine::clearStrategies(){
73 for(unsigned i
= 0; i
< d_enabledStrategies
.size(); ++i
){
74 delete d_enabledStrategies
[i
];
76 d_enabledStrategies
.clear();
77 d_needIteSkolemMap
.clear();
80 bool DecisionEngine::isRelevant(SatVariable var
)
82 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
83 if(d_relevancyStrategy
!= NULL
) {
84 //Assert(d_cnfStream->hasNode(var));
85 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
91 SatValue
DecisionEngine::getPolarity(SatVariable var
)
93 Debug("decision") << "getPolarity(" << var
<<")" << std::endl
;
94 if(d_relevancyStrategy
!= NULL
) {
95 Assert(isRelevant(var
));
96 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
98 return SAT_VALUE_UNKNOWN
;
102 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
104 Assert(false); // doing this so that we revisit what to do
105 // here. Currently not being used.
107 // d_result = SAT_VALUE_UNKNOWN;
108 // d_assertions.reserve(assertions.size());
109 // for(unsigned i = 0; i < assertions.size(); ++i)
110 // d_assertions.push_back(assertions[i]);
113 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
,
114 unsigned assertionsEnd
,
115 IteSkolemMap iteSkolemMap
)
117 // new assertions, reset whatever result we knew
118 d_result
= SAT_VALUE_UNKNOWN
;
120 // d_assertions.reserve(assertions.size());
121 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
122 d_assertions
.push_back(assertions
[i
]);
124 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
125 d_needIteSkolemMap
[i
]->
126 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
129 }/* CVC4 namespace */