mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

add experimental value tester caching to theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-11-02 13:05:16 -04:00
parent a61e1f17e8
commit 3ae336fa6f
2 changed files with 27 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/theory_str.cpp
View file

@ -41,6 +41,7 @@ theory_str::theory_str(ast_manager & m):
opt_DeferEQCConsistencyCheck(false), opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true), opt_CheckVariableScope(true),
opt_UseFastLengthTesterCache(true), opt_UseFastLengthTesterCache(true),
opt_UseFastValueTesterCache(true),
/* Internal setup */ /* Internal setup */
search_started(false), search_started(false),
m_autil(m), m_autil(m),
@ -7967,6 +7968,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
ptr_vector<expr> andList; ptr_vector<expr> andList;
for (long long i = l; i < h; i++) { 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()) )); orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()) ));
if (opt_AggressiveValueTesting) { if (opt_AggressiveValueTesting) {
literal l = mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()), false); 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]); 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))); andList.push_back(m.mk_eq(orList[orList.size() - 1], m.mk_eq(freeVar, strAst)));
} }
if (!coverAll) { if (!coverAll) {

15
src/smt/theory_str.h
View file

@ -89,6 +89,12 @@ namespace smt {
typedef union_find<theory_str> th_union_find; typedef union_find<theory_str> th_union_find;
typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map; typedef map<rational, expr*, obj_hash<rational>, default_eq<rational> > rational_map;
struct str_hash_proc {
unsigned operator()(std::string const & s) const {
return string_hash(s.c_str(), static_cast<unsigned>(s.length()), 17);
}
};
typedef map<std::string, expr*, str_hash_proc, default_eq<std::string> > string_map;
protected: protected:
// Some options that control how the solver operates. // Some options that control how the solver operates.
@ -176,6 +182,13 @@ namespace smt {
*/ */
bool opt_UseFastLengthTesterCache; 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; bool search_started;
arith_util m_autil; arith_util m_autil;
str_util m_strutil; str_util m_strutil;
@ -271,6 +284,8 @@ namespace smt {
// used when opt_FastLengthTesterCache is true // used when opt_FastLengthTesterCache is true
rational_map lengthTesterCache; rational_map lengthTesterCache;
// used when opt_FastValueTesterCache is true
string_map valueTesterCache;
th_union_find m_find; th_union_find m_find;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;