1 /********************* */
2 /*! \file decision_engine.cpp
4 ** Top contributors (to current version):
5 ** Kshitij Bansal, Tim King, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 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_options.h"
22 #include "options/smt_options.h"
28 DecisionEngine::DecisionEngine(context::Context
* sc
, context::UserContext
* uc
)
29 : d_enabledITEStrategies(),
31 d_relevancyStrategy(NULL
),
37 d_result(sc
, SAT_VALUE_UNKNOWN
),
40 Trace("decision") << "Creating decision engine" << std::endl
;
43 void DecisionEngine::init()
45 Assert(d_engineState
== 0);
48 Trace("decision-init") << "DecisionEngine::init()" << std::endl
;
49 Trace("decision-init") << " * options->decisionMode: "
50 << options::decisionMode() << std:: endl
;
51 Trace("decision-init") << " * options->decisionStopOnly: "
52 << options::decisionStopOnly() << std::endl
;
54 if (options::decisionMode() == options::DecisionMode::JUSTIFICATION
)
56 d_enabledITEStrategies
.emplace_back(new decision::JustificationHeuristic(
57 this, d_userContext
, d_satContext
));
58 d_needIteSkolemMap
.push_back(d_enabledITEStrategies
.back().get());
62 void DecisionEngine::shutdown()
64 Trace("decision") << "Shutting down decision engine" << std::endl
;
66 Assert(d_engineState
== 1);
69 d_enabledITEStrategies
.clear();
70 d_needIteSkolemMap
.clear();
73 bool DecisionEngine::isRelevant(SatVariable var
)
75 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
76 if(d_relevancyStrategy
!= NULL
) {
77 //Assert(d_cnfStream->hasNode(var));
78 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
84 SatValue
DecisionEngine::getPolarity(SatVariable var
)
86 Debug("decision") << "getPolarity(" << var
<<")" << std::endl
;
87 if(d_relevancyStrategy
!= NULL
) {
88 Assert(isRelevant(var
));
89 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
91 return SAT_VALUE_UNKNOWN
;
95 void DecisionEngine::addAssertions(
96 const preprocessing::AssertionPipeline
& assertions
)
98 // new assertions, reset whatever result we knew
99 d_result
= SAT_VALUE_UNKNOWN
;
101 for (const Node
& assertion
: assertions
)
103 d_assertions
.push_back(assertion
);
106 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
108 d_needIteSkolemMap
[i
]->addAssertions(assertions
);
112 }/* CVC4 namespace */