mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 13:29:11 +00:00
Code Activity

fix warnings for unused variables

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2016-05-17 13:54:22 -07:00
parent ec565ae7a0
commit 96e157e201
38 changed files with 180 additions and 184 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/ackermannization/lackr.cpp
View file

@ -134,7 +134,6 @@ void lackr::eager_enc() {
const fun2terms_map::iterator e = m_fun2terms.end();
for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
checkpoint();
func_decl* const fd = i->m_key;
app_set * const ts = i->get_value();
const app_set::iterator r = ts->end();
for (app_set::iterator j = ts->begin(); j != r; ++j) {
@ -143,8 +142,8 @@ void lackr::eager_enc() {
for (; k != r; ++k) {
app * const t1 = *j;
app * const t2 = *k;
SASSERT(t1->get_decl() == fd);
SASSERT(t2->get_decl() == fd);
SASSERT(t1->get_decl() == i->m_key);
SASSERT(t2->get_decl() == i->m_key);
if (t1 == t2) continue;
ackr(t1,t2);
}

1
src/ast/ast.cpp
View file

@ -1495,6 +1495,7 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
if (!m_family_manager.has_family(fid)) {
family_id new_fid = mk_family_id(fid_name);
(void)new_fid;
TRACE("copy_families_plugins", tout << "new target fid created: " << new_fid << " fid_name: " << fid_name << "\n";);
}
TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);

10
src/ast/rewriter/bv_trailing.cpp
View file

@ -67,9 +67,10 @@ struct bv_trailing::imp {
}
expr_ref out1(m);
expr_ref out2(m);
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min);
DEBUG_CODE(
const unsigned rm1 = remove_trailing(e1, min, out1, TRAILING_DEPTH);
const unsigned rm2 = remove_trailing(e2, min, out2, TRAILING_DEPTH);
SASSERT(rm1 == min && rm2 == min););
const bool are_eq = m.are_equal(out1, out2);
result = are_eq ? m.mk_true() : m.mk_eq(out1, out2);
return are_eq ? BR_DONE : BR_REWRITE2;
@ -122,9 +123,8 @@ struct bv_trailing::imp {
expr_ref tmp(m);
for (unsigned i = 0; i < num; ++i) {
expr * const curr = a->get_arg(i);
const unsigned crm = remove_trailing(curr, to_rm, tmp, depth - 1);
VERIFY(to_rm == remove_trailing(curr, to_rm, tmp, depth - 1));
new_args.push_back(tmp);
SASSERT(crm == to_rm);
}
result = m.mk_app(m_util.get_fid(), OP_BADD, new_args.size(), new_args.c_ptr());
return to_rm;

1
src/ast/simplifier/simplifier.cpp
View file

@ -63,6 +63,7 @@ void simplifier::operator()(expr * s, expr_ref & r, proof_ref & p) {
m_need_reset = true;
reinitialize();
expr * s_orig = s;
(void)s_orig;
expr * old_s;
expr * result;
proof * result_proof;

3
src/duality/duality_rpfp.cpp
View file

@ -2365,8 +2365,7 @@ namespace Duality {
Term CanonIneqTerm(const Term &p){
Term term,bound;
Term ps = p.simplify();
bool ok = IsCanonIneq(ps,term,bound);
assert(ok);
VERIFY(IsCanonIneq(ps,term,bound));
return term - bound;
}

4
src/math/euclid/euclidean_solver.cpp
View file

@ -580,8 +580,8 @@ struct euclidean_solver::imp {
void substitute_most_recent_solution(var x) {
SASSERT(!m_solution.empty());
equation & eq = *(m_solution.back());
TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n"; display(tout, eq); tout << "\n";);
TRACE("euclidean_solver", tout << "applying solution for x" << x << "\n";
display(tout, *(m_solution.back())); tout << "\n";);
occs & use_list = m_occs[x];
occs::iterator it = use_list.begin();
occs::iterator end = use_list.end();

7
src/math/polynomial/upolynomial.cpp
View file

@ -2759,6 +2759,7 @@ namespace upolynomial {
bool manager::refine_core(unsigned sz, numeral const * p, int sign_a, mpbq_manager & bqm, mpbq & a, mpbq & b) {
SASSERT(sign_a == eval_sign_at(sz, p, a));
int sign_b = -sign_a;
(void)sign_b;
SASSERT(sign_b == eval_sign_at(sz, p, b));
SASSERT(sign_a == -sign_b);
SASSERT(sign_a != 0 && sign_b != 0);
@ -2810,9 +2811,8 @@ namespace upolynomial {
bool manager::refine(unsigned sz, numeral const * p, mpbq_manager & bqm, mpbq & a, mpbq & b, unsigned prec_k) {
int sign_a = eval_sign_at(sz, p, a);
int sign_b = -sign_a;
SASSERT(eval_sign_at(sz, p, b) == sign_b);
SASSERT(sign_a != 0 && sign_b != 0);
SASSERT(eval_sign_at(sz, p, b) == -sign_a);
SASSERT(sign_a != 0);
return refine_core(sz, p, sign_a, bqm, a, b, prec_k);
}
@ -2928,6 +2928,7 @@ namespace upolynomial {
SASSERT(sign_a == eval_sign_at(sz, p, a));
}
int sign_b = -sign_a;
(void) sign_b;
SASSERT(sign_b == eval_sign_at(sz, p, b));
SASSERT(sign_a != 0 && sign_b != 0);
if (has_zero_roots(sz, p)) {

6
src/math/polynomial/upolynomial_factorization.cpp
View file

@ -371,9 +371,10 @@ void zp_square_free_factor(zp_manager & upm, numeral_vector const & f, zp_factor
bool zp_factor(zp_manager & upm, numeral_vector const & f, zp_factors & factors) {
unsigned p = get_p_from_manager(upm.m());
TRACE("polynomial::factorization", tout << "polynomial::factor("; upm.display(tout, f); tout << ") over Z_" << p << endl;);
TRACE("polynomial::factorization",
unsigned p = get_p_from_manager(upm.m());
tout << "polynomial::factor("; upm.display(tout, f); tout << ") over Z_" << p << endl;);
// get the sq-free parts (all of them will be monic)
zp_factors sq_free_factors(upm);
@ -435,6 +436,7 @@ bool zp_factor_square_free_berlekamp(zp_manager & upm, numeral_vector const & f,
// process the null space vectors (skip first one, it's [1, 0, ..., 0]) while generating the factors
unsigned d = upm.degree(f);
(void)d;
scoped_numeral_vector v_k(zpm);
while (Q_I.next_null_space_vector(v_k)) {

1
src/math/simplex/simplex_def.h
View file

@ -998,6 +998,7 @@ namespace simplex {
template<typename Ext>
bool simplex<Ext>::well_formed_row(row const& r) const {
var_t s = m_row2base[r.id()];
(void)s;
SASSERT(m_vars[s].m_base2row == r.id());
SASSERT(m_vars[s].m_is_base);
// SASSERT(m.is_neg(m_vars[s].m_base_coeff));

13
src/math/simplex/sparse_matrix_def.h
View file

@ -509,12 +509,13 @@ namespace simplex {
dead.insert(i);
continue;
}
SASSERT(!vars.contains(e.m_var));
SASSERT(!m.is_zero(e.m_coeff));
SASSERT(e.m_var != dead_id);
col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx];
SASSERT((unsigned)c.m_row_id == row_id);
SASSERT((unsigned)c.m_row_idx == i);
DEBUG_CODE(
SASSERT(!vars.contains(e.m_var));
SASSERT(!m.is_zero(e.m_coeff));
SASSERT(e.m_var != dead_id);
col_entry const& c = m_columns[e.m_var].m_entries[e.m_col_idx];
SASSERT((unsigned)c.m_row_id == row_id);
SASSERT((unsigned)c.m_row_idx == i););
vars.insert(e.m_var);
}
int idx = r.m_first_free_idx;

1
src/muz/pdr/pdr_farkas_learner.cpp
View file

@ -923,6 +923,7 @@ namespace pdr {
if (p->get_decl_kind() == PR_ASSERTED &&
bs.contains(m.get_fact(p))) {
expr* fact = m.get_fact(p);
(void)p0;
TRACE("farkas_learner",
tout << mk_ll_pp(p0,m) << "\n";
tout << "Add: " << mk_pp(p,m) << "\n";);

3
src/muz/rel/dl_external_relation.cpp
View file

@ -338,9 +338,8 @@ namespace datalog {
: m_plugin(p),
m_condition(condition, p.get_ast_manager()),
m_filter_fn(p.get_ast_manager()) {
ast_manager& m = p.get_ast_manager();
p.mk_filter_fn(relation_sort, condition, m_filter_fn);
SASSERT(m.is_bool(condition));
SASSERT(p.get_ast_manager().is_bool(condition));
}
virtual void operator()(relation_base & r) {

9
src/muz/rel/dl_finite_product_relation.cpp
View file

@ -1566,13 +1566,12 @@ namespace datalog {
return;
}
finite_product_relation_plugin & plugin = r.get_plugin();
if(!m_neg_intersection_join) {
}
scoped_rel<finite_product_relation> intersection = get((*m_neg_intersection_join)(r, neg));
SASSERT(&intersection->get_plugin()==&plugin); //the result of join is also finite product
SASSERT(r.get_signature()==intersection->get_signature());
DEBUG_CODE(
finite_product_relation_plugin & plugin = r.get_plugin();
SASSERT(&intersection->get_plugin()==&plugin); //the result of join is also finite product
SASSERT(r.get_signature()==intersection->get_signature()););
table_base & r_table = r.get_table();
table_plugin & tplugin = r_table.get_plugin();
relation_manager & rmgr = r.get_manager();

3
src/muz/rel/udoc_relation.cpp
View file

@ -404,7 +404,7 @@ namespace datalog {
rename_fn(udoc_relation const& t, unsigned cycle_len, const unsigned * cycle)
: convenient_relation_rename_fn(t.get_signature(), cycle_len, cycle) {
udoc_plugin& p = t.get_plugin();
ast_manager& m = p.get_ast_manager();
relation_signature const& sig1 = t.get_signature();
relation_signature const& sig2 = get_result_signature();
unsigned_vector permutation0, column_info;
@ -429,6 +429,7 @@ namespace datalog {
SASSERT(column == t.get_num_bits());
TRACE("doc",
ast_manager& m = p.get_ast_manager();
sig1.output(m, tout << "sig1: "); tout << "\n";
sig2.output(m, tout << "sig2: "); tout << "\n";
tout << "permute: ";

3
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -70,13 +70,12 @@ namespace datalog {
func_interp* f = model->get_func_interp(p);
if (!f) continue;
expr_ref body(m);
unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity();
TRACE("dl",
model_v2_pp(tout, *model);
tout << mk_pp(p, m) << "\n";
tout << mk_pp(q, m) << "\n";);
SASSERT(0 < arity_p);
SASSERT(0 < p->get_arity());
SASSERT(f);
model->register_decl(p, f->copy());
func_interp* g = alloc(func_interp, m, arity_q);

3
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -71,9 +71,8 @@ namespace datalog {
svector<bool> const& is_bound = m_bound[i];
func_interp* f = old_model->get_func_interp(p);
expr_ref body(m);
unsigned arity_p = p->get_arity();
unsigned arity_q = q->get_arity();
SASSERT(0 < arity_p);
SASSERT(0 < p->get_arity());
func_interp* g = alloc(func_interp, m, arity_q);
if (f) {

3
src/nlsat/nlsat_explain.cpp
View file

@ -1165,8 +1165,7 @@ namespace nlsat {
if (max_var(new_lit) < max) {
// The conflicting core may have redundant literals.
// We should check whether new_lit is true in the current model, and discard it if that is the case
lbool val = m_solver.value(new_lit);
SASSERT(val != l_undef);
VERIFY(m_solver.value(new_lit) != l_undef);
if (m_solver.value(new_lit) == l_false)
add_literal(new_lit);
new_lit = true_literal;

16
src/nlsat/nlsat_interval_set.cpp
View file

@ -102,14 +102,14 @@ namespace nlsat {
// Check if the intervals are valid, ordered, and are disjoint.
bool check_interval_set(anum_manager & am, unsigned sz, interval const * ints) {
for (unsigned i = 0; i < sz; i++) {
interval const & curr = ints[i];
SASSERT(check_interval(am, curr));
if (i < sz - 1) {
interval const & next = ints[i+1];
SASSERT(check_no_overlap(am, curr, next));
}
}
DEBUG_CODE(
for (unsigned i = 0; i < sz; i++) {
interval const & curr = ints[i];
SASSERT(check_interval(am, curr));
if (i < sz - 1) {
SASSERT(check_no_overlap(am, curr, ints[i+1]));
}
});
return true;
}

35
src/nlsat/nlsat_solver.cpp
View file

@ -1728,27 +1728,28 @@ namespace nlsat {
// -----------------------
bool check_watches() const {
for (var x = 0; x < num_vars(); x++) {
clause_vector const & cs = m_watches[x];
unsigned sz = cs.size();
for (unsigned i = 0; i < sz; i++) {
clause const & c = *(cs[i]);
SASSERT(max_var(c) == x);
}
}
DEBUG_CODE(
for (var x = 0; x < num_vars(); x++) {
clause_vector const & cs = m_watches[x];
unsigned sz = cs.size();
for (unsigned i = 0; i < sz; i++) {
SASSERT(max_var(*(cs[i])) == x);
}
});
return true;
}
bool check_bwatches() const {
for (bool_var b = 0; b < m_bwatches.size(); b++) {
clause_vector const & cs = m_bwatches[b];
unsigned sz = cs.size();
for (unsigned i = 0; i < sz; i++) {
clause const & c = *(cs[i]);
SASSERT(max_var(c) == null_var);
SASSERT(max_bvar(c) == b);
}
}
DEBUG_CODE(
for (bool_var b = 0; b < m_bwatches.size(); b++) {
clause_vector const & cs = m_bwatches[b];
unsigned sz = cs.size();
for (unsigned i = 0; i < sz; i++) {
clause const & c = *(cs[i]);
SASSERT(max_var(c) == null_var);
SASSERT(max_bvar(c) == b);
}
});
return true;
}

3
src/opt/hitting_sets.cpp
View file

@ -762,6 +762,7 @@ namespace opt {
}
bool invariant() {
DEBUG_CODE(
for (unsigned i = 0; i < m_fwatch.size(); ++i) {
for (unsigned j = 0; j < m_fwatch[i].size(); ++j) {
set const& S = *m_F[m_fwatch[i][j]];
@ -773,7 +774,7 @@ namespace opt {
set const& S = *m_T[m_twatch[i][j]];
SASSERT(S[0] == i || S[1] == i);
}
}
});
return true;
}

3
src/parsers/smt2/smt2parser.cpp
View file

@ -473,6 +473,7 @@ namespace smt2 {
void parse_sexpr() {
unsigned stack_pos = sexpr_stack().size();
(void)stack_pos;
unsigned num_frames = 0;
do {
unsigned line = m_scanner.get_line();
@ -631,6 +632,7 @@ namespace smt2 {
void parse_psort() {
unsigned stack_pos = psort_stack().size();
(void)stack_pos;
unsigned num_frames = 0;
do {
if (curr_is_identifier()) {
@ -693,6 +695,7 @@ namespace smt2 {
void parse_sort(char const* context) {
unsigned stack_pos = sort_stack().size();
(void)stack_pos;
unsigned num_frames = 0;
do {
if (curr_is_identifier()) {

3
src/qe/qe.cpp
View file

@ -1899,8 +1899,7 @@ namespace qe {
// The variable v is to be assigned a value in a range.
//
void constrain_assignment() {
expr* fml = m_current->fml();
SASSERT(fml);
SASSERT(m_current->fml());
rational k;
app* x;
if (!find_min_weight(x, k)) {

21
src/qe/qe_arith_plugin.cpp
View file

@ -1153,21 +1153,20 @@ namespace qe {
bool get_bound(contains_app& contains_x, app* a) {
ast_manager& m = m_util.get_manager();
app* x = contains_x.x();
if (m_mark.is_marked(a) ||
bool has_bound =
m_mark.is_marked(a) ||
get_le_bound(contains_x, a) ||
get_lt_bound(contains_x, a) ||
get_divides(contains_x, a) ||
get_nested_divs(contains_x, a)) {
TRACE("qe_verbose", tout << "Bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";);
get_nested_divs(contains_x, a);
if (has_bound) {
m_mark.mark(a, true);
return true;
}
else {
TRACE("qe", tout << "No bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";);
return false;
}
TRACE("qe_verbose",
ast_manager& m = m_util.get_manager();
app* x = contains_x.x();
tout << has_bound << " bound for " << mk_pp(x, m) << " within " << mk_pp(a, m) << "\n";);
return has_bound;
}
unsigned lt_size() { return m_lt_terms.size(); }
@ -2323,7 +2322,6 @@ public:
unsigned sz = bounds.size(is_strict, !is_lower);
bool is_strict_real = !is_eq_ctx && m_util.is_real(x) && !is_strict_ctx;
bool strict_resolve = is_strict || is_strict_ctx || is_strict_real;
app* atm = bounds.atoms(is_strict_ctx, is_lower)[index];
for (unsigned i = 0; i < sz; ++i) {
app* e = bounds.atoms(is_strict, !is_lower)[i];
@ -2341,6 +2339,7 @@ public:
m_ctx.add_constraint(true, mk_not(e), tmp);
TRACE("qe_verbose",
app* atm = bounds.atoms(is_strict_ctx, is_lower)[index];
tout << mk_pp(atm, m) << " ";
tout << mk_pp(e, m) << " ==>\n";
tout << mk_pp(tmp, m) << "\n";

3
src/qe/qe_sat_tactic.cpp
View file

@ -603,8 +603,7 @@ namespace qe {
m_solver.assert_expr(m.mk_iff(proxies.back(), m_assignments[i].get()));
TRACE("qe", tout << "assignment: " << mk_pp(m_assignments[i].get(), m) << "\n";);
}
lbool is_sat = m_solver.check(proxies.size(), proxies.c_ptr());
SASSERT(is_sat == l_false);
VERIFY(l_false == m_solver.check(proxies.size(), proxies.c_ptr()));
unsigned core_size = m_solver.get_unsat_core_size();
for (unsigned i = 0; i < core_size; ++i) {
core.push_back(proxy_map.find(m_solver.get_unsat_core_expr(i)));

6
src/sat/sat_integrity_checker.cpp
View file

@ -40,8 +40,7 @@ namespace sat {
if (it->is_clause()) {
if (it->get_clause_offset() == cls_off) {
// the blocked literal must be in the clause.
literal l = it->get_blocked_literal();
SASSERT(c.contains(l));
SASSERT(c.contains(it->get_blocked_literal()));
return true;
}
}
@ -154,6 +153,7 @@ namespace sat {
}
bool integrity_checker::check_watches() const {
DEBUG_CODE(
vector<watch_list>::const_iterator it = s.m_watches.begin();
vector<watch_list>::const_iterator end = s.m_watches.end();
for (unsigned l_idx = 0; it != end; ++it, ++l_idx) {
@ -193,7 +193,7 @@ namespace sat {
break;
}
}
}
});
return true;
}

91
src/sat/sat_sls.cpp
View file

@ -269,35 +269,36 @@ namespace sat {
}
void sls::check_invariant() {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
bool is_sat = c.satisfied_by(m_model);
SASSERT(is_sat != m_false.contains(i));
SASSERT(is_sat == (m_num_true[i] > 0));
}
DEBUG_CODE(
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
bool is_sat = c.satisfied_by(m_model);
SASSERT(is_sat != m_false.contains(i));
SASSERT(is_sat == (m_num_true[i] > 0));
});
}
void sls::check_use_list() {
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
for (unsigned j = 0; j < c.size(); ++j) {
unsigned idx = c[j].index();
SASSERT(m_use_list[idx].contains(i));
}
}
for (unsigned i = 0; i < m_use_list.size(); ++i) {
literal lit = to_literal(i);
for (unsigned j = 0; j < m_use_list[i].size(); ++j) {
clause const& c = *m_clauses[m_use_list[i][j]];
bool found = false;
for (unsigned k = 0; !found && k < c.size(); ++k) {
found = c[k] == lit;
DEBUG_CODE(
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const& c = *m_clauses[i];
for (unsigned j = 0; j < c.size(); ++j) {
unsigned idx = c[j].index();
SASSERT(m_use_list[idx].contains(i));
}
SASSERT(found);
}
}
for (unsigned i = 0; i < m_use_list.size(); ++i) {
literal lit = to_literal(i);
for (unsigned j = 0; j < m_use_list[i].size(); ++j) {
clause const& c = *m_clauses[m_use_list[i][j]];
bool found = false;
for (unsigned k = 0; !found && k < c.size(); ++k) {
found = c[k] == lit;
}
SASSERT(found);
}
});
}
void sls::display(std::ostream& out) const {
@ -556,8 +557,7 @@ namespace sat {
void wsls::recompute_hscores(literal lit) {
SASSERT(value_at(lit, m_model) == l_true);
bool_var v = lit.var();
TRACE("sat", tout << v << " := " << m_hscore[v] << "\n";);
TRACE("sat", tout << lit.var() << " := " << m_hscore[lit.var()] << "\n";);
unsigned_vector const& use1 = get_use(lit);
unsigned sz = use1.size();
for (unsigned i = 0; i < sz; ++i) {
@ -647,28 +647,29 @@ namespace sat {
// The hscore is the reward for flipping the truth value of variable v.
// hscore(v) = Sum weight(c) for num_true(c) = 0 and v in c
// - Sum weight(c) for num_true(c) = 1 and (v in c, M(v) or !v in c and !M(v))
for (unsigned v = 0; v < s.num_vars(); ++v) {
int hs = compute_hscore(v);
CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n"););
SASSERT(m_hscore[v] == hs);
}
DEBUG_CODE(
for (unsigned v = 0; v < s.num_vars(); ++v) {
int hs = compute_hscore(v);
CTRACE("sat", hs != m_hscore[v], display(tout << v << " - computed: " << hs << " - assigned: " << m_hscore[v] << "\n"););
SASSERT(m_hscore[v] == hs);
}
// The score(v) is the reward on soft clauses for flipping v.
for (unsigned j = 0; j < m_soft.size(); ++j) {
unsigned v = m_soft[j].var();
double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j];
SASSERT(m_sscore[v] == ss);
}
// The score(v) is the reward on soft clauses for flipping v.
for (unsigned j = 0; j < m_soft.size(); ++j) {
unsigned v = m_soft[j].var();
double ss = (l_true == value_at(m_soft[j], m_model))?(-m_weights[j]):m_weights[j];
SASSERT(m_sscore[v] == ss);
}
// m_H are values such that m_hscore > 0 and sscore = 0.
for (bool_var v = 0; v < m_hscore.size(); ++v) {
SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v));
}
// m_H are values such that m_hscore > 0 and sscore = 0.
for (bool_var v = 0; v < m_hscore.size(); ++v) {
SASSERT((m_hscore[v] > 0 && !m_tabu[v] && m_sscore[v] == 0) == m_H.contains(v));
}
// m_S are values such that hscore = 0, sscore > 0
for (bool_var v = 0; v < m_sscore.size(); ++v) {
SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v));
}
// m_S are values such that hscore = 0, sscore > 0
for (bool_var v = 0; v < m_sscore.size(); ++v) {
SASSERT((m_hscore[v] == 0 && m_sscore[v] > 0 && !m_tabu[v]) == m_S.contains(v));
});
}
void wsls::display(std::ostream& out) const {

8
src/sat/sat_solver.cpp
View file

@ -80,8 +80,7 @@ namespace sat {
SASSERT(!src.was_eliminated(v));
bool ext = src.m_external[v] != 0;
bool dvar = src.m_decision[v] != 0;
bool_var new_v = mk_var(ext, dvar);
SASSERT(v == new_v);
VERIFY(v == mk_var(ext, dvar));
}
}
{
@ -407,9 +406,8 @@ namespace sat {
unsigned num_lits = cls.size();
for (unsigned i = 1; i < num_lits; i++) {
literal l = cls[i];
lbool val = value(l);
CTRACE("sat", val != l_false, tout << l << ":=" << val;);
SASSERT(val == l_false);
CTRACE("sat", value(l) != l_false, tout << l << ":=" << value(l););
SASSERT(value(l) == l_false);
if (max_false_idx == UINT_MAX || lvl(l) > lvl(cls[max_false_idx]))
max_false_idx = i;
}

5
src/smt/smt_conflict_resolution.cpp
View file

@ -99,9 +99,10 @@ namespace smt {
This method may update m_antecedents, m_todo_js and m_todo_eqs.
*/
void conflict_resolution::eq_justification2literals(enode * lhs, enode * rhs, eq_justification js) {
ast_manager& m = get_manager();
SASSERT(m_antecedents);
TRACE("conflict_detail", tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
TRACE("conflict_detail",
ast_manager& m = get_manager();
tout << mk_pp(lhs->get_owner(), m) << " = " << mk_pp(rhs->get_owner(), m);
switch (js.get_kind()) {
case eq_justification::AXIOM: tout << " axiom\n"; break;
case eq_justification::EQUATION:

10
src/smt/smt_context.cpp
View file

@ -2259,6 +2259,7 @@ namespace smt {
}
unsigned ilvl = 0;
(void)ilvl;
for (unsigned j = 0; j < num; j++) {
expr * atom = cls->get_atom(j);
bool sign = cls->get_atom_sign(j);
@ -2855,8 +2856,7 @@ namespace smt {
propagate();
if (was_consistent && inconsistent()) {
// logical context became inconsistent during user PUSH
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
}
push_scope();
m_base_scopes.push_back(base_scope());
@ -3110,8 +3110,7 @@ namespace smt {
else {
TRACE("after_internalization", display(tout););
if (inconsistent()) {
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
r = l_false;
}
else {
@ -3197,8 +3196,7 @@ namespace smt {
init_assumptions(num_assumptions, assumptions);
TRACE("after_internalization", display(tout););
if (inconsistent()) {
bool res = resolve_conflict(); // build the proof
SASSERT(!res);
VERIFY(!resolve_conflict()); // build the proof
mk_unsat_core();
r = l_false;
}

2
src/smt/theory_arith_aux.h
View file

@ -1784,7 +1784,7 @@ namespace smt {
template<typename Ext>
typename theory_arith<Ext>::max_min_t theory_arith<Ext>::max_min(theory_var v, bool max, bool maintain_integrality, bool& has_shared) {
expr* e = get_enode(v)->get_owner();
(void)e;
SASSERT(!maintain_integrality || valid_assignment());
SASSERT(satisfy_bounds());
SASSERT(!is_quasi_base(v));

3
src/smt/theory_array.cpp
View file

@ -75,8 +75,7 @@ namespace smt {
ast_manager& m = get_manager();
context& ctx = get_context();
theory_var r = theory_array_base::mk_var(n);
theory_var r2 = m_find.mk_var();
SASSERT(r == r2);
VERIFY(r == m_find.mk_var());
SASSERT(r == static_cast<int>(m_var_data.size()));
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];

9
src/smt/theory_bv.cpp
View file

@ -457,8 +457,7 @@ namespace smt {
void theory_bv::fixed_var_eh(theory_var v) {
numeral val;
bool r = get_fixed_value(v, val);
SASSERT(r);
VERIFY(get_fixed_value(v, val));
unsigned sz = get_bv_size(v);
value_sort_pair key(val, sz);
theory_var v2;
@ -554,9 +553,8 @@ namespace smt {
void theory_bv::internalize_bv2int(app* n) {
SASSERT(!get_context().e_internalized(n));
ast_manager & m = get_manager();
context& ctx = get_context();
TRACE("bv", tout << mk_bounded_pp(n, m) << "\n";);
TRACE("bv", tout << mk_bounded_pp(n, get_manager()) << "\n";);
process_args(n);
mk_enode(n);
if (!ctx.relevancy()) {
@ -1142,9 +1140,8 @@ namespace smt {
}
void theory_bv::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
atom * a = get_bv2a(v);
TRACE("bv", tout << "assert: v" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
TRACE("bv", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";);
if (a->is_bit()) {
// The following optimization is not correct.
// Boolean variables created for performing bit-blasting are reused.

3
src/smt/theory_datatype.cpp
View file

@ -198,8 +198,7 @@ namespace smt {
theory_var theory_datatype::mk_var(enode * n) {
theory_var r = theory::mk_var(n);
theory_var r2 = m_find.mk_var();
SASSERT(r == r2);
VERIFY(r == m_find.mk_var());
SASSERT(r == static_cast<int>(m_var_data.size()));
m_var_data.push_back(alloc(var_data));
var_data * d = m_var_data[r];

33
src/smt/theory_diff_logic_def.h
View file

@ -273,8 +273,7 @@ bool theory_diff_logic<Ext>::internalize_atom(app * n, bool gate_ctx) {
template<typename Ext>
void theory_diff_logic<Ext>::internalize_eq_eh(app * atom, bool_var v) {
context & ctx = get_context();
ast_manager& m = get_manager();
TRACE("arith", tout << mk_pp(atom, m) << "\n";);
TRACE("arith", tout << mk_pp(atom, get_manager()) << "\n";);
app * lhs = to_app(atom->get_arg(0));
app * rhs = to_app(atom->get_arg(1));
app * s;
@ -606,7 +605,6 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
atom* a = 0;
m_bool_var2atom.find(bv, a);
SASSERT(a);
edge_id e_id = a->get_pos();
literal_vector lits;
for (unsigned i = 0; i < num_edges; ++i) {
@ -616,7 +614,7 @@ void theory_diff_logic<Ext>::new_edge(dl_var src, dl_var dst, unsigned num_edges
TRACE("dl_activity",
tout << mk_pp(le, get_manager()) << "\n";
tout << "edge: " << e_id << "\n";
tout << "edge: " << a->get_pos() << "\n";
ctx.display_literals_verbose(tout, lits.size(), lits.c_ptr());
tout << "\n";
);
@ -927,18 +925,19 @@ void theory_diff_logic<Ext>::display(std::ostream & out) const {
template<typename Ext>
bool theory_diff_logic<Ext>::is_consistent() const {
context& ctx = get_context();
for (unsigned i = 0; i < m_atoms.size(); ++i) {
atom* a = m_atoms[i];
bool_var bv = a->get_bool_var();
lbool asgn = ctx.get_assignment(bv);
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
SASSERT((asgn == l_true) == a->is_true());
int edge_id = a->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
}
}
DEBUG_CODE(
context& ctx = get_context();
for (unsigned i = 0; i < m_atoms.size(); ++i) {
atom* a = m_atoms[i];
bool_var bv = a->get_bool_var();
lbool asgn = ctx.get_assignment(bv);
if (ctx.is_relevant(ctx.bool_var2expr(bv)) && asgn != l_undef) {
SASSERT((asgn == l_true) == a->is_true());
int edge_id = a->get_asserted_edge();
SASSERT(m_graph.is_enabled(edge_id));
SASSERT(m_graph.is_feasible(edge_id));
}
});
return m_graph.is_feasible();
}
@ -1194,9 +1193,9 @@ theory_diff_logic<Ext>::maximize(theory_var v, expr_ref& blocker, bool& has_shar
ast_manager& m = get_manager();
update_simplex(S);
objective_term const& objective = m_objectives[v];
TRACE("arith",
objective_term const& objective = m_objectives[v];
for (unsigned i = 0; i < objective.size(); ++i) {
tout << "Coefficient " << objective[i].second
<< " of theory_var " << objective[i].first << "\n";

19
src/smt/theory_fpa.cpp
View file

@ -52,9 +52,8 @@ namespace smt {
expr_ref bv(m);
bv = m_th.wrap(m.mk_const(f));
unsigned bv_sz = m_th.m_bv_util.get_bv_size(bv);
unsigned ebits = m_th.m_fpa_util.get_ebits(s);
unsigned sbits = m_th.m_fpa_util.get_sbits(s);
SASSERT(bv_sz == ebits + sbits);
SASSERT(bv_sz == m_th.m_fpa_util.get_ebits(s) + sbits);
m_th.m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),
@ -231,10 +230,11 @@ namespace smt {
}
app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
ast_manager & m = m_th.get_manager();
TRACE("t_fpa_detail", for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
TRACE("t_fpa_detail",
ast_manager & m = m_th.get_manager();
for (unsigned i = 0; i < values.size(); i++)
tout << "value[" << i << "] = " << mk_ismt2_pp(values[i], m) << std::endl;);
mpf_manager & mpfm = m_fu.fm();
unsynch_mpz_manager & mpzm = mpfm.mpz_manager();
@ -254,8 +254,7 @@ namespace smt {
rational all_r(0);
scoped_mpz all_z(mpzm);
bool r = m_bu.is_numeral(values[0], all_r, bv_sz);
SASSERT(r);
VERIFY(m_bu.is_numeral(values[0], all_r, bv_sz));
SASSERT(bv_sz == (m_ebits + m_sbits));
SASSERT(all_r.is_int());
mpzm.set(all_z, all_r.to_mpq().numerator());
@ -316,8 +315,7 @@ namespace smt {
unsigned bv_sz;
rational val(0);
bool r = m_bu.is_numeral(values[0], val, bv_sz);
SASSERT(r);
VERIFY(m_bu.is_numeral(values[0], val, bv_sz));
SASSERT(bv_sz == 3);
switch (val.get_uint64())
@ -422,9 +420,8 @@ namespace smt {
expr_ref bv(m);
bv = wrap(e_conv);
unsigned bv_sz = m_bv_util.get_bv_size(bv);
unsigned ebits = m_fpa_util.get_ebits(m.get_sort(e_conv));
unsigned sbits = m_fpa_util.get_sbits(m.get_sort(e_conv));
SASSERT(bv_sz == ebits + sbits);
SASSERT(bv_sz == m_fpa_util.get_ebits(m.get_sort(e_conv)) + sbits);
m_converter.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv),
m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv),
m_bv_util.mk_extract(sbits - 2, 0, bv),

2
src/smt/theory_wmaxsat.cpp
View file

@ -260,7 +260,6 @@ void theory_wmaxsat::block() {
return;
}
++m_stats.m_num_blocks;
ast_manager& m = get_manager();
context& ctx = get_context();
literal_vector lits;
compare_cost compare_cost(*this);
@ -274,6 +273,7 @@ void theory_wmaxsat::block() {
lits.push_back(~literal(m_var2bool[costs[i]]));
}
TRACE("opt",
ast_manager& m = get_manager();
tout << "block: ";
for (unsigned i = 0; i < lits.size(); ++i) {
expr_ref tmp(m);

4
src/util/mpf.cpp
View file

@ -1092,6 +1092,7 @@ void mpf_manager::round_to_integral(mpf_rounding_mode rm, mpf const & x, mpf & o
bool tie = m_mpz_manager.eq(rem, shiftm1_p);
bool less_than_tie = m_mpz_manager.lt(rem, shiftm1_p);
bool more_than_tie = m_mpz_manager.gt(rem, shiftm1_p);
(void)less_than_tie;
TRACE("mpf_dbg", tout << "tie= " << tie << "; <tie = " << less_than_tie << "; >tie = " << more_than_tie << std::endl;);
if (tie) {
if ((rm == MPF_ROUND_NEAREST_TEVEN && m_mpz_manager.is_odd(div)) ||
@ -1888,6 +1889,7 @@ void mpf_manager::round(mpf_rounding_mode rm, mpf & o) {
const mpz & p_m1 = m_powers2(o.sbits+2);
const mpz & p_m2 = m_powers2(o.sbits+3);
(void)p_m1;
TRACE("mpf_dbg", tout << "p_m1 = " << m_mpz_manager.to_string(p_m1) << std::endl <<
"p_m2 = " << m_mpz_manager.to_string(p_m2) << std::endl;);
@ -2079,7 +2081,7 @@ void mpf_manager::round_sqrt(mpf_rounding_mode rm, mpf & o) {
bool round = !m_mpz_manager.is_even(o.significand);
m_mpz_manager.machine_div2k(o.significand, 1);
bool last = !m_mpz_manager.is_even(o.significand);
(void)last;
bool inc = false;
// Specialized rounding for sqrt, as there are no negative cases (or half-way cases?)

1
src/util/mpff.cpp
View file

@ -1395,6 +1395,7 @@ unsigned mpff_manager::prev_power_of_two(mpff const & a) {
bool mpff_manager::check(mpff const & n) const {
// n is zero or the most significand bit of the most significand word is 1.
unsigned * s = sig(n);
(void)s;
SASSERT(is_zero(n) || (s[m_precision - 1] & MIN_MSW) != 0);
// if n is zero, then the sign must be 0
SASSERT(!is_zero(n) || n.m_sign == 0);