diff options
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 96 |
1 files changed, 96 insertions, 0 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h new file mode 100644 index 000000000..cb2216d6d --- /dev/null +++ b/src/decision/justification_heuristic.h @@ -0,0 +1,96 @@ +/********************* */ +/*! \file justification_heuristic.h + ** \verbatim + ** Original author: kshitij + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Justification heuristic for decision making + ** + ** A ATGP-inspired justification-based decision heuristic. See + ** [insert reference] for more details. This code is, or not, based + ** on the CVC3 implementation of the same heuristic. + ** + ** It needs access to the simplified but non-clausal formula. + **/ + +#ifndef __CVC4__DECISION__JUSTIFICATION_HEURISTIC +#define __CVC4__DECISION__JUSTIFICATION_HEURISTIC + +#include "decision_engine.h" +#include "decision_strategy.h" + +#include "prop/sat_solver_types.h" +#include "expr/node.h" + +using namespace CVC4::prop; + +namespace CVC4 { + +namespace decision { + +class JustificationHeuristic : public DecisionStrategy { + set<SatVariable> d_justified; + unsigned d_prvsIndex; +public: + JustificationHeuristic(CVC4::DecisionEngine* de) : + DecisionStrategy(de) { + Trace("decision") << "Justification heuristic enabled" << std::endl; + } + prop::SatLiteral getNext() { + Trace("decision") << "JustificationHeuristic::getNext()" << std::endl; + + const vector<Node>& assertions = d_decisionEngine->getAssertions(); + + for(unsigned i = d_prvsIndex; i < assertions.size(); ++i) { + SatLiteral litDecision; + + /* Make sure there is a literal corresponding to the node */ + if( not d_decisionEngine->hasSatLiteral(assertions[i]) ) { + // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl; + continue; + // Assert(not lit.isNull()); + } + + SatLiteral lit = d_decisionEngine->getSatLiteral(assertions[i]); + SatValue desiredVal = d_decisionEngine->getSatValue(lit); + if(desiredVal == SAT_VALUE_UNKNOWN) desiredVal = SAT_VALUE_TRUE; + bool ret = findSplitterRec(lit, desiredVal, &litDecision); + if(ret == true) { + d_prvsIndex = i; + return litDecision; + } + } + + return prop::undefSatLiteral; + } + bool needSimplifiedPreITEAssertions() { return true; } + void notifyAssertionsAvailable() { + Trace("decision") << "JustificationHeuristic::notifyAssertionsAvailable()" + << " size = " << d_decisionEngine->getAssertions().size() + << std::endl; + /* clear the justifcation labels -- reconsider if/when to do + this */ + d_justified.clear(); + d_prvsIndex = 0; + } +private: + /* Do all the hardwork. */ + bool findSplitterRec(SatLiteral lit, SatValue value, SatLiteral* litDecision); + + /* Helper functions */ + void setJustified(SatVariable v); + bool checkJustified(SatVariable v); +};/* class JustificationHeuristic */ + +}/* namespace decision */ + +}/* namespace CVC4 */ + +#endif /* __CVC4__DECISION__JUSTIFICATION_HEURISTIC */ |