diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-17 10:26:46 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-04-17 08:26:46 -0700 |
commit | 5b00f8d6804bf9f71d6169634341011f99d59b8b (patch) | |
tree | 001bef3833e07195ce2119978f0098d681a2a5ef /src | |
parent | 29a06b999c4637197282405df7040d6773bd3858 (diff) |
Fix extended function decomposition (#2960)
Fixes #2958.
The issue was: we had substr(x,0,2) in R, and the "derivable substitution" modifed this to substr(substr(x,0,2),0,2) in R, since substr(x,0,2) was the representative of x (which is a bad choice, but regardless is legal). Then decomposition inference asked "can i reduce substr(substr(x,0,2),0,2) in R"? It determines substr(substr(x,0,2),0,2) in R rewrites to substr(x,0,2) in R, which is already true. However, substr(x,0,2) in R was what we started with.
The fix makes things much more conservative: we never mark extended functions reduced based on decomposition, since there isnt a strong argument based on an ordering.
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 26 |
1 files changed, 9 insertions, 17 deletions
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 6333bfee1..8731bd1a5 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -1705,8 +1705,8 @@ void TheoryStrings::checkExtfEval( int effort ) { } else { - bool reduced = false; - if (!einfo.d_const.isNull() && nrc.getType().isBoolean()) + // if this was a predicate which changed after substitution + rewriting + if (!einfo.d_const.isNull() && nrc.getType().isBoolean() && nrc != n) { bool pol = einfo.d_const == d_true; Node nrcAssert = pol ? nrc : nrc.negate(); @@ -1716,23 +1716,15 @@ void TheoryStrings::checkExtfEval( int effort ) { Trace("strings-extf-debug") << " decomposable..." << std::endl; Trace("strings-extf") << " resolve extf : " << sn << " -> " << nrc << ", const = " << einfo.d_const << std::endl; - reduced = sendInternalInference( + // We send inferences internal here, which may help show unsat. + // However, we do not make a determination whether n can be marked + // reduced since this argument may be circular: we may infer than n + // can be reduced to something else, but that thing may argue that it + // can be reduced to n, in theory. + sendInternalInference( einfo.d_exp, nrcAssert, effort == 0 ? "EXTF_d" : "EXTF_d-N"); - if (!reduced) - { - Trace("strings-extf") << "EXT: could not fully reduce "; - Trace("strings-extf") - << nAssert << " via " << nrcAssert << std::endl; - } - } - if (reduced) - { - getExtTheory()->markReduced(n); - } - else - { - to_reduce = nrc; } + to_reduce = nrc; } }else{ to_reduce = sterms[i]; |