diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:22:31 -0500 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2013-02-16 19:22:47 -0500 |
commit | 8f341b6dc401a780f4a84fd4c51063242e885149 (patch) | |
tree | db5e6c86ad632015edd4e3dac6f1812a53291c17 /src/decision/justification_heuristic.cpp | |
parent | 518ef0afb92533cfb059b05b4af3e2882d24c5a7 (diff) |
decision/: justification: refactor ITE out
Diffstat (limited to 'src/decision/justification_heuristic.cpp')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 77 |
1 files changed, 41 insertions, 36 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index d384e2b78..4e924de9e 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -256,42 +256,9 @@ bool JustificationHeuristic::findSplitterRec(TNode node, break; } - case kind::ITE: { - //[0]: if, [1]: then, [2]: else - SatValue ifVal = tryGetSatValue(node[0]); - if (ifVal == SAT_VALUE_UNKNOWN) { - - // are we better off trying false? if not, try true - SatValue ifDesiredVal = - (tryGetSatValue(node[2]) == desiredVal || - tryGetSatValue(node[1]) == invertValue(desiredVal)) - ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; - - if(findSplitterRec(node[0], ifDesiredVal)) { - return true; - } - Assert(false, "No controlling input found (6)"); - } else { - - // Try to justify 'if' - if (findSplitterRec(node[0], ifVal)) { - return true; - } - - // If that was successful, we need to go into only one of 'then' - // or 'else' - int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; - int chVal = tryGetSatValue(node[ch]); - if( (chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal) - && findSplitterRec(node[ch], desiredVal) ) { - return true; - } - } - Assert(litPresent == false || litVal == desiredVal, - "Output should be justified"); - setJustified(node); - return false; - } + case kind::ITE: + ret = handleITE(node, desiredVal); + break; default: Assert(false, "Unexpected Boolean operator"); @@ -348,3 +315,41 @@ bool JustificationHeuristic::handleBinaryHard return true; return findSplitterRec(node2, desiredVal2); } + +bool JustificationHeuristic::handleITE(TNode node, SatValue desiredVal) +{ + Debug("decision::jh") << " handleITE (" << node << ", " + << desiredVal << std::endl; + + //[0]: if, [1]: then, [2]: else + SatValue ifVal = tryGetSatValue(node[0]); + if (ifVal == SAT_VALUE_UNKNOWN) { + + // are we better off trying false? if not, try true [CHOICE] + SatValue ifDesiredVal = + (tryGetSatValue(node[2]) == desiredVal || + tryGetSatValue(node[1]) == invertValue(desiredVal)) + ? SAT_VALUE_FALSE : SAT_VALUE_TRUE; + + if(findSplitterRec(node[0], ifDesiredVal)) return true; + + Assert(false, "No controlling input found (6)"); + } else { + // Try to justify 'if' + if(findSplitterRec(node[0], ifVal)) return true; + + // If that was successful, we need to go into only one of 'then' + // or 'else' + int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2; + + // STALE code: remove after tests or mar 2013, whichever earlier + // int chVal = tryGetSatValue(node[ch]); + // Assert(chVal == SAT_VALUE_UNKNOWN || chVal == desiredVal); + // end STALE code: remove + + if( findSplitterRec(node[ch], desiredVal) ) { + return true; + } + }// else (...ifVal...) + return false; +} |