From 21be4e6d16bf35c3e83a1bdffa4639eebac6158b Mon Sep 17 00:00:00 2001 From: Egor Bredikhin <32983915+Egor18@users.noreply.github.com> Date: Tue, 5 Mar 2019 17:09:27 -0500 Subject: [PATCH 1/3] Fix misprint --- src/ast/array_decl_plugin.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/array_decl_plugin.cpp b/src/ast/array_decl_plugin.cpp index d2d1039fa..d361815b2 100644 --- a/src/ast/array_decl_plugin.cpp +++ b/src/ast/array_decl_plugin.cpp @@ -299,7 +299,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) { sort* srt2 = domain[i+1]; if (!m_manager->compatible_sorts(srt1, srt2)) { std::stringstream strm; - strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt2, *m_manager) << " do not match"; + strm << "domain sort " << sort_ref(srt2, *m_manager) << " and parameter sort " << sort_ref(srt1, *m_manager) << " do not match"; m_manager->raise_exception(strm.str()); UNREACHABLE(); return nullptr; From e05596e7e564d5009d1843fa28f62487596be4db Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Wed, 6 Mar 2019 11:41:56 -0500 Subject: [PATCH 2/3] z3str3: fix str.indexof with offset (issue #2092) --- src/smt/theory_str.cpp | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 50e666c70..37c5b6237 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1427,7 +1427,7 @@ namespace smt { // 0 < i < len(H) --> // H = hd ++ tl // len(hd) = i - // str.indexof(tl, N, 0) + // i + str.indexof(tl, N, 0) expr * H = nullptr; // "haystack" expr * N = nullptr; // "needle" @@ -1463,12 +1463,19 @@ namespace smt { expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); assert_implication(premise, conclusion); } - // case 4: 0 < i < len(H) + // case 3.5: H doesn't contain N + { + expr_ref premise(m.mk_not(u.str.mk_contains(H, N)), m); + expr_ref conclusion(ctx.mk_eq_atom(e, minus_one), m); + assert_implication(premise, conclusion); + } + // case 4: 0 < i < len(H) and H contains N { expr_ref premise1(m_autil.mk_gt(i, zero), m); //expr_ref premise2(m_autil.mk_lt(i, mk_strlen(H)), m); expr_ref premise2(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 _premise(m.mk_and(premise1, premise2), m); + expr_ref premise3(u.str.mk_contains(H, N), m); + expr_ref _premise(m.mk_and(premise1, premise2, premise3), m); expr_ref premise(_premise); th_rewriter rw(m); rw(premise); @@ -1479,7 +1486,8 @@ namespace smt { expr_ref_vector conclusion_terms(m); conclusion_terms.push_back(ctx.mk_eq_atom(H, mk_concat(hd, tl))); conclusion_terms.push_back(ctx.mk_eq_atom(mk_strlen(hd), i)); - conclusion_terms.push_back(ctx.mk_eq_atom(e, mk_indexof(tl, N))); + conclusion_terms.push_back(u.str.mk_contains(tl, N)); + conclusion_terms.push_back(ctx.mk_eq_atom(e, m_autil.mk_add(i, mk_indexof(tl, N)))); expr_ref conclusion(mk_and(conclusion_terms), m); assert_implication(premise, conclusion); From 5abc4a6d68d57bffeed98bf5c77394dfada32f75 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 6 Mar 2019 22:03:57 -0800 Subject: [PATCH 3/3] rewrite quantifiers in model evaluator #2171 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/th_rewriter.cpp | 10 ++++++++++ src/ast/rewriter/th_rewriter.h | 9 ++++++++- src/model/model_evaluator.cpp | 12 ++++++++++++ src/smt/theory_lra.cpp | 2 +- 4 files changed, 31 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 4fa8c4074..4c81ab665 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -839,3 +839,13 @@ expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) void th_rewriter::set_solver(expr_solver* solver) { m_imp->set_solver(solver); } + + +bool th_rewriter::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + return m_imp->cfg().reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); +} diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index 19a99f4d3..281c685f2 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -41,7 +41,7 @@ public: static void get_param_descrs(param_descrs & r); unsigned get_cache_size() const; unsigned get_num_steps() const; - + void operator()(expr_ref& term); void operator()(expr * t, expr_ref & result); void operator()(expr * t, expr_ref & result, proof_ref & result_pr); @@ -49,6 +49,13 @@ public: expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args); + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr); + void cleanup(); void reset(); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 968aca51f..d2f14d9b4 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -30,6 +30,7 @@ Revision History: #include "ast/rewriter/datatype_rewriter.h" #include "ast/rewriter/array_rewriter.h" #include "ast/rewriter/fpa_rewriter.h" +#include "ast/rewriter/th_rewriter.h" #include "ast/rewriter/rewriter_def.h" #include "ast/ast_pp.h" #include "ast/ast_util.h" @@ -126,6 +127,17 @@ struct evaluator_cfg : public default_rewriter_cfg { return false; } + bool reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, + expr * const * new_no_patterns, + expr_ref & result, + proof_ref & result_pr) { + th_rewriter th(m); + return th.reduce_quantifier(old_q, new_body, new_patterns, new_no_patterns, result, result_pr); + } + + br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { result_pr = nullptr; family_id fid = f->get_family_id(); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 81edb2c67..45ade8b46 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3332,7 +3332,7 @@ public: vi = m_theory_var2var_index[v]; st = m_solver->maximize_term(vi, term_max); } - TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n");); + TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << " " << term_max << "\n");); switch (st) { case lp::lp_status::OPTIMAL: { init_variable_values();