From bced5828f7c1dbcab586709a2a6f067a97fab1f7 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 13 Dec 2016 17:20:58 -0500 Subject: [PATCH] theory_str parameters --- src/smt/params/smt_params_helper.pyg | 4 +++- src/smt/params/theory_str_params.cpp | 2 ++ src/smt/params/theory_str_params.h | 16 +++++++++++++++- src/smt/theory_str.cpp | 14 ++++++-------- src/smt/theory_str.h | 12 ------------ 5 files changed, 26 insertions(+), 22 deletions(-) diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 49a786e69..feec8b01c 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -62,5 +62,7 @@ def_module_params(module_name='smt', ('dack.gc_inv_decay', DOUBLE, 0.8, 'Dynamic ackermannization garbage collection decay'), ('dack.threshold', UINT, 10, ' number of times the congruence rule must be used before Leibniz\'s axiom is expanded'), ('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.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') )) diff --git a/src/smt/params/theory_str_params.cpp b/src/smt/params/theory_str_params.cpp index c1fcb0412..f7a562842 100644 --- a/src/smt/params/theory_str_params.cpp +++ b/src/smt/params/theory_str_params.cpp @@ -21,4 +21,6 @@ Revision History: void theory_str_params::updt_params(params_ref const & _p) { smt_params_helper p(_p); m_AssertStrongerArrangements = p.str_strong_arrangements(); + m_AggressiveLengthTesting = p.str_aggressive_length_testing(); + m_AggressiveValueTesting = p.str_aggressive_value_testing(); } diff --git a/src/smt/params/theory_str_params.h b/src/smt/params/theory_str_params.h index 480ad1479..78c78089e 100644 --- a/src/smt/params/theory_str_params.h +++ b/src/smt/params/theory_str_params.h @@ -30,8 +30,22 @@ struct theory_str_params { */ bool m_AssertStrongerArrangements; + /* + * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities + * to prioritize trying concrete length options over choosing the "more" option. + */ + bool m_AggressiveLengthTesting; + + /* + * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities + * to prioritize trying concrete value options over choosing the "more" option. + */ + bool m_AggressiveValueTesting; + theory_str_params(params_ref const & p = params_ref()): - m_AssertStrongerArrangements(true) + m_AssertStrongerArrangements(true), + m_AggressiveLengthTesting(false), + m_AggressiveValueTesting(false) { updt_params(p); } diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 4eb15d6ad..fe89b4662 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -33,8 +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_AggressiveLengthTesting(false), - opt_AggressiveValueTesting(false), opt_AggressiveUnrollTesting(true), opt_EagerStringConstantLengthAssertions(true), opt_VerifyFinalCheckProgress(true), @@ -8364,7 +8362,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * << "val_indicator = " << mk_ismt2_pp(val_indicator, m) << std::endl << "lenstr = " << lenStr << std::endl << "tries = " << tries << std::endl; - if (opt_AggressiveValueTesting) { + if (m_params.m_AggressiveValueTesting) { tout << "note: aggressive value testing is enabled" << std::endl; } ); @@ -8408,7 +8406,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * 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) { + if (m_params.m_AggressiveValueTesting) { literal l = mk_eq(val_indicator, m_strutil.mk_string(longlong_to_string(i).c_str()), false); ctx.mark_as_relevant(l); ctx.force_phase(l); @@ -8429,7 +8427,7 @@ expr * theory_str::gen_val_options(expr * freeVar, expr * len_indicator, expr * } if (!coverAll) { orList.push_back(m.mk_eq(val_indicator, m_strutil.mk_string("more"))); - if (opt_AggressiveValueTesting) { + if (m_params.m_AggressiveValueTesting) { literal l = mk_eq(val_indicator, m_strutil.mk_string("more"), false); ctx.mark_as_relevant(l); ctx.force_phase(~l); @@ -8980,7 +8978,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr TRACE("t_str_detail", tout << "building andList and orList" << std::endl; - if (opt_AggressiveLengthTesting) { + if (m_params.m_AggressiveLengthTesting) { tout << "note: aggressive length testing is active" << std::endl; } ); @@ -9007,7 +9005,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr expr_ref or_expr(ctx.mk_eq_atom(indicator, str_indicator), m); orList.push_back(or_expr); - if (opt_AggressiveLengthTesting) { + if (m_params.m_AggressiveLengthTesting) { literal l = mk_eq(indicator, str_indicator, false); ctx.mark_as_relevant(l); ctx.force_phase(l); @@ -9019,7 +9017,7 @@ expr * theory_str::gen_len_test_options(expr * freeVar, expr * indicator, int tr // TODO cache mk_string("more") orList.push_back(m.mk_eq(indicator, m_strutil.mk_string("more"))); - if (opt_AggressiveLengthTesting) { + if (m_params.m_AggressiveLengthTesting) { literal l = mk_eq(indicator, m_strutil.mk_string("more"), false); ctx.mark_as_relevant(l); ctx.force_phase(~l); diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 30bf0b080..02b351167 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -100,18 +100,6 @@ namespace smt { protected: theory_str_params const & m_params; - /* - * If AggressiveLengthTesting is true, we manipulate the phase of length tester equalities - * to prioritize trying concrete length options over choosing the "more" option. - */ - bool opt_AggressiveLengthTesting; - - /* - * Similarly, if AggressiveValueTesting is true, we manipulate the phase of value tester equalities - * to prioritize trying concrete value options over choosing the "more" option. - */ - bool opt_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.