diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index 56b402ad5..62aac110d 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -65,6 +65,15 @@ void throw_z3_error(Z3_context c, Z3_error_code e) longjmp(g_catch_buffer, e); } +/** + \brief Error handling that depends on checking an error code on the context. + +*/ + +void nothrow_z3_error(Z3_context c, Z3_error_code e) { + // no-op +} + /** \brief Create a logical context. @@ -1592,18 +1601,16 @@ void error_code_example1() void error_code_example2() { Z3_config cfg; Z3_context ctx = NULL; - int r; + Z3_error_code e; printf("\nerror_code_example2\n"); LOG_MSG("error_code_example2"); - /* low tech try&catch */ - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { Z3_ast x, y, app; cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); Z3_del_config(cfg); x = mk_int_var(ctx, "x"); @@ -1611,11 +1618,14 @@ void error_code_example2() { printf("before Z3_mk_iff\n"); /* the next call will produce an error */ app = Z3_mk_iff(ctx, x, y); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { Z3_del_context(ctx); } @@ -1781,15 +1791,14 @@ void parser_example5() { Z3_config cfg; Z3_context ctx = NULL; Z3_solver s = NULL; - int r; + Z3_error_code e; printf("\nparser_example5\n"); LOG_MSG("parser_example5"); - r = setjmp(g_catch_buffer); - if (r == 0) { + if (1) { cfg = Z3_mk_config(); - ctx = mk_context_custom(cfg, throw_z3_error); + ctx = mk_context_custom(cfg, nothrow_z3_error); s = mk_solver(ctx); Z3_del_config(cfg); @@ -1798,12 +1807,15 @@ void parser_example5() { "(benchmark tst :extrafuns ((x Int (y Int)) :formula (> x y) :formula (> x 0))", 0, 0, 0, 0, 0, 0); + e = Z3_get_error_code(ctx); + if (e != Z3_OK) goto err; unreachable(); del_solver(ctx, s); Z3_del_context(ctx); } else { - printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, (Z3_error_code)r)); + err: + printf("Z3 error: %s.\n", Z3_get_error_msg(ctx, e)); if (ctx != NULL) { printf("Error message: '%s'.\n",Z3_get_smtlib_error(ctx)); del_solver(ctx, s); diff --git a/src/api/api_parsers.cpp b/src/api/api_parsers.cpp index f402f18c9..7641bd7c6 100644 --- a/src/api/api_parsers.cpp +++ b/src/api/api_parsers.cpp @@ -57,19 +57,20 @@ extern "C" { Z3_func_decl const decls[]) { Z3_TRY; LOG_Z3_parse_smtlib_string(c, str, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); bool ok = false; RESET_ERROR_CODE(); init_smtlib_parser(c, num_sorts, sort_names, sorts, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_string(str); } catch (...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); @@ -89,16 +90,17 @@ extern "C" { LOG_Z3_parse_smtlib_file(c, file_name, num_sorts, sort_names, types, num_decls, decl_names, decls); bool ok = false; RESET_ERROR_CODE(); - std::ostringstream outs; + std::ostringstream* outs = alloc(std::ostringstream); init_smtlib_parser(c, num_sorts, sort_names, types, num_decls, decl_names, decls); - mk_c(c)->m_smtlib_parser->set_error_stream(outs); + mk_c(c)->m_smtlib_parser->set_error_stream(*outs); try { ok = mk_c(c)->m_smtlib_parser->parse_file(file_name); } catch(...) { ok = false; } - mk_c(c)->m_smtlib_error_buffer = outs.str(); + mk_c(c)->m_smtlib_error_buffer = outs->str(); + dealloc(outs); if (!ok) { mk_c(c)->reset_parser(); SET_ERROR_CODE(Z3_PARSER_ERROR); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index d09129d37..eb38c5fa5 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 Z3_API 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; diff --git a/src/ast/rewriter/maximize_ac_sharing.cpp b/src/ast/rewriter/maximize_ac_sharing.cpp index d7e8df7a2..a838f59fa 100644 --- a/src/ast/rewriter/maximize_ac_sharing.cpp +++ b/src/ast/rewriter/maximize_ac_sharing.cpp @@ -54,13 +54,13 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr TRACE("ac_sharing_detail", tout << "args: "; for (unsigned i = 0; i < num_args; i++) tout << mk_pp(_args[i], m) << "\n";); try_to_reuse: if (num_args > 1 && num_args < MAX_NUM_ARGS_FOR_OPT) { - for (unsigned i = 0; i < num_args - 1; i++) { + for (unsigned i = 0; i + 1 < num_args; i++) { for (unsigned j = i + 1; j < num_args; j++) { if (contains(f, _args[i], _args[j])) { TRACE("ac_sharing_detail", tout << "reusing args: " << i << " " << j << "\n";); _args[i] = m.mk_app(f, _args[i], _args[j]); SASSERT(num_args > 1); - for (unsigned w = j; w < num_args - 1; w++) { + for (unsigned w = j; w + 1 < num_args; w++) { _args[w] = _args[w+1]; } num_args--; @@ -144,6 +144,7 @@ void maximize_ac_sharing::restore_entries(unsigned old_lim) { while (i != old_lim) { --i; entry * e = m_entries[i]; + m_cache.remove(e); m.dec_ref(e->m_arg1); m.dec_ref(e->m_arg2); } diff --git a/src/interp/iz3mgr.h b/src/interp/iz3mgr.h index 6ca8fae34..e4c294059 100755 --- a/src/interp/iz3mgr.h +++ b/src/interp/iz3mgr.h @@ -96,7 +96,7 @@ class ast_r : public ast_i { ast_r(const ast_r &other) : ast_i(other) { _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); } ast_r &operator=(const ast_r &other) { @@ -104,7 +104,7 @@ class ast_r : public ast_i { _m->dec_ref(_ast); _ast = other._ast; _m = other._m; - _m->inc_ref(_ast); + if (_m) _m->inc_ref(_ast); return *this; } diff --git a/src/model/model_core.cpp b/src/model/model_core.cpp index 4290700d4..833c254c3 100644 --- a/src/model/model_core.cpp +++ b/src/model/model_core.cpp @@ -86,18 +86,22 @@ void model_core::register_decl(func_decl * d, func_interp * fi) { void model_core::unregister_decl(func_decl * d) { decl2expr::obj_map_entry * ec = m_interp.find_core(d); if (ec && ec->get_data().m_value != 0) { + auto k = ec->get_data().m_key; + auto v = ec->get_data().m_value; m_interp.remove(d); m_const_decls.erase(d); - m_manager.dec_ref(ec->get_data().m_key); - m_manager.dec_ref(ec->get_data().m_value); + m_manager.dec_ref(k); + m_manager.dec_ref(v); return; } decl2finterp::obj_map_entry * ef = m_finterp.find_core(d); if (ef && ef->get_data().m_value != 0) { + auto k = ef->get_data().m_key; + auto v = ef->get_data().m_value; m_finterp.remove(d); m_func_decls.erase(d); - m_manager.dec_ref(ef->get_data().m_key); - dealloc(ef->get_data().m_value); + m_manager.dec_ref(k); + dealloc(v); } } diff --git a/src/muz/rel/tbv.cpp b/src/muz/rel/tbv.cpp index 7475750db..69cc4819a 100644 --- a/src/muz/rel/tbv.cpp +++ b/src/muz/rel/tbv.cpp @@ -74,8 +74,7 @@ tbv* tbv_manager::allocate(tbv const& bv) { } tbv* tbv_manager::allocate(uint64 val) { tbv* v = allocate0(); - for (unsigned bit = num_tbits(); bit > 0;) { - --bit; + for (unsigned bit = std::min(64u, num_tbits()); bit-- > 0;) { if (val & (1ULL << bit)) { set(*v, bit, BIT_1); } else { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index cc79e75ff..4447b399c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -2823,6 +2823,7 @@ namespace sat { pop(num_scopes); exchange_par(); reinit_assumptions(); + m_stats.m_units = init_trail_size(); } void solver::pop(unsigned num_scopes) { @@ -4032,25 +4033,11 @@ namespace sat { st.update("minimized lits", m_minimized_lits); st.update("dyn subsumption resolution", m_dyn_sub_res); st.update("blocked correction sets", m_blocked_corr_sets); + st.update("units", m_units); } void stats::reset() { - m_mk_var = 0; - m_mk_bin_clause = 0; - m_mk_ter_clause = 0; - m_mk_clause = 0; - m_conflict = 0; - m_propagate = 0; - m_bin_propagate = 0; - m_ter_propagate = 0; - m_decision = 0; - m_restart = 0; - m_gc_clause = 0; - m_del_clause = 0; - m_minimized_lits = 0; - m_dyn_sub_res = 0; - m_non_learned_generation = 0; - m_blocked_corr_sets = 0; + memset(this, sizeof(*this), 0); } void mk_stat::display(std::ostream & out) const { diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index c115b71bb..fa095623f 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -67,6 +67,7 @@ namespace sat { unsigned m_dyn_sub_res; unsigned m_non_learned_generation; unsigned m_blocked_corr_sets; + unsigned m_units; stats() { reset(); } void reset(); void collect_statistics(statistics & st) const; diff --git a/src/sat/sat_watched.h b/src/sat/sat_watched.h index 2bbf8aa77..d1333c314 100644 --- a/src/sat/sat_watched.h +++ b/src/sat/sat_watched.h @@ -109,10 +109,10 @@ namespace sat { bool operator!=(watched const & w) const { return !operator==(w); } }; - COMPILE_TIME_ASSERT(0 <= watched::BINARY && watched::BINARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::TERNARY && watched::TERNARY <= 3); - COMPILE_TIME_ASSERT(0 <= watched::CLAUSE && watched::CLAUSE <= 3); - COMPILE_TIME_ASSERT(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3); + static_assert(0 <= watched::BINARY && watched::BINARY <= 3, ""); + static_assert(0 <= watched::TERNARY && watched::TERNARY <= 3, ""); + static_assert(0 <= watched::CLAUSE && watched::CLAUSE <= 3, ""); + static_assert(0 <= watched::EXT_CONSTRAINT && watched::EXT_CONSTRAINT <= 3, ""); struct watched_lt { bool operator()(watched const & w1, watched const & w2) const { diff --git a/src/smt/smt_theory_var_list.h b/src/smt/smt_theory_var_list.h index d7e246824..aa2816786 100644 --- a/src/smt/smt_theory_var_list.h +++ b/src/smt/smt_theory_var_list.h @@ -67,9 +67,9 @@ namespace smt { }; // 32 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int)); + static_assert(sizeof(expr*) != 4 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int), "32 bit"); // 64 bit machine - COMPILE_TIME_ASSERT(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int)); + static_assert(sizeof(expr*) != 8 || sizeof(theory_var_list) == sizeof(theory_var_list *) + sizeof(int) + /* a structure must be aligned */ sizeof(int), "64 bit"); }; #endif /* SMT_THEORY_VAR_LIST_H_ */ diff --git a/src/tactic/portfolio/parallel_tactic.cpp b/src/tactic/portfolio/parallel_tactic.cpp index c8cb7e2ee..5cd508042 100644 --- a/src/tactic/portfolio/parallel_tactic.cpp +++ b/src/tactic/portfolio/parallel_tactic.cpp @@ -21,21 +21,73 @@ Notes: --*/ #include "util/scoped_ptr_vector.h" +#include "ast/ast_util.h" #include "solver/solver.h" +#include "solver/solver2tactic.h" #include "tactic/tactic.h" +#include "tactic/portfolio/fd_solver.h" class parallel_tactic : public tactic { + class solver_state { + ref m_solver; + expr_ref_vector m_cube; + unsigned m_units; + public: + solver_state(solver* s): m_solver(s), m_cube(s->get_manager()), m_units(0) {} + + solver_state& operator=(solver_state& other) { + m_solver = other.m_solver; + m_cube.reset(); + m_cube.append(other.m_cube); + m_units = other.m_units; + return *this; + } + + void update_units() { + m_units = 0; + statistics st; + m_solver->collect_statistics(st); + std::string units("units"); + for (unsigned i = st.size(); i-- > 0; ) { + if (st.get_key(i) == units) { + m_units = st.get_uint_value(i); + break; + } + } + } + + expr_ref cube() { return mk_and(m_cube); } + + void add_cube(expr* c) { m_cube.push_back(c); } + + unsigned num_units() const { return m_units; } + + solver& get_solver() { return *m_solver; } + + solver const& get_solver() const { return *m_solver; } + }; + +public: + bool operator()(solver_state* s1, solver_state* s2) const { + return s1->num_units() > s2->num_units(); + } +private: + + ast_manager* m_manager; + // parameters unsigned m_conflicts_lower_bound; unsigned m_conflicts_upper_bound; unsigned m_conflicts_growth_rate; unsigned m_conflicts_decay_rate; - unsigned m_num_threads; + unsigned m_num_threads; + + double m_progress; + unsigned m_max_conflicts; + statistics m_stats; - unsigned m_max_conflicts; - - sref_vector m_solvers; + vector m_solvers; scoped_ptr_vector m_managers; void init() { @@ -44,7 +96,8 @@ class parallel_tactic : public tactic { m_conflicts_growth_rate = 150; m_conflicts_decay_rate = 75; m_max_conflicts = m_conflicts_lower_bound; - m_num_threads = omp_get_num_threads(); + m_progress = 0; + m_num_threads = omp_get_num_threads(); // TBD adjust by possible threads used inside each solver. } unsigned get_max_conflicts() { @@ -56,13 +109,41 @@ class parallel_tactic : public tactic { } bool should_increase_conflicts() { - NOT_IMPLEMENTED_YET(); - return false; + return m_progress < 0; + } + + void update_progress(bool b) { + m_progress = 0.9 * m_progress + (b ? 1 : -1); } int pick_solvers() { - NOT_IMPLEMENTED_YET(); - return 1; + // order solvers by number of units in descending order + for (solver_state* s : m_solvers) s->update_units(); + std::sort(m_solvers.c_ptr(), m_solvers.c_ptr() + m_solvers.size(), *this); + TRACE("parallel_tactic", display(tout);); + return std::min(m_num_threads, m_solvers.size()); + } + + int max_num_splits() { + if (m_solvers.empty()) { + return m_num_threads; + } + uint64 max_mem = memory::get_max_memory_size(); + uint64 cur_mem = memory::get_allocation_size(); + uint64 sol_sz = cur_mem / m_solvers.size(); + + TRACE("parallel_tactic", tout << "max mem: " << max_mem << " cur mem: " << cur_mem << " num solvers: " << m_solvers.size() << "\n";); + if (max_mem <= cur_mem) { + return 0; + } + if (cur_mem == 0) { + return m_num_threads; + } + uint64 extra_solvers = (max_mem - cur_mem) / (2 * sol_sz); + if (extra_solvers > m_num_threads) { + return m_num_threads; + } + return static_cast(extra_solvers); } void update_max_conflicts() { @@ -86,11 +167,11 @@ class parallel_tactic : public tactic { return is_sat; } - lbool lookahead(solver& s) { + void cube(solver& s, expr_ref_vector& cubes) { ast_manager& m = s.get_manager(); params_ref p; p.set_uint("sat.lookahead.cube.cutoff", 1); - expr_ref_vector cubes(m); + s.updt_params(p); while (true) { expr_ref c = s.cube(); if (m.is_false(c)) { @@ -98,32 +179,13 @@ class parallel_tactic : public tactic { } cubes.push_back(c); } - if (cubes.empty()) { - return l_false; - } - for (unsigned i = 1; i < cubes.size(); ++i) { - ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode()); - solver* s1 = s.translate(*new_m, params_ref()); - ast_translation translate(m, *new_m); - expr_ref cube(translate(cubes[i].get()), *new_m); - s1->assert_expr(cube); - - #pragma omp critical (_solvers) - { - m_managers.push_back(new_m); - m_solvers.push_back(s1); - } - } - s.assert_expr(cubes[0].get()); - return l_true; } lbool solve(solver& s) { params_ref p; p.set_uint("sat.max_conflicts", get_max_conflicts()); s.updt_params(p); - lbool is_sat = s.check_sat(0, 0); - return is_sat; + return s.check_sat(0, 0); } void remove_unsat(svector& unsat) { @@ -131,12 +193,24 @@ class parallel_tactic : public tactic { unsat.reverse(); DEBUG_CODE(for (unsigned i = 0; i + 1 < unsat.size(); ++i) SASSERT(unsat[i] > unsat[i+1]);); for (int i : unsat) { - m_solvers.erase(i); + m_solvers[i]->get_solver().collect_statistics(m_stats); + dealloc(m_solvers[i]); + for (unsigned j = i + 1; j < m_solvers.size(); ++j) { + m_solvers[j - 1] = m_solvers[j]; + } + m_solvers.shrink(m_solvers.size() - 1); } unsat.reset(); } - lbool solve() { + void get_model(model_ref& mdl, int sat_index) { + SASSERT(sat_index != -1); + m_solvers[sat_index]->get_solver().get_model(mdl); + ast_translation translate(m_solvers[sat_index]->get_solver().get_manager(), *m_manager); + mdl = mdl->translate(translate); + } + + lbool solve(model_ref& mdl) { while (true) { int sz = pick_solvers(); @@ -147,72 +221,171 @@ class parallel_tactic : public tactic { int sat_index = -1; // Simplify phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :simplify " << sz << ")\n";); #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = simplify(*m_solvers[i]); + lbool is_sat = simplify(m_solvers[i]->get_solver()); switch (is_sat) { case l_false: unsat.push_back(i); break; case l_true: sat_index = i; break; case l_undef: break; } } - if (sat_index != -1) return l_true; // TBD: extact model + if (sat_index != -1) { + get_model(mdl, sat_index); + return l_true; + } sz -= unsat.size(); remove_unsat(unsat); if (sz == 0) continue; // Solve phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :solve " << sz << ")\n";); #pragma omp parallel for for (int i = 0; i < sz; ++i) { - lbool is_sat = solve(*m_solvers[i]); + lbool is_sat = solve(m_solvers[i]->get_solver()); switch (is_sat) { - case l_false: unsat.push_back(i); break; + case l_false: update_progress(true); unsat.push_back(i); break; case l_true: sat_index = i; break; - case l_undef: break; + case l_undef: update_progress(false); break; } } - if (sat_index != -1) return l_true; // TBD: extact model + if (sat_index != -1) { + get_model(mdl, sat_index); + return l_true; + } sz -= unsat.size(); remove_unsat(unsat); + + sz = std::min(max_num_splits(), sz); if (sz == 0) continue; + + vector cubes; + for (int i = 0; i < sz; ++i) { + cubes.push_back(expr_ref_vector(m_solvers[i]->get_solver().get_manager())); + } // Split phase. + IF_VERBOSE(1, verbose_stream() << "(solver.parallel :split " << sz << ")\n";); #pragma omp parallel for + for (int i = 0; i < sz; ++i) { + cube(m_solvers[i]->get_solver(), cubes[i]); + } + for (int i = 0; i < sz; ++i) { - lbool is_sat = lookahead(*m_solvers[i]); - switch (is_sat) { - case l_false: unsat.push_back(i); break; - case l_true: break; - case l_undef: break; + if (cubes[i].empty()) { + unsat.push_back(i); + continue; } + solver& s = m_solvers[i]->get_solver(); + ast_manager& m = s.get_manager(); + for (unsigned j = 1; j < cubes[i].size(); ++j) { + ast_manager * new_m = alloc(ast_manager, m, !m.proof_mode()); + solver* s1 = s.translate(*new_m, params_ref()); + ast_translation translate(m, *new_m); + expr_ref cube(translate(cubes[i][j].get()), *new_m); + s1->assert_expr(cube); + m_managers.push_back(new_m); + solver_state* st = alloc(solver_state, s1); + st->add_cube(cube); + m_solvers.push_back(st); + } + expr* cube0 = cubes[i][0].get(); + m_solvers[i]->add_cube(cube0); + s.assert_expr(cube0); } remove_unsat(unsat); - update_max_conflicts(); } return l_undef; } + std::ostream& display(std::ostream& out) { + for (solver_state* s : m_solvers) { + out << "solver units" << s->num_units() << "\n"; + out << "cube " << s->cube() << "\n"; + } + return out; + } + + public: - parallel_tactic(solver* s) { - m_solvers.push_back(s); // clone it? + parallel_tactic() : + m_manager(0) { + init(); } void operator ()(const goal_ref & g,goal_ref_buffer & result,model_converter_ref & mc,proof_converter_ref & pc,expr_dependency_ref & dep) { - NOT_IMPLEMENTED_YET(); + ast_manager& m = g->m(); + m_manager = &m; + params_ref p; + solver* s = mk_fd_solver(m, p); + m_solvers.push_back(alloc(solver_state, s)); + expr_ref_vector clauses(m); + ptr_vector assumptions; + obj_map bool2dep; + ref fmc; + extract_clauses_and_dependencies(g, clauses, assumptions, bool2dep, fmc); + for (expr * clause : clauses) { + s->assert_expr(clause); + } + SASSERT(assumptions.empty()); + model_ref mdl; + lbool is_sat = solve(mdl); + switch (is_sat) { + case l_true: + if (g->models_enabled()) { + mc = model2model_converter(mdl.get()); + mc = concat(fmc.get(), mc.get()); + } + g->reset(); + result.push_back(g.get()); + break; + case l_false: + SASSERT(!g->proofs_enabled()); + SASSERT(!g->unsat_core_enabled()); + g->assert_expr(m.mk_false(), nullptr, nullptr); + break; + case l_undef: + if (m.canceled()) { + throw tactic_exception(Z3_CANCELED_MSG); + } + result.push_back(g.get()); + break; + } } void cleanup() { - NOT_IMPLEMENTED_YET(); + for (solver_state * s : m_solvers) dealloc(s); + m_solvers.reset(); + init(); + m_manager = nullptr; } tactic* translate(ast_manager& m) { - NOT_IMPLEMENTED_YET(); - return 0; + return alloc(parallel_tactic); } + + virtual void updt_params(params_ref const & p) { + // TBD + } + virtual void collect_param_descrs(param_descrs & r) { + // TBD + } + + virtual void collect_statistics(statistics & st) const { + for (solver_state const * s : m_solvers) { + s->get_solver().collect_statistics(st); + } + st.copy(m_stats); + } + virtual void reset_statistics() { + m_stats.reset(); + } + }; -tactic * mk_parallel_tactic(solver* s) { - return alloc(parallel_tactic, s); +tactic * mk_parallel_tactic() { + return alloc(parallel_tactic); } diff --git a/src/tactic/portfolio/parallel_tactic.h b/src/tactic/portfolio/parallel_tactic.h index a84c7be4d..063d1480f 100644 --- a/src/tactic/portfolio/parallel_tactic.h +++ b/src/tactic/portfolio/parallel_tactic.h @@ -22,6 +22,6 @@ Notes: class solver; class tactic; -tactic * mk_parallel_tactic(solver* s); +tactic * mk_parallel_tactic(); #endif diff --git a/src/util/approx_set.h b/src/util/approx_set.h index e696d52ee..1cb7ae9f2 100644 --- a/src/util/approx_set.h +++ b/src/util/approx_set.h @@ -29,7 +29,7 @@ public: static const unsigned long long zero = 0ull; static const unsigned long long one = 1ull; }; -COMPILE_TIME_ASSERT(sizeof(unsigned long long) == 8); +static_assert(sizeof(unsigned long long) == 8, ""); template <> class approx_set_traits { public: @@ -37,7 +37,7 @@ public: static const unsigned zero = 0; static const unsigned one = 1; }; -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); template class approx_set_tpl : private T2U_Proc { diff --git a/src/util/bit_vector.h b/src/util/bit_vector.h index 6a254e399..2d42e35a2 100644 --- a/src/util/bit_vector.h +++ b/src/util/bit_vector.h @@ -24,7 +24,7 @@ Revision History: #include "util/vector.h" #include "util/memory_manager.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 4 bytes"); #define BV_DEFAULT_CAPACITY 2 class bit_vector { diff --git a/src/util/debug.h b/src/util/debug.h index e0ceb9a64..536df4588 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -90,7 +90,6 @@ bool is_debug_enabled(const char * tag); exit(-1); \ } -#define COMPILE_TIME_ASSERT(expr) static_assert(expr, "") void finalize_debug(); /* diff --git a/src/util/double_manager.h b/src/util/double_manager.h index 33cccf2af..7532a3b8b 100644 --- a/src/util/double_manager.h +++ b/src/util/double_manager.h @@ -97,7 +97,7 @@ public: } }; -COMPILE_TIME_ASSERT(sizeof(uint64) == sizeof(double)); +static_assert(sizeof(uint64) == sizeof(double), ""); #endif /* DOUBLE_MANAGER_H_ */ diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index d2e25294d..35bdce43d 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -182,6 +182,23 @@ unsigned long long memory::get_max_used_memory() { return r; } +#if defined(_WINDOWS) +#include "Windows.h" +#endif + +unsigned long long memory::get_max_memory_size() { +#if defined(_WINDOWS) + MEMORYSTATUSEX statex; + statex.dwLength = sizeof (statex); + GlobalMemoryStatusEx (&statex); + return statex.ullTotalPhys; +#else + NOT_IMPLEMENTED_YET(); + // two GB + return 1 << 31; +#endif +} + unsigned long long memory::get_allocation_count() { return g_memory_alloc_count; } diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 5aa512018..bbddfa67f 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -67,6 +67,7 @@ public: static unsigned long long get_allocation_size(); static unsigned long long get_max_used_memory(); static unsigned long long get_allocation_count(); + static unsigned long long get_max_memory_size(); // temporary hack to avoid out-of-memory crash in z3.exe static void exit_when_out_of_memory(bool flag, char const * msg); }; diff --git a/src/util/mpf.cpp b/src/util/mpf.cpp index 5e7233110..3218419a9 100644 --- a/src/util/mpf.cpp +++ b/src/util/mpf.cpp @@ -73,7 +73,7 @@ mpf_manager::~mpf_manager() { } void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, int value) { - COMPILE_TIME_ASSERT(sizeof(int) == 4); + static_assert(sizeof(int) == 4, "assume integers are 4 bytes"); o.sign = false; o.ebits = ebits; @@ -119,7 +119,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, mpf_rounding_mode void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { // double === mpf(11, 53) - COMPILE_TIME_ASSERT(sizeof(double) == 8); + static_assert(sizeof(double) == 8, "doubles are 8 bytes"); uint64 raw; memcpy(&raw, &value, sizeof(double)); @@ -155,7 +155,7 @@ void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, double value) { void mpf_manager::set(mpf & o, unsigned ebits, unsigned sbits, float value) { // single === mpf(8, 24) - COMPILE_TIME_ASSERT(sizeof(float) == 4); + static_assert(sizeof(float) == 4, "floats are 4 bytes"); unsigned int raw; memcpy(&raw, &value, sizeof(float)); diff --git a/src/util/mpff.cpp b/src/util/mpff.cpp index 459b0691c..eac9cc80c 100644 --- a/src/util/mpff.cpp +++ b/src/util/mpff.cpp @@ -27,8 +27,8 @@ Revision History: #include "util/bit_util.h" #include "util/trace.h" -COMPILE_TIME_ASSERT(sizeof(mpn_digit) == sizeof(unsigned)); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(mpn_digit) == sizeof(unsigned), ""); +static_assert(sizeof(unsigned) == 4, "unsigned haven't changed size for a while"); // MIN_MSW is an shorthand for 0x8000..00, i.e., the minimal most significand word. #define MIN_MSW (1u << (sizeof(unsigned) * 8 - 1)) diff --git a/src/util/mpn.cpp b/src/util/mpn.cpp index 65223133f..2059ea6fd 100644 --- a/src/util/mpn.cpp +++ b/src/util/mpn.cpp @@ -24,7 +24,7 @@ Revision History: #define max(a,b) (((a) > (b)) ? (a) : (b)) typedef uint64 mpn_double_digit; -COMPILE_TIME_ASSERT(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit)); +static_assert(sizeof(mpn_double_digit) == 2 * sizeof(mpn_digit), "size alignment"); const mpn_digit mpn_manager::zero = 0; diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp index 9569ac280..7ad472ef1 100644 --- a/src/util/mpz.cpp +++ b/src/util/mpz.cpp @@ -558,14 +558,13 @@ void mpz_manager::big_rem(mpz const & a, mpz const & b, mpz & c) { template void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { - if (is_small(a) && is_small(b)) { + static_assert(sizeof(a.m_val) == sizeof(int), "size mismatch"); + if (is_small(a) && is_small(b) && a.m_val != INT_MIN && b.m_val != INT_MIN) { int _a = a.m_val; int _b = b.m_val; if (_a < 0) _a = -_a; if (_b < 0) _b = -_b; unsigned r = u_gcd(_a, _b); - // Remark: r is (INT_MAX + 1) - // If a == b == INT_MIN set(c, r); } else { @@ -725,7 +724,7 @@ void mpz_manager::gcd(mpz const & a, mpz const & b, mpz & c) { #ifdef LEHMER_GCD // For now, it only works if sizeof(digit_t) == sizeof(unsigned) - COMPILE_TIME_ASSERT(sizeof(digit_t) == sizeof(unsigned)); + static_assert(sizeof(digit_t) == sizeof(unsigned), ""); int64 a_hat, b_hat, A, B, C, D, T, q, a_sz, b_sz; mpz a1, b1, t, r, tmp; @@ -1755,7 +1754,7 @@ void mpz_manager::mul2k(mpz & a, unsigned k) { } #ifndef _MP_GMP -COMPILE_TIME_ASSERT(sizeof(digit_t) == 4 || sizeof(digit_t) == 8); +static_assert(sizeof(digit_t) == 4 || sizeof(digit_t) == 8, ""); #endif template @@ -1822,7 +1821,7 @@ unsigned mpz_manager::log2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; @@ -1844,7 +1843,7 @@ unsigned mpz_manager::mlog2(mpz const & a) { if (is_small(a)) return ::log2((unsigned)-a.m_val); #ifndef _MP_GMP - COMPILE_TIME_ASSERT(sizeof(digit_t) == 8 || sizeof(digit_t) == 4); + static_assert(sizeof(digit_t) == 8 || sizeof(digit_t) == 4, ""); mpz_cell * c = a.m_ptr; unsigned sz = c->m_size; digit_t * ds = c->m_digits; diff --git a/src/util/uint_set.h b/src/util/uint_set.h index decaa42ad..0f3715cb1 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -22,7 +22,6 @@ Revision History: #include "util/util.h" #include "util/vector.h" -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); class uint_set : unsigned_vector { diff --git a/src/util/util.h b/src/util/util.h index facd5a3cb..9c2bbf7b9 100644 --- a/src/util/util.h +++ b/src/util/util.h @@ -34,13 +34,13 @@ Revision History: typedef unsigned long long uint64; #endif -COMPILE_TIME_ASSERT(sizeof(uint64) == 8); +static_assert(sizeof(uint64) == 8, "64 bits please"); #ifndef int64 typedef long long int64; #endif -COMPILE_TIME_ASSERT(sizeof(int64) == 8); +static_assert(sizeof(int64) == 8, "64 bits"); #ifndef INT64_MIN #define INT64_MIN static_cast(0x8000000000000000ull) @@ -112,7 +112,7 @@ inline unsigned next_power_of_two(unsigned v) { unsigned log2(unsigned v); unsigned uint64_log2(uint64 v); -COMPILE_TIME_ASSERT(sizeof(unsigned) == 4); +static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); // Return the number of 1 bits in v. static inline unsigned get_num_1bits(unsigned v) {