From b68a38ff96685071d931defd92ba5e9052c5237a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 8 May 2018 14:53:02 -0700 Subject: [PATCH 1/3] fixes for re.loop in theory_str --- src/smt/theory_str.cpp | 44 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 43 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 126594b06..531572502 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1829,6 +1829,14 @@ namespace smt { u.str.is_string(range1, range1val); u.str.is_string(range2, range2val); return zstring("[") + range1val + zstring("-") + range2val + zstring("]"); + } else if (u.re.is_loop(a_regex)) { + expr * body; + unsigned lo, hi; + u.re.is_loop(a_regex, body, lo, hi); + rational rLo(lo); + rational rHi(hi); + zstring bodyStr = get_std_regex_str(body); + return zstring("(") + bodyStr + zstring("{") + zstring(rLo.to_string().c_str()) + zstring(",") + zstring(rHi.to_string().c_str()) + zstring("})"); } else if (u.re.is_full_seq(a_regex)) { return zstring("(.*)"); } else if (u.re.is_full_char(a_regex)) { @@ -6644,6 +6652,7 @@ namespace smt { ENSURE(u.is_re(re)); expr * sub1; expr * sub2; + unsigned lo, hi; if (u.re.is_to_re(re, sub1)) { SASSERT(u.str.is_string(sub1)); zstring str; @@ -6662,6 +6671,9 @@ namespace smt { } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1)) { unsigned cx = estimate_regex_complexity(sub1); return _qmul(2, cx); + } else if (u.re.is_loop(re, sub1, lo, hi)) { + unsigned cx = estimate_regex_complexity(sub1); + return _qadd(lo, cx); } else if (u.re.is_range(re, sub1, sub2)) { SASSERT(u.str.is_string(sub1)); SASSERT(u.str.is_string(sub2)); @@ -6683,6 +6695,7 @@ namespace smt { ENSURE(u.is_re(re)); expr * sub1; expr * sub2; + unsigned lo, hi; if (u.re.is_to_re(re, sub1)) { SASSERT(u.str.is_string(sub1)); zstring str; @@ -6701,7 +6714,7 @@ namespace smt { unsigned cx1 = estimate_regex_complexity_under_complement(sub1); unsigned cx2 = estimate_regex_complexity_under_complement(sub2); return _qmul(cx1, cx2); - } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1)) { + } else if (u.re.is_star(re, sub1) || u.re.is_plus(re, sub1) || u.re.is_loop(re, sub1, lo, hi)) { unsigned cx = estimate_regex_complexity_under_complement(sub1); return _qmul(2, cx); } else if (u.re.is_range(re, sub1, sub2)) { @@ -6735,6 +6748,7 @@ namespace smt { bool theory_str::check_regex_length_linearity_helper(expr * re, bool already_star) { expr * sub1; expr * sub2; + unsigned lo, hi; if (u.re.is_to_re(re)) { return true; } else if (u.re.is_concat(re, sub1, sub2)) { @@ -6756,6 +6770,8 @@ namespace smt { } else if (u.re.is_complement(re)) { // TODO can we do better? return false; + } else if (u.re.is_loop(re, sub1, lo, hi)) { + return check_regex_length_linearity_helper(sub1, already_star); } else { TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;); UNREACHABLE(); return false; @@ -6766,6 +6782,7 @@ namespace smt { void theory_str::check_subterm_lengths(expr * re, integer_set & lens) { expr * sub1; expr * sub2; + unsigned lo, hi; if (u.re.is_to_re(re, sub1)) { SASSERT(u.str.is_string(sub1)); zstring(str); @@ -6820,6 +6837,14 @@ namespace smt { lens.reset(); } else if (u.re.is_complement(re)) { lens.reset(); + } else if (u.re.is_loop(re, sub1, lo, hi)) { + integer_set lens_1; + check_subterm_lengths(sub1, lens_1); + for (unsigned i = lo; i <= hi; ++i) { + for (auto j : lens_1) { + lens.insert(i * j); + } + } } else { TRACE("str", tout << "WARNING: unknown regex term " << mk_pp(re, get_manager()) << std::endl;); lens.reset(); @@ -6841,6 +6866,7 @@ namespace smt { ast_manager & m = get_manager(); expr * sub1; expr * sub2; + unsigned lo, hi; if (u.re.is_to_re(re, sub1)) { SASSERT(u.str.is_string(sub1)); zstring str; @@ -6909,6 +6935,22 @@ namespace smt { expr_ref retval(ctx.mk_eq_atom(lenVar, m_autil.mk_add_simplify(sum_terms)), m); return retval; } + } else if (u.re.is_loop(re, sub1, lo, hi)) { + expr * v1 = mk_int_var("rlen"); + freeVariables.push_back(v1); + expr_ref r1 = infer_all_regex_lengths(v1, sub1, freeVariables); + expr_ref_vector v1_choices(m); + for (unsigned i = lo; i <= hi; ++i) { + rational rI(i); + expr_ref v1_i(ctx.mk_eq_atom(lenVar, m_autil.mk_mul(m_autil.mk_numeral(rI, true), v1)), m); + v1_choices.push_back(v1_i); + } + expr_ref_vector finalResult(m); + finalResult.push_back(r1); + finalResult.push_back(mk_or(v1_choices)); + expr_ref retval(mk_and(finalResult), m); + SASSERT(retval); + return retval; } else if (u.re.is_range(re, sub1, sub2)) { SASSERT(u.str.is_string(sub1)); SASSERT(u.str.is_string(sub2)); From c65dbaea90b6f9d632b8ffbc61f41b54f7aa906e Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 7 Aug 2018 15:12:37 -0400 Subject: [PATCH 2/3] z3str3: fix contains-indexof precondition --- src/smt/theory_str.cpp | 17 +++++++++++++---- 1 file changed, 13 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index a6ef6eac2..aadcb63a7 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1388,7 +1388,7 @@ namespace smt { // (but don't introduce it if it isn't already in the instance) expr_ref haystack(ex->get_arg(0), m), needle(ex->get_arg(1), m), startIdx(ex->get_arg(2), m); expr_ref zeroAst(mk_int(0), m); - // (H contains N) <==> (H indexof N, i) >= 0 + // (H contains N) <==> (H indexof N, 0) >= 0 expr_ref premise(u.str.mk_contains(haystack, needle), m); ctx.internalize(premise, false); expr_ref conclusion(m_autil.mk_ge(ex, zeroAst), m); @@ -1482,14 +1482,23 @@ namespace smt { { // heuristic: integrate with str.contains information // (but don't introduce it if it isn't already in the instance) - // (H contains N) <==> (H indexof N, i) >= 0 + // (0 <= i < len(H)) ==> (H contains N) <==> (H indexof N, i) >= 0 + expr_ref precondition1(m_autil.mk_gt(i, minus_one), m); + //expr_ref precondition2(m_autil.mk_lt(i, mk_strlen(H)), m); + expr_ref precondition2(m.mk_not(m_autil.mk_ge(m_autil.mk_add(i, m_autil.mk_mul(minus_one, mk_strlen(H))), zero)), m); + expr_ref _precondition(m.mk_and(precondition1, precondition2), m); + expr_ref precondition(_precondition); + th_rewriter rw(m); + rw(precondition); + expr_ref premise(u.str.mk_contains(H, N), m); ctx.internalize(premise, false); expr_ref conclusion(m_autil.mk_ge(e, zero), m); expr_ref containsAxiom(ctx.mk_eq_atom(premise, conclusion), m); - SASSERT(containsAxiom); + expr_ref finalAxiom(rewrite_implication(precondition, containsAxiom), m); + SASSERT(finalAxiom); // we can't assert this during init_search as it breaks an invariant if the instance becomes inconsistent - m_delayed_assertions_todo.push_back(containsAxiom); + m_delayed_assertions_todo.push_back(finalAxiom); } } From 0aca1ad4c1ee2337baf079899d6fdbfb66d5661a Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Fri, 10 Aug 2018 17:37:23 -0500 Subject: [PATCH 3/3] feat(smt/dt): expose the configuration param for datatype case splits --- src/smt/params/smt_params.cpp | 1 + src/smt/params/smt_params_helper.pyg | 3 ++- src/smt/params/theory_datatype_params.h | 9 +++++---- 3 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/smt/params/smt_params.cpp b/src/smt/params/smt_params.cpp index 3ad20cf90..650afda25 100644 --- a/src/smt/params/smt_params.cpp +++ b/src/smt/params/smt_params.cpp @@ -63,6 +63,7 @@ void smt_params::updt_params(params_ref const & p) { theory_bv_params::updt_params(p); theory_pb_params::updt_params(p); // theory_array_params::updt_params(p); + theory_datatype_params::updt_params(p); updt_local_params(p); } diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg index 3f4105c34..76e9f03b1 100644 --- a/src/smt/params/smt_params_helper.pyg +++ b/src/smt/params/smt_params_helper.pyg @@ -94,5 +94,6 @@ def_module_params(module_name='smt', ('core.extend_patterns', BOOL, False, 'extend unsat core with literals that trigger (potential) quantifier instances'), ('core.extend_patterns.max_distance', UINT, UINT_MAX, 'limits the distance of a pattern-extended unsat core'), ('core.extend_nonlocal_patterns', BOOL, False, 'extend unsat cores with literals that have quantifiers with patterns that contain symbols which are not in the quantifier\'s body'), - ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none') + ('lemma_gc_strategy', UINT, 0, 'lemma garbage collection strategy: 0 - fixed, 1 - geometric, 2 - at restart, 3 - none'), + ('dt_lazy_splits', UINT, 1, 'How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy') )) diff --git a/src/smt/params/theory_datatype_params.h b/src/smt/params/theory_datatype_params.h index 9f801e46c..d2d851ffe 100644 --- a/src/smt/params/theory_datatype_params.h +++ b/src/smt/params/theory_datatype_params.h @@ -19,6 +19,8 @@ Revision History: #ifndef THEORY_DATATYPE_PARAMS_H_ #define THEORY_DATATYPE_PARAMS_H_ +#include "smt/params/smt_params_helper.hpp" + struct theory_datatype_params { unsigned m_dt_lazy_splits; @@ -26,11 +28,10 @@ struct theory_datatype_params { m_dt_lazy_splits(1) { } -#if 0 - void register_params(ini_params & p) { - p.register_unsigned_param("dt_lazy_splits", m_dt_lazy_splits, "How lazy datatype splits are performed: 0- eager, 1- lazy for infinite types, 2- lazy"); + void updt_params(params_ref const & _p) { + smt_params_helper p(_p); + m_dt_lazy_splits = p.dt_lazy_splits(); } -#endif void display(std::ostream & out) const { out << "m_dt_lazy_splits=" << m_dt_lazy_splits << std::endl; } };