mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

address unused variable warnings from OSX build log

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-03-05 15:33:33 -08:00
parent aa1ddd169a
commit 4cd1efc50e
3 changed files with 11 additions and 48 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/ackermannization/ackermannize_bv_tactic.cpp
View file

@ -24,8 +24,7 @@ Revision History:
class ackermannize_bv_tactic : public tactic {
public:
ackermannize_bv_tactic(ast_manager& m, params_ref const& p)
: m_m(m)
, m_p(p)
: m(m), m_p(p)
{}
virtual ~ackermannize_bv_tactic() { }
@ -36,7 +35,6 @@ public:
proof_converter_ref & pc,
expr_dependency_ref & core) {
mc = 0;
ast_manager& m(g->m());
tactic_report report("ackermannize", *g);
fail_if_unsat_core_generation("ackermannize", g);
fail_if_proof_generation("ackermannize", g);
@ -44,11 +42,11 @@ public:
expr_ref_vector flas(m);
const unsigned sz = g->size();
for (unsigned i = 0; i < sz; i++) flas.push_back(g->form(i));
scoped_ptr<lackr> imp = alloc(lackr, m, m_p, m_st, flas, NULL);
flas.reset();
lackr lackr(m, m_p, m_st, flas, NULL);
// mk result
goal_ref resg(alloc(goal, *g, true));
const bool success = imp->mk_ackermann(resg, m_lemma_limit);
const bool success = lackr.mk_ackermann(resg, m_lemma_limit);
if (!success) { // Just pass on the input unchanged
result.reset();
result.push_back(g.get());
@ -60,12 +58,12 @@ public:
result.push_back(resg.get());
// report model
if (g->models_enabled()) {
mc = mk_ackermannize_bv_model_converter(m, imp->get_info());
mc = mk_ackermannize_bv_model_converter(m, lackr.get_info());
}
resg->inc_depth();
TRACE("ackermannize", resg->display(tout););
SASSERT(resg->is_well_sorted());
resg->inc_depth();
TRACE("ackermannize", resg->display(tout););
SASSERT(resg->is_well_sorted());
}
@ -86,7 +84,7 @@ public:
return alloc(ackermannize_bv_tactic, m, m_p);
}
private:
ast_manager& m_m;
ast_manager& m;
params_ref m_p;
lackr_stats m_st;
double m_lemma_limit;

36
src/smt/arith_eq_adapter.cpp
View file

@ -152,40 +152,7 @@ namespace smt {
// 5) theory_arith fails to internalize (+ (* -1 x) (* -1 x)), and Z3 crashes.
//
#if 0
// This block of code uses the simplifier for creating the literals t1 >= t2 and t1 <= t2.
// It has serious performance problems in VCC benchmarks.
// The problem seems to be the following:
// t1 and t2 are slacks (i.e., names for linear polynomials).
// The simplifier will create inequalities that will indirectly imply that t1 >= t2 and t1 <= t2.
// Example if: t1 := 1 + a
// t2 := 2 + b
// the simplifier will create
// a - b >= -1
// a - b <= -1
// These inequalities imply that 1+a >= 2+b and 1+a <= 2+b,
// but the tableau is complete different.
// BTW, note that we don't really need to handle the is_numeral case when using
// the simplifier. However, doing that, it seems we minimize the performance problem.
expr_ref le(m);
expr_ref ge(m);
if (m_util.is_numeral(t1))
std::swap(t1, t2);
if (m_util.is_numeral(t2)) {
le = m_util.mk_le(t1, t2);
ge = m_util.mk_ge(t1, t2);
}
else {
arith_simplifier_plugin & s = *(get_simplifier());
s.mk_le(t1, t2, le);
s.mk_ge(t1, t2, ge);
}
TRACE("arith_eq_adapter_perf", tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
#else
// Old version that used to be buggy.
// I fixed the theory arithmetic internalizer to accept non simplified terms of the form t1 - t2
// Requires that the theory arithmetic internalizer accept non simplified terms of the form t1 - t2
// if t1 and t2 already have slacks (theory variables) associated with them.
// It also accepts terms with repeated variables (Issue #429).
app * le = 0;
@ -207,7 +174,6 @@ namespace smt {
}
TRACE("arith_eq_adapter_perf",
tout << mk_ismt2_pp(t1_eq_t2, m) << "\n" << mk_ismt2_pp(le, m) << "\n" << mk_ismt2_pp(ge, m) << "\n";);
#endif
ctx.push_trail(already_processed_trail(m_already_processed, n1, n2));
m_already_processed.insert(n1, n2, data(t1_eq_t2, le, ge));

3
src/smt/arith_eq_adapter.h
View file

@ -65,7 +65,6 @@ namespace smt {
theory & m_owner;
theory_arith_params & m_params;
arith_util & m_util;
arith_simplifier_plugin * m_as;
already_processed m_already_processed;
enode_pair_vector m_restart_pairs;
@ -76,7 +75,7 @@ namespace smt {
enode * get_enode(theory_var v) const { return m_owner.get_enode(v); }
public:
arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u), m_as(0) {}
arith_eq_adapter(theory & owner, theory_arith_params & params, arith_util & u):m_owner(owner), m_params(params), m_util(u) {}
void new_eq_eh(theory_var v1, theory_var v2);
void new_diseq_eh(theory_var v1, theory_var v2);
void reset_eh();