mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 11:25:51 +00:00
Code Activity

take shortcuts during binary search length testing when length is known from integer theory

Browse source
This commit is contained in:
Murphy Berzish 2017-10-13 11:39:33 -04:00
parent ec7ea8a763
commit 7b536e910e
1 changed files with 10 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/smt/theory_str.cpp
View file

@ -10216,6 +10216,16 @@ namespace smt {
} }
refresh_theory_var(firstTester); refresh_theory_var(firstTester);
{
rational freeVar_len_value;
if (get_len_value(freeVar, freeVar_len_value)) {
TRACE("str", tout << "special case: length of freeVar is known to be " << freeVar_len_value << std::endl;);
midPoint = freeVar_len_value;
upperBound = midPoint * 2;
windowSize = upperBound;
}
}
binary_search_len_tester_stack[freeVar].push_back(firstTester); binary_search_len_tester_stack[freeVar].push_back(firstTester);
m_trail_stack.push(binary_search_trail<theory_str>(binary_search_len_tester_stack, freeVar)); m_trail_stack.push(binary_search_trail<theory_str>(binary_search_len_tester_stack, freeVar));
binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize); binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize);
@ -10244,7 +10254,6 @@ namespace smt {
expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) {
ast_manager & m = get_manager(); ast_manager & m = get_manager();
context & ctx = get_context();
TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;); TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;);