mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
unused warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
e6e1d94cf9
commit
637a0fa139
|
@ -41,8 +41,8 @@ struct ast_pp_dot_st {
|
|||
m_pp(pp),
|
||||
m_next_id(0),
|
||||
m_id_map(),
|
||||
m_to_print(),
|
||||
m_printed(),
|
||||
m_to_print(),
|
||||
m_first(true) {}
|
||||
|
||||
~ast_pp_dot_st() = default;
|
||||
|
|
|
@ -3076,8 +3076,6 @@ void fpa2bv_converter::mk_to_ieee_bv(func_decl * f, unsigned num, expr * const *
|
|||
split_fp(x, sgn, e, s);
|
||||
mk_is_nan(x, x_is_nan);
|
||||
|
||||
sort * fp_srt = m.get_sort(x);
|
||||
|
||||
expr_ref unspec(m);
|
||||
mk_to_ieee_bv_unspecified(f, num, args, unspec);
|
||||
|
||||
|
|
|
@ -149,8 +149,6 @@ namespace spacer {
|
|||
expr_ref val(m), tmp(m);
|
||||
proof_ref pr(m);
|
||||
pr = m.mk_asserted(m.mk_true());
|
||||
obj_map<expr, unsigned>::iterator it = diseqs.begin();
|
||||
obj_map<expr, unsigned>::iterator end = diseqs.end();
|
||||
for (auto const& kv : diseqs) {
|
||||
if (kv.m_value >= threshold) {
|
||||
model.eval(kv.m_key, val);
|
||||
|
|
|
@ -81,6 +81,8 @@ static bool matches_fact(expr_ref_vector &args, expr* &match)
|
|||
}
|
||||
|
||||
|
||||
// TBD: move to ast/proofs/elim_aux_assertions
|
||||
|
||||
class elim_aux_assertions {
|
||||
app_ref m_aux;
|
||||
public:
|
||||
|
@ -404,6 +406,7 @@ void virtual_solver::refresh()
|
|||
m_head = 0;
|
||||
}
|
||||
|
||||
#ifdef NOT_USED_ANYWHERE
|
||||
void virtual_solver::reset()
|
||||
{
|
||||
SASSERT(!m_pushed);
|
||||
|
@ -411,6 +414,7 @@ void virtual_solver::reset()
|
|||
m_assertions.reset();
|
||||
m_factory.refresh();
|
||||
}
|
||||
#endif
|
||||
|
||||
void virtual_solver::get_labels(svector<symbol> &r)
|
||||
{
|
||||
|
|
|
@ -91,8 +91,9 @@ public:
|
|||
virtual void set_produce_models(bool f);
|
||||
virtual bool get_produce_models();
|
||||
virtual smt_params &fparams();
|
||||
#ifdef NOT_USED_ANYWHERE
|
||||
virtual void reset();
|
||||
|
||||
#endif
|
||||
virtual void set_progress_callback(progress_callback *callback)
|
||||
{UNREACHABLE();}
|
||||
|
||||
|
|
|
@ -218,7 +218,6 @@ namespace smt {
|
|||
ast_manager & m = get_manager();
|
||||
ext_skolems = alloc(func_decl_ref_vector, m);
|
||||
for (unsigned i = 0; i < dimension; ++i) {
|
||||
sort * ext_sk_domain[2] = { s_array, s_array };
|
||||
func_decl * ext_sk_decl = util.mk_array_ext(s_array, i);
|
||||
ext_skolems->push_back(ext_sk_decl);
|
||||
}
|
||||
|
|
|
@ -441,7 +441,7 @@ ptr_vector<expr> const & dom_simplify_tactic::tree(expr * e) {
|
|||
}
|
||||
|
||||
|
||||
// ----------------------
|
||||
// ---------------------
|
||||
// expr_substitution_simplifier
|
||||
|
||||
bool expr_substitution_simplifier::assert_expr(expr * t, bool sign) {
|
||||
|
|
|
@ -95,7 +95,6 @@ class dom_simplify_tactic : public tactic {
|
|||
expr_ref_vector m_trail, m_args;
|
||||
obj_map<expr, expr*> m_result;
|
||||
expr_dominators m_dominators;
|
||||
unsigned m_scope_level;
|
||||
unsigned m_depth;
|
||||
unsigned m_max_depth;
|
||||
ptr_vector<expr> m_empty;
|
||||
|
@ -128,8 +127,7 @@ public:
|
|||
dom_simplify_tactic(ast_manager & m, dom_simplifier* s, params_ref const & p = params_ref()):
|
||||
m(m), m_simplifier(s), m_params(p),
|
||||
m_trail(m), m_args(m),
|
||||
m_dominators(m),
|
||||
m_scope_level(0), m_depth(0), m_max_depth(1024), m_forward(true) {}
|
||||
m_dominators(m), m_depth(0), m_max_depth(1024), m_forward(true) {}
|
||||
|
||||
|
||||
virtual ~dom_simplify_tactic();
|
||||
|
|
Loading…
Reference in a new issue