mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

finite overlap models with binary search

Browse source
This commit is contained in:
Murphy Berzish 2017-01-17 14:49:57 -05:00
parent 794e210958
commit a570149b57
1 changed files with 9 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_str.cpp
View file

@ -6681,7 +6681,15 @@ void theory_str::finite_model_test(expr * testvar, expr * str) {
}
// check for any sort of existing length tester we might interfere with
if (m_params.m_UseBinarySearch) {
NOT_IMPLEMENTED_YET();
if (binary_search_len_tester_stack.contains(v) && !binary_search_len_tester_stack[v].empty()) {
TRACE("t_str_detail", tout << "already found existing length testers for " << mk_pp(v, m) << std::endl;);
continue;
} else {
// start binary search as normal
expr_ref implLhs(ctx.mk_eq_atom(testvar, str), m);
expr_ref implRhs(binary_search_length_test(v, NULL, ""), m);
assert_implication(implLhs, implRhs);
}
} else {
bool map_effectively_empty = false;
if (fvar_len_count_map.find(v) == fvar_len_count_map.end()) {