From 7b34efada78d48d2d1d55896662092605d57e5d1 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Sun, 4 Sep 2016 18:48:15 -0400 Subject: [PATCH] add aggressive unroll test option to theory_str --- src/smt/theory_str.cpp | 18 ++++++++++++++++++ src/smt/theory_str.h | 6 ++++++ 2 files changed, 24 insertions(+) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index f19553864..749b9c036 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -32,6 +32,7 @@ theory_str::theory_str(ast_manager & m): /* Options */ opt_AggressiveLengthTesting(false), opt_AggressiveValueTesting(false), + opt_AggressiveUnrollTesting(true), opt_EagerStringConstantLengthAssertions(true), opt_VerifyFinalCheckProgress(true), opt_LCMUnrollStep(2), @@ -8265,6 +8266,7 @@ expr * theory_str::gen_unroll_conditional_options(expr * var, std::set & int tries = unroll_tries_map[var][unrolls].size(); for (int i = 0; i < tries; i++) { + // TODO possibly missing a scope check here expr * tester = unroll_tries_map[var][unrolls][i]; bool testerHasValue = false; expr * testerVal = get_eqc_value(tester, testerHasValue); @@ -8318,6 +8320,10 @@ 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) { + TRACE("t_str_detail", tout << "note: aggressive unroll testing is active" << std::endl;); + } + expr_ref_vector orItems(mgr); expr_ref_vector andItems(mgr); @@ -8325,6 +8331,12 @@ 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) { + literal l = mk_eq(testerVar, m_strutil.mk_string(iStr), false); + ctx.mark_as_relevant(l); + ctx.force_phase(l); + } + orItems.push_back(testerEqAst); std::string unrollStrInstance = get_unrolled_string(lcmStr, i); @@ -8338,6 +8350,12 @@ 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) { + literal l = mk_eq(testerVar, m_strutil.mk_string("more"), false); + ctx.mark_as_relevant(l); + ctx.force_phase(~l); + } + orItems.push_back(testerEqMore); int nextLowerLenBound = h * lcmStr.length(); expr_ref more2(ctx.mk_eq_atom(testerEqMore, diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 8a0a2ea81..6ce46abb4 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -96,6 +96,12 @@ namespace smt { */ 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. + */ + bool opt_AggressiveUnrollTesting; + /* * Setting EagerStringConstantLengthAssertions to true allows some methods, * in particular internalize_term(), to add