diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-08-29 21:15:33 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-08-29 21:15:33 -0700 |
commit | d45b5e1ae2b0d4812e41673bba16de0114070fc1 (patch) | |
tree | ba111f037eaf2164d2903762072dfde434099fd0 /src/theory | |
parent | 974fc1d23c2b6091c26cf316964c4c16c5e2733f (diff) |
Better heuristic for str.code/re.range (#3220)
To make sure that our `str.code` function is injectve (except for -1 in
the codomain), we send the inference that `str.code(x) == -1 v
str.code(x) != str.code(y) v x == y` for each pair of `str.code` terms.
Because of the order of disjuncts, `str.code(x) != str.code(y)` was
usually assigned true. This in turn lead to a difficult problem for the
arithmetic engine if there were more `str.code` applications than the
size of the domain. E.g. if we had `0 <= str.code(xi) < 10` for 0 <= i
<= 10, then the arithmetic engine had a difficult time finding a
conflict. This PR improves the heuristic by setting the phase of
`str.code(x) != str.code(y)` to false, so we prefer to keep the
`str.code` values equal instead of trying to make them different.
This change is also reflected in the models produced for inputs
involving `str.code`: Previously, we were producing models with
different values for the `str.code` whereas now the models are much more
uniform.
The PR adds two regressions, one testing `str.code` performance directly
and one testing it for `str.code` terms generated by `re.range`.
Signed-off-by: Andres Noetzli <anoetzli@amazon.com>
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/strings/inference_manager.cpp | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 1 |
2 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/strings/inference_manager.cpp b/src/theory/strings/inference_manager.cpp index 6cc1e7b44..97f9666bd 100644 --- a/src/theory/strings/inference_manager.cpp +++ b/src/theory/strings/inference_manager.cpp @@ -274,6 +274,7 @@ bool InferenceManager::sendSplit(Node a, Node b, const char* c, bool preq) void InferenceManager::sendPhaseRequirement(Node lit, bool pol) { + lit = Rewriter::rewrite(lit); d_pendingReqPhase[lit] = pol; } diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 2f51000ab..65f06c008 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2800,6 +2800,7 @@ void TheoryStrings::checkCodes() Node eqn = c1[0].eqNode(c2[0]); // str.code(x)==-1 V str.code(x)!=str.code(y) V x==y Node inj_lem = nm->mkNode(kind::OR, eq_no, deq, eqn); + d_im.sendPhaseRequirement(deq, false); d_im.sendInference(d_empty_vec, inj_lem, "Code_Inj"); } } |