From 3da78f9d8015676b36e3869a3f9a665aa29f1d10 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 1 Nov 2016 20:35:01 -0400 Subject: [PATCH 1/5] experimental cached length testers in theory_str --- src/smt/theory_str.cpp | 24 +++++++++++++++++++++--- src/smt/theory_str.h | 12 ++++++++++++ 2 files changed, 33 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 1050e4a66..45b715247 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -40,6 +40,7 @@ theory_str::theory_str(ast_manager & m): opt_DisableIntegerTheoryIntegration(false), opt_DeferEQCConsistencyCheck(false), opt_CheckVariableScope(true), + opt_UseFastLengthTesterCache(true), /* Internal setup */ search_started(false), m_autil(m), @@ -8536,9 +8537,25 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr ); for (int i = l; i < h; ++i) { - std::string i_str = int_to_string(i); - expr_ref str_indicator(m_strutil.mk_string(i_str), m); - expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); // ARGUMENT 2 IS BOGUS! WRONG SORT + expr_ref str_indicator(m); + if (opt_UseFastLengthTesterCache) { + rational ri(i); + expr * lookup_val; + if(lengthTesterCache.find(ri, lookup_val)) { + str_indicator = expr_ref(lookup_val, m); + } else { + // no match; create and insert + std::string i_str = int_to_string(i); + expr_ref new_val(m_strutil.mk_string(i_str), m); + lengthTesterCache.insert(ri, new_val); + m_trail.push_back(new_val); + str_indicator = expr_ref(new_val, m); + } + } else { + std::string i_str = int_to_string(i); + expr_ref str_indicator(m_strutil.mk_string(i_str), m); + } + expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); orList.push_back(or_expr); if (opt_AggressiveLengthTesting) { @@ -8551,6 +8568,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr andList.push_back(and_expr); } + // TODO cache mk_string("more") orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more"))); if (opt_AggressiveLengthTesting) { literal l = mk_eq(indicator, m_strutil.mk_string("more"), false); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 43552f31a..9b41c583b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -88,6 +88,8 @@ namespace smt { typedef trail_stack th_trail_stack; typedef union_find th_union_find; + typedef map, default_eq > rational_map; + protected: // Some options that control how the solver operates. @@ -167,6 +169,13 @@ namespace smt { */ bool opt_CheckVariableScope; + /* + * If UseFastLengthTesterCache is set to true, + * length tester terms will not be generated from scratch each time they are needed, + * but will be saved in a map and looked up. + */ + bool opt_UseFastLengthTesterCache; + bool search_started; arith_util m_autil; str_util m_strutil; @@ -260,6 +269,9 @@ namespace smt { obj_pair_map concat_astNode_map; + // used when opt_FastLengthTesterCache is true + rational_map lengthTesterCache; + th_union_find m_find; th_trail_stack m_trail_stack; theory_var get_var(expr * n) const; From a61e1f17e872075cc784e06de4061a5b24941d5e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 2 Nov 2016 12:35:14 -0400 Subject: [PATCH 2/5] fix crash in gen_len_test_options when fast length testers are disabled --- src/smt/theory_str.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 45b715247..5f024dead 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -8553,7 +8553,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr } } else { std::string i_str = int_to_string(i); - expr_ref str_indicator(m_strutil.mk_string(i_str), m); + str_indicator = expr_ref(m_strutil.mk_string(i_str), m); } expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); orList.push_back(or_expr); From 3ae336fa6f178aa41403140c98d061a2ea560411 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 2 Nov 2016 13:05:16 -0400 Subject: [PATCH 3/5] add experimental value tester caching to theory_str --- src/smt/theory_str.cpp | 13 ++++++++++++- src/smt/theory_str.h | 15 +++++++++++++++ 2 files changed, 27 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 5f024dead..c7cbff04e 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -41,6 +41,7 @@ theory_str::theory_str(ast_manager & m): opt_DeferEQCConsistencyCheck(false), opt_CheckVariableScope(true), opt_UseFastLengthTesterCache(true), + opt_UseFastValueTesterCache(true), /* Internal setup */ search_started(false), m_autil(m), @@ -7967,6 +7968,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * ptr_vector andList; for (long long i = l; i < h; i++) { + // TODO can we share the val_indicator constants with the length tester cache? orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()) )); if (opt_AggressiveValueTesting) { literal l = mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()), false); @@ -7975,7 +7977,16 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * } std::string aStr = gen_val_string(len, options[i - l]); - expr * strAst = m_strutil.mk_string(aStr); + expr * strAst; + if (opt_UseFastValueTesterCache) { + if (!valueTesterCache.find(aStr, strAst)) { + strAst = m_strutil.mk_string(aStr); + valueTesterCache.insert(aStr, strAst); + m_trail.push_back(strAst); + } + } else { + strAst = m_strutil.mk_string(aStr); + } andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst))); } if (!coverAll) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 9b41c583b..b04e21fca 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -89,6 +89,12 @@ namespace smt { typedef union_find th_union_find; typedef map, default_eq > rational_map; + struct str_hash_proc { + unsigned operator()(std::string const & s) const { + return string_hash(s.c_str(), static_cast(s.length()), 17); + } + }; + typedef map > string_map; protected: // Some options that control how the solver operates. @@ -176,6 +182,13 @@ namespace smt { */ bool opt_UseFastLengthTesterCache; + /* + * If UseFastValueTesterCache is set to true, + * value tester terms will not be generated from scratch each time they are needed, + * but will be saved in a map and looked up. + */ + bool opt_UseFastValueTesterCache; + bool search_started; arith_util m_autil; str_util m_strutil; @@ -271,6 +284,8 @@ namespace smt { // used when opt_FastLengthTesterCache is true rational_map lengthTesterCache; + // used when opt_FastValueTesterCache is true + string_map valueTesterCache; th_union_find m_find; th_trail_stack m_trail_stack; From 521e0e175be66fcb5140ff3ac766ebb35ef3cd56 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 8 Nov 2016 14:23:10 -0500 Subject: [PATCH 4/5] refresh reused split vars in theory_str this fixes kaluza/unsat/big/7907, now SAT in ~30s --- src/smt/theory_str.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index c7cbff04e..a9a290ab1 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -2726,6 +2726,9 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) { t2 = varForBreakConcat[key2][1]; xorFlag = varForBreakConcat[key2][2]; } + // TODO do I need to refresh the xorFlag, which is an integer var, and if so, how? + refresh_theory_var(t1); + refresh_theory_var(t2); } // For split types 0 through 2, we can get away with providing @@ -3048,6 +3051,8 @@ void theory_str::process_concat_eq_type2(expr * concatAst1, expr * concatAst2) { temp1 = varForBreakConcat[key2][0]; xorFlag = varForBreakConcat[key2][1]; } + // TODO refresh xorFlag? + refresh_theory_var(temp1); } int splitType = -1; @@ -3361,6 +3366,7 @@ void theory_str::process_concat_eq_type3(expr * concatAst1, expr * concatAst2) { temp1 = varForBreakConcat[key2][0]; xorFlag = varForBreakConcat[key2][1]; } + refresh_theory_var(temp1); } @@ -3857,6 +3863,7 @@ void theory_str::process_concat_eq_type6(expr * concatAst1, expr * concatAst2) { commonVar = (entry2->second)[0]; xorFlag = (entry2->second)[1]; } + refresh_theory_var(commonVar); } expr ** or_item = alloc_svect(expr*, (overlapLen.size() + 1)); From 61d1d5e8b0a87381ac429a06786c3db28c4e9aa2 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 8 Nov 2016 15:20:47 -0500 Subject: [PATCH 5/5] add cache for length terms to theory_str, but it seems to slow things down so I disabled it --- src/smt/theory_str.cpp | 17 +++++++++++++++-- src/smt/theory_str.h | 3 +++ 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a9a290ab1..4e5e45ce7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -696,8 +696,21 @@ app * theory_str::mk_strlen(expr * e) { int len = strlen(strval); return m_autil.mk_numeral(rational(len), true); } else { - expr * args[1] = {e}; - return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args); + if (false) { + // use cache + app * lenTerm = NULL; + if (!length_ast_map.find(e, lenTerm)) { + expr * args[1] = {e}; + lenTerm = get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args); + length_ast_map.insert(e, lenTerm); + m_trail.push_back(lenTerm); + } + return lenTerm; + } else { + // always regen + expr * args[1] = {e}; + return get_manager().mk_app(get_id(), OP_STRLEN, 0, 0, 1, args); + } } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index b04e21fca..48ebf049b 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -287,6 +287,9 @@ namespace smt { // used when opt_FastValueTesterCache is true string_map valueTesterCache; + // cache mapping each string S to Length(S) + obj_map length_ast_map; + th_union_find m_find; th_trail_stack m_trail_stack; theory_var get_var(expr * n) const;