diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-02 14:45:21 -0600 |
| commit | 1f4b954a2cc7667a56a3007fa75c125fba93ed23 (patch) | |
| tree | ea8734e89aa5fba170781c7148d3fd886c597d4e /src/decision | |
| parent | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (diff) | |
Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
Diffstat (limited to 'src/decision')
| -rw-r--r-- | src/decision/justification_heuristic.cpp | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index cfa478c7d..c0d65cbe6 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -142,10 +142,10 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D inline void computeXorIffDesiredValues (Kind k, SatValue desiredVal, SatValue &desiredVal1, SatValue &desiredVal2) { - Assert(k == kind::IFF || k == kind::XOR); + Assert(k == kind::EQUAL || k == kind::XOR); bool shouldInvert = - (desiredVal == SAT_VALUE_TRUE && k == kind::IFF) || + (desiredVal == SAT_VALUE_TRUE && k == kind::EQUAL) || (desiredVal == SAT_VALUE_FALSE && k == kind::XOR); if(desiredVal1 == SAT_VALUE_UNKNOWN && @@ -449,6 +449,10 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) /* What type of node is this */ Kind k = node.getKind(); theory::TheoryId tId = theory::kindToTheoryId(k); + bool isAtom = + (k == kind::BOOLEAN_TERM_VARIABLE ) || + ( (tId != theory::THEORY_BOOL) && + (k != kind::EQUAL || (!node[0].getType().isBoolean())) ); /* Some debugging stuff */ Debug("decision::jh") << "kind = " << k << std::endl @@ -459,7 +463,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) /** * If not in theory of booleans, check if this is something to split-on. */ - if(tId != theory::THEORY_BOOL) { + if(isAtom) { // if node has embedded ites, resolve that first if(handleEmbeddedITEs(node) == FOUND_SPLITTER) return FOUND_SPLITTER; @@ -516,7 +520,7 @@ JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal) break; case kind::XOR: - case kind::IFF: { + case kind::EQUAL: { SatValue desiredVal1 = tryGetSatValue(node[0]); SatValue desiredVal2 = tryGetSatValue(node[1]); computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2); |