diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 18:19:02 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:05:10 -0500 |
commit | 518ef0afb92533cfb059b05b4af3e2882d24c5a7 (patch) | |
tree | ceb535ed14258b40da02f26c9a408808b4a57a9d /src/decision/justification_heuristic.h | |
parent | ac53a61122c39c421ee7a8c10e2604ce468fc6f3 (diff) |
refactoring justification_heuristic code
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 32 |
1 files changed, 21 insertions, 11 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index 272dffc88..b0f42c583 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -84,6 +84,9 @@ class JustificationHeuristic : public ITEDecisionStrategy { * function */ hash_set<TNode,TNodeHashFunction> d_visitedComputeITE; + + /** current decision for the recursive call */ + SatLiteral d_curDecision; public: JustificationHeuristic(CVC4::DecisionEngine* de, context::Context *uc, @@ -95,7 +98,11 @@ public: d_giveup("decision::jh::giveup", 0), d_timestat("decision::jh::time"), d_assertions(uc), - d_iteAssertions(uc) { + d_iteAssertions(uc), + d_iteCache(), + d_visited(), + d_visitedComputeITE(), + d_curDecision() { StatisticsRegistry::registerStat(&d_helfulness); StatisticsRegistry::registerStat(&d_giveup); StatisticsRegistry::registerStat(&d_timestat); @@ -194,22 +201,17 @@ public: private: SatLiteral findSplitter(TNode node, SatValue desiredVal) { - bool ret; - SatLiteral litDecision; - ret = findSplitterRec(node, desiredVal, &litDecision); - if(ret == true) { - Debug("decision") << "Yippee!!" << std::endl; + d_curDecision = undefSatLiteral; + if(findSplitterRec(node, desiredVal)) { ++d_helfulness; - return litDecision; - } else { - return undefSatLiteral; - } + } + return d_curDecision; } /** * Do all the hard work. */ - bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision); + bool findSplitterRec(TNode node, SatValue value); /* Helper functions */ void setJustified(TNode); @@ -224,6 +226,14 @@ private: /* Compute all term-ITEs in a node recursively */ void computeITEs(TNode n, IteList &l); + + bool handleAndOrEasy(TNode node, SatValue desiredVal); + bool handleAndOrHard(TNode node, SatValue desiredVal); + bool handleBinaryEasy(TNode node1, SatValue desiredVal1, + TNode node2, SatValue desiredVal2); + bool handleBinaryHard(TNode node1, SatValue desiredVal1, + TNode node2, SatValue desiredVal2); + };/* class JustificationHeuristic */ }/* namespace decision */ |