mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 02:15:19 +00:00
fix debug build, unused variable warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
df492e200f
commit
4bcf1bf2f6
|
@ -474,13 +474,15 @@ void pattern_inference::reset_pre_patterns() {
|
|||
m_pre_patterns.reset();
|
||||
}
|
||||
|
||||
|
||||
#ifdef _TRACE
|
||||
static void dump_app_vector(std::ostream & out, ptr_vector<app> const & v, ast_manager & m) {
|
||||
ptr_vector<app>::const_iterator it = v.begin();
|
||||
ptr_vector<app>::const_iterator end = v.end();
|
||||
for (; it != end; ++it)
|
||||
out << mk_pp(*it, m) << "\n";
|
||||
}
|
||||
#endif
|
||||
|
||||
bool pattern_inference::is_forbidden(app * n) const {
|
||||
func_decl const * decl = n->get_decl();
|
||||
if (is_ground(n))
|
||||
|
|
|
@ -25,7 +25,7 @@ bv_bounds::conv_res bv_bounds::record(app * v, numeral lo, numeral hi, bool nega
|
|||
TRACE("bv_bounds", tout << "record0 " << mk_ismt2_pp(v, m_m) << ":" << (negated ? "~[" : "[") << lo << ";" << hi << "]" << std::endl;);
|
||||
const unsigned bv_sz = m_bv_util.get_bv_size(v);
|
||||
const numeral& one = numeral::one();
|
||||
SASSERT(numerl::zero() <= lo);
|
||||
SASSERT(numeral::zero() <= lo);
|
||||
SASSERT(lo <= hi);
|
||||
SASSERT(hi < numeral::power_of_two(bv_sz));
|
||||
numeral vmax, vmin;
|
||||
|
|
|
@ -88,7 +88,7 @@ namespace datalog {
|
|||
svector<bool> m_can_remove, m_can_expand;
|
||||
obj_map<expr, unsigned_vector> m_positions;
|
||||
public:
|
||||
visitor(context& c, substitution & s): st_visitor(s), m_context(c) {}
|
||||
visitor(context& c, substitution & s): st_visitor(s), m_context(c) { (void) m_context; }
|
||||
virtual bool operator()(expr* e);
|
||||
void reset() { m_unifiers.reset(); }
|
||||
void reset(unsigned sz);
|
||||
|
|
|
@ -113,6 +113,8 @@ unsigned arith_eq_solver::find_abs_min(vector<numeral>& values) {
|
|||
return index;
|
||||
}
|
||||
|
||||
#ifdef _TRACE
|
||||
|
||||
static void print_row(std::ostream& out, vector<rational> const& row) {
|
||||
for(unsigned i = 0; i < row.size(); ++i) {
|
||||
out << row[i] << " ";
|
||||
|
@ -125,6 +127,7 @@ static void print_rows(std::ostream& out, vector<vector<rational> > const& rows)
|
|||
print_row(out, rows[i]);
|
||||
}
|
||||
}
|
||||
#endif
|
||||
|
||||
//
|
||||
// The gcd of the coefficients to variables have to divide the
|
||||
|
|
|
@ -490,6 +490,7 @@ namespace smt {
|
|||
#ifdef _PROFILE_MAM
|
||||
m_counter = 0;
|
||||
#endif
|
||||
(void)m_lbl_hasher;
|
||||
}
|
||||
|
||||
#ifdef _PROFILE_MAM
|
||||
|
@ -2881,6 +2882,7 @@ namespace smt {
|
|||
- first_idx: index to be used as head of the multi-pattern mp
|
||||
*/
|
||||
void add_pattern(quantifier * qa, app * mp, unsigned first_idx) {
|
||||
(void)m_ast_manager;
|
||||
SASSERT(m_ast_manager.is_pattern(mp));
|
||||
SASSERT(first_idx < mp->get_num_args());
|
||||
app * p = to_app(mp->get_arg(first_idx));
|
||||
|
|
|
@ -335,23 +335,6 @@ namespace smt {
|
|||
}
|
||||
}
|
||||
|
||||
static bool find_arg(app * n, expr * t, expr * & other) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
if (n->get_arg(0) == t) {
|
||||
other = n->get_arg(1);
|
||||
return true;
|
||||
}
|
||||
else if (n->get_arg(1) == t) {
|
||||
other = n->get_arg(0);
|
||||
return true;
|
||||
}
|
||||
return false;
|
||||
}
|
||||
|
||||
static bool check_args(app * n, expr * t1, expr * t2) {
|
||||
SASSERT(n->get_num_args() == 2);
|
||||
return (n->get_arg(0) == t1 && n->get_arg(1) == t2) || (n->get_arg(1) == t1 && n->get_arg(0) == t2);
|
||||
}
|
||||
|
||||
/**
|
||||
\brief Internalize the given formula into the logical context.
|
||||
|
|
|
@ -112,7 +112,6 @@ namespace smt {
|
|||
};
|
||||
|
||||
class fpa_rm_value_proc : public model_value_proc {
|
||||
theory_fpa & m_th;
|
||||
ast_manager & m;
|
||||
fpa_util & m_fu;
|
||||
bv_util & m_bu;
|
||||
|
@ -120,7 +119,7 @@ namespace smt {
|
|||
|
||||
public:
|
||||
fpa_rm_value_proc(theory_fpa * th) :
|
||||
m_th(*th), m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
|
||||
m(th->get_manager()), m_fu(th->m_fpa_util), m_bu(th->m_bv_util) {}
|
||||
|
||||
void add_dependency(enode * e) { m_deps.push_back(model_value_dependency(e)); }
|
||||
|
||||
|
|
|
@ -102,6 +102,7 @@ namespace smt {
|
|||
m_enabled.push_back(true);
|
||||
m_normalize = true;
|
||||
bool_var bv = register_var(var, true);
|
||||
(void)bv;
|
||||
TRACE("opt", tout << "enable: v" << m_bool2var[bv] << " b" << bv << " " << mk_pp(var, get_manager()) << "\n";
|
||||
tout << wfml << "\n";);
|
||||
return var;
|
||||
|
|
Loading…
Reference in a new issue