From 866035d786ca69860359d7833a6c15108f7c0740 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 24 Mar 2017 09:40:18 +0000 Subject: [PATCH 01/10] 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 02/10] 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 03/10] 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 04/10] 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 05/10] 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 06/10] 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 07/10] 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 08/10] 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 09/10] 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 10/10] 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)