mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

redo length testing with concrete length, linear search only

Browse source
This commit is contained in:
Murphy Berzish 2017-09-25 15:21:59 -04:00
parent 317e2b1898
commit ec7ea8a763
1 changed files with 15 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

35
src/smt/theory_str.cpp
View file

@ -9887,6 +9887,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);
@ -10233,26 +10248,6 @@ namespace smt {
TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;);
// special case: if we would be length testing for the first time,
// but already know a value for length from the integer solver,
// don't give any other options
{
rational freeVar_len;
if (lenTesterInCbEq == NULL && get_len_value(freeVar, freeVar_len)) {
TRACE("str", tout << "length of free var " << mk_pp(freeVar, m) << " already given to be " << freeVar_len << std::endl;);
expr * newTester = mk_internal_lenTest_var(freeVar, 0);
expr * concreteLength_lhs = ctx.mk_eq_atom(newTester, mk_string(freeVar_len.to_string().c_str()));
expr * concreteLength_rhs = ctx.mk_eq_atom(mk_strlen(freeVar), m_autil.mk_numeral(freeVar_len, true));
expr * concreteLength_assert = ctx.mk_eq_atom(concreteLength_lhs, concreteLength_rhs);
m_trail.push_back(concreteLength_assert);
TRACE("str", tout << mk_pp(concreteLength_assert, m) << std::endl;);
expr * valueAssert = gen_free_var_options(freeVar, newTester, zstring(freeVar_len.to_string().c_str()), NULL, zstring(""));
m_trail.push_back(valueAssert);
TRACE("str", tout << mk_pp(valueAssert, m) << std::endl;);
return m.mk_and(concreteLength_assert, valueAssert);
}
}
if (m_params.m_UseBinarySearch) {
TRACE("str", tout << "using binary search heuristic" << std::endl;);
return binary_search_length_test(freeVar, lenTesterInCbEq, lenTesterValue);