From b2af690c6d38bbbaeaae4e0311eb69ab48fa79cb Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 22 Sep 2017 12:31:46 -0400 Subject: [PATCH 1/4] enable binary search for theory_str --- src/smt/params/smt_params_helper.pyg | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index d6ca8c9b2..937aa6a2b 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -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'), From 317e2b189848f65cd7d55d08acbf65f2111b5824 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 22 Sep 2017 12:32:13 -0400 Subject: [PATCH 2/4] take shortcuts during length testing when length is known from integer theory --- src/smt/theory_str.cpp | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 8a141665c..fe00bb35d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -10229,9 +10229,30 @@ namespace smt { expr * theory_str::gen_len_val_options_for_free_var(expr * freeVar, expr * lenTesterInCbEq, zstring lenTesterValue) { ast_manager & m = get_manager(); + context & ctx = get_context(); 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); From ec7ea8a763f6b5647ab53db289131082b69f61b4 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Mon, 25 Sep 2017 15:21:59 -0400 Subject: [PATCH 3/4] 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); From 7b536e910ee0dba7088f47f5f69fd3392998c8a6 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Fri, 13 Oct 2017 11:39:33 -0400 Subject: [PATCH 4/4] take shortcuts during binary search length testing when length is known from integer theory --- src/smt/theory_str.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 70e564a50..644863919 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -10216,6 +10216,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(binary_search_len_tester_stack, freeVar)); 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) { ast_manager & m = get_manager(); - context & ctx = get_context(); TRACE("str", tout << "gen for free var " << mk_ismt2_pp(freeVar, m) << std::endl;);