mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Merge pull request #1337 from mtrberzi/fix-length-testing
Optimizations for length testing in theory_str
This commit is contained in:
commit
29d643cc23
|
@ -74,7 +74,7 @@ def_module_params(module_name='smt',
|
|||
('str.fast_length_tester_cache', BOOL, False, 'cache length tester constants instead of regenerating them'),
|
||||
('str.fast_value_tester_cache', BOOL, True, 'cache value tester constants instead of regenerating them'),
|
||||
('str.string_constant_cache', BOOL, True, 'cache all generated string constants generated from anywhere in theory_str'),
|
||||
('str.use_binary_search', BOOL, False, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
|
||||
('str.use_binary_search', BOOL, True, 'use a binary search heuristic for finding concrete length values for free variables in theory_str (set to False to use linear search)'),
|
||||
('str.binary_search_start', UINT, 64, 'initial upper bound for theory_str binary search'),
|
||||
('theory_aware_branching', BOOL, False, 'Allow the context to use extra information from theory solvers regarding literal branching prioritization.'),
|
||||
('str.finite_overlap_models', BOOL, False, 'attempt a finite model search for overlapping variables instead of completely giving up on the arrangement'),
|
||||
|
|
|
@ -9907,6 +9907,21 @@ namespace smt {
|
|||
expr_ref freeVarLen(mk_strlen(freeVar), m);
|
||||
SASSERT(freeVarLen);
|
||||
|
||||
{
|
||||
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;);
|
||||
expr_ref concreteOption(ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ), m);
|
||||
expr_ref concreteValue(ctx.mk_eq_atom(
|
||||
ctx.mk_eq_atom(indicator, mk_string(freeVar_len_value.to_string().c_str()) ),
|
||||
ctx.mk_eq_atom(freeVarLen, m_autil.mk_numeral(freeVar_len_value, true))), m);
|
||||
expr_ref finalAxiom(m.mk_and(concreteOption, concreteValue), m);
|
||||
SASSERT(finalAxiom);
|
||||
m_trail.push_back(finalAxiom);
|
||||
return finalAxiom;
|
||||
}
|
||||
}
|
||||
|
||||
expr_ref_vector orList(m);
|
||||
expr_ref_vector andList(m);
|
||||
|
||||
|
@ -10221,6 +10236,16 @@ namespace smt {
|
|||
}
|
||||
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);
|
||||
m_trail_stack.push(binary_search_trail<theory_str>(binary_search_len_tester_stack, freeVar));
|
||||
binary_search_info new_info(lowerBound, midPoint, upperBound, windowSize);
|
||||
|
|
Loading…
Reference in a new issue