From 1ab7ab9d744d5cddec94ae539d4d52233fedcb16 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Mar 2017 11:09:36 -0700 Subject: [PATCH 01/23] fix double ownership of enode marking causing crash during tracing. Issue #952 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- src/smt/smt_conflict_resolution.cpp | 6 +++--- src/smt/smt_context.cpp | 1 + 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index b6157f3ff..104f3ae6c 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } + static void error_handler(Z3_context c, Z3_error_code e) { std::cout << "ex\n"; Z3_THROW(exception(Z3_get_error_msg(c, e))); std::cout << "unreach\n"; } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; diff --git a/src/smt/smt_conflict_resolution.cpp b/src/smt/smt_conflict_resolution.cpp index 7dd9144fe..8d90f9583 100644 --- a/src/smt/smt_conflict_resolution.cpp +++ b/src/smt/smt_conflict_resolution.cpp @@ -59,9 +59,9 @@ namespace smt { SASSERT(n->trans_reaches(n->get_root())); while (n) { if (Set) - n->set_mark(); + n->set_mark2(); else - n->unset_mark(); + n->unset_mark2(); n = n->m_trans.m_target; } } @@ -84,7 +84,7 @@ namespace smt { mark_enodes_in_trans(n1); while (true) { SASSERT(n2); - if (n2->is_marked()) { + if (n2->is_marked2()) { mark_enodes_in_trans(n1); return n2; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9336322f7..6bc5cc6ab 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4214,6 +4214,7 @@ namespace smt { for (unsigned i = 0; i < m_asserted_formulas.get_num_formulas(); ++i) { expr* e = m_asserted_formulas.get_formula(i); if (is_quantifier(e)) { + TRACE("context", tout << mk_pp(e, m) << "\n";); quantifier* q = to_quantifier(e); if (!m.is_rec_fun_def(q)) continue; SASSERT(q->get_num_patterns() == 1); From 62e87d647474e539ef9274e244869dac8615fa8c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Mar 2017 11:10:19 -0700 Subject: [PATCH 02/23] fix double ownership of enode marking causing crash during tracing. Issue #952 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 104f3ae6c..b6157f3ff 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -140,7 +140,7 @@ namespace z3 { class context { bool m_enable_exceptions; Z3_context m_ctx; - static void error_handler(Z3_context c, Z3_error_code e) { std::cout << "ex\n"; Z3_THROW(exception(Z3_get_error_msg(c, e))); std::cout << "unreach\n"; } + static void error_handler(Z3_context /*c*/, Z3_error_code /*e*/) { /* do nothing */ } void init(config & c) { m_ctx = Z3_mk_context_rc(c); m_enable_exceptions = true; From 37167a8dd607d27fb666222b63bfeef188de5789 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 23 Mar 2017 19:53:23 +0000 Subject: [PATCH 03/23] Fixed excessive trace output --- src/smt/smt_context_pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index ff45c5089..74c759510 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -606,7 +606,7 @@ namespace smt { case b_justification::CLAUSE: { clause * cls = j.get_clause(); out << "clause "; - if (cls) display_literals_verbose(out, cls->get_num_literals(), cls->begin_literals()); + if (cls) display_literals(out, cls->get_num_literals(), cls->begin_literals()); break; } case b_justification::JUSTIFICATION: { From c56c7fd649a41e5b99a1ae150d059d895cd3cf69 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 01:31:00 -0700 Subject: [PATCH 04/23] add handlers for dense difference logic Signed-off-by: Nikolaj Bjorner --- src/opt/opt_solver.cpp | 27 ++++++++++++++++++++++++++- src/smt/theory_dense_diff_logic_def.h | 2 ++ 2 files changed, 28 insertions(+), 1 deletion(-) diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 8ae4e467f..bc6462a18 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -358,6 +358,7 @@ namespace opt { } smt::theory_opt& opt = get_optimizer(); smt::theory_var v = m_objective_vars[var]; + TRACE("opt", tout << "v" << var << " " << val << "\n";); if (typeid(smt::theory_inf_arith) == typeid(opt)) { smt::theory_inf_arith& th = dynamic_cast(opt); @@ -387,8 +388,32 @@ namespace opt { smt::theory_rdl& th = dynamic_cast(opt); return th.mk_ge(m_fm, v, val); } + + if (typeid(smt::theory_dense_i) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_i& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } - // difference logic? + if (typeid(smt::theory_dense_mi) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_mi& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + if (typeid(smt::theory_dense_si) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_si& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + if (typeid(smt::theory_dense_smi) == typeid(opt) && + val.get_infinitesimal().is_zero()) { + smt::theory_dense_smi& th = dynamic_cast(opt); + return th.mk_ge(m_fm, v, val); + } + + IF_VERBOSE(0, verbose_stream() << "WARNING: unhandled theory " << typeid(opt).name() << "\n";); return expr_ref(m.mk_true(), m); } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index 628eeea83..ed94ee62c 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -1019,6 +1019,7 @@ namespace smt { template theory_var theory_dense_diff_logic::add_objective(app* term) { + TRACE("opt", tout << mk_pp(term, get_manager()) << "\n";); objective_term objective; theory_var result = m_objectives.size(); rational q(1), r(0); @@ -1053,6 +1054,7 @@ namespace smt { ast_manager& m = get_manager(); objective_term const& t = m_objectives[v]; expr_ref e(m), f(m), f2(m); + TRACE("opt", tout << "mk_ineq " << v << " " << val << "\n";); if (t.size() == 1 && t[0].second.is_one()) { f = get_enode(t[0].first)->get_owner(); } From ec4770622690fc29b2eb0557b7d644651a92b90c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 02:23:50 -0700 Subject: [PATCH 05/23] fix constant offset and handling of ite in difference logic optimizer code-path. Issue #946 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 7 ++++++- src/smt/theory_dense_diff_logic_def.h | 6 ++++-- 2 files changed, 10 insertions(+), 3 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index cd40944b2..d1b7a489e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -273,7 +273,8 @@ namespace opt { display_benchmark(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n";); lbool is_sat = s.check_sat(0,0); - TRACE("opt", tout << "initial search result: " << is_sat << "\n";); + TRACE("opt", tout << "initial search result: " << is_sat << "\n"; + s.display(tout);); if (is_sat != l_false) { s.get_model(m_model); s.get_labels(m_labels); @@ -1037,6 +1038,10 @@ namespace opt { TRACE("opt", tout << "Purifying " << term << "\n";); term = purify(fm, term); } + else if (m.is_ite(term)) { + TRACE("opt", tout << "Purifying " << term << "\n";); + term = purify(fm, term); + } if (fm) { m_model_converter = concat(m_model_converter.get(), fm.get()); } diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h index ed94ee62c..addb5d92b 100644 --- a/src/smt/theory_dense_diff_logic_def.h +++ b/src/smt/theory_dense_diff_logic_def.h @@ -868,7 +868,8 @@ namespace smt { e = ctx.get_enode(to_app(n)); } else { - e = ctx.mk_enode(to_app(n), false, false, true); + ctx.internalize(n, false); + e = ctx.get_enode(n); } v = e->get_th_var(get_id()); if (v == null_theory_var) { @@ -1008,7 +1009,8 @@ namespace smt { inf_eps result(rational(0), r); blocker = mk_gt(v, result); IF_VERBOSE(10, verbose_stream() << blocker << "\n";); - return result; + r += m_objective_consts[v]; + return inf_eps(rational(0), r); } default: TRACE("opt", tout << "unbounded\n"; ); From 866035d786ca69860359d7833a6c15108f7c0740 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 09:40:18 +0000 Subject: [PATCH 06/23] Disabled debug output --- src/smt/smt_context_pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 74c759510..73d822fb4 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -613,7 +613,7 @@ namespace smt { out << "justification "; literal_vector lits; const_cast(*m_conflict_resolution).justification2literals(j.get_justification(), lits); - display_literals_verbose(out, lits.size(), lits.c_ptr()); + display_literals(out, lits.size(), lits.c_ptr()); break; } default: From e9cd4d10570c7e035489841ebadc9ce08df8a1a9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 11:51:36 +0000 Subject: [PATCH 07/23] Build fix for systems that don't come with SSE4.1 support by default --- src/util/hwf.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index f84f7fe40..ac39db71a 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -52,8 +52,10 @@ Revision History: #ifdef USE_INTRINSICS #include +#ifdef __SSE4_1__ #include #endif +#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) From 7f9c37e19d4bab0eaeaed586513c812f271603f5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 14:23:39 +0000 Subject: [PATCH 08/23] VS2017 SSE4 intrinsics build fix --- src/util/hwf.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index ac39db71a..f8e4ff69b 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -52,10 +52,8 @@ Revision History: #ifdef USE_INTRINSICS #include -#ifdef __SSE4_1__ #include #endif -#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) @@ -306,7 +304,9 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o // According to the Intel Architecture manual, the x87-instrunction FRNDINT is the // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. #ifdef _WINDOWS -#ifdef USE_INTRINSICS +#if defined(USE_INTRINSICS) && \ + (defined(_WINDOWS) && defined(__AVX__)) || \ + (!defined(_WINDOWS) && defined(__SSE4_1__) ) switch (rm) { case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break; From d10dec2218657023d8adcfc0a1b5e6c4a61aba97 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 14:31:06 +0000 Subject: [PATCH 09/23] Removed unused variable --- src/ast/rewriter/rewriter_def.h | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index aecc1c93a..76f149df7 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -189,10 +189,9 @@ bool rewriter_tpl::constant_fold(app * t, frame & fr) { result_stack().shrink(fr.m_spos); result_stack().push_back(arg); fr.m_state = REWRITE_BUILTIN; - unsigned max_depth = fr.m_max_depth; if (visit(arg, fr.m_max_depth)) { m_r = result_stack().back(); - result_stack().pop_back(); + result_stack().pop_back(); result_stack().pop_back(); result_stack().push_back(m_r); cache_result(t, m_r, m_pr, fr.m_cache_result); From 0399e5e2d339505a9b34a66358133ef872549077 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 14:49:24 +0000 Subject: [PATCH 10/23] Fixed variable initialization warning --- src/sat/sat_solver.cpp | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index a66f82486..9c858a29a 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -101,7 +101,7 @@ namespace sat { if (!it->is_binary_non_learned_clause()) continue; literal l2 = it->get_literal(); - if (l.index() > l2.index()) + if (l.index() > l2.index()) continue; mk_clause_core(l, l2); } @@ -223,7 +223,7 @@ namespace sat { if (propagate_bin_clause(l1, l2)) { if (scope_lvl() == 0) return; - if (!learned) + if (!learned) m_clauses_to_reinit.push_back(clause_wrapper(l1, l2)); } m_stats.m_mk_bin_clause++; @@ -248,7 +248,7 @@ namespace sat { void solver::push_reinit_stack(clause & c) { TRACE("sat_reinit", tout << "adding to reinit stack: " << c << "\n";); m_clauses_to_reinit.push_back(clause_wrapper(c)); - c.set_reinit_stack(true); + c.set_reinit_stack(true); } @@ -257,7 +257,7 @@ namespace sat { clause * r = m_cls_allocator.mk_clause(3, lits, learned); bool reinit = attach_ter_clause(*r); if (reinit && !learned) push_reinit_stack(*r); - + if (learned) m_learned.push_back(r); else @@ -806,22 +806,22 @@ namespace sat { m_params.set_uint("random_seed", m_rand()); if (i == 1 + num_threads/2) { m_params.set_sym("phase", symbol("random")); - } + } solvers[i] = alloc(sat::solver, m_params, rlims[i], 0); solvers[i]->copy(*this); solvers[i]->set_par(&par); - scoped_rlimit.push_child(&solvers[i]->rlimit()); + scoped_rlimit.push_child(&solvers[i]->rlimit()); } set_par(&par); m_params.set_sym("phase", saved_phase); int finished_id = -1; std::string ex_msg; - par_exception_kind ex_kind; + par_exception_kind ex_kind = DEFAULT_EX; unsigned error_code = 0; lbool result = l_undef; #pragma omp parallel for for (int i = 0; i < num_threads; ++i) { - try { + try { lbool r = l_undef; if (i < num_extra_solvers) { r = solvers[i]->check(num_lits, lits); @@ -851,7 +851,7 @@ namespace sat { rlims[j].cancel(); } } - } + } } catch (z3_error & err) { if (i == 0) { @@ -871,7 +871,7 @@ namespace sat { m_stats = solvers[finished_id]->m_stats; } - for (int i = 0; i < num_extra_solvers; ++i) { + for (int i = 0; i < num_extra_solvers; ++i) { dealloc(solvers[i]); } if (finished_id == -1) { @@ -1140,7 +1140,7 @@ namespace sat { for (unsigned i = 0; !inconsistent() && i < m_assumptions.size(); ++i) { assign(m_assumptions[i], justification()); } - TRACE("sat", + TRACE("sat", for (unsigned i = 0; i < m_assumptions.size(); ++i) { index_set s; if (m_antecedents.find(m_assumptions[i].var(), s)) { @@ -2037,7 +2037,7 @@ namespace sat { } } - literal consequent = m_not_l; + literal consequent = m_not_l; justification js = m_conflict; @@ -3115,7 +3115,7 @@ namespace sat { literal_pair p(l1, l2); if (!seen_bc.contains(p)) { seen_bc.insert(p); - mc.add_edge(l1.index(), l2.index()); + mc.add_edge(l1.index(), l2.index()); } } vector _mutexes; @@ -3168,7 +3168,7 @@ namespace sat { } void solver::fixup_consequence_core() { - index_set s; + index_set s; TRACE("sat", tout << m_core << "\n";); for (unsigned i = 0; i < m_core.size(); ++i) { TRACE("sat", tout << m_core[i] << ": "; display_index_set(tout, m_antecedents.find(m_core[i].var())) << "\n";); @@ -3218,20 +3218,20 @@ namespace sat { while (true) { ++num_iterations; SASSERT(!inconsistent()); - + lbool r = bounded_search(); if (r != l_undef) { fixup_consequence_core(); return r; } - + extract_fixed_consequences(num_units, asms, unfixed_vars, conseq); if (m_conflicts > m_config.m_max_conflicts) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-conflicts = " << m_conflicts << "\")\n";); return l_undef; } - + restart(); simplify_problem(); if (check_inconsistent()) { @@ -3239,11 +3239,11 @@ namespace sat { return l_false; } gc(); - + if (m_config.m_restart_max <= num_iterations) { IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "(sat \"abort: max-restarts\")\n";); return l_undef; - } + } } } From fb105afac2ed8ec35e6f5c9706d8c596b95a06d7 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 15:22:33 +0000 Subject: [PATCH 11/23] Windows build fix --- src/util/hwf.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index f8e4ff69b..5572ee252 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -305,8 +305,8 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o // same in 32-bit and 64-bit mode. The _mm_round_* intrinsics are SSE4 extensions. #ifdef _WINDOWS #if defined(USE_INTRINSICS) && \ - (defined(_WINDOWS) && defined(__AVX__)) || \ - (!defined(_WINDOWS) && defined(__SSE4_1__) ) + (defined(_WINDOWS) && (defined(__AVX__) || defined(_M_X64))) || \ + (!defined(_WINDOWS) && defined(__SSE4_1__)) switch (rm) { case 0: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_NEAREST_INT)); break; case 2: _mm_store_sd(&o.value, _mm_round_pd(_mm_set_sd(x.value), _MM_FROUND_TO_POS_INF)); break; From f8d022a18060ac6abe6429c7e6e79ecdaf15fc02 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 15:25:18 +0000 Subject: [PATCH 12/23] Non-windows build fix --- src/util/hwf.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index 5572ee252..e577e15df 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -52,8 +52,10 @@ Revision History: #ifdef USE_INTRINSICS #include +#if defined(_MSC_VER) || defined(__SSE4_1__) #include #endif +#endif hwf_manager::hwf_manager() : m_mpz_manager(m_mpq_manager) From 3bbe5eceeb0e0a51c6d11d7a2ba2d54fb6d52dbc Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 15:53:46 +0000 Subject: [PATCH 13/23] fix for --get-describe --- scripts/mk_util.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 17ab8dea0..f05250ae7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2685,8 +2685,8 @@ def get_full_version_string(major, minor, build, revision): if GIT_HASH: res += " " + GIT_HASH if GIT_DESCRIBE: - branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD', '--long']) - res += " master " + check_output(['git', 'describe']) + branch = check_output(['git', 'rev-parse', '--abbrev-ref', 'HEAD']) + res += " " + branch + " " + check_output(['git', 'describe']) return '"' + res + '"' # Update files with the version number From e05cee757ba715aa3631a32ea4b8ee92cede2d7c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 10:10:42 -0700 Subject: [PATCH 14/23] properly handle recursive function definitions #898 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/cmd_context.cpp | 7 +++++-- src/sat/sat_simplifier.cpp | 1 + src/smt/smt_context.cpp | 32 +++++--------------------------- src/smt/smt_context.h | 2 -- src/smt/smt_model_checker.cpp | 2 +- 5 files changed, 12 insertions(+), 32 deletions(-) diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 2551f0aa0..7060d79ad 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -739,8 +739,11 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s lhs = m().mk_app(f, binding.size(), binding.c_ptr()); eq = m().mk_eq(lhs, e); if (!ids.empty()) { - expr* pat = m().mk_pattern(lhs); - eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 1, &pat); + if (!is_app(e)) { + throw cmd_exception("Z3 only supports recursive definitions that are proper terms (not binders or variables)"); + } + expr* pats[2] = { m().mk_pattern(lhs), m().mk_pattern(to_app(e)) }; + eq = m().mk_forall(ids.size(), f->get_domain(), ids.c_ptr(), eq, 0, m().rec_fun_qid(), symbol::null, 2, pats); } // diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 007751220..8b753fb67 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -149,6 +149,7 @@ namespace sat { } void simplifier::operator()(bool learned) { + std::cout << s.rlimit().count() << "\n"; if (s.inconsistent()) return; if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 6bc5cc6ab..f1b043556 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4217,40 +4217,18 @@ namespace smt { TRACE("context", tout << mk_pp(e, m) << "\n";); quantifier* q = to_quantifier(e); if (!m.is_rec_fun_def(q)) continue; - SASSERT(q->get_num_patterns() == 1); + SASSERT(q->get_num_patterns() == 2); expr* fn = to_app(q->get_pattern(0))->get_arg(0); + expr* body = to_app(q->get_pattern(1))->get_arg(0); SASSERT(is_app(fn)); func_decl* f = to_app(fn)->get_decl(); - expr* eq = q->get_expr(); - expr_ref body(m); - if (is_fun_def(fn, q->get_expr(), body)) { - func_interp* fi = alloc(func_interp, m, f->get_arity()); - fi->set_else(body); - m_model->register_decl(f, fi); - } + func_interp* fi = alloc(func_interp, m, f->get_arity()); + fi->set_else(body); + m_model->register_decl(f, fi); } } } - bool context::is_fun_def(expr* f, expr* body, expr_ref& result) { - expr* t1, *t2, *t3; - if (m_manager.is_eq(body, t1, t2) || m_manager.is_iff(body, t1, t2)) { - if (t1 == f) return result = t2, true; - if (t2 == f) return result = t1, true; - return false; - } - if (m_manager.is_ite(body, t1, t2, t3)) { - expr_ref body1(m_manager), body2(m_manager); - if (is_fun_def(f, t2, body1) && is_fun_def(f, t3, body2)) { - // f is not free in t1 - result = m_manager.mk_ite(t1, body1, body2); - return true; - } - } - return false; - } - - }; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 2a555e6b5..1f57a7550 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1167,8 +1167,6 @@ namespace smt { void add_rec_funs_to_model(); - bool is_fun_def(expr* f, expr* q, expr_ref& body); - public: bool can_propagate() const; diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index 093d215b6..dfdb035c5 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -318,7 +318,7 @@ namespace smt { bool model_checker::check_rec_fun(quantifier* q) { TRACE("model_checker", tout << mk_pp(q, m) << "\n";); - SASSERT(q->get_num_patterns() == 1); + SASSERT(q->get_num_patterns() == 2); // first pattern is the function, second is the body. expr* fn = to_app(q->get_pattern(0))->get_arg(0); SASSERT(is_app(fn)); func_decl* f = to_app(fn)->get_decl(); From 723b507a887499517c69182947a2c611f7487edb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 24 Mar 2017 10:11:39 -0700 Subject: [PATCH 15/23] properly handle recursive function definitions #898 Signed-off-by: Nikolaj Bjorner --- src/sat/sat_simplifier.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 8b753fb67..007751220 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -149,7 +149,6 @@ namespace sat { } void simplifier::operator()(bool learned) { - std::cout << s.rlimit().count() << "\n"; if (s.inconsistent()) return; if (!m_subsumption && !m_elim_blocked_clauses && !m_resolution) From 3a9857940e21e6978ba7a75548b6cf26c4707386 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 25 Mar 2017 19:31:01 +0100 Subject: [PATCH 16/23] add missing axioms for str.at. Issue #953 Signed-off-by: Nikolaj Bjorner --- src/ast/bv_decl_plugin.h | 10 +++++----- src/ast/macros/macro_util.cpp | 36 ++++++++++++++--------------------- src/ast/macros/macro_util.h | 3 +-- src/smt/theory_seq.cpp | 15 +++++++++++++++ 4 files changed, 35 insertions(+), 29 deletions(-) diff --git a/src/ast/bv_decl_plugin.h b/src/ast/bv_decl_plugin.h index ac0ff7f79..33cf094b9 100644 --- a/src/ast/bv_decl_plugin.h +++ b/src/ast/bv_decl_plugin.h @@ -406,11 +406,11 @@ public: app * mk_bv_not(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNOT, arg); } app * mk_bv_xor(unsigned num, expr * const * args) { return m_manager.mk_app(get_fid(), OP_BXOR, num, args); } app * mk_bv_neg(expr * arg) { return m_manager.mk_app(get_fid(), OP_BNEG, arg); } - app * mk_bv_urem(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); } - app * mk_bv_srem(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); } - app * mk_bv_add(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } - app * mk_bv_sub(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } - app * mk_bv_mul(expr * arg1, expr * arg2) { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } + app * mk_bv_urem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BUREM, arg1, arg2); } + app * mk_bv_srem(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSREM, arg1, arg2); } + app * mk_bv_add(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BADD, arg1, arg2); } + app * mk_bv_sub(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BSUB, arg1, arg2); } + app * mk_bv_mul(expr * arg1, expr * arg2) const { return m_manager.mk_app(get_fid(), OP_BMUL, arg1, arg2); } app * mk_zero_extend(unsigned n, expr* e) { parameter p(n); return m_manager.mk_app(get_fid(), OP_ZERO_EXT, 1, &p, 1, &e); diff --git a/src/ast/macros/macro_util.cpp b/src/ast/macros/macro_util.cpp index 99732871c..fce6f1b28 100644 --- a/src/ast/macros/macro_util.cpp +++ b/src/ast/macros/macro_util.cpp @@ -19,22 +19,22 @@ Revision History: --*/ #include"macro_util.h" #include"occurs.h" +#include"ast_util.h" #include"arith_simplifier_plugin.h" -#include"basic_simplifier_plugin.h" #include"bv_simplifier_plugin.h" #include"var_subst.h" #include"ast_pp.h" #include"ast_ll_pp.h" -#include"ast_util.h" #include"for_each_expr.h" #include"well_sorted.h" +#include"bool_rewriter.h" macro_util::macro_util(ast_manager & m, simplifier & s): m_manager(m), + m_bv(m), m_simplifier(s), m_arith_simp(0), m_bv_simp(0), - m_basic_simp(0), m_forbidden_set(0), m_curr_clause(0) { } @@ -55,24 +55,17 @@ bv_simplifier_plugin * macro_util::get_bv_simp() const { return m_bv_simp; } -basic_simplifier_plugin * macro_util::get_basic_simp() const { - if (m_basic_simp == 0) { - const_cast(this)->m_basic_simp = static_cast(m_simplifier.get_plugin(m_manager.get_basic_family_id())); - } - SASSERT(m_basic_simp != 0); - return m_basic_simp; -} bool macro_util::is_bv(expr * n) const { - return get_bv_simp()->is_bv(n); + return m_bv.is_bv(n); } bool macro_util::is_bv_sort(sort * s) const { - return get_bv_simp()->is_bv_sort(s); + return m_bv.is_bv_sort(s); } bool macro_util::is_add(expr * n) const { - return get_arith_simp()->is_add(n) || get_bv_simp()->is_add(n); + return get_arith_simp()->is_add(n) || m_bv.is_bv_add(n); } bool macro_util::is_times_minus_one(expr * n, expr * & arg) const { @@ -80,11 +73,11 @@ bool macro_util::is_times_minus_one(expr * n, expr * & arg) const { } bool macro_util::is_le(expr * n) const { - return get_arith_simp()->is_le(n) || get_bv_simp()->is_le(n); + return get_arith_simp()->is_le(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); } bool macro_util::is_le_ge(expr * n) const { - return get_arith_simp()->is_le_ge(n) || get_bv_simp()->is_le_ge(n); + return get_arith_simp()->is_le_ge(n) || m_bv.is_bv_ule(n) || m_bv.is_bv_sle(n); } poly_simplifier_plugin * macro_util::get_poly_simp_for(sort * s) const { @@ -102,7 +95,7 @@ app * macro_util::mk_zero(sort * s) const { void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const { if (is_bv(t1)) { - get_bv_simp()->mk_sub(t1, t2, r); + r = m_bv.mk_bv_sub(t1, t2); } else { get_arith_simp()->mk_sub(t1, t2, r); @@ -111,7 +104,7 @@ void macro_util::mk_sub(expr * t1, expr * t2, expr_ref & r) const { void macro_util::mk_add(expr * t1, expr * t2, expr_ref & r) const { if (is_bv(t1)) { - get_bv_simp()->mk_add(t1, t2, r); + r = m_bv.mk_bv_add(t1, t2); } else { get_arith_simp()->mk_add(t1, t2, r); @@ -429,7 +422,7 @@ void macro_util::quasi_macro_head_to_macro_head(app * qhead, unsigned & num_decl new_args.push_back(new_var); new_conds.push_back(new_cond); } - get_basic_simp()->mk_and(new_conds.size(), new_conds.c_ptr(), cond); + bool_rewriter(m_manager).mk_and(new_conds.size(), new_conds.c_ptr(), cond); head = m_manager.mk_app(qhead->get_decl(), new_args.size(), new_args.c_ptr()); num_decls = next_var_idx; } @@ -687,7 +680,7 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def, if (cond == 0) new_cond = extra_cond; else - get_basic_simp()->mk_and(cond, extra_cond, new_cond); + bool_rewriter(m_manager).mk_and(cond, extra_cond, new_cond); } else { hint_to_macro_head(m_manager, head, num_decls, new_head); @@ -719,20 +712,19 @@ void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_con if (m_curr_clause == 0) return; SASSERT(is_clause(m_manager, m_curr_clause)); - basic_simplifier_plugin * bs = get_basic_simp(); expr_ref_buffer neg_other_lits(m_manager); unsigned num_lits = get_clause_num_literals(m_manager, m_curr_clause); for (unsigned i = 0; i < num_lits; i++) { expr * l = get_clause_literal(m_manager, m_curr_clause, i); if (l != except_lit) { expr_ref neg_l(m_manager); - bs->mk_not(l, neg_l); + bool_rewriter(m_manager).mk_not(l, neg_l); neg_other_lits.push_back(neg_l); } } if (neg_other_lits.empty()) return; - get_basic_simp()->mk_and(neg_other_lits.size(), neg_other_lits.c_ptr(), extra_cond); + bool_rewriter(m_manager).mk_and(neg_other_lits.size(), neg_other_lits.c_ptr(), extra_cond); } void macro_util::collect_poly_args(expr * n, expr * exception, ptr_buffer & args) { diff --git a/src/ast/macros/macro_util.h b/src/ast/macros/macro_util.h index 033f6ecb4..8aa8e550e 100644 --- a/src/ast/macros/macro_util.h +++ b/src/ast/macros/macro_util.h @@ -62,10 +62,10 @@ public: private: ast_manager & m_manager; + bv_util m_bv; simplifier & m_simplifier; arith_simplifier_plugin * m_arith_simp; bv_simplifier_plugin * m_bv_simp; - basic_simplifier_plugin * m_basic_simp; obj_hashtable * m_forbidden_set; bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); } @@ -99,7 +99,6 @@ public: arith_simplifier_plugin * get_arith_simp() const; bv_simplifier_plugin * get_bv_simp() const; - basic_simplifier_plugin * get_basic_simp() const; bool is_macro_head(expr * n, unsigned num_decls) const; bool is_left_simple_macro(expr * n, unsigned num_decls, app_ref & head, expr_ref & def) const; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index daf5e3702..663d4cbe1 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1981,6 +1981,7 @@ bool theory_seq::solve_nc(unsigned idx) { } if (c != n.contains()) { m_ncs.push_back(nc(c, deps)); + m_new_propagation = true; return true; } return false; @@ -2403,6 +2404,14 @@ void theory_seq::display(std::ostream & out) const { } } + if (!m_ncs.empty()) { + out << "Non contains:\n"; + for (unsigned i = 0; i < m_ncs.size(); ++i) { + out << "not " << mk_pp(m_ncs[i].contains(), m) << "\n"; + display_deps(out << " <- ", m_ncs[i].deps()); out << "\n"; + } + } + } void theory_seq::display_equations(std::ostream& out) const { @@ -3496,6 +3505,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) { let e = at(s, i) 0 <= i < len(s) -> s = xey & len(x) = i & len(e) = 1 + i < 0 \/ i >= len(s) -> e = empty */ void theory_seq::add_at_axiom(expr* e) { @@ -3509,13 +3519,18 @@ void theory_seq::add_at_axiom(expr* e) { expr_ref y = mk_skolem(m_post, s, mk_sub(mk_sub(len_s, i), one)); expr_ref xey = mk_concat(x, e, y); expr_ref len_x(m_util.str.mk_length(x), m); + expr_ref emp(m_util.str.mk_empty(m.get_sort(e)), m); literal i_ge_0 = mk_literal(m_autil.mk_ge(i, zero)); literal i_ge_len_s = mk_literal(m_autil.mk_ge(mk_sub(i, m_util.str.mk_length(s)), zero)); + add_axiom(~i_ge_0, i_ge_len_s, mk_seq_eq(s, xey)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(one, len_e, false)); add_axiom(~i_ge_0, i_ge_len_s, mk_eq(i, len_x, false)); + + add_axiom(i_ge_0, mk_eq(s, emp, false)); + add_axiom(~i_ge_len_s, mk_eq(s, emp, false)); } /** From 041520f72753f7c4283ccc9bc133df0da9f0d080 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 28 Mar 2017 18:17:22 +0100 Subject: [PATCH 17/23] SMT2 compliancy fix; NRA includes conversion of Int numerals --- src/ast/arith_decl_plugin.cpp | 59 ++++++++++++++++++++--------------- src/ast/arith_decl_plugin.h | 2 ++ 2 files changed, 36 insertions(+), 25 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index 546f037de..1c01496cf 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -35,7 +35,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper { ~algebraic_numbers_wrapper() { } - + unsigned mk_id(algebraic_numbers::anum const & val) { SASSERT(!m_amanager.is_rational(val)); unsigned new_id = m_id_gen.mk(); @@ -121,7 +121,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { m_int_decl = m->mk_sort(symbol("Int"), sort_info(id, INT_SORT)); m->inc_ref(m_int_decl); sort * i = m_int_decl; - + sort * b = m->mk_bool_sort(); #define MK_PRED(FIELD, NAME, KIND, SORT) { \ @@ -140,7 +140,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_PRED(m_i_ge_decl, ">=", OP_GE, i); MK_PRED(m_i_lt_decl, "<", OP_LT, i); MK_PRED(m_i_gt_decl, ">", OP_GT, i); - + #define MK_AC_OP(FIELD, NAME, KIND, SORT) { \ func_decl_info info(id, KIND); \ info.set_associative(); \ @@ -205,7 +205,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { MK_UNARY(m_asinh_decl, "asinh", OP_ASINH, r); MK_UNARY(m_acosh_decl, "acosh", OP_ACOSH, r); MK_UNARY(m_atanh_decl, "atanh", OP_ATANH, r); - + func_decl * pi_decl = m->mk_const_decl(symbol("pi"), r, func_decl_info(id, OP_PI)); m_pi = m->mk_const(pi_decl); m->inc_ref(m_pi); @@ -213,7 +213,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * e_decl = m->mk_const_decl(symbol("euler"), r, func_decl_info(id, OP_E)); m_e = m->mk_const(e_decl); m->inc_ref(m_e); - + func_decl * z_pw_z_int = m->mk_const_decl(symbol("0^0-int"), i, func_decl_info(id, OP_0_PW_0_INT)); m_0_pw_0_int = m->mk_const(z_pw_z_int); m->inc_ref(m_0_pw_0_int); @@ -221,7 +221,7 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) { func_decl * z_pw_z_real = m->mk_const_decl(symbol("0^0-real"), r, func_decl_info(id, OP_0_PW_0_REAL)); m_0_pw_0_real = m->mk_const(z_pw_z_real); m->inc_ref(m_0_pw_0_real); - + MK_OP(m_neg_root_decl, "neg-root", OP_NEG_ROOT, r); MK_UNARY(m_div_0_decl, "/0", OP_DIV_0, r); MK_UNARY(m_idiv_0_decl, "div0", OP_IDIV_0, i); @@ -285,7 +285,8 @@ arith_decl_plugin::arith_decl_plugin(): m_idiv_0_decl(0), m_mod_0_decl(0), m_u_asin_decl(0), - m_u_acos_decl(0) { + m_u_acos_decl(0), + m_convert_int_numerals_to_real(false) { } arith_decl_plugin::~arith_decl_plugin() { @@ -418,7 +419,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { if (val.is_unsigned()) { unsigned u_val = val.get_unsigned(); if (u_val < MAX_SMALL_NUM_TO_CACHE) { - if (is_int) { + if (is_int && !m_convert_int_numerals_to_real) { app * r = m_small_ints.get(u_val, 0); if (r == 0) { parameter p[2] = { parameter(val), parameter(1) }; @@ -442,7 +443,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) { } parameter p[2] = { parameter(val), parameter(static_cast(is_int)) }; func_decl * decl; - if (is_int) + if (is_int && !m_convert_int_numerals_to_real) decl = m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); else decl = m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)); @@ -479,14 +480,14 @@ static bool has_real_arg(ast_manager * m, unsigned num_args, expr * const * args } static bool is_const_op(decl_kind k) { - return - k == OP_PI || + return + k == OP_PI || k == OP_E || k == OP_0_PW_0_INT || k == OP_0_PW_0_REAL; } - -func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + +func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, arity); @@ -503,7 +504,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } } -func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned num_args, expr * const * args, sort * range) { if (k == OP_NUM) return mk_num_decl(num_parameters, parameters, num_args); @@ -521,9 +522,17 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters } void arith_decl_plugin::get_sort_names(svector& sort_names, symbol const & logic) { - // TODO: only define Int and Real in the right logics - sort_names.push_back(builtin_name("Int", INT_SORT)); - sort_names.push_back(builtin_name("Real", REAL_SORT)); + if (logic == "NRA" || + logic == "QF_NRA" || + logic == "QF_UFNRA") { + m_convert_int_numerals_to_real = true; + sort_names.push_back(builtin_name("Real", REAL_SORT)); + } + else { + // TODO: only define Int and Real in the right logics + sort_names.push_back(builtin_name("Int", INT_SORT)); + sort_names.push_back(builtin_name("Real", REAL_SORT)); + } } void arith_decl_plugin::get_op_names(svector& op_names, symbol const & logic) { @@ -563,16 +572,16 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con } bool arith_decl_plugin::is_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_IRRATIONAL_ALGEBRAIC_NUM) || is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_E); } bool arith_decl_plugin::is_unique_value(app * e) const { - return - is_app_of(e, m_family_id, OP_NUM) || + return + is_app_of(e, m_family_id, OP_NUM) || is_app_of(e, m_family_id, OP_PI) || is_app_of(e, m_family_id, OP_E); } @@ -671,7 +680,7 @@ expr_ref arith_util::mk_mul_simplify(expr_ref_vector const& args) { } expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { expr_ref result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(1), true); @@ -681,7 +690,7 @@ expr_ref arith_util::mk_mul_simplify(unsigned sz, expr* const* args) { break; default: result = mk_mul(sz, args); - break; + break; } return result; } @@ -692,7 +701,7 @@ expr_ref arith_util::mk_add_simplify(expr_ref_vector const& args) { } expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { expr_ref result(m_manager); - + switch (sz) { case 0: result = mk_numeral(rational(0), true); @@ -702,7 +711,7 @@ expr_ref arith_util::mk_add_simplify(unsigned sz, expr* const* args) { break; default: result = mk_add(sz, args); - break; + break; } return result; } diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index 410c50852..668eebcc9 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -152,6 +152,8 @@ protected: ptr_vector m_small_ints; ptr_vector m_small_reals; + bool m_convert_int_numerals_to_real; + func_decl * mk_func_decl(decl_kind k, bool is_real); virtual void set_manager(ast_manager * m, family_id id); decl_kind fix_kind(decl_kind k, unsigned arity); From ef3d340c85e4dbe7bdfb74303bae3468cfe35d59 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 31 Mar 2017 12:04:46 +0100 Subject: [PATCH 18/23] Improved decl_collector for uninterpreted sorts in :print_benchmark output --- src/ast/decl_collector.cpp | 28 +++++++++++++++++++++------- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index b663a9df3..773ebefc7 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -23,8 +23,21 @@ void decl_collector::visit_sort(sort * n) { family_id fid = n->get_family_id(); if (m().is_uninterp(n)) m_sorts.push_back(n); - if (fid == m_dt_fid) + if (fid == m_dt_fid) { m_sorts.push_back(n); + + unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); + for (unsigned i = 0; i < num_cnstr; i++) { + func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); + m_decls.push_back(cnstr); + ptr_vector const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); + unsigned num_cas = cnstr_acc.size(); + for (unsigned j = 0; j < num_cas; j++) { + func_decl * accsr = cnstr_acc.get(j); + m_decls.push_back(accsr); + } + } + } } bool decl_collector::is_bool(sort * s) { @@ -38,14 +51,15 @@ void decl_collector::visit_func(func_decl * n) { m_preds.push_back(n); else m_decls.push_back(n); - } + } } decl_collector::decl_collector(ast_manager & m, bool preds): m_manager(m), - m_sep_preds(preds) { + m_sep_preds(preds), + m_dt_util(m) { m_basic_fid = m_manager.get_basic_family_id(); - m_dt_fid = m_manager.mk_family_id("datatype"); + m_dt_fid = m_dt_util.get_family_id(); } void decl_collector::visit(ast* n) { @@ -55,7 +69,7 @@ void decl_collector::visit(ast* n) { n = todo.back(); todo.pop_back(); if (!m_visited.is_marked(n)) { - m_visited.mark(n, true); + m_visited.mark(n, true); switch(n->get_kind()) { case AST_APP: { app * a = to_app(n); @@ -64,7 +78,7 @@ void decl_collector::visit(ast* n) { } todo.push_back(a->get_decl()); break; - } + } case AST_QUANTIFIER: { quantifier * q = to_quantifier(n); unsigned num_decls = q->get_num_decls(); @@ -77,7 +91,7 @@ void decl_collector::visit(ast* n) { } break; } - case AST_SORT: + case AST_SORT: visit_sort(to_sort(n)); break; case AST_FUNC_DECL: { From 0fb31611135d0d3fc305414ff449e522d92f63ec Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 31 Mar 2017 12:10:51 +0100 Subject: [PATCH 19/23] Updated declarations in decl_collector --- src/ast/decl_collector.h | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 678f3805d..0067d18eb 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -21,6 +21,7 @@ Revision History: #define SMT_DECL_COLLECTOR_H_ #include"ast.h" +#include"datatype_decl_plugin.h" class decl_collector { ast_manager & m_manager; @@ -28,9 +29,10 @@ class decl_collector { ptr_vector m_sorts; ptr_vector m_decls; ptr_vector m_preds; - ast_mark m_visited; - family_id m_basic_fid; - family_id m_dt_fid; + ast_mark m_visited; + family_id m_basic_fid; + family_id m_dt_fid; + datatype_util m_dt_util; void visit_sort(sort* n); bool is_bool(sort* s); From c99205fa7e9931cea4a267d789cbd8c83744c320 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 08:12:53 -0700 Subject: [PATCH 20/23] return box model based on index. Issue #955 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/basic_cmds.cpp | 35 +++++++++++++++++++++++++++------- src/cmd_context/cmd_context.h | 1 + src/opt/opt_context.cpp | 8 ++++++++ src/opt/opt_context.h | 1 + 4 files changed, 38 insertions(+), 7 deletions(-) diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index d951f7710..f09d35158 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -100,13 +100,34 @@ public: ATOMIC_CMD(exit_cmd, "exit", "exit.", ctx.print_success(); throw stop_parser_exception();); -ATOMIC_CMD(get_model_cmd, "get-model", "retrieve model for the last check-sat command", { - if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) - throw cmd_exception("model is not available"); - model_ref m; - ctx.get_check_sat_result()->get_model(m); - ctx.display_model(m); -}); +class get_model_cmd : public cmd { + unsigned m_index; +public: + get_model_cmd(): cmd("get-model"), m_index(0) {} + virtual char const * get_usage() const { return "[]"; } + virtual char const * get_descr(cmd_context & ctx) const { + return "retrieve model for the last check-sat command.\nSupply optional index if retrieving a model corresponding to a box optimization objective"; + } + virtual unsigned get_arity() const { return VAR_ARITY; } + virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_UINT; } + virtual void set_next_arg(cmd_context & ctx, unsigned index) { m_index = index; } + virtual void execute(cmd_context & ctx) { + if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) + throw cmd_exception("model is not available"); + model_ref m; + if (m_index > 0 && ctx.get_opt()) { + ctx.get_opt()->get_box_model(m, m_index); + } + else { + ctx.get_check_sat_result()->get_model(m); + } + ctx.display_model(m); + } + virtual void reset(cmd_context& ctx) { + m_index = 0; + } +}; + ATOMIC_CMD(get_assignment_cmd, "get-assignment", "retrieve assignment", { if (!ctx.is_model_available() || ctx.get_check_sat_result() == 0) diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h index 8eee632dc..92943c71c 100644 --- a/src/cmd_context/cmd_context.h +++ b/src/cmd_context/cmd_context.h @@ -124,6 +124,7 @@ public: virtual bool is_pareto() = 0; virtual void set_logic(symbol const& s) = 0; virtual bool print_model() const = 0; + virtual void get_box_model(model_ref& mdl, unsigned index) = 0; virtual void updt_params(params_ref const& p) = 0; }; diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index d1b7a489e..af3c57baa 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -342,6 +342,14 @@ namespace opt { fix_model(mdl); } + void context::get_box_model(model_ref& mdl, unsigned index) { + if (index >= m_box_models.size()) { + throw default_exception("index into models is out of bounds"); + } + mdl = m_box_models[index]; + fix_model(mdl); + } + lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) { if (scoped) get_solver().push(); lbool result = m_optsmt.lex(index, is_max); diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h index f51f75830..53bfc19c5 100644 --- a/src/opt/opt_context.h +++ b/src/opt/opt_context.h @@ -186,6 +186,7 @@ namespace opt { virtual bool print_model() const; virtual void set_model(model_ref& _m) { m_model = _m; } virtual void get_model(model_ref& _m); + virtual void get_box_model(model_ref& _m, unsigned index); virtual void fix_model(model_ref& _m); virtual void collect_statistics(statistics& stats) const; virtual proof* get_proof() { return 0; } From 8f798fef1a10706f9871f7baff12b564326d6fc7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 08:24:12 -0700 Subject: [PATCH 21/23] fix python interface for string extract to take symbolic indices per bug report from Kun Wei Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 16d7fbb5f..568ffe9a2 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -3701,12 +3701,8 @@ def Extract(high, low, a): high = StringVal(high) if is_seq(high): s = high - offset = _py2expr(low, high.ctx) - length = _py2expr(a, high.ctx) - - if __debug__: - _z3_assert(is_int(offset) and is_int(length), "Second and third arguments must be integers") - return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) + offset, length = _coerce_exprs(low, a, s.ctx) + return SeqRef(Z3_mk_seq_extract(s.ctx_ref(), s.as_ast(), offset.as_ast(), length.as_ast()), s.ctx) if __debug__: _z3_assert(low <= high, "First argument must be greater than or equal to second argument") _z3_assert(_is_int(high) and high >= 0 and _is_int(low) and low >= 0, "First and second arguments must be non negative integers") From 582880346e8c8ad814f59391d304a04bdc3b5cef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 09:22:56 -0700 Subject: [PATCH 22/23] add index option to 'eval' command for box objectives. Issue #955 Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 66 +++++++++++++++++++++++++++---- src/cmd_context/eval_cmd.cpp | 9 ++++- 2 files changed, 66 insertions(+), 9 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a62eea6ea..3d7da43a7 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -12,6 +12,7 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2015-12-5 + Murphy Berzish 2017-02-21 Notes: @@ -514,30 +515,56 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu bool constantPos = m_autil.is_numeral(b, pos); bool constantLen = m_autil.is_numeral(c, len); - // case 1: pos<0 or len<0 + // case 1: pos<0 or len<=0 // rewrite to "" - if ( (constantPos && pos.is_neg()) || (constantLen && len.is_neg()) ) { + if ( (constantPos && pos.is_neg()) || (constantLen && !len.is_pos()) ) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } // case 1.1: pos >= length(base) // rewrite to "" - if (constantBase && constantPos && pos.get_unsigned() >= s.length()) { + if (constantBase && constantPos && pos >= rational(s.length())) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } + constantPos &= pos.is_unsigned(); + constantLen &= len.is_unsigned(); + if (constantBase && constantPos && constantLen) { if (pos.get_unsigned() + len.get_unsigned() >= s.length()) { // case 2: pos+len goes past the end of the string unsigned _len = s.length() - pos.get_unsigned() + 1; result = m_util.str.mk_string(s.extract(pos.get_unsigned(), _len)); - return BR_DONE; } else { // case 3: pos+len still within string result = m_util.str.mk_string(s.extract(pos.get_unsigned(), len.get_unsigned())); - return BR_DONE; } + return BR_DONE; + } + + if (constantPos && constantLen) { + unsigned _pos = pos.get_unsigned(); + unsigned _len = len.get_unsigned(); + SASSERT(_len > 0); + expr_ref_vector as(m()), bs(m()); + m_util.str.get_concat(a, as); + for (unsigned i = 0; i < as.size() && _len > 0; ++i) { + if (m_util.str.is_unit(as[i].get())) { + if (_pos == 0) { + bs.push_back(as[i].get()); + --_len; + } + else { + --_pos; + } + } + else { + return BR_FAILED; + } + } + result = m_util.str.mk_concat(bs); + return BR_DONE; } return BR_FAILED; @@ -640,10 +667,33 @@ br_status seq_rewriter::mk_seq_at(expr* a, expr* b, expr_ref& result) { result = m_util.str.mk_empty(m().get_sort(a)); return BR_DONE; } - if (m_util.str.is_string(a, c) && r.is_unsigned() && r < rational(c.length())) { - result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1)); + if (m_util.str.is_string(a, c)) { + if (r.is_unsigned() && r < rational(c.length())) { + result = m_util.str.mk_string(c.extract(r.get_unsigned(), 1)); + } + else { + result = m_util.str.mk_empty(m().get_sort(a)); + } return BR_DONE; - } + } + if (r.is_unsigned()) { + len = r.get_unsigned(); + expr_ref_vector as(m()); + m_util.str.get_concat(a, as); + for (unsigned i = 0; i < as.size(); ++i) { + if (m_util.str.is_unit(as[i].get())) { + if (len == 0) { + result = as[i].get(); + return BR_DONE; + } + --len; + } + else { + return BR_FAILED; + } + } + } + } return BR_FAILED; } diff --git a/src/cmd_context/eval_cmd.cpp b/src/cmd_context/eval_cmd.cpp index 94583001b..86078a13c 100644 --- a/src/cmd_context/eval_cmd.cpp +++ b/src/cmd_context/eval_cmd.cpp @@ -38,6 +38,7 @@ public: virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { model_evaluator::get_param_descrs(p); insert_timeout(p); + p.insert("model_index", CPK_UINT, "(default: 0) index of model from box optimization objective"); } virtual void prepare(cmd_context & ctx) { @@ -58,9 +59,15 @@ public: if (!ctx.is_model_available()) throw cmd_exception("model is not available"); model_ref md; + unsigned index = m_params.get_uint("model_index", 0); check_sat_result * last_result = ctx.get_check_sat_result(); SASSERT(last_result); - last_result->get_model(md); + if (index == 0 || !ctx.get_opt()) { + last_result->get_model(md); + } + else { + ctx.get_opt()->get_box_model(md, index); + } expr_ref r(ctx.m()); unsigned timeout = m_params.get_uint("timeout", UINT_MAX); unsigned rlimit = m_params.get_uint("rlimit", 0); From c4b26cd691ddfa303b36a6b5a37ac1948352e5be Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 31 Mar 2017 16:38:15 -0700 Subject: [PATCH 23/23] add bypass to allow recursive functions from API Signed-off-by: Nikolaj Bjorner --- src/api/api_quant.cpp | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index bf64aa571..e87b9446f 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -69,14 +69,17 @@ extern "C" { } expr * const* ps = reinterpret_cast(patterns); expr * const* no_ps = reinterpret_cast(no_patterns); - pattern_validator v(mk_c(c)->m()); - for (unsigned i = 0; i < num_patterns; i++) { - if (!v(num_decls, ps[i], 0, 0)) { - SET_ERROR_CODE(Z3_INVALID_PATTERN); - return 0; + symbol qid = to_symbol(quantifier_id); + bool is_rec = mk_c(c)->m().rec_fun_qid() == qid; + if (!is_rec) { + pattern_validator v(mk_c(c)->m()); + for (unsigned i = 0; i < num_patterns; i++) { + if (!v(num_decls, ps[i], 0, 0)) { + SET_ERROR_CODE(Z3_INVALID_PATTERN); + return 0; + } } } - sort* const* ts = reinterpret_cast(sorts); svector names; for (unsigned i = 0; i < num_decls; ++i) { @@ -88,7 +91,7 @@ extern "C" { (0 != is_forall), names.size(), ts, names.c_ptr(), to_expr(body), weight, - to_symbol(quantifier_id), + qid, to_symbol(skolem_id), num_patterns, ps, num_no_patterns, no_ps