mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

add more parameters for theory_str

Browse source
This commit is contained in:
Murphy Berzish 2016-12-13 19:38:40 -05:00
parent bced5828f7
commit 27a2c20c1c
5 changed files with 37 additions and 30 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/params/smt_params_helper.pyg
View file

@ -64,5 +64,9 @@ def_module_params(module_name='smt',
('core.validate', BOOL, False, 'validate unsat core produced by SMT context'),
('str.strong_arrangements', BOOL, True, 'assert equivalences instead of implications when generating string arrangement axioms'),
('str.aggressive_length_testing', BOOL, False, 'prioritize testing concrete length values over generating more options'),
('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options')
('str.aggressive_value_testing', BOOL, False, 'prioritize testing concrete string constant values over generating more options'),
('str.aggressive_unroll_testing', BOOL, True, 'prioritize testing concrete regex unroll counts over generating more options'),
('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')
))

3
src/smt/params/theory_str_params.cpp
View file

@ -23,4 +23,7 @@ void theory_str_params::updt_params(params_ref const & _p) {
m_AssertStrongerArrangements = p.str_strong_arrangements();
m_AggressiveLengthTesting = p.str_aggressive_length_testing();
m_AggressiveValueTesting = p.str_aggressive_value_testing();
m_AggressiveUnrollTesting = p.str_aggressive_unroll_testing();
m_UseFastLengthTesterCache = p.str_fast_length_tester_cache();
m_UseFastValueTesterCache = p.str_fast_value_tester_cache();
}

25
src/smt/params/theory_str_params.h
View file

@ -42,10 +42,33 @@ struct theory_str_params {
*/
bool m_AggressiveValueTesting;
/*
* If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
* to prioritize trying concrete unroll counts over choosing the "more" option.
*/
bool m_AggressiveUnrollTesting;
/*
* 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 m_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 m_UseFastValueTesterCache;
theory_str_params(params_ref const & p = params_ref()):
m_AssertStrongerArrangements(true),
m_AggressiveLengthTesting(false),
m_AggressiveValueTesting(false)
m_AggressiveValueTesting(false),
m_AggressiveUnrollTesting(true),
m_UseFastLengthTesterCache(false),
m_UseFastValueTesterCache(true)
{
updt_params(p);
}

13
src/smt/theory_str.cpp
View file

@ -33,7 +33,6 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
theory(m.mk_family_id("str")),
m_params(params),
/* Options */
opt_AggressiveUnrollTesting(true),
opt_EagerStringConstantLengthAssertions(true),
opt_VerifyFinalCheckProgress(true),
opt_LCMUnrollStep(2),
@ -41,8 +40,6 @@ theory_str::theory_str(ast_manager & m, theory_str_params const & params):
opt_DisableIntegerTheoryIntegration(false),
opt_DeferEQCConsistencyCheck(false),
opt_CheckVariableScope(true),
opt_UseFastLengthTesterCache(true),
opt_UseFastValueTesterCache(true),
/* Internal setup */
search_started(false),
m_autil(m),
@ -8414,7 +8411,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr *
std::string aStr = gen_val_string(len, options[i - l]);
expr * strAst;
if (opt_UseFastValueTesterCache) {
if (m_params.m_UseFastValueTesterCache) {
if (!valueTesterCache.find(aStr, strAst)) {
strAst = m_strutil.mk_string(aStr);
valueTesterCache.insert(aStr, strAst);
@ -8905,7 +8902,7 @@ expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * test
TRACE("t_str_detail", tout << "entry: var = " << mk_pp(var, mgr) << ", lcmStr = " << lcmStr
<< ", l = " << l << ", h = " << h << std::endl;);
if (opt_AggressiveUnrollTesting) {
if (m_params.m_AggressiveUnrollTesting) {
TRACE("t_str_detail", tout << "note: aggressive unroll testing is active" << std::endl;);
}
@ -8916,7 +8913,7 @@ expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * test
std::string iStr = int_to_string(i);
expr_ref testerEqAst(ctx.mk_eq_atom(testerVar, m_strutil.mk_string(iStr)), mgr);
TRACE("t_str_detail", tout << "testerEqAst = " << mk_pp(testerEqAst, mgr) << std::endl;);
if (opt_AggressiveUnrollTesting) {
if (m_params.m_AggressiveUnrollTesting) {
literal l = mk_eq(testerVar, m_strutil.mk_string(iStr), false);
ctx.mark_as_relevant(l);
ctx.force_phase(l);
@ -8935,7 +8932,7 @@ expr * theory_str::gen_unroll_assign(expr * var, std::string lcmStr, expr * test
}
expr_ref testerEqMore(ctx.mk_eq_atom(testerVar, m_strutil.mk_string("more")), mgr);
TRACE("t_str_detail", tout << "testerEqMore = " << mk_pp(testerEqMore, mgr) << std::endl;);
if (opt_AggressiveUnrollTesting) {
if (m_params.m_AggressiveUnrollTesting) {
literal l = mk_eq(testerVar, m_strutil.mk_string("more"), false);
ctx.mark_as_relevant(l);
ctx.force_phase(~l);
@ -8985,7 +8982,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr
for (int i = l; i < h; ++i) {
expr_ref str_indicator(m);
if (opt_UseFastLengthTesterCache) {
if (m_params.m_UseFastLengthTesterCache) {
rational ri(i);
expr * lookup_val;
if(lengthTesterCache.find(ri, lookup_val)) {

20
src/smt/theory_str.h
View file

@ -100,12 +100,6 @@ namespace smt {
protected:
theory_str_params const & m_params;
/*
* If AggressiveUnrollTesting is true, we manipulate the phase of regex unroll tester equalities
* to prioritize trying concrete unroll counts over choosing the "more" option.
*/
bool opt_AggressiveUnrollTesting;
/*
* Setting EagerStringConstantLengthAssertions to true allows some methods,
* in particular internalize_term(), to add
@ -164,20 +158,6 @@ 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;
/*
* 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;