From 27a2c20c1cf38e55cc4995749de4475864b5ef39 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 13 Dec 2016 19:38:40 -0500 Subject: [PATCH] add more parameters for theory_str --- src/smt/params/smt_params_helper.pyg | 6 +++++- src/smt/params/theory_str_params.cpp | 3 +++ src/smt/params/theory_str_params.h | 25 ++++++++++++++++++++++++- src/smt/theory_str.cpp | 13 +++++-------- src/smt/theory_str.h | 20 -------------------- 5 files changed, 37 insertions(+), 30 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index feec8b01c..cf861a28a 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -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') + )) diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index f7a562842..f952c6c87 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -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(); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 78c78089e..f4e7ecf33 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -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); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index fe89b4662..b18d51a98 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -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)) { diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 02b351167..2a9997517 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -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;