1 /********************* */
2 /*! \file decision_engine.cpp
4 ** Top contributors (to current version):
5 ** Kshitij Bansal, Tim King, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** \brief Decision engine
16 #include "decision/decision_engine.h"
18 #include "decision/decision_attributes.h"
19 #include "decision/justification_heuristic.h"
20 #include "expr/node.h"
21 #include "options/decision_mode.h"
22 #include "options/decision_options.h"
23 #include "options/smt_options.h"
29 DecisionEngine::DecisionEngine(context::Context
*sc
,
30 context::UserContext
*uc
) :
31 d_enabledStrategies(),
33 d_relevancyStrategy(NULL
),
39 d_result(sc
, SAT_VALUE_UNKNOWN
),
42 Trace("decision") << "Creating decision engine" << std::endl
;
45 void DecisionEngine::init()
47 Assert(d_engineState
== 0);
50 Trace("decision-init") << "DecisionEngine::init()" << std::endl
;
51 Trace("decision-init") << " * options->decisionMode: "
52 << options::decisionMode() << std:: endl
;
53 Trace("decision-init") << " * options->decisionStopOnly: "
54 << options::decisionStopOnly() << std::endl
;
56 if(options::decisionMode() == decision::DECISION_STRATEGY_INTERNAL
) { }
57 if(options::decisionMode() == decision::DECISION_STRATEGY_JUSTIFICATION
) {
58 ITEDecisionStrategy
* ds
=
59 new decision::JustificationHeuristic(this, d_userContext
, d_satContext
);
61 d_needIteSkolemMap
.push_back(ds
);
66 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
68 d_enabledStrategies
.push_back(ds
);
71 void DecisionEngine::clearStrategies(){
72 for(unsigned i
= 0; i
< d_enabledStrategies
.size(); ++i
){
73 delete d_enabledStrategies
[i
];
75 d_enabledStrategies
.clear();
76 d_needIteSkolemMap
.clear();
79 bool DecisionEngine::isRelevant(SatVariable var
)
81 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
82 if(d_relevancyStrategy
!= NULL
) {
83 //Assert(d_cnfStream->hasNode(var));
84 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
90 SatValue
DecisionEngine::getPolarity(SatVariable var
)
92 Debug("decision") << "getPolarity(" << var
<<")" << std::endl
;
93 if(d_relevancyStrategy
!= NULL
) {
94 Assert(isRelevant(var
));
95 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
97 return SAT_VALUE_UNKNOWN
;
101 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
)
103 Assert(false); // doing this so that we revisit what to do
104 // here. Currently not being used.
106 // d_result = SAT_VALUE_UNKNOWN;
107 // d_assertions.reserve(assertions.size());
108 // for(unsigned i = 0; i < assertions.size(); ++i)
109 // d_assertions.push_back(assertions[i]);
112 void DecisionEngine::addAssertions(const vector
<Node
> &assertions
,
113 unsigned assertionsEnd
,
114 IteSkolemMap iteSkolemMap
)
116 // new assertions, reset whatever result we knew
117 d_result
= SAT_VALUE_UNKNOWN
;
119 // d_assertions.reserve(assertions.size());
120 for(unsigned i
= 0; i
< assertions
.size(); ++i
)
121 d_assertions
.push_back(assertions
[i
]);
123 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
124 d_needIteSkolemMap
[i
]->
125 addAssertions(assertions
, assertionsEnd
, iteSkolemMap
);
128 }/* CVC4 namespace */