From fa93bc419d31fde6bfc7f4a8b42b384de1ec22e4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 1 May 2018 10:53:36 -0700 Subject: [PATCH] fix build Signed-off-by: Nikolaj Bjorner --- examples/c/test_capi.c | 24 ++++++++------ src/ackermannization/ackr_model_converter.cpp | 2 +- .../lackr_model_converter_lazy.cpp | 2 +- src/muz/spacer/spacer_itp_solver.h | 4 +-- src/muz/transforms/dl_mk_karr_invariants.cpp | 4 ++- .../dl_mk_quantifier_abstraction.cpp | 4 +-- src/muz/transforms/dl_mk_scale.cpp | 2 +- src/sat/sat_solver.cpp | 6 ++-- src/smt/smt_solver.cpp | 2 +- src/smt/tactic/smt_tactic.cpp | 2 -- src/smt/theory_pb.cpp | 8 ++--- src/tactic/aig/aig.cpp | 2 +- .../portfolio/bounded_int2bv_solver.cpp | 2 +- src/tactic/portfolio/enum2bv_solver.cpp | 32 +++++++++---------- 14 files changed, 47 insertions(+), 49 deletions(-) diff --git a/examples/c/test_capi.c b/examples/c/test_capi.c index e49b2991f..6761b3f8d 100644 --- a/examples/c/test_capi.c +++ b/examples/c/test_capi.c @@ -378,7 +378,7 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) { Z3_sort t; Z3_symbol f_name, t_name; - Z3_ast q; + Z3_ast_vector q; t = Z3_get_range(ctx, f); @@ -394,13 +394,14 @@ void assert_comm_axiom(Z3_context ctx, Z3_solver s, Z3_func_decl f) /* Inside the parser, type t will be referenced using the symbol 'T'. */ t_name = Z3_mk_string_symbol(ctx, "T"); - q = Z3_parse_smtlib2_string(ctx, "(assert (forall ((x T) (y T)) (= (f x y) (f y x))))", 1, &t_name, &t, 1, &f_name, &f); - printf("assert axiom:\n%s\n", Z3_ast_to_string(ctx, q)); - Z3_solver_assert(ctx, s, q); + printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, q)); + for (unsigned i = 0; i < Z3_ast_vector_size(ctx, q); ++i) { + Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, q, i)); + } } /** @@ -1642,7 +1643,7 @@ void parser_example2() Z3_ast x, y; Z3_symbol names[2]; Z3_func_decl decls[2]; - Z3_ast f; + Z3_ast_vector f; printf("\nparser_example2\n"); LOG_MSG("parser_example2"); @@ -1665,8 +1666,11 @@ void parser_example2() 0, 0, 0, /* 'x' and 'y' declarations are inserted as 'a' and 'b' into the parser symbol table. */ 2, names, decls); - printf("formula: %s\n", Z3_ast_to_string(ctx, f)); - Z3_solver_assert(ctx, s, f); + printf("formula: %s\n", Z3_ast_vector_to_string(ctx, f)); + printf("assert axiom:\n%s\n", Z3_ast_vector_to_string(ctx, f)); + for (unsigned i = 0; i < Z3_ast_vector_size(ctx, f); ++i) { + Z3_solver_assert(ctx, s, Z3_ast_vector_get(ctx, f, i)); + } check(ctx, s, Z3_L_TRUE); del_solver(ctx, s); @@ -1685,7 +1689,7 @@ void parser_example3() Z3_symbol g_name; Z3_sort g_domain[2]; Z3_func_decl g; - Z3_ast thm; + Z3_ast_vector thm; printf("\nparser_example3\n"); LOG_MSG("parser_example3"); @@ -1710,8 +1714,8 @@ void parser_example3() "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (g x 0) (g 0 y)))))", 0, 0, 0, 1, &g_name, &g); - printf("formula: %s\n", Z3_ast_to_string(ctx, thm)); - prove(ctx, s, thm, Z3_TRUE); + printf("formula: %s\n", Z3_ast_vector_to_string(ctx, thm)); + prove(ctx, s, Z3_ast_vector_get(ctx, thm, 0), Z3_TRUE); del_solver(ctx, s); Z3_del_context(ctx); diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp index 8b43d5e71..9e87a1a69 100644 --- a/src/ackermannization/ackr_model_converter.cpp +++ b/src/ackermannization/ackr_model_converter.cpp @@ -61,7 +61,7 @@ public: } } - virtual void display(std::ostream & out) { + void display(std::ostream & out) override { out << "(ackr-model-converter)\n"; } diff --git a/src/ackermannization/lackr_model_converter_lazy.cpp b/src/ackermannization/lackr_model_converter_lazy.cpp index 5d0fff59f..a37373aab 100644 --- a/src/ackermannization/lackr_model_converter_lazy.cpp +++ b/src/ackermannization/lackr_model_converter_lazy.cpp @@ -46,7 +46,7 @@ public: NOT_IMPLEMENTED_YET(); } - virtual void display(std::ostream & out) { + void display(std::ostream & out) override { out << "(lackr-model-converter)\n"; } diff --git a/src/muz/spacer/spacer_itp_solver.h b/src/muz/spacer/spacer_itp_solver.h index 99bf08871..466e0a2f1 100644 --- a/src/muz/spacer/spacer_itp_solver.h +++ b/src/muz/spacer/spacer_itp_solver.h @@ -110,9 +110,7 @@ public: void set_produce_models(bool f) override { m_solver.set_produce_models(f);} void assert_expr_core(expr *t) override { m_solver.assert_expr(t);} void assert_expr_core2(expr *t, expr *a) override { NOT_IMPLEMENTED_YET();} - virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); } - virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); } - virtual expr_ref_vector cube(expr_ref_vector&, unsigned) { return expr_ref_vector(m); } + expr_ref_vector cube(expr_ref_vector&, unsigned) override { return expr_ref_vector(m); } void push() override; void pop(unsigned n) override; diff --git a/src/muz/transforms/dl_mk_karr_invariants.cpp b/src/muz/transforms/dl_mk_karr_invariants.cpp index 68a13818c..fd14538c5 100644 --- a/src/muz/transforms/dl_mk_karr_invariants.cpp +++ b/src/muz/transforms/dl_mk_karr_invariants.cpp @@ -152,7 +152,9 @@ namespace datalog { return mc; } - virtual void display(std::ostream& out) { out << "(add-invariant-model-converter)\n"; } + void display(std::ostream& out) override { + out << "(add-invariant-model-converter)\n"; + } private: void mk_body(matrix const& M, expr_ref& body) { diff --git a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp index 2d0cb9146..e9a4f2f54 100644 --- a/src/muz/transforms/dl_mk_quantifier_abstraction.cpp +++ b/src/muz/transforms/dl_mk_quantifier_abstraction.cpp @@ -53,9 +53,9 @@ namespace datalog { return alloc(qa_model_converter, m); } - virtual void display(std::ostream& out) { display_add(out, m); } + void display(std::ostream& out) override { display_add(out, m); } - virtual void get_units(obj_map& units) { units.reset(); } + void get_units(obj_map& units) override { units.reset(); } void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector const& bound) { m_old_funcs.push_back(old_p); diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index b73e7e55e..0144948bd 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -100,7 +100,7 @@ namespace datalog { return nullptr; } - virtual void display(std::ostream& out) { out << "(scale-model-converter)\n"; } + void display(std::ostream& out) override { out << "(scale-model-converter)\n"; } }; diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp index 825a1170a..673afeab0 100644 --- a/src/sat/sat_solver.cpp +++ b/src/sat/sat_solver.cpp @@ -39,8 +39,6 @@ namespace sat { m_par(nullptr), m_cls_allocator_idx(false), m_cleaner(*this), - m_par_id(0), - m_par_syncing_clauses(false), m_simplifier(*this, p), m_scc(*this, p), m_asymm_branch(*this, p), @@ -55,7 +53,9 @@ namespace sat { m_qhead(0), m_scope_lvl(0), m_search_lvl(0), - m_params(p) { + m_params(p), + m_par_id(0), + m_par_syncing_clauses(false) { init_reason_unknown(); updt_params(p); m_conflicts_since_gc = 0; diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp index b493f9df3..378e56314 100644 --- a/src/smt/smt_solver.cpp +++ b/src/smt/smt_solver.cpp @@ -244,7 +244,7 @@ namespace smt { return m_context.get_formula(idx); } - virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) { + expr_ref_vector cube(expr_ref_vector& vars, unsigned cutoff) override { ast_manager& m = get_manager(); if (!m_cuber) { m_cuber = alloc(cuber, *this); diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 8d052ccf2..cc0f0f207 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -305,13 +305,11 @@ tactic * mk_smt_tactic_using(bool auto_config, params_ref const & _p) { tactic * mk_psmt_tactic(ast_manager& m, params_ref const& p, symbol const& logic) { parallel_params pp(p); - bool use_parallel = pp.enable(); return pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p); } tactic * mk_psmt_tactic_using(ast_manager& m, bool auto_config, params_ref const& _p, symbol const& logic) { parallel_params pp(_p); - bool use_parallel = pp.enable(); params_ref p = _p; p.set_bool("auto_config", auto_config); return using_params(pp.enable() ? mk_parallel_tactic(mk_smt_solver(m, p, logic), p) : mk_smt_tactic(p), p); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 40965ee82..e34a16eec 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -317,6 +317,7 @@ namespace smt { void theory_pb::card::set_conflict(theory_pb& th, literal l) { SASSERT(validate_conflict(th)); context& ctx = th.get_context(); + (void)ctx; literal_vector& lits = th.get_literals(); SASSERT(ctx.get_assignment(l) == l_false); SASSERT(ctx.get_assignment(lit()) == l_true); @@ -343,7 +344,7 @@ namespace smt { bool theory_pb::card::validate_assign(theory_pb& th, literal_vector const& lits, literal l) { context& ctx = th.get_context(); - SASSERT(ctx.get_assignment(l) == l_undef); + VERIFY(ctx.get_assignment(l) == l_undef); for (unsigned i = 0; i < lits.size(); ++i) { SASSERT(ctx.get_assignment(lits[i]) == l_true); } @@ -906,7 +907,6 @@ namespace smt { } std::ostream& theory_pb::display(std::ostream& out, card const& c, bool values) const { - ast_manager& m = get_manager(); context& ctx = get_context(); out << c.lit(); if (c.lit() != null_literal) { @@ -1494,12 +1494,10 @@ namespace smt { if (v == null_bool_var) continue; card* c = m_var_infos[v].m_card; if (c) { - unsigned np = c->num_propagations(); c->reset_propagations(); literal lit = c->lit(); if (c->is_aux() && ctx.get_assign_level(lit) > ctx.get_search_level()) { double activity = ctx.get_activity(v); - // std::cout << "activity: " << ctx.get_activity(v) << " " << np << "\n"; if (activity <= 0) { nz++; } @@ -2528,7 +2526,6 @@ namespace smt { normalize_active_coeffs(); for (unsigned i = 0; i < m_active_vars.size(); ++i) { bool_var v = m_active_vars[i]; - int coeff = get_coeff(v); literal lit(v, get_coeff(v) < 0); args.push_back(literal2expr(lit)); coeffs.push_back(rational(get_abs_coeff(v))); @@ -2541,7 +2538,6 @@ namespace smt { void theory_pb::display_resolved_lemma(std::ostream& out) const { context& ctx = get_context(); - literal_vector const& lits = ctx.assigned_literals(); bool_var v; unsigned lvl; out << "num marks: " << m_num_marks << "\n"; diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index 1c23faba5..805a8321a 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -636,7 +636,7 @@ struct aig_manager::imp { bool check_cache() const { for (auto const& kv : m_cache) { - SASSERT(ref_count(kv.m_value) > 0); + VERIFY(ref_count(kv.m_value) > 0); } return true; } diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp index a659e5803..8767644f3 100644 --- a/src/tactic/portfolio/bounded_int2bv_solver.cpp +++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp @@ -177,7 +177,7 @@ public: return mc; } - virtual model_converter_ref get_model_converter() const { + model_converter_ref get_model_converter() const override { model_converter_ref mc = external_model_converter(); mc = concat(mc.get(), m_solver->get_model_converter().get()); return mc; diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp index 030453759..6b5fe9056 100644 --- a/src/tactic/portfolio/enum2bv_solver.cpp +++ b/src/tactic/portfolio/enum2bv_solver.cpp @@ -83,13 +83,13 @@ public: return m_solver->check_sat(num_assumptions, assumptions); } - virtual void updt_params(params_ref const & p) { solver::updt_params(p); m_solver->updt_params(p); } - virtual void collect_param_descrs(param_descrs & r) { m_solver->collect_param_descrs(r); } - virtual void set_produce_models(bool f) { m_solver->set_produce_models(f); } - virtual void set_progress_callback(progress_callback * callback) { m_solver->set_progress_callback(callback); } - virtual void collect_statistics(statistics & st) const { m_solver->collect_statistics(st); } - virtual void get_unsat_core(ptr_vector & r) { m_solver->get_unsat_core(r); } - virtual void get_model_core(model_ref & mdl) { + void updt_params(params_ref const & p) override { solver::updt_params(p); m_solver->updt_params(p); } + void collect_param_descrs(param_descrs & r) override { m_solver->collect_param_descrs(r); } + void set_produce_models(bool f) override { m_solver->set_produce_models(f); } + void set_progress_callback(progress_callback * callback) override { m_solver->set_progress_callback(callback); } + void collect_statistics(statistics & st) const override { m_solver->collect_statistics(st); } + void get_unsat_core(ptr_vector & r) override { m_solver->get_unsat_core(r); } + void get_model_core(model_ref & mdl) override { m_solver->get_model(mdl); if (mdl) { model_converter_ref mc = local_model_converter(); @@ -113,24 +113,24 @@ public: return concat(mc0(), local_model_converter()); } - virtual model_converter_ref get_model_converter() const { + model_converter_ref get_model_converter() const override { model_converter_ref mc = external_model_converter(); mc = concat(mc.get(), m_solver->get_model_converter().get()); return mc; } - virtual proof * get_proof() { return m_solver->get_proof(); } - virtual std::string reason_unknown() const { return m_solver->reason_unknown(); } - virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); } - virtual void get_labels(svector & r) { m_solver->get_labels(r); } - virtual ast_manager& get_manager() const { return m; } - virtual lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) { + proof * get_proof() override { return m_solver->get_proof(); } + std::string reason_unknown() const override { return m_solver->reason_unknown(); } + void set_reason_unknown(char const* msg) override { m_solver->set_reason_unknown(msg); } + void get_labels(svector & r) override { m_solver->get_labels(r); } + ast_manager& get_manager() const override { return m; } + lbool find_mutexes(expr_ref_vector const& vars, vector& mutexes) override { return m_solver->find_mutexes(vars, mutexes); } - virtual expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) { + expr_ref_vector cube(expr_ref_vector& vars, unsigned backtrack_level) override { return m_solver->cube(vars, backtrack_level); } - virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) { + lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) override { datatype_util dt(m); bv_util bv(m); expr_ref_vector bvars(m), conseq(m), bounds(m);