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
,
29 context::UserContext
*uc
) :
30 d_enabledStrategies(),
32 d_relevancyStrategy(NULL
),
38 d_result(sc
, SAT_VALUE_UNKNOWN
),
41 Trace("decision") << "Creating decision engine" << std::endl
;
44 void DecisionEngine::init()
46 Assert(d_engineState
== 0);
49 Trace("decision-init") << "DecisionEngine::init()" << std::endl
;
50 Trace("decision-init") << " * options->decisionMode: "
51 << options::decisionMode() << std:: endl
;
52 Trace("decision-init") << " * options->decisionStopOnly: "
53 << options::decisionStopOnly() << std::endl
;
55 if (options::decisionMode() == options::DecisionMode::JUSTIFICATION
)
57 ITEDecisionStrategy
* ds
=
58 new decision::JustificationHeuristic(this, d_userContext
, d_satContext
);
60 d_needIteSkolemMap
.push_back(ds
);
65 void DecisionEngine::enableStrategy(DecisionStrategy
* ds
)
67 d_enabledStrategies
.push_back(ds
);
70 void DecisionEngine::clearStrategies(){
71 for(unsigned i
= 0; i
< d_enabledStrategies
.size(); ++i
){
72 delete d_enabledStrategies
[i
];
74 d_enabledStrategies
.clear();
75 d_needIteSkolemMap
.clear();
78 bool DecisionEngine::isRelevant(SatVariable var
)
80 Debug("decision") << "isRelevant(" << var
<<")" << std::endl
;
81 if(d_relevancyStrategy
!= NULL
) {
82 //Assert(d_cnfStream->hasNode(var));
83 return d_relevancyStrategy
->isRelevant( d_cnfStream
->getNode(SatLiteral(var
)) );
89 SatValue
DecisionEngine::getPolarity(SatVariable var
)
91 Debug("decision") << "getPolarity(" << var
<<")" << std::endl
;
92 if(d_relevancyStrategy
!= NULL
) {
93 Assert(isRelevant(var
));
94 return d_relevancyStrategy
->getPolarity( d_cnfStream
->getNode(SatLiteral(var
)) );
96 return SAT_VALUE_UNKNOWN
;
100 void DecisionEngine::addAssertions(
101 const preprocessing::AssertionPipeline
& assertions
)
103 // new assertions, reset whatever result we knew
104 d_result
= SAT_VALUE_UNKNOWN
;
106 for (const Node
& assertion
: assertions
)
108 d_assertions
.push_back(assertion
);
111 for(unsigned i
= 0; i
< d_needIteSkolemMap
.size(); ++i
)
113 d_needIteSkolemMap
[i
]->addAssertions(assertions
);
117 }/* CVC4 namespace */