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

experimental cached length testers in theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-11-01 20:35:01 -04:00
parent 452eed6626
commit 3da78f9d80
2 changed files with 33 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

20
src/smt/theory_str.cpp
View file

@ -40,6 +40,7 @@ theory_str::theory_str(ast_manager & m):
opt_DisableIntegerTheoryIntegration(false), opt_DisableIntegerTheoryIntegration(false),
opt_DeferEQCConsistencyCheck(false), opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true), opt_CheckVariableScope(true),
opt_UseFastLengthTesterCache(true),
/* Internal setup */ /* Internal setup */
search_started(false), search_started(false),
m_autil(m), 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) { for (int i = l; i < h; ++i) {
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); std::string i_str = int_to_string(i);
expr_ref str_indicator(m_strutil.mk_string(i_str), m); 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 or_expr(ctx.mk_eq_atom(indicator, str_indicator), m);
orList.push_back(or_expr); orList.push_back(or_expr);
if (opt_AggressiveLengthTesting) { 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); andList.push_back(and_expr);
} }
// TODO cache mk_string("more")
orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more"))); orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more")));
if (opt_AggressiveLengthTesting) { if (opt_AggressiveLengthTesting) {
literal l = mk_eq(indicator, m_strutil.mk_string("more"), false); literal l = mk_eq(indicator, m_strutil.mk_string("more"), false);

12
src/smt/theory_str.h
View file

@ -88,6 +88,8 @@ namespace smt {
typedef trail_stack<theory_str> th_trail_stack; typedef trail_stack<theory_str> th_trail_stack;
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;
protected: protected:
// Some options that control how the solver operates. // Some options that control how the solver operates.
@ -167,6 +169,13 @@ namespace smt {
*/ */
bool opt_CheckVariableScope; 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; bool search_started;
arith_util m_autil; arith_util m_autil;
str_util m_strutil; str_util m_strutil;
@ -260,6 +269,9 @@ namespace smt {
obj_pair_map<expr, expr, expr*> concat_astNode_map; obj_pair_map<expr, expr, expr*> concat_astNode_map;
// used when opt_FastLengthTesterCache is true
rational_map lengthTesterCache;
th_union_find m_find; th_union_find m_find;
th_trail_stack m_trail_stack; th_trail_stack m_trail_stack;
theory_var get_var(expr * n) const; theory_var get_var(expr * n) const;