diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:58:07 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:58:07 -0500 |
commit | 3e495881142c623d9099869dba1147b6ea5ebae5 (patch) | |
tree | b214a2ad56a9a9a108969dc9a748aea79b66b7d5 /src/decision/justification_heuristic.h | |
parent | 8f341b6dc401a780f4a84fd4c51063242e885149 (diff) |
decision/ : jh: refactor embedded ITE, other minor
other minor: cleanup some remaning fragments of GiveUpException(),
hopefully all is gone now.
Diffstat (limited to 'src/decision/justification_heuristic.h')
-rw-r--r-- | src/decision/justification_heuristic.h | 15 |
1 files changed, 3 insertions, 12 deletions
diff --git a/src/decision/justification_heuristic.h b/src/decision/justification_heuristic.h index a1a39cd6a..4be436351 100644 --- a/src/decision/justification_heuristic.h +++ b/src/decision/justification_heuristic.h @@ -36,13 +36,6 @@ namespace CVC4 { namespace decision { -class GiveUpException : public Exception { -public: - GiveUpException() : - Exception("justification heuristic: giving up") { - } -};/* class GiveUpException */ - class JustificationHeuristic : public ITEDecisionStrategy { typedef std::vector<pair<TNode,TNode> > IteList; typedef hash_map<TNode,IteList,TNodeHashFunction> IteCache; @@ -138,11 +131,8 @@ public: SatValue desiredVal = SAT_VALUE_TRUE; SatLiteral litDecision; - try { - litDecision = findSplitter(d_assertions[i], desiredVal); - }catch(GiveUpException &e) { - return prop::undefSatLiteral; - } + + litDecision = findSplitter(d_assertions[i], desiredVal); if(litDecision != undefSatLiteral) { d_prvsIndex = i; @@ -234,6 +224,7 @@ private: bool handleBinaryHard(TNode node1, SatValue desiredVal1, TNode node2, SatValue desiredVal2); bool handleITE(TNode node, SatValue desiredVal); + bool handleEmbeddedITEs(TNode node); };/* class JustificationHeuristic */ }/* namespace decision */ |