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<expr, bool>& units) { units.reset(); }
+ void get_units(obj_map<expr, bool>& units) override { units.reset(); }
void insert(func_decl* old_p, func_decl* new_p, expr_ref_vector& sub, sort_ref_vector& sorts, svector<bool> 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<expr> & 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<expr> & 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<symbol> & r) { m_solver->get_labels(r); }
- virtual ast_manager& get_manager() const { return m; }
- virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_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<symbol> & r) override { m_solver->get_labels(r); }
+ ast_manager& get_manager() const override { return m; }
+ lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_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);