diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-17 17:20:37 +0000 |
commit | 7742c4211f765c2ba2637a211265c20789b861ee (patch) | |
tree | 05622a9df5dc2c900608b8e2ac5611d70e3208c6 /src/decision | |
parent | ccd77233892ace44fd4852999e66534d1c2283ea (diff) |
A dummy decision engine. Expected performance impact: none.
Adds DecisionEngine and an abstract class DecisionStrategy
which other strategies will derive from eventually.
Full revision summary of merged commits:
r3241 merge from trunk
r3240 fix
r3239 WIP
r3238 JH, CVC3 code: 5% done -- 5% translated
r3237 JH groundwork
r3236 make make regrss pass
r3234 hueristic->heuristic
r3229 JustificationHeuristic: EOD-WIP
r3228 DecisionEngine: hookup assetions
r3227 move ITE outside simplifyAssertions
r3226 DecisionStrategy abstract class
r3222 DecisionEngine: begin
Diffstat (limited to 'src/decision')
-rw-r--r-- | src/decision/Makefile | 4 | ||||
-rw-r--r-- | src/decision/Makefile.am | 13 | ||||
-rw-r--r-- | src/decision/decision_engine.cpp | 55 | ||||
-rw-r--r-- | src/decision/decision_engine.h | 150 | ||||
-rw-r--r-- | src/decision/decision_strategy.h | 50 | ||||
-rw-r--r-- | src/decision/justification_heuristic.cpp | 393 | ||||
-rw-r--r-- | src/decision/justification_heuristic.h | 96 |
7 files changed, 761 insertions, 0 deletions
diff --git a/src/decision/Makefile b/src/decision/Makefile new file mode 100644 index 000000000..27978f85f --- /dev/null +++ b/src/decision/Makefile @@ -0,0 +1,4 @@ +topdir = ../.. +srcdir = src/decision + +include $(topdir)/Makefile.subdir diff --git a/src/decision/Makefile.am b/src/decision/Makefile.am new file mode 100644 index 000000000..c399cbf71 --- /dev/null +++ b/src/decision/Makefile.am @@ -0,0 +1,13 @@ +AM_CPPFLAGS = \ + -D__BUILDING_CVC4LIB \ + -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. +AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) + +noinst_LTLIBRARIES = libdecision.la + +libdecision_la_SOURCES = \ + decision_engine.h \ + decision_engine.cpp \ + decision_strategy.h \ + justification_heuristic.h \ + justification_heuristic.cpp diff --git a/src/decision/decision_engine.cpp b/src/decision/decision_engine.cpp new file mode 100644 index 000000000..936ac8e73 --- /dev/null +++ b/src/decision/decision_engine.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \file decision_engine.cpp + ** \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 Decision engine + ** + ** Decision engine + **/ + +#include "decision/decision_engine.h" +#include "decision/justification_heuristic.h" + +#include "expr/node.h" +#include "util/options.h" + +using namespace std; + +namespace CVC4 { + +DecisionEngine::DecisionEngine() : d_needSimplifiedPreITEAssertions() { + const Options* options = Options::current(); + Trace("decision") << "Creating decision engine" << std::endl; + if(options->decisionMode == Options::DECISION_STRATEGY_INTERNAL) { } + if(options->decisionMode == Options::DECISION_STRATEGY_JUSTIFICATION) { + DecisionStrategy* ds = new decision::JustificationHeuristic(this); + enableStrategy(ds); + } +} + +void DecisionEngine::enableStrategy(DecisionStrategy* ds) +{ + d_enabledStrategies.push_back(ds); + if( ds->needSimplifiedPreITEAssertions() ) + d_needSimplifiedPreITEAssertions.push_back(ds); +} + +void DecisionEngine::informSimplifiedPreITEAssertions(const vector<Node> &assertions) +{ + d_assertions.reserve(assertions.size()); + for(unsigned i = 0; i < assertions.size(); ++i) + d_assertions.push_back(assertions[i]); + for(unsigned i = 0; i < d_needSimplifiedPreITEAssertions.size(); ++i) + d_needSimplifiedPreITEAssertions[i]->notifyAssertionsAvailable(); +} + +}/* CVC4 namespace */ diff --git a/src/decision/decision_engine.h b/src/decision/decision_engine.h new file mode 100644 index 000000000..d4037acff --- /dev/null +++ b/src/decision/decision_engine.h @@ -0,0 +1,150 @@ +/********************* */ +/*! \file decision_engine.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 Decision engine + ** + ** Decision engine + **/ + +#ifndef __CVC4__DECISION__DECISION_ENGINE_H +#define __CVC4__DECISION__DECISION_ENGINE_H + +#include <vector> + +#include "decision/decision_strategy.h" + +#include "expr/node.h" +#include "prop/cnf_stream.h" +#include "prop/prop_engine.h" +#include "prop/sat_solver_types.h" +#include "util/output.h" + +using namespace std; +using namespace CVC4::prop; +using namespace CVC4::decision; + +namespace CVC4 { + +class DecisionEngine { + + vector <DecisionStrategy* > d_enabledStrategies; + vector <DecisionStrategy* > d_needSimplifiedPreITEAssertions; + + vector <Node> d_assertions; + + // PropEngine* d_propEngine; + CnfStream* d_cnfStream; + DPLLSatSolverInterface* d_satSolver; +public: + // Necessary functions + + /** Constructor, enables decision stragies based on options */ + DecisionEngine(); + + /** Destructor, currently does nothing */ + ~DecisionEngine() { + Trace("decision") << "Destroying decision engine" << std::endl; + } + + // void setPropEngine(PropEngine* pe) { + // // setPropEngine should not be called more than once + // Assert(d_propEngine == NULL); + // Assert(pe != NULL); + // d_propEngine = pe; + // } + + void setSatSolver(DPLLSatSolverInterface* ss) { + // setPropEngine should not be called more than once + Assert(d_satSolver == NULL); + Assert(ss != NULL); + d_satSolver = ss; + } + + void setCnfStream(CnfStream* cs) { + // setPropEngine should not be called more than once + Assert(d_cnfStream == NULL); + Assert(cs != NULL); + d_cnfStream = cs; + } + + + // Interface for External World to use our services + + /** Gets the next decision based on strategies that are enabled */ + SatLiteral getNext() { + SatLiteral ret = undefSatLiteral; + for(unsigned i = 0; i < d_enabledStrategies.size() + and ret == undefSatLiteral; ++i) { + ret = d_enabledStrategies[i]->getNext(); + } + return ret; + } + + /** + * This is called by SmtEngine, at shutdown time, just before + * destruction. It is important because there are destruction + * ordering issues between some parts of the system. For now, + * there's nothing to do here in the DecisionEngine. + */ + void shutdown() { + Trace("decision") << "Shutting down decision engine" << std::endl; + } + + + // External World helping us help the Strategies + + /** If one of the enabled strategies needs them */ + bool needSimplifiedPreITEAssertions() { + return d_needSimplifiedPreITEAssertions.size() > 0; + } + void informSimplifiedPreITEAssertions(const vector<Node> &assertions); + + + // Interface for Strategies to use stuff stored in Decision Engine + // (which was possibly requested by them on initialization) + + /** + * Get the assertions. Strategies are notified when these are available. + */ + const vector<Node>& getAssertions() { + return d_assertions; + } + + + // Interface for Strategies to get information about External World + + bool hasSatLiteral(Node n) { + return d_cnfStream->hasLiteral(n); + } + SatLiteral getSatLiteral(Node n) { + return d_cnfStream->getLiteral(n); + } + SatValue getSatValue(SatLiteral l) { + return d_satSolver->value(l); + } + Node getNode(SatLiteral l) { + return d_cnfStream->getNode(l); + } + +private: + /** + * Enable a particular decision strategy, also updating + * corresponding vector<DecisionStrategy*>-s is the engine + */ + void enableStrategy(DecisionStrategy* ds); + +};/* DecisionEngine class */ + +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__DECISION_ENGINE_H */ diff --git a/src/decision/decision_strategy.h b/src/decision/decision_strategy.h new file mode 100644 index 000000000..abcbbaace --- /dev/null +++ b/src/decision/decision_strategy.h @@ -0,0 +1,50 @@ +/********************* */ +/*! \file decision_strategy.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 Decision stategy + ** + ** Decision strategy + **/ + +#ifndef __CVC4__DECISION__DECISION_STRATEGY_H +#define __CVC4__DECISION__DECISION_STRATEGY_H + +#include "prop/sat_solver_types.h" + +namespace CVC4 { + +class DecisionEngine; + +namespace decision { + +class DecisionStrategy { +protected: + DecisionEngine* d_decisionEngine; +public: + DecisionStrategy(DecisionEngine* de) : + d_decisionEngine(de) { + } + + virtual ~DecisionStrategy() { } + + virtual prop::SatLiteral getNext() = 0; + + virtual bool needSimplifiedPreITEAssertions() { return false; } + + virtual void notifyAssertionsAvailable() { return; } +}; + +}/* decision namespace */ +}/* CVC4 namespace */ + +#endif /* __CVC4__DECISION__DECISION_STRATEGY_H */ diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp new file mode 100644 index 000000000..4b017ef45 --- /dev/null +++ b/src/decision/justification_heuristic.cpp @@ -0,0 +1,393 @@ +/********************* */ +/*! \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 -- note below. + ** + ** It needs access to the simplified but non-clausal formula. + **/ +/*****************************************************************************/ +/*! + *\file search_sat.cpp + *\brief Implementation of Search engine with generic external sat solver + * + * Author: Clark Barrett + * + * Created: Wed Dec 7 21:00:24 2005 + * + * <hr> + * + * License to use, copy, modify, sell and/or distribute this software + * and its documentation for any purpose is hereby granted without + * royalty, subject to the terms and conditions defined in the \ref + * LICENSE file provided with this distribution. + * + * <hr> + */ +/*****************************************************************************/ + +#include "justification_heuristic.h" + + +/*** + +Summary of the algorithm: + + + +***/ + +/* + +CVC3 code <----> this code + + value desiredVal + getValue(lit) litVal + +***/ + +void JustificationHeuristic::setJustified(SatVariable v) +{ + d_justified.insert(v); +} + +bool JustificationHeuristic::checkJustified(SatVariable v) +{ + return d_justified.find(v) != d_justified.end(); +} + +SatValue invertValue(SatValue v) +{ + if(v == SAT_VALUE_UNKNOWN) return SAT_VALUE_UNKNOWN; + else if(v == SAT_VALUE_TRUE) return SAT_VALUE_FALSE; + else return SAT_VALUE_TRUE; +} + +bool JustificationHeuristic::findSplitterRec(SatLiteral lit, SatValue desiredVal, SatLiteral* litDecision) +//bool SearchSat::findSplitterRec(Lit lit, Var::Val value, Lit* litDecision) +{ + // if(not ) { + // // Warning() << "JustificationHeuristic encountered a variable not in SatSolver." << std::endl; + // return false; + // // Assert(not lit.isNull()); + // } + + /** + * TODO -- Base case. Way CVC3 seems to handle is that it has + * literals correpsonding to true and false. We'll have to take care + * somewhere else. + */ + + // Var v = lit.getVar(); + SatVariable v = lit.getSatVariable(); + SatValue litVal = d_decisionEngine->getSatValue(lit); + + // if (lit.isFalse() || lit.isTrue()) return false; + if (v == 0) return false; + + + /* You'd better know what you want */ + // DebugAssert(value != Var::UNKNOWN, "expected known value"); + Assert(desiredVal != SAT_VALUE_UNKNOWN, "expected known value"); + + /* Good luck, hope you can get what you want */ + // DebugAssert(getValue(lit) == value || getValue(lit) == Var::UNKNOWN, + // "invariant violated"); + Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN, + "invariant voilated"); + + + if (checkJustified(v)) return false; + + if (lit.isNegated()) { + desiredVal = invertValue(desiredVal); + } + + Node node = d_decisionEngine->getNode(lit); + Trace("decision") << "lit = " << lit << std::endl; + Trace("decision") << node.getKind() << std::endl; + Trace("decision") << node << std::endl; + + /* + if (d_cnfManager->numFanins(v) == 0) { + if (getValue(v) != Var::UNKNOWN) { + setJustified(v); + return false; + } + else { + *litDecision = Lit(v, value == Var::TRUE_VAL); + return true; + } + } + */ + if(node.getNumChildren() == 0) { + if(litVal != SAT_VALUE_UNKNOWN) { + setJustified(v); + return false; + } else { + *litDecision = SatLiteral(v, desiredVal == SAT_VALUE_TRUE ); + return true; + } + } + + + /* + else if (d_cnfManager->concreteVar(v).isAbsAtomicFormula()) { + // This node represents a predicate with embedded ITE's + // We handle this case specially in order to catch the + // corner case when a variable is in its own fanin. + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + varTmp = litTmp.getVar(); + DebugAssert(!litTmp.isInverted(),"Expected positive fanin"); + if (checkJustified(varTmp)) continue; + DebugAssert(d_cnfManager->concreteVar(varTmp).getKind() == ITE, + "Expected ITE"); + DebugAssert(getValue(varTmp) == Var::TRUE_VAL,"Expected TRUE"); + Lit cIf = d_cnfManager->getFanin(varTmp,0); + Lit cThen = d_cnfManager->getFanin(varTmp,1); + Lit cElse = d_cnfManager->getFanin(varTmp,2); + if (getValue(cIf) == Var::UNKNOWN) { + if (getValue(cElse) == Var::TRUE_VAL || + getValue(cThen) == Var::FALSE_VAL) { + ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); + } + else { + ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); + } + if (!ret) { + cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; + DebugAssert(false,"No controlling input found (1)"); + } + return true; + } + else if (getValue(cIf) == Var::TRUE_VAL) { + if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { + return true; + } + if (cThen.getVar() != v && + (getValue(cThen) == Var::UNKNOWN || + getValue(cThen) == Var::TRUE_VAL) && + findSplitterRec(cThen, Var::TRUE_VAL, litDecision)) { + return true; + } + } + else { + if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { + return true; + } + if (cElse.getVar() != v && + (getValue(cElse) == Var::UNKNOWN || + getValue(cElse) == Var::TRUE_VAL) && + findSplitterRec(cElse, Var::TRUE_VAL, litDecision)) { + return true; + } + } + setJustified(varTmp); + } + if (getValue(v) != Var::UNKNOWN) { + setJustified(v); + return false; + } + else { + *litDecision = Lit(v, value == Var::TRUE_VAL); + return true; + } + } + + int kind = d_cnfManager->concreteVar(v).getKind(); + Var::Val valHard = Var::FALSE_VAL; + switch (kind) { + case AND: + valHard = Var::TRUE_VAL; + case OR: + if (value == valHard) { + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + if (findSplitterRec(litTmp, valHard, litDecision)) { + return true; + } + } + DebugAssert(getValue(v) == valHard, "Output should be justified"); + setJustified(v); + return false; + } + else { + Var::Val valEasy = Var::invertValue(valHard); + n = d_cnfManager->numFanins(v); + for (i=0; i < n; ++i) { + litTmp = d_cnfManager->getFanin(v, i); + if (getValue(litTmp) != valHard) { + if (findSplitterRec(litTmp, valEasy, litDecision)) { + return true; + } + DebugAssert(getValue(v) == valEasy, "Output should be justified"); + setJustified(v); + return false; + } + } + DebugAssert(false, "No controlling input found (2)"); + } + break; + case IMPLIES: + DebugAssert(d_cnfManager->numFanins(v) == 2, "Expected 2 fanins"); + if (value == Var::FALSE_VAL) { + litTmp = d_cnfManager->getFanin(v, 0); + if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) { + return true; + } + litTmp = d_cnfManager->getFanin(v, 1); + if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::FALSE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + else { + litTmp = d_cnfManager->getFanin(v, 0); + if (getValue(litTmp) != Var::TRUE_VAL) { + if (findSplitterRec(litTmp, Var::FALSE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + litTmp = d_cnfManager->getFanin(v, 1); + if (getValue(litTmp) != Var::FALSE_VAL) { + if (findSplitterRec(litTmp, Var::TRUE_VAL, litDecision)) { + return true; + } + DebugAssert(getValue(v) == Var::TRUE_VAL, "Output should be justified"); + setJustified(v); + return false; + } + DebugAssert(false, "No controlling input found (3)"); + } + break; + case IFF: { + litTmp = d_cnfManager->getFanin(v, 0); + Var::Val val = getValue(litTmp); + if (val != Var::UNKNOWN) { + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + if (value == Var::FALSE_VAL) val = Var::invertValue(val); + litTmp = d_cnfManager->getFanin(v, 1); + + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + else { + val = getValue(d_cnfManager->getFanin(v, 1)); + if (val == Var::UNKNOWN) val = Var::FALSE_VAL; + if (value == Var::FALSE_VAL) val = Var::invertValue(val); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(false, "Unable to find controlling input (4)"); + } + break; + } + case XOR: { + litTmp = d_cnfManager->getFanin(v, 0); + Var::Val val = getValue(litTmp); + if (val != Var::UNKNOWN) { + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + if (value == Var::TRUE_VAL) val = Var::invertValue(val); + litTmp = d_cnfManager->getFanin(v, 1); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + else { + val = getValue(d_cnfManager->getFanin(v, 1)); + if (val == Var::UNKNOWN) val = Var::FALSE_VAL; + if (value == Var::TRUE_VAL) val = Var::invertValue(val); + if (findSplitterRec(litTmp, val, litDecision)) { + return true; + } + DebugAssert(false, "Unable to find controlling input (5)"); + } + break; + } + case ITE: { + Lit cIf = d_cnfManager->getFanin(v, 0); + Lit cThen = d_cnfManager->getFanin(v, 1); + Lit cElse = d_cnfManager->getFanin(v, 2); + if (getValue(cIf) == Var::UNKNOWN) { + if (getValue(cElse) == value || + getValue(cThen) == Var::invertValue(value)) { + ret = findSplitterRec(cIf, Var::FALSE_VAL, litDecision); + } + else { + ret = findSplitterRec(cIf, Var::TRUE_VAL, litDecision); + } + if (!ret) { + cout << d_cnfManager->concreteVar(cIf.getVar()) << endl; + DebugAssert(false,"No controlling input found (6)"); + } + return true; + } + else if (getValue(cIf) == Var::TRUE_VAL) { + if (findSplitterRec(cIf, Var::TRUE_VAL, litDecision)) { + return true; + } + if (cThen.isVar() && cThen.getVar() != v && + (getValue(cThen) == Var::UNKNOWN || + getValue(cThen) == value) && + findSplitterRec(cThen, value, litDecision)) { + return true; + } + } + else { + if (findSplitterRec(cIf, Var::FALSE_VAL, litDecision)) { + return true; + } + if (cElse.isVar() && cElse.getVar() != v && + (getValue(cElse) == Var::UNKNOWN || + getValue(cElse) == value) && + findSplitterRec(cElse, value, litDecision)) { + return true; + } + } + DebugAssert(getValue(v) == value, "Output should be justified"); + setJustified(v); + return false; + } + default: + DebugAssert(false, "Unexpected Boolean operator"); + break; + } + FatalAssert(false, "Should be unreachable"); + ------------------------------------------------ */ + return false; + + Unreachable(); + +}/* findRecSplit method */ 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 */ |