From c92c431570e6fcf0359ed9e415415ae788d2dec8 Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Mon, 1 Oct 2018 16:32:04 +0200 Subject: [PATCH 01/18] adding call to update_max_generation --- src/smt/mam.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 00e079989..70741fa67 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -2571,6 +2571,7 @@ namespace smt { m_n1 = m_context.get_enode_eq_to(static_cast(m_pc)->m_label, static_cast(m_pc)->m_num_args, m_args.c_ptr()); \ if (m_n1 == 0 || !m_context.is_relevant(m_n1)) \ goto backtrack; \ + update_max_generation(m_n1, nullptr); \ m_registers[static_cast(m_pc)->m_oreg] = m_n1; \ m_pc = m_pc->m_next; \ goto main_loop; From cdbfd9654f9fa9f73ab42827a185af776357f59f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Janiszewski?= Date: Mon, 1 Oct 2018 21:14:25 +0200 Subject: [PATCH 02/18] Drop unused CV-qualifiers from scalar return values --- src/util/lp/lar_core_solver.h | 2 +- src/util/lp/numeric_pair.h | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/util/lp/lar_core_solver.h b/src/util/lp/lar_core_solver.h index 904550339..52290c69a 100644 --- a/src/util/lp/lar_core_solver.h +++ b/src/util/lp/lar_core_solver.h @@ -817,7 +817,7 @@ public: } - const bool column_is_bounded(unsigned j) const { + bool column_is_bounded(unsigned j) const { switch(m_column_types()[j]) { case column_type::fixed: case column_type::boxed: diff --git a/src/util/lp/numeric_pair.h b/src/util/lp/numeric_pair.h index e98d76cbb..ed740d645 100644 --- a/src/util/lp/numeric_pair.h +++ b/src/util/lp/numeric_pair.h @@ -57,10 +57,10 @@ public: template <> class numeric_traits { public: static bool precise() { return true; } - static int const zero() { return 0; } - static int const one() { return 1; } + static int zero() { return 0; } + static int one() { return 1; } static bool is_zero(int v) { return v == 0; } - static double const get_double(int const & d) { return d; } + static double get_double(int const & d) { return d; } static bool is_int(int) {return true;} static bool is_pos(int j) {return j > 0;} static bool is_neg(int j) {return j < 0;} From f145873603ca8b83a5a84e299528b7dfad7c845b Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:22:20 +0100 Subject: [PATCH 03/18] CI Test From aaae3118de5d3faadffcdc9344089f377b6ecae6 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 1 Oct 2018 20:26:05 +0100 Subject: [PATCH 04/18] CI Test From 661826e27f196967b1775eb4e419b5d8f9847535 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Micha=C5=82=20Janiszewski?= Date: Mon, 1 Oct 2018 21:35:48 +0200 Subject: [PATCH 05/18] Add missing template instantion for lar_core_solver::m_r_solver --- src/util/lp/lp_core_solver_base.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/lp/lp_core_solver_base.cpp b/src/util/lp/lp_core_solver_base.cpp index 00c1322c2..e71f65d5d 100644 --- a/src/util/lp/lp_core_solver_base.cpp +++ b/src/util/lp/lp_core_solver_base.cpp @@ -84,6 +84,7 @@ template lp::lp_core_solver_base >::lp_core_s const vector >&); template bool lp::lp_core_solver_base >::print_statistics_with_cost_and_check_that_the_time_is_over(lp::numeric_pair, std::ostream&); template void lp::lp_core_solver_base >::snap_xN_to_bounds_and_fill_xB(); +template void lp::lp_core_solver_base >::solve_Ax_eq_b(); template void lp::lp_core_solver_base >::solve_Bd(unsigned int); template bool lp::lp_core_solver_base >::update_basis_and_x(int, int, lp::numeric_pair const&); template void lp::lp_core_solver_base >::update_x(unsigned int, const lp::numeric_pair&); From 08c58ae61484a5b191da8cb39f4579b46d5fd411 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Oct 2018 15:52:22 -0700 Subject: [PATCH 06/18] make the unsat/sat verdicts from cubing produce empty clause and models respectively Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 2 ++ src/sat/sat_solver.cpp | 28 ++++++++++++++++++++++++++-- 2 files changed, 28 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index 4ca2c5f84..c252efb69 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2137,6 +2137,8 @@ namespace sat { if (lit == null_literal) { vars.reset(); for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v); + m_model.reset(); + init_model(); return l_true; } TRACE("sat", tout << "choose: " << lit << " cube: " << m_cube_state.m_cube << "\n";); diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 7ddc80813..59cb2aac4 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1014,14 +1014,38 @@ namespace sat { } lbool solver::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { - if (!m_cuber) { + bool is_first = !m_cuber; + if (is_first) { m_cuber = alloc(lookahead, *this); } lbool result = m_cuber->cube(vars, lits, backtrack_level); m_cuber->update_cube_statistics(m_aux_stats); - if (result == l_false) { + switch (result) { + case l_false: dealloc(m_cuber); m_cuber = nullptr; + if (is_first) { + pop_to_base_level(); + set_conflict(justification()); + } + break; + case l_true: { + pop_to_base_level(); + model const& mdl = m_cuber->get_model(); + for (bool_var v = 0; v < mdl.size(); ++v) { + if (value(v) != l_undef) { + continue; + } + literal l(v, false); + if (mdl[v] != l_true) l.neg(); + push(); + assign_core(l, justification()); + } + mk_model(); + break; + } + default: + break; } return result; } From cdfc19a8856be9b803ac472bcddfda7dbe33f1d5 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 09:11:19 +0700 Subject: [PATCH 07/18] Use nullptr. --- src/api/api_ast.cpp | 10 +++---- src/api/api_goal.cpp | 2 +- src/api/api_quant.cpp | 8 +++--- src/api/api_solver.cpp | 8 +++--- src/ast/ast.cpp | 2 +- src/ast/normal_forms/defined_names.cpp | 2 +- src/ast/normal_forms/name_exprs.cpp | 2 +- src/model/model.cpp | 4 +-- src/muz/spacer/spacer_context.cpp | 2 +- src/muz/spacer/spacer_proof_utils.cpp | 2 +- src/opt/opt_context.cpp | 2 +- src/parsers/smt2/smt2parser.cpp | 2 +- src/qe/qe_lite.cpp | 2 +- src/qe/qe_solve_plugin.cpp | 2 +- src/sat/ba_solver.cpp | 2 +- src/sat/sat_drat.cpp | 2 +- src/sat/sat_local_search.cpp | 2 +- src/sat/sat_local_search.h | 2 +- src/sat/sat_lookahead.cpp | 2 +- src/sat/sat_solver.cpp | 8 +++--- src/sat/tactic/goal2sat.cpp | 6 ++--- src/smt/smt_context.h | 2 +- src/smt/smt_model_checker.cpp | 2 +- src/smt/tactic/smt_tactic.cpp | 4 +-- src/smt/theory_lra.cpp | 14 +++++----- src/smt/theory_pb.cpp | 32 +++++++++++------------ src/smt/theory_pb.h | 2 +- src/smt/theory_seq.cpp | 4 +-- src/smt/theory_str.cpp | 26 +++++++++--------- src/smt/theory_str.h | 2 +- src/solver/parallel_tactic.cpp | 2 +- src/solver/solver_na2as.cpp | 2 +- src/tactic/arith/degree_shift_tactic.cpp | 2 +- src/tactic/arith/lia2card_tactic.cpp | 2 +- src/tactic/fd_solver/enum2bv_solver.cpp | 2 +- src/tactic/generic_model_converter.h | 2 +- src/tactic/portfolio/solver2lookahead.cpp | 2 +- src/tactic/proof_converter.cpp | 2 +- src/tactic/sine_filter.cpp | 2 +- src/tactic/tactical.cpp | 4 +-- src/test/main.cpp | 6 ++--- src/test/smt2print_parse.cpp | 2 +- src/util/lp/nra_solver.cpp | 2 +- src/util/obj_ref.h | 2 +- 44 files changed, 98 insertions(+), 98 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 52be66e77..a28315cda 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -468,7 +468,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_symbol_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; @@ -486,7 +486,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_sort_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -504,7 +504,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_ast_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -522,7 +522,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_func_decl_parameter(c, d, idx); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -596,7 +596,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_domain(c, d, i); RESET_ERROR_CODE(); - CHECK_VALID_AST(d, 0); + CHECK_VALID_AST(d, nullptr); if (i >= to_func_decl(d)->get_arity()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); diff --git a/src/api/api_goal.cpp b/src/api/api_goal.cpp index cb3bb7478..3d75c3dba 100644 --- a/src/api/api_goal.cpp +++ b/src/api/api_goal.cpp @@ -163,7 +163,7 @@ extern "C" { if (to_goal_ref(g)->mc()) (*to_goal_ref(g)->mc())(m_ref->m_model); RETURN_Z3(of_model(m_ref)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_goal Z3_API Z3_goal_translate(Z3_context c, Z3_goal g, Z3_context target) { diff --git a/src/api/api_quant.cpp b/src/api/api_quant.cpp index 6d6d19d56..49aa09727 100644 --- a/src/api/api_quant.cpp +++ b/src/api/api_quant.cpp @@ -155,7 +155,7 @@ extern "C" { expr_ref result(mk_c(c)->m()); if (num_decls == 0) { SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); - RETURN_Z3(0); + RETURN_Z3(nullptr); } sort* const* ts = reinterpret_cast(types); @@ -166,7 +166,7 @@ extern "C" { result = mk_c(c)->m().mk_lambda(names.size(), ts, names.c_ptr(), to_expr(body)); mk_c(c)->save_ast_trail(result.get()); return of_ast(result.get()); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_ast Z3_API Z3_mk_lambda_const(Z3_context c, @@ -178,7 +178,7 @@ extern "C" { RESET_ERROR_CODE(); if (num_decls == 0) { SET_ERROR_CODE(Z3_INVALID_USAGE, nullptr); - RETURN_Z3(0); + RETURN_Z3(nullptr); } svector _names; @@ -196,7 +196,7 @@ extern "C" { result = mk_c(c)->m().mk_lambda(_vars.size(), _vars.c_ptr(), _names.c_ptr(), result); mk_c(c)->save_ast_trail(result.get()); return of_ast(result.get()); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index 5a4537a4a..fc4e01f3a 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -369,7 +369,7 @@ extern "C" { v->m_ast_vector.push_back(f); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } Z3_ast_vector Z3_API Z3_solver_get_non_units(Z3_context c, Z3_solver s) { @@ -384,7 +384,7 @@ extern "C" { v->m_ast_vector.push_back(f); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } static Z3_lbool _solver_check(Z3_context c, Z3_solver s, unsigned num_assumptions, Z3_ast const assumptions[]) { @@ -631,7 +631,7 @@ extern "C" { } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); - return 0; + return nullptr; } } Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m()); @@ -644,7 +644,7 @@ extern "C" { to_ast_vector_ref(vs).push_back(a); } RETURN_Z3(of_ast_vector(v)); - Z3_CATCH_RETURN(0); + Z3_CATCH_RETURN(nullptr); } diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 65d3c7821..8750425a8 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -424,7 +424,7 @@ sort * get_sort(expr const * n) { return to_quantifier(n)->get_sort(); default: UNREACHABLE(); - return 0; + return nullptr; } } diff --git a/src/ast/normal_forms/defined_names.cpp b/src/ast/normal_forms/defined_names.cpp index b63c947a9..88ded842f 100644 --- a/src/ast/normal_forms/defined_names.cpp +++ b/src/ast/normal_forms/defined_names.cpp @@ -221,7 +221,7 @@ void defined_names::impl::mk_definition(expr * e, app * n, sort_ref_buffer & var args.push_back(m.mk_var(q->get_num_decls() - i - 1, q->get_decl_sort(i))); } array_util autil(m); - func_decl * f = 0; + func_decl * f = nullptr; if (autil.is_as_array(n2, f)) { n3 = m.mk_app(f, args.size()-1, args.c_ptr() + 1); } diff --git a/src/ast/normal_forms/name_exprs.cpp b/src/ast/normal_forms/name_exprs.cpp index 5e9af1c2d..bb2543b3e 100644 --- a/src/ast/normal_forms/name_exprs.cpp +++ b/src/ast/normal_forms/name_exprs.cpp @@ -127,7 +127,7 @@ class name_nested_formulas : public name_exprs_core { ast_manager & m; expr * m_root; - pred(ast_manager & m):m(m), m_root(0) {} + pred(ast_manager & m):m(m), m_root(nullptr) {} bool operator()(expr * t) override { TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m) << "\n";); diff --git a/src/model/model.cpp b/src/model/model.cpp index 83adfc87e..a1fdfc980 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -351,7 +351,7 @@ bool model::can_inline_def(top_sort& ts, func_decl* f) { expr_ref model::cleanup_expr(top_sort& ts, expr* e, unsigned current_partition) { - if (!e) return expr_ref(0, m); + if (!e) return expr_ref(nullptr, m); TRACE("model", tout << "cleaning up:\n" << mk_pp(e, m) << "\n";); @@ -453,7 +453,7 @@ void model::remove_decls(ptr_vector & decls, func_decl_set const & s) expr_ref model::get_inlined_const_interp(func_decl* f) { expr* v = get_const_interp(f); - if (!v) return expr_ref(0, m); + if (!v) return expr_ref(nullptr, m); top_sort st(m); expr_ref result1(v, m); expr_ref result2 = cleanup_expr(st, v, UINT_MAX); diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index dd6656954..30b68ebf6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -1325,7 +1325,7 @@ bool pred_transformer::is_qblocked (pob &n) { // assert cti s->assert_expr(n.post()); - lbool res = s->check_sat(0, 0); + lbool res = s->check_sat(0, nullptr); // if (res == l_false) { // expr_ref_vector core(m); diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index ed02513f1..a73d24d49 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -600,7 +600,7 @@ namespace spacer { proof* hypothesis_reducer::reduce_core(proof* pf) { SASSERT(m.is_false(m.get_fact(pf))); - proof *res = NULL; + proof *res = nullptr; ptr_vector todo; todo.push_back(pf); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index b1296f71e..87da85af5 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -281,7 +281,7 @@ namespace opt { symbol pri = optp.priority(); IF_VERBOSE(1, verbose_stream() << "(optimize:check-sat)\n"); - lbool is_sat = s.check_sat(0,0); + lbool is_sat = s.check_sat(0,nullptr); TRACE("opt", s.display(tout << "initial search result: " << is_sat << "\n");); if (is_sat != l_false) { s.get_model(m_model); diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index 403ea4c85..1a16b817b 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -2608,7 +2608,7 @@ namespace smt2 { check_rparen("invalid get-value command, ')' expected"); model_ref md; - if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == 0) + if (!m_ctx.is_model_available(md) || m_ctx.get_check_sat_result() == nullptr) throw cmd_exception("model is not available"); if (index != 0) { m_ctx.get_opt()->get_box_model(md, index); diff --git a/src/qe/qe_lite.cpp b/src/qe/qe_lite.cpp index da45d17ca..d900bff5d 100644 --- a/src/qe/qe_lite.cpp +++ b/src/qe/qe_lite.cpp @@ -394,7 +394,7 @@ namespace eq { expr* const* args = &e; if (is_lambda(q)) { r = q; - pr = 0; + pr = nullptr; return; } flatten_args(q, num_args, args); diff --git a/src/qe/qe_solve_plugin.cpp b/src/qe/qe_solve_plugin.cpp index 6ec840de1..dae1faf6f 100644 --- a/src/qe/qe_solve_plugin.cpp +++ b/src/qe/qe_solve_plugin.cpp @@ -156,7 +156,7 @@ namespace qe { std::swap(e1, e2); } // y + -1*x == 0 --> y = x - expr *a0 = 0, *a1 = 0, *x = 0; + expr *a0 = nullptr, *a1 = nullptr, *x = nullptr; if (a.is_zero(e2) && a.is_add(e1, a0, a1)) { if (a.is_times_minus_one(a1, x)) { e1 = a0; diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp index de6635d09..4f06c2e98 100644 --- a/src/sat/ba_solver.cpp +++ b/src/sat/ba_solver.cpp @@ -1527,7 +1527,7 @@ namespace sat { return p; } - ba_solver::ba_solver(): m_solver(0), m_lookahead(0), m_unit_walk(0), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { + ba_solver::ba_solver(): m_solver(nullptr), m_lookahead(nullptr), m_unit_walk(nullptr), m_constraint_id(0), m_ba(*this), m_sort(m_ba) { TRACE("ba", tout << this << "\n";); m_num_propagations_since_pop = 0; } diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp index 00a3fa076..932e9b35e 100644 --- a/src/sat/sat_drat.cpp +++ b/src/sat/sat_drat.cpp @@ -26,7 +26,7 @@ Notes: namespace sat { drat::drat(solver& s): s(s), - m_out(0), + m_out(nullptr), m_inconsistent(false), m_check_unsat(false), m_check_sat(false), diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp index af2447fc2..9b79e2964 100644 --- a/src/sat/sat_local_search.cpp +++ b/src/sat/sat_local_search.cpp @@ -529,7 +529,7 @@ namespace sat { } lbool local_search::check() { - return check(0, 0); + return check(0, nullptr); } #define PROGRESS(tries, flips) \ diff --git a/src/sat/sat_local_search.h b/src/sat/sat_local_search.h index 8a63898c3..5fd69a740 100644 --- a/src/sat/sat_local_search.h +++ b/src/sat/sat_local_search.h @@ -277,7 +277,7 @@ namespace sat { lbool check(); - lbool check(unsigned sz, literal const* assumptions, parallel* p = 0); + lbool check(unsigned sz, literal const* assumptions, parallel* p = nullptr); local_search_config& config() { return m_config; } diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index c252efb69..bbc1106bb 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -33,7 +33,7 @@ namespace sat { } lookahead::scoped_ext::~scoped_ext() { - if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(0); + if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(nullptr); } lookahead::scoped_assumptions::scoped_assumptions(lookahead& p, literal_vector const& lits): p(p), lits(lits) { diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 59cb2aac4..b58d2296b 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -66,13 +66,13 @@ namespace sat { m_next_simplify = 0; m_num_checkpoints = 0; m_simplifications = 0; - m_ext = 0; + m_ext = nullptr; m_cuber = nullptr; m_mc.set_solver(this); } solver::~solver() { - m_ext = 0; + m_ext = nullptr; SASSERT(check_invariant()); TRACE("sat", tout << "Delete clauses\n";); del_clauses(m_clauses); @@ -1157,7 +1157,7 @@ namespace sat { srch.config().set_config(m_config); srch.import(*this, false); scoped_rl.push_child(&srch.rlimit()); - lbool r = srch.check(num_lits, lits, 0); + lbool r = srch.check(num_lits, lits, nullptr); m_model = srch.get_model(); // srch.collect_statistics(m_aux_stats); return r; @@ -1294,7 +1294,7 @@ namespace sat { if (!canceled) { rlimit().reset_cancel(); } - set_par(0, 0); + set_par(nullptr, 0); ls.reset(); uw.reset(); if (finished_id == -1) { diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp index dc4dfc3a8..d42a28ac0 100644 --- a/src/sat/tactic/goal2sat.cpp +++ b/src/sat/tactic/goal2sat.cpp @@ -72,7 +72,7 @@ struct goal2sat::imp { imp(ast_manager & _m, params_ref const & p, sat::solver & s, atom2bool_var & map, dep2asm_map& dep2asm, bool default_external): m(_m), pb(m), - m_ext(0), + m_ext(nullptr), m_solver(s), m_map(map), m_dep2asm(dep2asm), @@ -1063,7 +1063,7 @@ void sat2goal::mc::insert(sat::bool_var v, app * atom, bool aux) { expr_ref sat2goal::mc::lit2expr(sat::literal l) { if (!m_var2expr.get(l.var())) { - app* aux = m.mk_fresh_const(0, m.mk_bool_sort()); + app* aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); m_var2expr.set(l.var(), aux); if (!m_gmc) m_gmc = alloc(generic_model_converter, m, "sat2goal"); m_gmc->hide(aux->get_decl()); @@ -1107,7 +1107,7 @@ struct sat2goal::imp { SASSERT(m_lit2expr.get((~l).index()) == 0); app* aux = mc ? mc->var2expr(l.var()) : nullptr; if (!aux) { - aux = m.mk_fresh_const(0, m.mk_bool_sort()); + aux = m.mk_fresh_const(nullptr, m.mk_bool_sort()); if (mc) { mc->insert(l.var(), aux, true); } diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index ff92f6f95..5733829a3 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -565,7 +565,7 @@ namespace smt { return m_asserted_formulas.has_quantifiers(); } - fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = 0) { + fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) { return m_fingerprints.insert(data, data_hash, num_args, args, def); } diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index c3af41dcf..02b0e16be 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -577,7 +577,7 @@ namespace smt { } if (inst.m_def) { - m_context->internalize_assertion(inst.m_def, 0, gen); + m_context->internalize_assertion(inst.m_def, nullptr, gen); } TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n"; diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 50fe47985..6aa365383 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -217,7 +217,7 @@ public: model_ref md; m_ctx->get_model(md); buffer r; - m_ctx->get_relevant_labels(0, r); + m_ctx->get_relevant_labels(nullptr, r); labels_vec rv; rv.append(r.size(), r.c_ptr()); model_converter_ref mc; @@ -270,7 +270,7 @@ public: model_ref md; m_ctx->get_model(md); buffer r; - m_ctx->get_relevant_labels(0, r); + m_ctx->get_relevant_labels(nullptr, r); labels_vec rv; rv.append(r.size(), r.c_ptr()); in->add(model_and_labels2model_converter(md.get(), rv)); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5b1de851e..db031d043 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1054,7 +1054,7 @@ public: // to_int (to_real x) = x // to_real(to_int(x)) <= x < to_real(to_int(x)) + 1 void mk_to_int_axiom(app* n) { - expr* x = 0, *y = 0; + expr* x = nullptr, *y = nullptr; VERIFY (a.is_to_int(n, x)); if (a.is_to_real(x, y)) { mk_axiom(th.mk_eq(y, n, false)); @@ -1070,7 +1070,7 @@ public: // is_int(x) <=> to_real(to_int(x)) = x void mk_is_int_axiom(app* n) { - expr* x = 0; + expr* x = nullptr; VERIFY(a.is_is_int(n, x)); literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false); literal is_int = ctx().get_literal(n); @@ -1450,7 +1450,7 @@ public: st = FC_GIVEUP; break; } - if (m_not_handled != 0) { + if (m_not_handled != nullptr) { TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";); st = FC_GIVEUP; } @@ -2080,12 +2080,12 @@ public: m_core2.push_back(~c); } m_core2.push_back(lit); - justification * js = 0; + justification * js = nullptr; if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(), m_params.size(), m_params.c_ptr()); } - ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } else { ctx().assign( @@ -2140,7 +2140,7 @@ public: rational const& k1 = b.get_value(); lp_bounds & bounds = m_bounds[v]; - lp_api::bound* end = 0; + lp_api::bound* end = nullptr; lp_api::bound* lo_inf = end, *lo_sup = end; lp_api::bound* hi_inf = end, *hi_sup = end; @@ -2798,7 +2798,7 @@ public: justification* js = ctx().mk_justification( ext_theory_eq_propagation_justification( - get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, 0)); + get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr)); TRACE("arith", for (unsigned i = 0; i < m_core.size(); ++i) { diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index e389c819e..2fb0187f8 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -897,7 +897,7 @@ namespace smt { void theory_pb::watch_literal(literal lit, card* c) { init_watch(lit.var()); ptr_vector* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()]; - if (cards == 0) { + if (cards == nullptr) { cards = alloc(ptr_vector); m_var_infos[lit.var()].m_lit_cwatch[lit.sign()] = cards; } @@ -961,13 +961,13 @@ namespace smt { void theory_pb::add_clause(card& c, literal_vector const& lits) { m_stats.m_num_conflicts++; context& ctx = get_context(); - justification* js = 0; + justification* js = nullptr; c.inc_propagations(*this); if (!resolve_conflict(c, lits)) { if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } SASSERT(ctx.inconsistent()); } @@ -1027,7 +1027,7 @@ namespace smt { } void theory_pb::assign_eh(bool_var v, bool is_true) { - ptr_vector* ineqs = 0; + ptr_vector* ineqs = nullptr; context& ctx = get_context(); literal nlit(v, is_true); init_watch(v); @@ -1060,7 +1060,7 @@ namespace smt { } ptr_vector* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()]; - if (cards != 0 && !cards->empty() && !ctx.inconsistent()) { + if (cards != nullptr && !cards->empty() && !ctx.inconsistent()) { ptr_vector::iterator it = cards->begin(), it2 = it, end = cards->end(); for (; it != end; ++it) { if (ctx.get_assignment((*it)->lit()) != l_true) { @@ -1088,7 +1088,7 @@ namespace smt { } card* crd = m_var_infos[v].m_card; - if (crd != 0 && !ctx.inconsistent()) { + if (crd != nullptr && !ctx.inconsistent()) { crd->init_watch(*this, is_true); } @@ -1527,7 +1527,7 @@ namespace smt { else { z++; clear_watch(*c); - m_var_infos[v].m_card = 0; + m_var_infos[v].m_card = nullptr; dealloc(c); m_card_trail[i] = null_bool_var; ctx.remove_watch(v); @@ -1671,7 +1671,7 @@ namespace smt { if (v != null_bool_var) { card* c = m_var_infos[v].m_card; clear_watch(*c); - m_var_infos[v].m_card = 0; + m_var_infos[v].m_card = nullptr; dealloc(c); } } @@ -1774,11 +1774,11 @@ namespace smt { context& ctx = get_context(); TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - " << lits << "\n"; display(tout, c, true);); - justification* js = 0; + justification* js = nullptr; if (proofs_enabled()) { js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr()); } - ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } @@ -1894,11 +1894,11 @@ namespace smt { break; case b_justification::JUSTIFICATION: { justification* j = js.get_justification(); - card_justification* pbj = 0; + card_justification* pbj = nullptr; if (j->get_from_theory() == get_id()) { pbj = dynamic_cast(j); } - if (pbj != 0) { + if (pbj != nullptr) { card& c2 = pbj->get_card(); result = card2expr(c2); } @@ -2170,11 +2170,11 @@ namespace smt { VERIFY(internalize_card(atl, false)); bool_var abv = ctx.get_bool_var(atl); m_antecedents.push_back(literal(abv)); - justification* js = 0; + justification* js = nullptr; if (proofs_enabled()) { - js = 0; // + js = nullptr; } - ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, 0); + ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, nullptr); } bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) { @@ -2403,7 +2403,7 @@ namespace smt { } #endif SASSERT(validate_antecedents(m_antecedents)); - ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0))); + ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr))); DEBUG_CODE( m_antecedents.push_back(~alit); diff --git a/src/smt/theory_pb.h b/src/smt/theory_pb.h index 7e9c55a12..3a0ee723f 100644 --- a/src/smt/theory_pb.h +++ b/src/smt/theory_pb.h @@ -258,7 +258,7 @@ namespace smt { card_watch* m_lit_cwatch[2]; card* m_card; - var_info(): m_var_watch(0), m_ineq(0), m_card(0) + var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr) { m_lit_watch[0] = nullptr; m_lit_watch[1] = nullptr; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 857691b8b..233be9e31 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1120,7 +1120,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons break; } if (flag) { - expr* nl_fst = 0; + expr* nl_fst = nullptr; if (e.rs().size()>1 && is_var(e.rs().get(0))) nl_fst = e.rs().get(0); if (nl_fst && nl_fst != r_fst) { @@ -1173,7 +1173,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons break; } if (flag) { - expr* nl_fst = 0; + expr* nl_fst = nullptr; if (e.rs().size()>1 && is_var(e.rs().get(0))) nl_fst = e.rs().get(0); if (nl_fst && nl_fst != r_fst) { diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index aadcb63a7..d902aa533 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -6745,8 +6745,8 @@ namespace smt { } unsigned theory_str::estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2) { - ENSURE(aut1 != NULL); - ENSURE(aut2 != NULL); + ENSURE(aut1 != nullptr); + ENSURE(aut2 != nullptr); return _qmul(aut1->num_states(), aut2->num_states()); } @@ -6999,7 +6999,7 @@ namespace smt { * and the equality with 0 is based on whether solutions of length 0 are allowed. */ void theory_str::find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -7051,7 +7051,7 @@ namespace smt { * if it exists, or -1 otherwise. */ bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); if (aut->final_states().size() < 1) { // no solutions at all @@ -7161,7 +7161,7 @@ namespace smt { * if a shorter solution exists, or -1 otherwise. */ bool theory_str::refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); if (aut->final_states().empty()) { // no solutions at all! @@ -7280,7 +7280,7 @@ namespace smt { return retval; } else { TRACE("str", tout << "ERROR: unrecognized automaton path constraint " << mk_pp(cond, m) << ", cannot translate" << std::endl;); - retval = NULL; + retval = nullptr; return retval; } } @@ -7293,7 +7293,7 @@ namespace smt { * are returned in `characterConstraints`. */ expr_ref theory_str::generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints) { - ENSURE(aut != NULL); + ENSURE(aut != nullptr); context & ctx = get_context(); ast_manager & m = get_manager(); @@ -10582,12 +10582,12 @@ namespace smt { } } // foreach(term in str_in_re_terms) - eautomaton * aut_inter = NULL; + eautomaton * aut_inter = nullptr; CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;); for (svector::iterator aut_it = intersect_constraints.begin(); aut_it != intersect_constraints.end(); ++aut_it) { regex_automaton_under_assumptions aut = *aut_it; - if (aut_inter == NULL) { + if (aut_inter == nullptr) { // start somewhere aut_inter = aut.get_automaton(); used_intersect_constraints.push_back(aut); @@ -10637,7 +10637,7 @@ namespace smt { } } } // foreach(entry in intersect_constraints) - if (aut_inter != NULL) { + if (aut_inter != nullptr) { aut_inter->compress(); } TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;); @@ -10668,7 +10668,7 @@ namespace smt { } conflict_lhs = mk_and(conflict_terms); - if (used_intersect_constraints.size() > 1 && aut_inter != NULL) { + if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) { // check whether the intersection is only the empty string unsigned initial_state = aut_inter->init(); if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) { @@ -10686,7 +10686,7 @@ namespace smt { } } - if (aut_inter != NULL && aut_inter->is_empty()) { + if (aut_inter != nullptr && aut_inter->is_empty()) { TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;); expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m); assert_axiom(conflict_clause); @@ -12231,7 +12231,7 @@ namespace smt { // - in the same EQC as freeVar if (term_appears_as_subterm(freeVar, re_str)) { TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;); - return NULL; + return nullptr; } } } diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h index 419084091..b626c5b07 100644 --- a/src/smt/theory_str.h +++ b/src/smt/theory_str.h @@ -164,7 +164,7 @@ protected: rational upper_bound; public: regex_automaton_under_assumptions() : - re_term(NULL), aut(NULL), polarity(false), + re_term(nullptr), aut(nullptr), polarity(false), assume_lower_bound(false), assume_upper_bound(false) {} regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) : diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 142ba4bb8..f0bb65315 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -676,7 +676,7 @@ public: fail_if_proof_generation("parallel-tactic", g); ast_manager& m = g->m(); solver* s = m_solver->translate(m, m_params); - solver_state* st = alloc(solver_state, 0, s, m_params); + solver_state* st = alloc(solver_state, nullptr, s, m_params); m_queue.add_task(st); expr_ref_vector clauses(m); ptr_vector assumptions; diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp index 41853b19a..a3fcd0e0b 100644 --- a/src/solver/solver_na2as.cpp +++ b/src/solver/solver_na2as.cpp @@ -31,7 +31,7 @@ solver_na2as::solver_na2as(ast_manager & m): solver_na2as::~solver_na2as() {} void solver_na2as::assert_expr_core2(expr * t, expr * a) { - if (a == 0) { + if (a == nullptr) { assert_expr_core(t); } else { diff --git a/src/tactic/arith/degree_shift_tactic.cpp b/src/tactic/arith/degree_shift_tactic.cpp index c15285703..b713c3055 100644 --- a/src/tactic/arith/degree_shift_tactic.cpp +++ b/src/tactic/arith/degree_shift_tactic.cpp @@ -204,7 +204,7 @@ class degree_shift_tactic : public tactic { for (auto const& kv : m_var2degree) { SASSERT(kv.m_value.is_int()); SASSERT(kv.m_value >= rational(2)); - app * fresh = m.mk_fresh_const(0, kv.m_key->get_decl()->get_range()); + app * fresh = m.mk_fresh_const(nullptr, kv.m_key->get_decl()->get_range()); m_pinned.push_back(fresh); m_var2var.insert(kv.m_key, fresh); if (m_produce_models) { diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index 88e4a5583..027b6d91c 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -36,7 +36,7 @@ class lia2card_tactic : public tactic { expr* m_expr; bound(unsigned lo, unsigned hi, expr* b): m_lo(lo), m_hi(hi), m_expr(b) {} - bound(): m_lo(0), m_hi(0), m_expr(0) {} + bound(): m_lo(0), m_hi(0), m_expr(nullptr) {} }; struct lia_rewriter_cfg : public default_rewriter_cfg { diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index a864d9631..185f23d13 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -148,7 +148,7 @@ public: // translate enumeration constants to bit-vectors. for (expr* v : vars) { - func_decl* f = 0; + func_decl* f = nullptr; if (is_app(v) && is_uninterp_const(v) && m_rewriter.enum2bv().find(to_app(v)->get_decl(), f)) { bvars.push_back(m.mk_const(f)); } diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index c67dd5eff..69bc35a3f 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -45,7 +45,7 @@ public: void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } - void hide(func_decl * f) { m_entries.push_back(entry(f, 0, m, HIDE)); } + void hide(func_decl * f) { m_entries.push_back(entry(f, nullptr, m, HIDE)); } void add(func_decl * d, expr* e); diff --git a/src/tactic/portfolio/solver2lookahead.cpp b/src/tactic/portfolio/solver2lookahead.cpp index 0c18ab079..63b28793d 100644 --- a/src/tactic/portfolio/solver2lookahead.cpp +++ b/src/tactic/portfolio/solver2lookahead.cpp @@ -20,5 +20,5 @@ Notes: #include "solver/solver.h" solver * mk_solver2lookahead(solver* s) { - return 0; + return nullptr; } diff --git a/src/tactic/proof_converter.cpp b/src/tactic/proof_converter.cpp index f1a209487..faa9a36db 100644 --- a/src/tactic/proof_converter.cpp +++ b/src/tactic/proof_converter.cpp @@ -130,7 +130,7 @@ proof_ref apply(ast_manager & m, proof_converter_ref & pc1, proof_converter_ref_ for (unsigned i = 0; i < sz; i++) { proof_ref pr(m); SASSERT(pc2s[i]); // proof production is enabled - pr = pc2s[i]->operator()(m, 0, 0); + pr = pc2s[i]->operator()(m, 0, nullptr); prs.push_back(pr); } return (*pc1)(m, sz, prs.c_ptr()); diff --git a/src/tactic/sine_filter.cpp b/src/tactic/sine_filter.cpp index b1db12964..1612670a4 100644 --- a/src/tactic/sine_filter.cpp +++ b/src/tactic/sine_filter.cpp @@ -54,7 +54,7 @@ public: TRACE("sine", tout << new_forms.size();); g->reset(); for (unsigned i = 0; i < new_forms.size(); i++) { - g->assert_expr(new_forms.get(i), 0, 0); + g->assert_expr(new_forms.get(i), nullptr, nullptr); } g->inc_depth(); g->updt_prec(goal::OVER); diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index 43087f50f..a71ea738c 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -636,7 +636,7 @@ public: else { SASSERT(is_decided_unsat(r2)); - if (cores_enabled && r2[0]->dep(0) != 0) { + if (cores_enabled && r2[0]->dep(0) != nullptr) { expr_dependency_ref * new_dep = alloc(expr_dependency_ref, new_m); *new_dep = r2[0]->dep(0); core_buffer.set(i, new_dep); @@ -674,7 +674,7 @@ public: ast_translation translator(*(managers[i]), m, false); goal_ref_buffer * r = goals_vect[i]; unsigned j = result.size(); - if (r != 0) { + if (r != nullptr) { for (unsigned k = 0; k < r->size(); k++) { result.push_back((*r)[k]->translate(translator)); } diff --git a/src/test/main.cpp b/src/test/main.cpp index d330610d9..811b67407 100644 --- a/src/test/main.cpp +++ b/src/test/main.cpp @@ -78,11 +78,11 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t int i = 1; while (i < argc) { char * arg = argv[i]; - char * eq_pos = 0; + char * eq_pos = nullptr; if (arg[0] == '-' || arg[0] == '/') { char * opt_name = arg + 1; - char * opt_arg = 0; + char * opt_arg = nullptr; char * colon = strchr(arg, ':'); if (colon) { opt_arg = colon + 1; @@ -97,7 +97,7 @@ void parse_cmd_line_args(int argc, char ** argv, bool& do_display_usage, bool& t else if (strcmp(opt_name, "v") == 0) { if (!opt_arg) error("option argument (/v:level) is missing."); - long lvl = strtol(opt_arg, 0, 10); + long lvl = strtol(opt_arg, nullptr, 10); set_verbosity_level(lvl); } else if (strcmp(opt_name, "w") == 0) { diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp index 99ffb726c..81b7ba1e9 100644 --- a/src/test/smt2print_parse.cpp +++ b/src/test/smt2print_parse.cpp @@ -19,7 +19,7 @@ void test_print(Z3_context ctx, Z3_ast_vector av) { Z3_ast a = Z3_mk_and(ctx, Z3_ast_vector_size(ctx, av), args); Z3_inc_ref(ctx, a); delete[] args; - char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", 0, 0, 0, 0, 0, a); + char const* spec1 = Z3_benchmark_to_smtlib_string(ctx, "test", nullptr, nullptr, nullptr, 0, nullptr, a); Z3_dec_ref(ctx, a); std::cout << "spec1: benchmark->string\n" << spec1 << "\n"; diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index 0d28058e8..200bdd2bc 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -154,7 +154,7 @@ namespace nra { polynomial::polynomial* ps[1] = { p }; bool even[1] = { false }; nlsat::literal lit = m_nlsat->mk_ineq_literal(nlsat::atom::kind::EQ, 1, ps, even); - m_nlsat->mk_clause(1, &lit, 0); + m_nlsat->mk_clause(1, &lit, nullptr); } void add_constraint(unsigned idx) { diff --git a/src/util/obj_ref.h b/src/util/obj_ref.h index 885601375..8908f2cdd 100644 --- a/src/util/obj_ref.h +++ b/src/util/obj_ref.h @@ -115,7 +115,7 @@ public: */ T * steal() { T * r = m_obj; - m_obj = 0; + m_obj = nullptr; return r; } }; From 489582f7fa9986e6576442ebce4943a754f7bdbd Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 09:19:14 +0700 Subject: [PATCH 08/18] Remove unused sat_par files. These look like they were replaced by `sat_parallel` files and aren't currently built or used. --- src/sat/sat_par.cpp | 45 -------------------------------------------- src/sat/sat_par.h | 39 -------------------------------------- src/sat/sat_solver.h | 1 - 3 files changed, 85 deletions(-) delete mode 100644 src/sat/sat_par.cpp delete mode 100644 src/sat/sat_par.h diff --git a/src/sat/sat_par.cpp b/src/sat/sat_par.cpp deleted file mode 100644 index e3d5727ed..000000000 --- a/src/sat/sat_par.cpp +++ /dev/null @@ -1,45 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - sat_par.cpp - -Abstract: - - Utilities for parallel SAT solving. - -Author: - - Nikolaj Bjorner (nbjorner) 2017-1-29. - -Revision History: - ---*/ -#include "sat/sat_par.h" - - -namespace sat { - - par::par() {} - - void par::exchange(literal_vector const& in, unsigned& limit, literal_vector& out) { - #pragma omp critical (par_solver) - { - if (limit < m_units.size()) { - // this might repeat some literals. - out.append(m_units.size() - limit, m_units.c_ptr() + limit); - } - for (unsigned i = 0; i < in.size(); ++i) { - literal lit = in[i]; - if (!m_unit_set.contains(lit.index())) { - m_unit_set.insert(lit.index()); - m_units.push_back(lit); - } - } - limit = m_units.size(); - } - } - -}; - diff --git a/src/sat/sat_par.h b/src/sat/sat_par.h deleted file mode 100644 index 001036a98..000000000 --- a/src/sat/sat_par.h +++ /dev/null @@ -1,39 +0,0 @@ -/*++ -Copyright (c) 2017 Microsoft Corporation - -Module Name: - - sat_par.h - -Abstract: - - Utilities for parallel SAT solving. - -Author: - - Nikolaj Bjorner (nbjorner) 2017-1-29. - -Revision History: - ---*/ -#ifndef SAT_PAR_H_ -#define SAT_PAR_H_ - -#include "sat/sat_types.h" -#include "util/hashtable.h" -#include "util/map.h" - -namespace sat { - - class par { - typedef hashtable index_set; - literal_vector m_units; - index_set m_unit_set; - public: - par(); - void exchange(literal_vector const& in, unsigned& limit, literal_vector& out); - }; - -}; - -#endif diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h index ad972b2af..e6e6c9d7b 100644 --- a/src/sat/sat_solver.h +++ b/src/sat/sat_solver.h @@ -37,7 +37,6 @@ Revision History: #include "sat/sat_drat.h" #include "sat/sat_parallel.h" #include "sat/sat_local_search.h" -#include "sat/sat_par.h" #include "util/params.h" #include "util/statistics.h" #include "util/stopwatch.h" From bb979a194e5baa3dc3c0632f00825e7c0627c40a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Oct 2018 19:32:44 -0700 Subject: [PATCH 09/18] remove unused return value of mk_enode following #1856 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 5b1de851e..c5dee4600 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -341,7 +341,7 @@ class theory_lra::imp { } app_ref cnst(a.mk_numeral(rational(c), is_int), m); TRACE("arith", tout << "add " << cnst << "\n";); - enode* e = mk_enode(cnst); + mk_enode(cnst); theory_var v = mk_var(cnst); var = m_solver->add_var(v, true); m_theory_var2var_index.setx(v, var, UINT_MAX); From be8a9c611e17d526792cb5b1b192726704b23a76 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Oct 2018 19:49:18 -0700 Subject: [PATCH 10/18] incorporate #1854 Signed-off-by: Nikolaj Bjorner --- CMakeLists.txt | 4 ++++ src/util/memory_manager.h | 4 +++- 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index a086afd71..28cd9fa33 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -383,6 +383,10 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") # FIXME: Remove "x.." when CMP0054 is set to NEW + elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel") + set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") + # Intel's compiler requires linking with libiomp5 + list(APPEND Z3_DEPENDENT_LIBS "iomp5") elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") set(SSE_FLAGS "/arch:SSE2") else() diff --git a/src/util/memory_manager.h b/src/util/memory_manager.h index 5cb7dc467..fec7c12b4 100644 --- a/src/util/memory_manager.h +++ b/src/util/memory_manager.h @@ -27,7 +27,9 @@ Revision History: # define __has_builtin(x) 0 #endif -#ifdef __GNUC__ +#ifdef __INTEL_COMPILER +# define ALLOC_ATTR __attribute__((malloc)) +#elif __GNUC__ # if (__GNUC__ * 100 + __GNUC_MINOR__) >= 409 || __has_builtin(returns_nonnull) # define GCC_RET_NON_NULL __attribute__((returns_nonnull)) # else From 9d0aa4d02d3c2fb5c33abbffa55358bed8e65f33 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 1 Oct 2018 20:22:02 -0700 Subject: [PATCH 11/18] update empty cube case for sat/undef cases Signed-off-by: Nikolaj Bjorner --- src/sat/sat_lookahead.cpp | 20 ++++++++++---------- src/sat/sat_lookahead.h | 2 ++ src/sat/sat_solver.cpp | 1 + src/sat/sat_solver/inc_sat_solver.cpp | 25 +++++++++++++++++-------- 4 files changed, 30 insertions(+), 18 deletions(-) diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index bbc1106bb..a6ff6a3b0 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -2057,6 +2057,15 @@ namespace sat { return h; } + bool lookahead::should_cutoff(unsigned depth) { + return depth > 0 && + ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) || + (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || + (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) || + (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || + (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)); + } + lbool lookahead::cube(bool_var_vector& vars, literal_vector& lits, unsigned backtrack_level) { scoped_ext _scoped_ext(*this); lits.reset(); @@ -2102,22 +2111,13 @@ namespace sat { } backtrack_level = UINT_MAX; depth = m_cube_state.m_cube.size(); - if ((m_config.m_cube_cutoff == depth_cutoff && depth == m_config.m_cube_depth) || - (m_config.m_cube_cutoff == freevars_cutoff && m_freevars.size() <= m_init_freevars * m_config.m_cube_freevars) || - (m_config.m_cube_cutoff == psat_cutoff && psat_heur() >= m_config.m_cube_psat_trigger) || - (m_config.m_cube_cutoff == adaptive_freevars_cutoff && m_freevars.size() < m_cube_state.m_freevars_threshold) || - (m_config.m_cube_cutoff == adaptive_psat_cutoff && psat_heur() >= m_cube_state.m_psat_threshold)) { + if (should_cutoff(depth)) { double dec = (1.0 - pow(m_config.m_cube_fraction, depth)); m_cube_state.m_freevars_threshold *= dec; m_cube_state.m_psat_threshold *= 2.0 - dec; set_conflict(); m_cube_state.inc_cutoff(); -#if 0 - // return cube of all literals, not just the ones in the main cube - lits.append(m_trail.size() - init_trail, m_trail.c_ptr() + init_trail); -#else lits.append(m_cube_state.m_cube); -#endif vars.reset(); for (auto v : m_freevars) if (in_reduced_clause(v)) vars.push_back(v); backtrack(m_cube_state.m_cube, m_cube_state.m_is_decision); diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h index df954bdf1..c2282e779 100644 --- a/src/sat/sat_lookahead.h +++ b/src/sat/sat_lookahead.h @@ -558,6 +558,8 @@ namespace sat { double psat_heur(); + bool should_cutoff(unsigned depth); + public: lookahead(solver& s) : m_s(s), diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index b58d2296b..b65abd41c 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -1030,6 +1030,7 @@ namespace sat { } break; case l_true: { + lits.reset(); pop_to_base_level(); model const& mdl = m_cuber->get_model(); for (bool_var v = 0; v < mdl.size(); ++v) { diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 5de64b496..7a77e3b4e 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -308,6 +308,12 @@ public: return nullptr; } + expr_ref_vector last_cube() { + expr_ref_vector result(m); + result.push_back(m.mk_false()); + return result; + } + expr_ref_vector cube(expr_ref_vector& vs, unsigned backtrack_level) override { if (!is_internalized()) { lbool r = internalize_formulas(); @@ -326,15 +332,18 @@ public: } sat::literal_vector lits; lbool result = m_solver.cube(vars, lits, backtrack_level); - if (result == l_false || lits.empty()) { - expr_ref_vector result(m); - result.push_back(m.mk_false()); - return result; - } - if (result == l_true) { - IF_VERBOSE(1, verbose_stream() << "formulas are SAT\n"); + switch (result) { + case l_true: return expr_ref_vector(m); - } + case l_false: + return last_cube(); + default: + SASSERT(!lits.empty()); + if (lits.empty()) { + IF_VERBOSE(0, verbose_stream() << "empty cube for undef\n";); + } + break; + } expr_ref_vector fmls(m); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); From 373b691709790b276e9b69c8c9c57ca1540c51fd Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 10:26:38 +0700 Subject: [PATCH 12/18] Use 'override' where possible. --- src/muz/spacer/spacer_generalizers.cpp | 2 +- src/muz/spacer/spacer_generalizers.h | 8 +- src/muz/transforms/dl_mk_synchronize.h | 2 +- src/opt/maxres.cpp | 10 +- src/opt/opt_cmds.cpp | 54 +++++------ src/opt/sortmax.cpp | 4 +- src/opt/wmax.cpp | 4 +- src/sat/ba_solver.h | 106 ++++++++++----------- src/sat/sat_lookahead.cpp | 2 +- src/sat/tactic/goal2sat.h | 2 +- src/smt/theory_lra.cpp | 2 +- src/smt/theory_pb.cpp | 6 +- src/smt/theory_str.cpp | 2 +- src/solver/parallel_tactic.cpp | 12 +-- src/tactic/core/symmetry_reduce_tactic.cpp | 2 +- src/tactic/dependency_converter.cpp | 18 ++-- src/tactic/generic_model_converter.h | 2 +- src/tactic/tactical.cpp | 6 +- src/util/lp/lar_solver.h | 2 +- 19 files changed, 123 insertions(+), 123 deletions(-) diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index b0fb6c2d3..6f9758337 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -50,7 +50,7 @@ namespace{ contains_array_op_proc(ast_manager &manager) : m(manager), m_array_fid(m.mk_family_id("array")) {} - virtual bool operator()(expr *e) { + bool operator()(expr *e) override { return is_app(e) && to_app(e)->get_family_id() == m_array_fid; } }; diff --git a/src/muz/spacer/spacer_generalizers.h b/src/muz/spacer/spacer_generalizers.h index 45ae472bd..e83cc1bc9 100644 --- a/src/muz/spacer/spacer_generalizers.h +++ b/src/muz/spacer/spacer_generalizers.h @@ -117,11 +117,11 @@ class lemma_quantifier_generalizer : public lemma_generalizer { int m_offset; public: lemma_quantifier_generalizer(context &ctx, bool normalize_cube = true); - virtual ~lemma_quantifier_generalizer() {} - virtual void operator()(lemma_ref &lemma); + ~lemma_quantifier_generalizer() override {} + void operator()(lemma_ref &lemma) override; - virtual void collect_statistics(statistics& st) const; - virtual void reset_statistics() {m_st.reset();} + void collect_statistics(statistics& st) const override; + void reset_statistics() override {m_st.reset();} private: bool generalize(lemma_ref &lemma, app *term); diff --git a/src/muz/transforms/dl_mk_synchronize.h b/src/muz/transforms/dl_mk_synchronize.h index 6f4b3ca40..77f45e91f 100644 --- a/src/muz/transforms/dl_mk_synchronize.h +++ b/src/muz/transforms/dl_mk_synchronize.h @@ -126,7 +126,7 @@ namespace datalog { */ mk_synchronize(context & ctx, unsigned priority = 22500); - rule_set * operator()(rule_set const & source); + rule_set * operator()(rule_set const & source) override; }; }; diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp index f52c56a60..0b5f20db8 100644 --- a/src/opt/maxres.cpp +++ b/src/opt/maxres.cpp @@ -144,7 +144,7 @@ public: } } - virtual ~maxres() {} + ~maxres() override {} bool is_literal(expr* l) { return @@ -332,7 +332,7 @@ public: } - virtual lbool operator()() { + lbool operator()() override { m_defs.reset(); switch(m_st) { case s_primal: @@ -343,7 +343,7 @@ public: return l_undef; } - virtual void collect_statistics(statistics& st) const { + void collect_statistics(statistics& st) const override { st.update("maxres-cores", m_stats.m_num_cores); st.update("maxres-correction-sets", m_stats.m_num_cs); } @@ -781,7 +781,7 @@ public: TRACE("opt", tout << "after remove: " << asms << "\n";); } - virtual void updt_params(params_ref& _p) { + void updt_params(params_ref& _p) override { maxsmt_solver_base::updt_params(_p); opt_params p(_p); m_hill_climb = p.maxres_hill_climb(); @@ -816,7 +816,7 @@ public: return l_true; } - virtual void commit_assignment() { + void commit_assignment() override { if (m_found_feasible_optimum) { TRACE("opt", tout << "Committing feasible solution\n" << m_defs << " " << m_asms;); s().assert_expr(m_defs); diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index d8e301e08..f01df0bdd 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -56,33 +56,33 @@ public: m_opt(opt) {} - virtual ~assert_soft_cmd() { + ~assert_soft_cmd() override { } - virtual void reset(cmd_context & ctx) { + void reset(cmd_context & ctx) override { m_idx = 0; m_formula = nullptr; } - virtual char const * get_usage() const { return " [:weight ] [:id ]"; } - virtual char const * get_main_descr() const { return "assert soft constraint with optional weight and identifier"; } + char const * get_usage() const override { return " [:weight ] [:id ]"; } + char const * get_main_descr() const override { return "assert soft constraint with optional weight and identifier"; } // command invocation - virtual void prepare(cmd_context & ctx) { + void prepare(cmd_context & ctx) override { reset(ctx); } - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { if (m_idx == 0) return CPK_EXPR; return parametric_cmd::next_arg_kind(ctx); } - virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) { + void init_pdescrs(cmd_context & ctx, param_descrs & p) override { p.insert("weight", CPK_NUMERAL, "(default: 1) penalty of not satisfying constraint."); p.insert("id", CPK_SYMBOL, "(default: null) partition identifier for soft constraints."); } - virtual void set_next_arg(cmd_context & ctx, expr * t) { + void set_next_arg(cmd_context & ctx, expr * t) override { SASSERT(m_idx == 0); if (!ctx.m().is_bool(t)) { throw cmd_exception("Invalid type for expression. Expected Boolean type."); @@ -91,11 +91,11 @@ public: ++m_idx; } - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { if (!m_formula) { throw cmd_exception("assert-soft requires a formulas as argument."); } @@ -107,7 +107,7 @@ public: reset(ctx); } - virtual void finalize(cmd_context & ctx) { + void finalize(cmd_context & ctx) override { } }; @@ -123,14 +123,14 @@ public: m_opt(opt) {} - virtual void reset(cmd_context & ctx) { } - virtual char const * get_usage() const { return ""; } - virtual char const * get_descr(cmd_context & ctx) const { return "check sat modulo objective function";} - virtual unsigned get_arity() const { return 1; } - virtual void prepare(cmd_context & ctx) {} - virtual cmd_arg_kind next_arg_kind(cmd_context & ctx) const { return CPK_EXPR; } + void reset(cmd_context & ctx) override { } + char const * get_usage() const override { return ""; } + char const * get_descr(cmd_context & ctx) const override { return "check sat modulo objective function";} + unsigned get_arity() const override { return 1; } + void prepare(cmd_context & ctx) override {} + cmd_arg_kind next_arg_kind(cmd_context & ctx) const override { return CPK_EXPR; } - virtual void set_next_arg(cmd_context & ctx, expr * t) { + void set_next_arg(cmd_context & ctx, expr * t) override { if (!is_app(t)) { throw cmd_exception("malformed objective term: it cannot be a quantifier or bound variable"); } @@ -138,11 +138,11 @@ public: ctx.print_success(); } - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { } }; @@ -154,18 +154,18 @@ public: m_opt(opt) {} - virtual void reset(cmd_context & ctx) { } - virtual char const * get_usage() const { return "(get-objectives)"; } - virtual char const * get_descr(cmd_context & ctx) const { return "retrieve the objective values (after optimization)"; } - virtual unsigned get_arity() const { return 0; } - virtual void prepare(cmd_context & ctx) {} + void reset(cmd_context & ctx) override { } + char const * get_usage() const override { return "(get-objectives)"; } + char const * get_descr(cmd_context & ctx) const override { return "retrieve the objective values (after optimization)"; } + unsigned get_arity() const override { return 0; } + void prepare(cmd_context & ctx) override {} - virtual void failure_cleanup(cmd_context & ctx) { + void failure_cleanup(cmd_context & ctx) override { reset(ctx); } - virtual void execute(cmd_context & ctx) { + void execute(cmd_context & ctx) override { if (!ctx.ignore_check()) { get_opt(ctx, m_opt).display_assignment(ctx.regular_stream()); } diff --git a/src/opt/sortmax.cpp b/src/opt/sortmax.cpp index 1fafa12bd..df361f24a 100644 --- a/src/opt/sortmax.cpp +++ b/src/opt/sortmax.cpp @@ -39,9 +39,9 @@ namespace opt { sortmax(maxsat_context& c, weights_t& ws, expr_ref_vector const& soft): maxsmt_solver_base(c, ws, soft), m_sort(*this), m_trail(m), m_fresh(m) {} - virtual ~sortmax() {} + ~sortmax() override {} - lbool operator()() { + lbool operator()() override { obj_map soft; if (!init()) { return l_false; diff --git a/src/opt/wmax.cpp b/src/opt/wmax.cpp index e4eb7e06b..ee7f92a23 100644 --- a/src/opt/wmax.cpp +++ b/src/opt/wmax.cpp @@ -49,9 +49,9 @@ namespace opt { m_trail(m), m_defs(m) {} - virtual ~wmax() {} + ~wmax() override {} - lbool operator()() { + lbool operator()() override { TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); obj_map soft; diff --git a/src/sat/ba_solver.h b/src/sat/ba_solver.h index bae59f45a..26887e3b1 100644 --- a/src/sat/ba_solver.h +++ b/src/sat/ba_solver.h @@ -128,7 +128,7 @@ namespace sat { virtual void set_k(unsigned k) { VERIFY(k < 4000000000); m_k = k; } virtual unsigned get_coeff(unsigned i) const { UNREACHABLE(); return 0; } unsigned k() const { return m_k; } - virtual bool well_formed() const; + bool well_formed() const override; }; class card : public pb_base { @@ -140,13 +140,13 @@ namespace sat { literal& operator[](unsigned i) { return m_lits[i]; } literal const* begin() const { return m_lits; } literal const* end() const { return static_cast(m_lits) + m_size; } - virtual void negate(); - virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } - virtual literal_vector literals() const { return literal_vector(m_size, m_lits); } - virtual bool is_watching(literal l) const; - virtual literal get_lit(unsigned i) const { return m_lits[i]; } - virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; } - virtual unsigned get_coeff(unsigned i) const { return 1; } + void negate() override; + void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); } + literal_vector literals() const override { return literal_vector(m_size, m_lits); } + bool is_watching(literal l) const override; + literal get_lit(unsigned i) const override { return m_lits[i]; } + void set_lit(unsigned i, literal l) override { m_lits[i] = l; } + unsigned get_coeff(unsigned i) const override { return 1; } }; @@ -173,14 +173,14 @@ namespace sat { void update_max_sum(); void set_num_watch(unsigned s) { m_num_watch = s; } bool is_cardinality() const; - virtual void negate(); - virtual void set_k(unsigned k) { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } - virtual void swap(unsigned i, unsigned j) { std::swap(m_wlits[i], m_wlits[j]); } - virtual literal_vector literals() const { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } - virtual bool is_watching(literal l) const; - virtual literal get_lit(unsigned i) const { return m_wlits[i].second; } - virtual void set_lit(unsigned i, literal l) { m_wlits[i].second = l; } - virtual unsigned get_coeff(unsigned i) const { return m_wlits[i].first; } + void negate() override; + void set_k(unsigned k) override { m_k = k; VERIFY(k < 4000000000); update_max_sum(); } + void swap(unsigned i, unsigned j) override { std::swap(m_wlits[i], m_wlits[j]); } + literal_vector literals() const override { literal_vector lits; for (auto wl : *this) lits.push_back(wl.second); return lits; } + bool is_watching(literal l) const override; + literal get_lit(unsigned i) const override { return m_wlits[i].second; } + void set_lit(unsigned i, literal l) override { m_wlits[i].second = l; } + unsigned get_coeff(unsigned i) const override { return m_wlits[i].first; } }; class xr : public constraint { @@ -191,13 +191,13 @@ namespace sat { literal operator[](unsigned i) const { return m_lits[i]; } literal const* begin() const { return m_lits; } literal const* end() const { return begin() + m_size; } - virtual void negate() { m_lits[0].neg(); } - virtual void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); } - virtual bool is_watching(literal l) const; - virtual literal_vector literals() const { return literal_vector(size(), begin()); } - virtual literal get_lit(unsigned i) const { return m_lits[i]; } - virtual void set_lit(unsigned i, literal l) { m_lits[i] = l; } - virtual bool well_formed() const; + void negate() override { m_lits[0].neg(); } + void swap(unsigned i, unsigned j) override { std::swap(m_lits[i], m_lits[j]); } + bool is_watching(literal l) const override; + literal_vector literals() const override { return literal_vector(size(), begin()); } + literal get_lit(unsigned i) const override { return m_lits[i]; } + void set_lit(unsigned i, literal l) override { m_lits[i] = l; } + bool well_formed() const override; }; @@ -484,44 +484,44 @@ namespace sat { public: ba_solver(); - virtual ~ba_solver(); - virtual void set_solver(solver* s) { m_solver = s; } - virtual void set_lookahead(lookahead* l) { m_lookahead = l; } - virtual void set_unit_walk(unit_walk* u) { m_unit_walk = u; } + ~ba_solver() override; + void set_solver(solver* s) override { m_solver = s; } + void set_lookahead(lookahead* l) override { m_lookahead = l; } + void set_unit_walk(unit_walk* u) override { m_unit_walk = u; } void add_at_least(bool_var v, literal_vector const& lits, unsigned k); void add_pb_ge(bool_var v, svector const& wlits, unsigned k); void add_xr(literal_vector const& lits); - virtual bool propagate(literal l, ext_constraint_idx idx); - virtual lbool resolve_conflict(); - virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r); - virtual void asserted(literal l); - virtual check_result check(); - virtual void push(); - virtual void pop(unsigned n); - virtual void simplify(); - virtual void clauses_modifed(); - virtual lbool get_phase(bool_var v); - virtual bool set_root(literal l, literal r); - virtual void flush_roots(); - virtual std::ostream& display(std::ostream& out) const; - virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const; - virtual void collect_statistics(statistics& st) const; - virtual extension* copy(solver* s); - virtual extension* copy(lookahead* s, bool learned); - virtual void find_mutexes(literal_vector& lits, vector & mutexes); - virtual void pop_reinit(); - virtual void gc(); - virtual double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const; - virtual bool is_extended_binary(ext_justification_idx idx, literal_vector & r); - virtual void init_use_list(ext_use_list& ul); - virtual bool is_blocked(literal l, ext_constraint_idx idx); - virtual bool check_model(model const& m) const; + bool propagate(literal l, ext_constraint_idx idx) override; + lbool resolve_conflict() override; + void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r) override; + void asserted(literal l) override; + check_result check() override; + void push() override; + void pop(unsigned n) override; + void simplify() override; + void clauses_modifed() override; + lbool get_phase(bool_var v) override; + bool set_root(literal l, literal r) override; + void flush_roots() override; + std::ostream& display(std::ostream& out) const override; + std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const override; + void collect_statistics(statistics& st) const override; + extension* copy(solver* s) override; + extension* copy(lookahead* s, bool learned) override; + void find_mutexes(literal_vector& lits, vector & mutexes) override; + void pop_reinit() override; + void gc() override; + double get_reward(literal l, ext_justification_idx idx, literal_occs_fun& occs) const override; + bool is_extended_binary(ext_justification_idx idx, literal_vector & r) override; + void init_use_list(ext_use_list& ul) override; + bool is_blocked(literal l, ext_constraint_idx idx) override; + bool check_model(model const& m) const override; ptr_vector const & constraints() const { return m_constraints; } void display(std::ostream& out, constraint const& c, bool values) const; - virtual bool validate(); + bool validate() override; }; diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp index bbc1106bb..0da914b71 100644 --- a/src/sat/sat_lookahead.cpp +++ b/src/sat/sat_lookahead.cpp @@ -1217,7 +1217,7 @@ namespace sat { lookahead& lh; public: lookahead_literal_occs_fun(lookahead& lh): lh(lh) {} - double operator()(literal l) { return lh.literal_occs(l); } + double operator()(literal l) override { return lh.literal_occs(l); } }; // Ternary clause managagement: diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h index d86b2d7e4..514b65311 100644 --- a/src/sat/tactic/goal2sat.h +++ b/src/sat/tactic/goal2sat.h @@ -86,7 +86,7 @@ public: public: mc(ast_manager& m); - virtual ~mc() {} + ~mc() override {} // flush model converter from SAT solver to this structure. void flush_smc(sat::solver& s, atom2bool_var const& map); void operator()(model_ref& md) override; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index db031d043..a27f4ff83 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -147,7 +147,7 @@ class theory_lra::imp { imp& m_imp; public: resource_limit(imp& i): m_imp(i) { } - virtual bool get_cancel_flag() { return m_imp.m.canceled(); } + bool get_cancel_flag() override { return m_imp.m.canceled(); } }; diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 2fb0187f8..90d1a5481 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -759,18 +759,18 @@ namespace smt { card& get_card() { return m_card; } - virtual void get_antecedents(conflict_resolution& cr) { + void get_antecedents(conflict_resolution& cr) override { cr.mark_literal(m_card.lit()); for (unsigned i = m_card.k(); i < m_card.size(); ++i) { cr.mark_literal(~m_card.lit(i)); } } - virtual theory_id get_from_theory() const { + theory_id get_from_theory() const override { return m_fid; } - virtual proof* mk_proof(smt::conflict_resolution& cr) { + proof* mk_proof(smt::conflict_resolution& cr) override { ptr_buffer prs; ast_manager& m = cr.get_context().get_manager(); expr_ref fact(m); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index d902aa533..324e1f54a 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -110,7 +110,7 @@ namespace smt { public: seq_expr_solver(ast_manager& m, smt_params& fp): m_kernel(m, fp) {} - virtual lbool check_sat(expr* e) { + lbool check_sat(expr* e) override { m_kernel.push(); m_kernel.assert_expr(e); lbool r = m_kernel.check(); diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index f0bb65315..4ee93ff37 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -672,7 +672,7 @@ public: init(); } - void operator ()(const goal_ref & g,goal_ref_buffer & result) { + void operator ()(const goal_ref & g,goal_ref_buffer & result) override { fail_if_proof_generation("parallel-tactic", g); ast_manager& m = g->m(); solver* s = m_solver->translate(m, m_params); @@ -719,29 +719,29 @@ public: return pp.conquer_batch_size(); } - void cleanup() { + void cleanup() override { m_queue.reset(); } - tactic* translate(ast_manager& m) { + tactic* translate(ast_manager& m) override { solver* s = m_solver->translate(m, m_params); return alloc(parallel_tactic, s, m_params); } - virtual void updt_params(params_ref const & p) { + void updt_params(params_ref const & p) override { m_params.copy(p); parallel_params pp(p); m_conquer_delay = pp.conquer_delay(); } - virtual void collect_statistics(statistics & st) const { + void collect_statistics(statistics & st) const override { st.copy(m_stats); st.update("par unsat", m_num_unsat); st.update("par models", m_models.size()); st.update("par progress", m_progress); } - virtual void reset_statistics() { + void reset_statistics() override { m_stats.reset(); } }; diff --git a/src/tactic/core/symmetry_reduce_tactic.cpp b/src/tactic/core/symmetry_reduce_tactic.cpp index d288adbc7..784686a5e 100644 --- a/src/tactic/core/symmetry_reduce_tactic.cpp +++ b/src/tactic/core/symmetry_reduce_tactic.cpp @@ -40,7 +40,7 @@ public: void operator()(goal_ref const & g, goal_ref_buffer & result) override; - virtual void cleanup() override; + void cleanup() override; }; class ac_rewriter { diff --git a/src/tactic/dependency_converter.cpp b/src/tactic/dependency_converter.cpp index 34c864526..dcd50717b 100644 --- a/src/tactic/dependency_converter.cpp +++ b/src/tactic/dependency_converter.cpp @@ -27,15 +27,15 @@ public: unit_dependency_converter(expr_dependency_ref& d) : m_dep(d) {} - virtual expr_dependency_ref operator()() { return m_dep; } + expr_dependency_ref operator()() override { return m_dep; } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { expr_dependency_translation tr(translator); expr_dependency_ref d(tr(m_dep), translator.to()); return alloc(unit_dependency_converter, d); } - virtual void display(std::ostream& out) { + void display(std::ostream& out) override { out << m_dep.get() << "\n"; } }; @@ -47,18 +47,18 @@ public: concat_dependency_converter(dependency_converter* c1, dependency_converter* c2) : m_dc1(c1), m_dc2(c2) {} - virtual expr_dependency_ref operator()() { + expr_dependency_ref operator()() override { expr_dependency_ref d1 = (*m_dc1)(); expr_dependency_ref d2 = (*m_dc2)(); ast_manager& m = d1.get_manager(); return expr_dependency_ref(m.mk_join(d1, d2), m); } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { return alloc(concat_dependency_converter, m_dc1->translate(translator), m_dc2->translate(translator)); } - virtual void display(std::ostream& out) { + void display(std::ostream& out) override { m_dc1->display(out); m_dc2->display(out); } @@ -73,7 +73,7 @@ public: for (unsigned i = 0; i < n; ++i) m_goals.push_back(goals[i]); } - virtual expr_dependency_ref operator()() { + expr_dependency_ref operator()() override { expr_dependency_ref result(m.mk_empty_dependencies(), m); for (goal_ref g : m_goals) { dependency_converter_ref dc = g->dc(); @@ -81,13 +81,13 @@ public: } return result; } - virtual dependency_converter * translate(ast_translation & translator) { + dependency_converter * translate(ast_translation & translator) override { goal_ref_buffer goals; for (goal_ref g : m_goals) goals.push_back(g->translate(translator)); return alloc(goal_dependency_converter, goals.size(), goals.c_ptr()); } - virtual void display(std::ostream& out) { out << "goal-dep\n"; } + void display(std::ostream& out) override { out << "goal-dep\n"; } }; diff --git a/src/tactic/generic_model_converter.h b/src/tactic/generic_model_converter.h index 69bc35a3f..750a22cd4 100644 --- a/src/tactic/generic_model_converter.h +++ b/src/tactic/generic_model_converter.h @@ -41,7 +41,7 @@ class generic_model_converter : public model_converter { public: generic_model_converter(ast_manager & m, char const* orig) : m(m), m_orig(orig) {} - virtual ~generic_model_converter(); + ~generic_model_converter() override; void hide(expr* e) { SASSERT(is_app(e) && to_app(e)->get_num_args() == 0); hide(to_app(e)->get_decl()); } diff --git a/src/tactic/tactical.cpp b/src/tactic/tactical.cpp index a71ea738c..98f6be343 100644 --- a/src/tactic/tactical.cpp +++ b/src/tactic/tactical.cpp @@ -744,7 +744,7 @@ public: SASSERT(t); } - virtual ~unary_tactical() { } + ~unary_tactical() override { } void operator()(goal_ref const & in, goal_ref_buffer& result) override { m_t->operator()(in, result); @@ -1003,7 +1003,7 @@ public: SASSERT(m_p); } - virtual ~cond_tactical() {} + ~cond_tactical() override {} void operator()(goal_ref const & in, goal_ref_buffer & result) override { if (m_p->operator()(*(in.get())).is_true()) @@ -1035,7 +1035,7 @@ public: SASSERT(m_p); } - virtual ~fail_if_tactic() {} + ~fail_if_tactic() override {} void cleanup() override {} diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 4189bad4e..8541a9b86 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -397,7 +397,7 @@ public: column_type get_column_type(unsigned j) const; - std::string get_column_name(unsigned j) const; + std::string get_column_name(unsigned j) const override; bool all_constrained_variables_are_registered(const vector>& left_side); From 7bc283b84ec9e33b6fc72ef3240ee5ee8f5e6b7c Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 10:38:41 +0700 Subject: [PATCH 13/18] Avoid unnecessary copies in for-range loops. --- src/ast/rewriter/pb2bv_rewriter.cpp | 2 +- src/smt/theory_seq.cpp | 4 ++-- src/test/lp/argument_parser.h | 6 +++--- src/test/lp/lp.cpp | 16 ++++++++-------- 4 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp index d1def83a1..0faf08515 100644 --- a/src/ast/rewriter/pb2bv_rewriter.cpp +++ b/src/ast/rewriter/pb2bv_rewriter.cpp @@ -458,7 +458,7 @@ struct pb2bv_rewriter::imp { result = m.mk_true(); expr_ref_vector carry(m), new_carry(m); m_base.push_back(bound + rational::one()); - for (rational b_i : m_base) { + for (const rational& b_i : m_base) { unsigned B = b_i.get_unsigned(); unsigned d_i = (bound % b_i).get_unsigned(); bound = div(bound, b_i); diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 233be9e31..093a47146 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1375,8 +1375,8 @@ bool theory_seq::branch_variable_mb() { continue; } rational l1, l2; - for (auto elem : len1) l1 += elem; - for (auto elem : len2) l2 += elem; + for (const auto& elem : len1) l1 += elem; + for (const auto& elem : len2) l2 += elem; if (l1 != l2) { TRACE("seq", tout << "lengths are not compatible\n";); expr_ref l = mk_concat(e.ls()); diff --git a/src/test/lp/argument_parser.h b/src/test/lp/argument_parser.h index c8566ce34..ce59632d2 100644 --- a/src/test/lp/argument_parser.h +++ b/src/test/lp/argument_parser.h @@ -112,7 +112,7 @@ public: std::string usage_string() { std::string ret = ""; std::vector unknown_options; - for (auto t : m_free_args) { + for (const auto & t : m_free_args) { if (starts_with(t, "-") || starts_with(t, "\\")) { unknown_options.push_back(t); } @@ -120,7 +120,7 @@ public: if (unknown_options.size()) { ret = "Unknown options:"; } - for (auto unknownOption : unknown_options) { + for (const auto & unknownOption : unknown_options) { ret += unknownOption; ret += ","; } @@ -140,7 +140,7 @@ public: return; } std::cout << "options are: " << std::endl; - for (std::string s : m_used_options) { + for (const std::string & s : m_used_options) { std::cout << s << std::endl; } for (auto & t : m_used_options_with_after_string) { diff --git a/src/test/lp/lp.cpp b/src/test/lp/lp.cpp index ff9de0e58..ffdbb5af8 100644 --- a/src/test/lp/lp.cpp +++ b/src/test/lp/lp.cpp @@ -1161,14 +1161,14 @@ void setup_solver(unsigned max_iterations, unsigned time_limit, bool look_for_mi bool values_are_one_percent_close(double a, double b); void print_x(mps_reader & reader, lp_solver * solver) { - for (auto name : reader.column_names()) { + for (const auto & name : reader.column_names()) { std::cout << name << "=" << solver->get_column_value_by_name(name) << ' '; } std::cout << std::endl; } void compare_solutions(mps_reader & reader, lp_solver * solver, lp_solver * solver0) { - for (auto name : reader.column_names()) { + for (const auto & name : reader.column_names()) { double a = solver->get_column_value_by_name(name); double b = solver0->get_column_value_by_name(name); if (!values_are_one_percent_close(a, b)) { @@ -1299,7 +1299,7 @@ void solve_mps_in_rational(std::string file_name, bool dual, argument_parser & / std::cout << "status is " << lp_status_to_string(solver->get_status()) << std::endl; if (solver->get_status() == lp_status::OPTIMAL) { if (reader.column_names().size() < 20) { - for (auto name : reader.column_names()) { + for (const auto & name : reader.column_names()) { std::cout << name << "=" << solver->get_column_value_by_name(name).get_double() << ' '; } } @@ -1414,7 +1414,7 @@ void solve_mps_with_known_solution(std::string file_name, std::unordered_map get_solution_map(lp_solver * lps, mps_reader & reader) { std::unordered_map ret; - for (auto it : reader.column_names()) { + for (const auto & it : reader.column_names()) { ret[it] = lps->get_column_value_by_name(it); } return ret; @@ -2487,7 +2487,7 @@ void test_lar_solver(argument_parser & args_parser) { std::string file_list = args_parser.get_option_value("--filelist"); if (file_list.size() > 0) { - for (std::string fn : get_file_names_from_file_list(file_list)) + for (const std::string & fn : get_file_names_from_file_list(file_list)) test_lar_on_file(fn, args_parser); return; } @@ -3624,7 +3624,7 @@ void test_lp_local(int argn, char**argv) { } std::string file_list = args_parser.get_option_value("--filelist"); if (file_list.size() > 0) { - for (std::string fn : get_file_names_from_file_list(file_list)) + for (const std::string & fn : get_file_names_from_file_list(file_list)) solve_mps(fn, args_parser); return finalize(0); } From 1067a5363f74c55f26f4146d993e6b923fdc478d Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 08:34:57 +0700 Subject: [PATCH 14/18] theory_lra: Remove unused variable. --- src/smt/theory_lra.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index d3475bdc1..171c4de0a 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1569,7 +1569,6 @@ public: VERIFY(a.is_idiv(n, p, q)); theory_var v = mk_var(n); theory_var v1 = mk_var(p); - theory_var v2 = mk_var(q); rational r1 = get_value(v1); rational r2; From 6d2936e5fc20a26cac2ed37d39dd94d7d89f86f2 Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 08:35:12 +0700 Subject: [PATCH 15/18] watch_list: Fix indentation. --- src/smt/watch_list.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/smt/watch_list.cpp b/src/smt/watch_list.cpp index 9835142f6..778e93021 100644 --- a/src/smt/watch_list.cpp +++ b/src/smt/watch_list.cpp @@ -36,10 +36,10 @@ namespace smt { void watch_list::expand() { if (m_data == nullptr) { - unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; + unsigned size = DEFAULT_WATCH_LIST_SIZE + HEADER_SIZE; unsigned * mem = reinterpret_cast(alloc_svect(char, size)); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif *mem = 0; ++mem; @@ -62,9 +62,9 @@ namespace smt { unsigned * mem = reinterpret_cast(alloc_svect(char, new_capacity + HEADER_SIZE)); unsigned curr_end_cls = end_cls_core(); #ifdef _AMD64_ - ++mem; // make sure data is aligned in 64 bit machines + ++mem; // make sure data is aligned in 64 bit machines #endif - *mem = curr_end_cls; + *mem = curr_end_cls; ++mem; SASSERT(bin_bytes <= new_capacity); unsigned new_begin_bin = new_capacity - bin_bytes; From a76397d3b8174583db90c75f84ab60f8fa0c831f Mon Sep 17 00:00:00 2001 From: Bruce Mitchener Date: Tue, 2 Oct 2018 17:38:09 +0700 Subject: [PATCH 16/18] Refer to macOS rather than Mac OS / OSX. --- CMakeLists.txt | 2 +- README.md | 6 +++--- examples/c++/README | 4 ++-- examples/c/README | 4 ++-- examples/java/README | 2 +- examples/maxsat/README | 4 ++-- examples/ml/README | 2 +- examples/python/example.py | 2 +- examples/tptp/README | 4 ++-- src/api/python/README.txt | 4 ++-- src/api/python/setup.py | 2 +- src/cmd_context/pdecl.h | 2 +- src/math/polynomial/polynomial.cpp | 2 +- src/shell/main.cpp | 2 +- src/util/hwf.cpp | 12 ++++++------ src/util/scoped_timer.cpp | 10 +++++----- src/util/stopwatch.h | 2 +- 17 files changed, 33 insertions(+), 33 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 28cd9fa33..500b67100 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -240,7 +240,7 @@ if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") endif() elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") - # Does OSX really not need any special flags? + # Does macOS really not need any special flags? message(STATUS "Platform: Darwin") elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") message(STATUS "Platform: FreeBSD") diff --git a/README.md b/README.md index 447034a84..e02719161 100644 --- a/README.md +++ b/README.md @@ -12,8 +12,8 @@ See the [release notes](RELEASE_NOTES) for notes on various stable releases of Z ## Build status -| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | OSX | TravisCI | -| ----------- | ----------- | ----------- | ---------- | ---------- | --- | -------- | +| Windows x64 | Windows x86 | Windows x64 | Ubuntu x64 | Debian x64 | macOS | TravisCI | +| ----------- | ----------- | ----------- | ---------- | ---------- | ----- | -------- | [![win64-badge](https://z3build.visualstudio.com/_apis/public/build/definitions/2e0aa542-a22c-4b1a-8dcd-3ebae8e12db4/4/badge)](https://z3build.visualstudio.com/Z3Build/_build/index?definitionId=4) | [![win32-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/4/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=4) | [![win64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/7/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=7) | [![ubuntu-x64-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/3/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=3) | [![debian-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/5/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=5) | [![osx-badge](https://cz3.visualstudio.com/_apis/public/build/definitions/bf14bcc7-ebd4-4240-812c-5972fa59e0ad/2/badge)](https://cz3.visualstudio.com/Z3/_build/index?definitionId=2) | [![Build Status](https://travis-ci.org/Z3Prover/z3.svg?branch=master)](https://travis-ci.org/Z3Prover/z3) [1]: #building-z3-on-windows-using-visual-studio-command-prompt @@ -75,7 +75,7 @@ A 32 bit build should work similarly (but is untested); the same is true for 32/ By default, it will install z3 executable at ``PREFIX/bin``, libraries at ``PREFIX/lib``, and include files at ``PREFIX/include``, where ``PREFIX`` installation prefix if inferred by the ``mk_make.py`` script. It is usually -``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and OSX. Use +``/usr`` for most Linux distros, and ``/usr/local`` for FreeBSD and macOS. Use the ``--prefix=`` command line option to change the install prefix. For example: ```bash diff --git a/examples/c++/README b/examples/c++/README index 56775e537..2b3c5affc 100644 --- a/examples/c++/README +++ b/examples/c++/README @@ -5,6 +5,6 @@ in the build directory. This command will create the executable cpp_example. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. \ No newline at end of file +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/examples/c/README b/examples/c/README index 4ca71e0f8..af9dd39f6 100644 --- a/examples/c/README +++ b/examples/c/README @@ -5,7 +5,7 @@ in the build directory. This command will create the executable c_example. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/examples/java/README b/examples/java/README index 1939afc49..d3ff93fe0 100644 --- a/examples/java/README +++ b/examples/java/README @@ -10,5 +10,5 @@ which can be run on Windows via On Linux and FreeBSD, we must use LD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample -On OSX, the corresponding option is DYLD_LIBRARY_PATH: +On macOS, the corresponding option is DYLD_LIBRARY_PATH: DYLD_LIBRARY_PATH=. java -cp com.microsoft.z3.jar:. JavaExample diff --git a/examples/maxsat/README b/examples/maxsat/README index 6c24da66b..8c7d3b0f7 100644 --- a/examples/maxsat/README +++ b/examples/maxsat/README @@ -5,8 +5,8 @@ in the build directory. This command will create the executable maxsat. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) with the build directory. You need that to be able to find the Z3 shared library. +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. This directory contains a test file (ex.smt) that can be used as input for the maxsat test application. diff --git a/examples/ml/README b/examples/ml/README index 1c474fe33..9797b85e3 100644 --- a/examples/ml/README +++ b/examples/ml/README @@ -20,4 +20,4 @@ ocamlfind ocamlopt -o ml_example -package Z3 -linkpkg ml_example.ml Note that the resulting binaries depend on the shared z3 library (libz3.dll/.so/.dylb), which needs to be in the PATH (Windows), LD_LIBRARY_PATH -(Linux), or DYLD_LIBRARY_PATH (OSX). +(Linux), or DYLD_LIBRARY_PATH (macOS). diff --git a/examples/python/example.py b/examples/python/example.py index a17668506..761ae10be 100644 --- a/examples/python/example.py +++ b/examples/python/example.py @@ -20,7 +20,7 @@ # export PYTHONPATH=MYZ3/bin/python # python example.py -# Running this example on OSX: +# Running this example on macOS: # export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin # export PYTHONPATH=MYZ3/bin/python # python example.py diff --git a/examples/tptp/README b/examples/tptp/README index c28a53da4..b3edfe6a8 100644 --- a/examples/tptp/README +++ b/examples/tptp/README @@ -5,9 +5,9 @@ in the build directory. This command will create the executable tptp. On Windows, you can just execute it. -On OSX and Linux, you must install z3 first using +On macOS and Linux, you must install z3 first using sudo make install -OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OSX) +OR update LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (macOS) with the build directory. You need that to be able to find the Z3 shared library. diff --git a/src/api/python/README.txt b/src/api/python/README.txt index 9831c6fc6..9312b1119 100644 --- a/src/api/python/README.txt +++ b/src/api/python/README.txt @@ -12,8 +12,8 @@ If you are using a 64-bit Python interpreter, you should use msbuild /p:configuration=external /p:platform=x64 -On Linux and OSX, you must install Z3Py, before trying example.py. -To install Z3Py on Linux and OSX, you should execute the following +On Linux and macOS, you must install Z3Py, before trying example.py. +To install Z3Py on Linux and macOS, you should execute the following command in the Z3 root directory sudo make install-z3py diff --git a/src/api/python/setup.py b/src/api/python/setup.py index bce681584..2a750fee6 100644 --- a/src/api/python/setup.py +++ b/src/api/python/setup.py @@ -73,7 +73,7 @@ def _build_z3(): if subprocess.call(['nmake'], env=build_env, cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") - else: # linux and osx + else: # linux and macOS if subprocess.call(['make', '-j', str(multiprocessing.cpu_count())], env=build_env, cwd=BUILD_DIR) != 0: raise LibError("Unable to build Z3.") diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h index 12e6399fe..d994a1e8f 100644 --- a/src/cmd_context/pdecl.h +++ b/src/cmd_context/pdecl.h @@ -53,7 +53,7 @@ public: class psort_inst_cache; #if defined(__APPLE__) && defined(__MACH__) -// CMW: for some unknown reason, llvm on OSX does not like the name `psort' +// CMW: for some unknown reason, llvm on macOS does not like the name `psort' #define psort Z3_psort #endif diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index 35a95ce82..24658fdcf 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -100,7 +100,7 @@ namespace polynomial { struct lt_var { bool operator()(power const & p1, power const & p2) { - // CMW: The assertion below does not hold on OSX, because + // CMW: The assertion below does not hold on macOS, because // their implementation of std::sort will try to compare // two items at the same index instead of comparing // the indices directly. I suspect that the purpose of diff --git a/src/shell/main.cpp b/src/shell/main.cpp index 1c8b6908d..3b97d4462 100644 --- a/src/shell/main.cpp +++ b/src/shell/main.cpp @@ -91,7 +91,7 @@ void display_usage() { std::cout << " -pp:name display Z3 parameter description, if 'name' is not provided, then all module names are listed.\n"; std::cout << " --" << " all remaining arguments are assumed to be part of the input file name. This option allows Z3 to read files with strange names such as: -foo.smt2.\n"; std::cout << "\nResources:\n"; - // timeout and memout are now available on Linux and OSX too. + // timeout and memout are now available on Linux and macOS too. std::cout << " -T:timeout set the timeout (in seconds).\n"; std::cout << " -t:timeout set the soft timeout (in milli seconds). It only kills the current query.\n"; std::cout << " -memory:Megabytes set a limit for virtual memory consumption.\n"; diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp index b8f481329..32b1343e3 100644 --- a/src/util/hwf.cpp +++ b/src/util/hwf.cpp @@ -45,7 +45,7 @@ Revision History: // For SSE2, it is best to use compiler intrinsics because this makes it completely // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects // the x87 FPU, even when /arch:SSE2 is on. -// Luckily, these are kind of standardized, at least for Windows/Linux/OSX. +// Luckily, these are kind of standardized, at least for Windows/Linux/macOS. #ifdef __clang__ #undef USE_INTRINSICS #endif @@ -75,14 +75,14 @@ hwf_manager::hwf_manager() : #endif #endif #else - // OSX/Linux: Nothing. + // macOS/Linux: Nothing. #endif // We only set the precision of the FPU here in the constructor. At the moment, there are no // other parts of the code that could overwrite this, and Windows takes care of context switches. // CMW: I'm not sure what happens on CPUs with hyper-threading (since the FPU is shared). - // I have yet to discover whether Linux and OSX save the FPU state when switching context. + // I have yet to discover whether Linux and macOS save the FPU state when switching context. // As long as we stick to using the SSE2 FPU though, there shouldn't be any problems with respect // to the precision (not sure about the rounding modes though). } @@ -279,7 +279,7 @@ void hwf_manager::fma(mpf_rounding_mode rm, hwf const & x, hwf const & y, hwf co #endif #endif #else - // Linux, OSX + // Linux, macOS o.value = ::fma(x.value, y.value, z.value); #endif #endif @@ -331,7 +331,7 @@ void hwf_manager::round_to_integral(mpf_rounding_mode rm, hwf const & x, hwf & o } #endif #else - // Linux, OSX. + // Linux, macOS. o.value = nearbyint(x.value); #endif } @@ -623,7 +623,7 @@ void hwf_manager::set_rounding_mode(mpf_rounding_mode rm) UNREACHABLE(); // Note: MPF_ROUND_NEAREST_TAWAY is not supported by the hardware! } #endif -#else // OSX/Linux +#else // macOS/Linux switch (rm) { case MPF_ROUND_NEAREST_TEVEN: SETRM(FE_TONEAREST); diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 8078c46ee..9850699be 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -27,7 +27,7 @@ Revision History: // Windows #include #elif defined(__APPLE__) && defined(__MACH__) -// Mac OS X +// macOS #include #include #include @@ -59,7 +59,7 @@ struct scoped_timer::imp { HANDLE m_timer; bool m_first; #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS pthread_t m_thread_id; pthread_attr_t m_attributes; unsigned m_interval; @@ -89,7 +89,7 @@ struct scoped_timer::imp { } } #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS static void * thread_func(void * arg) { scoped_timer::imp * st = static_cast(arg); @@ -153,7 +153,7 @@ struct scoped_timer::imp { ms, WT_EXECUTEINTIMERTHREAD); #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS m_interval = ms?ms:0xFFFFFFFF; if (pthread_attr_init(&m_attributes) != 0) throw default_exception("failed to initialize timer thread attributes"); @@ -194,7 +194,7 @@ struct scoped_timer::imp { m_timer, INVALID_HANDLE_VALUE); #elif defined(__APPLE__) && defined(__MACH__) - // Mac OS X + // macOS // If the waiting-thread is not up and waiting yet, // we can make sure that it finishes quickly by diff --git a/src/util/stopwatch.h b/src/util/stopwatch.h index c606824b4..2c7551df0 100644 --- a/src/util/stopwatch.h +++ b/src/util/stopwatch.h @@ -70,7 +70,7 @@ public: #undef min -#elif defined(__APPLE__) && defined (__MACH__) // Mac OS X +#elif defined(__APPLE__) && defined (__MACH__) // macOS #include #include From a376a8d3432be226127af80c71877a13246412fd Mon Sep 17 00:00:00 2001 From: Kirill Bobyrev Date: Tue, 2 Oct 2018 16:14:01 +0300 Subject: [PATCH 17/18] [NFC] Cleanup arith_eq_solver.(cpp|h) Use for-range loops instead of for-index loops where possible, remove trailing whitespaces. This patch does not affect functionality. --- src/smt/arith_eq_solver.cpp | 135 ++++++++++++++++++------------------ src/smt/arith_eq_solver.h | 24 +++---- 2 files changed, 78 insertions(+), 81 deletions(-) diff --git a/src/smt/arith_eq_solver.cpp b/src/smt/arith_eq_solver.cpp index 128b35dd1..883255b8a 100644 --- a/src/smt/arith_eq_solver.cpp +++ b/src/smt/arith_eq_solver.cpp @@ -12,14 +12,11 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2012-02-25 - + --*/ #include "smt/arith_eq_solver.h" -arith_eq_solver::~arith_eq_solver() { -} - arith_eq_solver::arith_eq_solver(ast_manager & m, params_ref const& p): m(m), m_params(p), @@ -93,9 +90,9 @@ void arith_eq_solver::gcd_normalize(vector& values) { if (g.is_zero() || g.is_one()) { return; } - for (unsigned i = 0; i < values.size(); ++i) { - values[i] = values[i] / g; - SASSERT(values[i].is_int()); + for (auto &value : values) { + value /= g; + SASSERT(value.is_int()); } } @@ -116,9 +113,9 @@ unsigned arith_eq_solver::find_abs_min(vector& values) { #ifdef _TRACE static void print_row(std::ostream& out, vector const& row) { - for(unsigned i = 0; i < row.size(); ++i) { - out << row[i] << " "; - } + for(unsigned i = 0; i < row.size(); ++i) { + out << row[i] << " "; + } out << "\n"; } @@ -165,7 +162,7 @@ bool arith_eq_solver::solve_integer_equation( bool& is_fresh ) { - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "solving: "; print_row(tout, values); ); @@ -174,31 +171,31 @@ bool arith_eq_solver::solve_integer_equation( // // Given: // a1*x1 + a2*x2 + .. + a_n*x_n + a_{n+1} = 0 - // + // // Assume gcd(a1,..,a_n,a_{n+1}) = 1 // Assume gcd(a1,...,a_n) divides a_{n+1} (eg. gcd(a1,..,an) = 1) - // + // // post-condition: values[index] = -1. - // + // // Let a_index be index of least absolute value. // // If |a_index| = 1, then return row and index. // Otherwise: // Let m = |a_index| + 1 // Set - // - // m*x_index' - // = + // + // m*x_index' + // = // ((a1 mod_hat m)*x1 + (a2 mod_hat m)*x2 + .. + (a_n mod_hat m)*x_n + (k mod_hat m)) - // = + // = // (a1'*x1 + a2'*x2 + .. (-)1*x_index + ...) - // + // // <=> Normalize signs so that sign to x_index is -1. // (-)a1'*x1 + (-)a2'*x2 + .. -1*x_index + ... + m*x_index' = 0 - // + // // Return row, where the coefficient to x_index is implicit. // Instead used the coefficient 'm' at position 'index'. - // + // gcd_normalize(values); if (!gcd_test(values)) { @@ -216,8 +213,8 @@ bool arith_eq_solver::solve_integer_equation( return true; } if (a.is_one()) { - for (unsigned i = 0; i < values.size(); ++i) { - values[i].neg(); + for (auto &value : values) { + value.neg(); } } is_fresh = !abs_a.is_one(); @@ -225,19 +222,19 @@ bool arith_eq_solver::solve_integer_equation( if (is_fresh) { numeral m = abs_a + numeral(1); - for (unsigned i = 0; i < values.size(); ++i) { - values[i] = mod_hat(values[i], m); + for (auto &value : values) { + value = mod_hat(value, m); } if (values[index].is_one()) { - for (unsigned i = 0; i < values.size(); ++i) { - values[i].neg(); + for (auto &value : values) { + value.neg(); } } SASSERT(values[index].is_minus_one()); values[index] = m; } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "solved at index " << index << ": "; print_row(tout, values); ); @@ -253,7 +250,7 @@ void arith_eq_solver::substitute( ) { SASSERT(1 <= index && index < s.size()); - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "substitute " << index << ":\n"; print_row(tout, r); print_row(tout, s); @@ -272,21 +269,21 @@ void arith_eq_solver::substitute( // s encodes an equation that contains a variable // with a unit coefficient. // - // Let + // Let // c = r[index] // s = s[index]*x + s'*y = 0 // r = c*x + r'*y = 0 - // - // => + // + // => // // 0 - // = - // -sign(s[index])*c*s + r - // = + // = + // -sign(s[index])*c*s + r + // = // -s[index]*sign(s[index])*c*x - sign(s[index])*c*s'*y + c*x + r'*y - // = + // = // -c*x - sign(s[index])*c*s'*y + c*x + r'*y - // = + // = // -sign(s[index])*c*s'*y + r'*y // numeral sign_s = s[index].is_pos()?numeral(1):numeral(-1); @@ -301,36 +298,36 @@ void arith_eq_solver::substitute( // // s encodes a substitution using an auxiliary variable. // the auxiliary variable is at position 'index'. - // - // Let + // + // Let // c = r[index] // s = s[index]*x + s'*y = 0 // r = c*x + r'*y = 0 // // s encodes : x |-> s[index]*x' + s'*y // - // Set: + // Set: // // r := c*s + r'*y - // + // r[index] = numeral(0); for (unsigned i = 0; i < r.size(); ++i) { r[i] += c*s[i]; - } + } for (unsigned i = r.size(); i < s.size(); ++i) { r.push_back(c*s[i]); } - } + } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "result: "; print_row(tout, r); ); } bool arith_eq_solver::solve_integer_equations( - vector& rows, + vector& rows, row& unsat_row ) { @@ -340,10 +337,10 @@ bool arith_eq_solver::solve_integer_equations( // // Naive integer equation solver where only units are eliminated. -// +// bool arith_eq_solver::solve_integer_equations_units( - vector& rows, + vector& rows, row& unsat_row ) { @@ -351,7 +348,7 @@ bool arith_eq_solver::solve_integer_equations_units( TRACE("arith_eq_solver", print_rows(tout << "solving:\n", rows);); unsigned_vector todo, done; - + for (unsigned i = 0; i < rows.size(); ++i) { todo.push_back(i); row& r = rows[i]; @@ -360,9 +357,9 @@ bool arith_eq_solver::solve_integer_equations_units( unsat_row = r; TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); ); return false; - } + } } - for (unsigned i = 0; i < todo.size(); ++i) { + for (unsigned i = 0; i < todo.size(); ++i) { row& r = rows[todo[i]]; gcd_normalize(r); if (!gcd_test(r)) { @@ -388,7 +385,7 @@ bool arith_eq_solver::solve_integer_equations_units( todo.push_back(done[j]); done.erase(done.begin()+j); --j; - } + } } } else { @@ -396,7 +393,7 @@ bool arith_eq_solver::solve_integer_equations_units( } } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << ((done.size()<=1)?"solved ":"incomplete check ") << done.size() << "\n"; for (unsigned i = 0; i < done.size(); ++i) { print_row(tout, rows[done[i]]); @@ -411,12 +408,12 @@ bool arith_eq_solver::solve_integer_equations_units( // // Partial solver based on the omega test equalities. -// unsatisfiability is not preserved when eliminating +// unsatisfiability is not preserved when eliminating // auxiliary variables. // bool arith_eq_solver::solve_integer_equations_omega( - vector & rows, + vector & rows, row& unsat_row ) { @@ -460,16 +457,16 @@ bool arith_eq_solver::solve_integer_equations_omega( // // solved_row: -x_index + m*sigma + r1 = 0 // unsat_row: k*sigma + r2 = 0 - // - // <=> - // + // + // <=> + // // solved_row: -k*x_index + k*m*sigma + k*r1 = 0 // unsat_row: m*k*sigma + m*r2 = 0 // // => // // m*k*sigma + m*r2 + k*x_index - k*m*sigma - k*r1 = 0 - // + // for (unsigned l = 0; l < unsat_row.size(); ++l) { unsat_row[l] *= m; unsat_row[l] -= k*solved_row[l]; @@ -479,7 +476,7 @@ bool arith_eq_solver::solve_integer_equations_omega( } gcd_normalize(unsat_row); - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << "gcd: "; print_row(tout, solved_row); print_row(tout, unsat_row); @@ -525,18 +522,18 @@ bool arith_eq_solver::solve_integer_equations_omega( // // Eliminate variables by searching for combination of rows where -// the coefficients have gcd = 1. -// +// the coefficients have gcd = 1. +// bool arith_eq_solver::solve_integer_equations_gcd( - vector & rows, + vector & rows, row& unsat_row ) -{ +{ unsigned_vector live, useful, gcd_pos; vector gcds; rational u, v; - + if (rows.empty()) { return true; } @@ -548,7 +545,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( unsat_row = r; TRACE("arith_eq_solver", print_row(tout << "input is unsat: ", unsat_row); ); return false; - } + } } unsigned max_column = rows[0].size(); bool change = true; @@ -579,7 +576,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( if (j == live.size()) { continue; } - + change = true; // found gcd, now identify reduced set of rows with GCD = 1. g = abs(rows[live[j]][i]); @@ -592,7 +589,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( useful.push_back(gcd_pos[j]); g = gcd(g, gcds[j]); SASSERT(j == 0 || gcd(g,gcds[j-1]).is_one()); - } + } } // // we now have a set "useful" of rows whose combined GCD = 1. @@ -600,7 +597,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( // row& r0 = rows[useful[0]]; for (j = 1; j < useful.size(); ++j) { - row& r1 = rows[useful[j]]; + row& r1 = rows[useful[j]]; g = gcd(r0[i], r1[i], u, v); for (unsigned k = 0; k < max_column; ++k) { r0[k] = u*r0[k] + v*r1[k]; @@ -626,7 +623,7 @@ bool arith_eq_solver::solve_integer_equations_gcd( } } - TRACE("arith_eq_solver", + TRACE("arith_eq_solver", tout << ((live.size()<=1)?"solved ":"incomplete check ") << live.size() << "\n"; for (unsigned i = 0; i < live.size(); ++i) { print_row(tout, rows[live[i]]); diff --git a/src/smt/arith_eq_solver.h b/src/smt/arith_eq_solver.h index b2db35ee1..68e58334d 100644 --- a/src/smt/arith_eq_solver.h +++ b/src/smt/arith_eq_solver.h @@ -12,7 +12,7 @@ Abstract: Author: Nikolaj Bjorner (nbjorner) 2012-02-25 - + --*/ #ifndef ARITH_EQ_SOLVER_H_ #define ARITH_EQ_SOLVER_H_ @@ -35,45 +35,45 @@ class arith_eq_solver { void prop_mod_const(expr * e, unsigned depth, numeral const& k, expr_ref& result); - bool gcd_test(vector& value); + bool gcd_test(vector& values); unsigned find_abs_min(vector& values); void gcd_normalize(vector& values); void substitute(vector& r, vector const& s, unsigned index); bool solve_integer_equations_units( - vector > & rows, + vector > & rows, vector& unsat_row ); - + bool solve_integer_equations_omega( - vector > & rows, + vector > & rows, vector& unsat_row ); void compute_hnf(vector >& A); bool solve_integer_equations_hermite( - vector > & rows, + vector > & rows, vector& unsat_row ); bool solve_integer_equations_gcd( - vector > & rows, + vector > & rows, vector& unsat_row ); public: arith_eq_solver(ast_manager & m, params_ref const& p = params_ref()); - ~arith_eq_solver(); + ~arith_eq_solver() = default; // Integer linear solver for a single equation. // The array values contains integer coefficients - // + // // Determine integer solutions to: // // a+k = 0 // // where a = sum_i a_i*k_i - // + // typedef vector row; typedef vector matrix; @@ -90,14 +90,14 @@ public: // a+k = 0 // // where a = sum_i a_i*k_i - // + // // Solution, if there is any, is returned as a substitution. // The return value is "true". // If there is no solution, then return "false". // together with equality "eq_unsat", such that // // eq_unsat = 0 - // + // // is implied and is unsatisfiable over the integers. // From 5bf57c270071a29835a8dcafa93f411a91ad56f7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 2 Oct 2018 08:14:19 -0700 Subject: [PATCH 18/18] fix cubing semantics Signed-off-by: Nikolaj Bjorner --- src/sat/sat_solver/inc_sat_solver.cpp | 17 ++++++++--------- src/solver/tactic2solver.cpp | 1 + 2 files changed, 9 insertions(+), 9 deletions(-) diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 7a77e3b4e..df2da82e7 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -308,9 +308,9 @@ public: return nullptr; } - expr_ref_vector last_cube() { + expr_ref_vector last_cube(bool is_sat) { expr_ref_vector result(m); - result.push_back(m.mk_false()); + result.push_back(is_sat ? m.mk_true() : m.mk_false()); return result; } @@ -334,16 +334,16 @@ public: lbool result = m_solver.cube(vars, lits, backtrack_level); switch (result) { case l_true: - return expr_ref_vector(m); + return last_cube(true); case l_false: - return last_cube(); + return last_cube(false); default: - SASSERT(!lits.empty()); - if (lits.empty()) { - IF_VERBOSE(0, verbose_stream() << "empty cube for undef\n";); - } break; } + if (lits.empty()) { + set_reason_unknown(m_solver.get_reason_unknown()); + return expr_ref_vector(m); + } expr_ref_vector fmls(m); expr_ref_vector lit2expr(m); lit2expr.resize(m_solver.num_vars() * 2); @@ -358,7 +358,6 @@ public: vs.push_back(x); } } - if (fmls.empty()) { IF_VERBOSE(0, verbose_stream() << "no literals were produced in cube\n"); } return fmls; } diff --git a/src/solver/tactic2solver.cpp b/src/solver/tactic2solver.cpp index cf0c6f9bc..3a905bafd 100644 --- a/src/solver/tactic2solver.cpp +++ b/src/solver/tactic2solver.cpp @@ -79,6 +79,7 @@ public: expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { + set_reason_unknown("cubing is not supported on tactics"); return expr_ref_vector(get_manager()); }