From ec7ea8a763f6b5647ab53db289131082b69f61b4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 25 Sep 2017 15:21:59 -0400 Subject: [PATCH] redo length testing with concrete length, linear search only --- src/smt/theory_str.cpp | 35 +++++++++++++++-------------------- 1 file changed, 15 insertions(+), 20 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index fe00bb35d..70e564a50 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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);