mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-22 11:07:51 +00:00
Code Activity

Merge branch 'develop' into regex-develop

Browse source 
Conflicts:
	src/smt/theory_str.h
This commit is contained in:
Murphy Berzish 2018-02-12 17:25:50 -05:00
commit 54206e3674
798 changed files with 9382 additions and 9208 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1056,7 +1056,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a;
expr* x = 0;
expr* x = nullptr;
if (m_util.is_numeral(arg, a)) {
result = m_util.mk_numeral(floor(a), true);
return BR_DONE;
@ -1303,7 +1303,7 @@ expr * arith_rewriter::mk_sin_value(rational const & k) {
expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false));
return neg ? m_util.mk_uminus(result) : result;
}
return 0;
return nullptr;
}
br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
@ -1327,7 +1327,7 @@ br_status arith_rewriter::mk_sin_core(expr * arg, expr_ref & result) {
if (is_pi_multiple(arg, k)) {
result = mk_sin_value(k);
if (result.get() != 0)
if (result.get() != nullptr)
return BR_REWRITE_FULL;
}
@ -1386,7 +1386,7 @@ br_status arith_rewriter::mk_cos_core(expr * arg, expr_ref & result) {
if (is_pi_multiple(arg, k)) {
k = k + rational(1, 2);
result = mk_sin_value(k);
if (result.get() != 0)
if (result.get() != nullptr)
return BR_REWRITE_FULL;
}
@ -1443,7 +1443,7 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) {
if (is_pi_multiple(arg, k)) {
expr_ref n(m()), d(m());
n = mk_sin_value(k);
if (n.get() == 0)
if (n.get() == nullptr)
goto end;
if (is_zero(n)) {
result = n;

2
src/ast/rewriter/bit2int.cpp
View file

@ -273,7 +273,7 @@ void bit2int::visit(app* n) {
// bv2int(x) <= z - bv2int(y) -> bv2int(x) + bv2int(y) <= z
//
expr* e1 = 0, *e2 = 0;
expr* e1 = nullptr, *e2 = nullptr;
expr_ref tmp1(m_manager), tmp2(m_manager);
expr_ref tmp3(m_manager);
expr_ref pos1(m_manager), neg1(m_manager);

2
src/ast/rewriter/bit2int.h
View file

@ -77,7 +77,7 @@ protected:
bool mk_add(expr* e1, expr* e2, expr_ref& result);
expr * get_cached(expr * n) const;
bool is_cached(expr * n) const { return get_cached(n) != 0; }
bool is_cached(expr * n) const { return get_cached(n) != nullptr; }
void cache_result(expr * n, expr * r);
void reset_cache() { m_cache.reset(); }
void flush_cache() { m_cache.cleanup(); }

10
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
View file

@ -200,7 +200,7 @@ struct blaster_rewriter_cfg : public default_rewriter_cfg {
sort * b = m().mk_bool_sort();
m_out.reset();
for (unsigned i = 0; i < bv_size; i++) {
m_out.push_back(m().mk_fresh_const(0, b));
m_out.push_back(m().mk_fresh_const(nullptr, b));
}
r = mk_mkbv(m_out);
m_const2bits.insert(f, r);
@ -342,11 +342,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
bits.push_back(m().mk_app(butil().get_family_id(), OP_BIT2BOOL, 1, &p, 1, &t));
}
result = mk_mkbv(bits);
result_pr = 0;
result_pr = nullptr;
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
result_pr = nullptr;
TRACE("bit_blaster", tout << f->get_name() << " ";
for (unsigned i = 0; i < num; ++i) tout << mk_pp(args[i], m()) << " ";
tout << "\n";);
@ -569,7 +569,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
if (t->get_idx() >= m_bindings.size())
return false;
result = m_bindings.get(m_bindings.size() - t->get_idx() - 1);
result_pr = 0;
result_pr = nullptr;
return true;
}
@ -616,7 +616,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend);
result = m().mk_quantifier(old_q->is_forall(), new_decl_sorts.size(), new_decl_sorts.c_ptr(), new_decl_names.c_ptr(),
new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(),
old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
result_pr = nullptr;
m_bindings.shrink(old_sz);
return true;
}

2
src/ast/rewriter/bool_rewriter.cpp
View file

@ -585,7 +585,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
*/
br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
expr* cond = 0, *t = 0, *e = 0;
expr* cond = nullptr, *t = nullptr, *e = nullptr;
VERIFY(m().is_ite(ite, cond, t, e));
SASSERT(m().is_value(val));

2
src/ast/rewriter/bool_rewriter.h
View file

@ -183,7 +183,7 @@ struct bool_rewriter_cfg : public default_rewriter_cfg {
bool flat_assoc(func_decl * f) const { return m_r.flat() && (m_r.m().is_and(f) || m_r.m().is_or(f)); }
bool rewrite_patterns() const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
result_pr = nullptr;
if (f->get_family_id() != m_r.get_fid())
return BR_FAILED;
return m_r.mk_app_core(f, num, args, result);

22
src/ast/rewriter/bv_bounds.cpp
View file

@ -200,7 +200,7 @@ bv_bounds::conv_res bv_bounds::convert(expr * e, vector<ninterval>& nis, bool ne
}
// v + c1 <= v + c2
app * v1(NULL), *v2(NULL);
app * v1(nullptr), *v2(nullptr);
numeral val1, val2;
if (is_constant_add(bv_sz, lhs, v1, val1)
&& is_constant_add(bv_sz, rhs, v2, val2)
@ -412,7 +412,7 @@ bool bv_bounds::add_constraint(expr* e) {
}
// v + c1 <= v + c2
app * v1(NULL), *v2(NULL);
app * v1(nullptr), *v2(nullptr);
numeral val1, val2;
if (is_constant_add(bv_sz, lhs, v1, val1)
&& is_constant_add(bv_sz, rhs, v2, val2)
@ -449,7 +449,7 @@ bool bv_bounds::add_constraint(expr* e) {
return m_okay;
}
bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) {
bool bv_bounds::add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate) {
TRACE("bv_bounds", tout << "bound_unsigned " << mk_ismt2_pp(v, m_m) << ": " << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;);
const unsigned bv_sz = m_bv_util.get_bv_size(v);
const numeral& zero = numeral::zero();
@ -472,7 +472,7 @@ bool bv_bounds::add_bound_unsigned(app * v, numeral a, numeral b, bool negate) {
}
}
bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, bool negate, vector<ninterval>& nis) {
bv_bounds::conv_res bv_bounds::convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis) {
TRACE("bv_bounds", tout << "convert_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~[" : "[") << a << ";" << b << "]" << std::endl;);
const unsigned bv_sz = m_bv_util.get_bv_size(v);
SASSERT(a <= b);
@ -496,7 +496,7 @@ bv_bounds::conv_res bv_bounds::convert_signed(app * v, numeral a, numeral b, boo
}
}
bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) {
bool bv_bounds::add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate) {
TRACE("bv_bounds", tout << "bound_signed " << mk_ismt2_pp(v, m_m) << ":" << (negate ? "~" : " ") << a << ";" << b << std::endl;);
const unsigned bv_sz = m_bv_util.get_bv_size(v);
SASSERT(a <= b);
@ -519,7 +519,7 @@ bool bv_bounds::add_bound_signed(app * v, numeral a, numeral b, bool negate) {
}
}
bool bv_bounds::bound_lo(app * v, numeral l) {
bool bv_bounds::bound_lo(app * v, const numeral& l) {
SASSERT(in_range(v, l));
TRACE("bv_bounds", tout << "lower " << mk_ismt2_pp(v, m_m) << ":" << l << std::endl;);
// l <= v
@ -530,7 +530,7 @@ bool bv_bounds::bound_lo(app * v, numeral l) {
return m_okay;
}
bool bv_bounds::bound_up(app * v, numeral u) {
bool bv_bounds::bound_up(app * v, const numeral& u) {
SASSERT(in_range(v, u));
TRACE("bv_bounds", tout << "upper " << mk_ismt2_pp(v, m_m) << ":" << u << std::endl;);
// v <= u
@ -541,7 +541,7 @@ bool bv_bounds::bound_up(app * v, numeral u) {
return m_okay;
}
bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) {
bool bv_bounds::add_neg_bound(app * v, const numeral& a, const numeral& b) {
TRACE("bv_bounds", tout << "negative bound " << mk_ismt2_pp(v, m_m) << ":" << a << ";" << b << std::endl;);
bv_bounds::interval negative_interval(a, b);
SASSERT(m_bv_util.is_bv(v));
@ -550,8 +550,8 @@ bool bv_bounds::add_neg_bound(app * v, numeral a, numeral b) {
SASSERT(a <= b);
intervals_map::obj_map_entry * const e = m_negative_intervals.find_core(v);
intervals * ivs(NULL);
if (e == 0) {
intervals * ivs(nullptr);
if (e == nullptr) {
ivs = alloc(intervals);
m_negative_intervals.insert(v, ivs);
}
@ -621,7 +621,7 @@ bool bv_bounds::is_sat_core(app * v) {
if (!has_lower) lower = numeral::zero();
if (!has_upper) upper = (numeral::power_of_two(bv_sz) - one);
TRACE("bv_bounds", tout << "is_sat bound:" << lower << "-" << upper << std::endl;);
intervals * negative_intervals(NULL);
intervals * negative_intervals(nullptr);
const bool has_neg_intervals = m_negative_intervals.find(v, negative_intervals);
bool is_sat(false);
numeral new_lo = lower;

18
src/ast/rewriter/bv_bounds.h
View file

@ -49,11 +49,11 @@ public: // bounds addition methods
**/
bool add_constraint(expr* e);
bool bound_up(app * v, numeral u); // v <= u
bool bound_lo(app * v, numeral l); // l <= v
inline bool add_neg_bound(app * v, numeral a, numeral b); // not (a<=v<=b)
bool add_bound_signed(app * v, numeral a, numeral b, bool negate);
bool add_bound_unsigned(app * v, numeral a, numeral b, bool negate);
bool bound_up(app * v, const numeral& u); // v <= u
bool bound_lo(app * v, const numeral& l); // l <= v
inline bool add_neg_bound(app * v, const numeral& a, const numeral& b); // not (a<=v<=b)
bool add_bound_signed(app * v, const numeral& a, const numeral& b, bool negate);
bool add_bound_unsigned(app * v, const numeral& a, const numeral& b, bool negate);
public:
bool is_sat(); ///< Determine if the set of considered constraints is satisfiable.
bool is_okay();
@ -70,7 +70,7 @@ protected:
enum conv_res { CONVERTED, UNSAT, UNDEF };
conv_res convert(expr * e, vector<ninterval>& nis, bool negated);
conv_res record(app * v, numeral lo, numeral hi, bool negated, vector<ninterval>& nis);
conv_res convert_signed(app * v, numeral a, numeral b, bool negate, vector<ninterval>& nis);
conv_res convert_signed(app * v, const numeral& a, const numeral& b, bool negate, vector<ninterval>& nis);
typedef vector<interval> intervals;
typedef obj_map<app, intervals*> intervals_map;
@ -83,7 +83,7 @@ protected:
bool m_okay;
bool is_sat(app * v);
bool is_sat_core(app * v);
inline bool in_range(app *v, numeral l);
inline bool in_range(app *v, const numeral& l);
inline bool is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val);
void record_singleton(app * v, numeral& singleton_value);
inline bool to_bound(const expr * e) const;
@ -99,7 +99,7 @@ inline bool bv_bounds::to_bound(const expr * e) const {
&& !m_bv_util.is_numeral(e);
}
inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) {
inline bool bv_bounds::in_range(app *v, const bv_bounds::numeral& n) {
const unsigned bv_sz = m_bv_util.get_bv_size(v);
const bv_bounds::numeral zero(0);
const bv_bounds::numeral mod(rational::power_of_two(bv_sz));
@ -109,7 +109,7 @@ inline bool bv_bounds::in_range(app *v, bv_bounds::numeral n) {
inline bool bv_bounds::is_constant_add(unsigned bv_sz, expr * e, app*& v, numeral& val) {
SASSERT(e && !v);
SASSERT(m_bv_util.get_bv_size(e) == bv_sz);
expr *lhs(NULL), *rhs(NULL);
expr *lhs(nullptr), *rhs(nullptr);
if (!m_bv_util.is_bv_add(e, lhs, rhs)) {
v = to_app(e);
val = rational(0);

2
src/ast/rewriter/bv_elim.cpp
View file

@ -58,7 +58,7 @@ bool bv_elim_cfg::reduce_quantifier(quantifier * q,
_sorts.push_back(m.mk_bool_sort());
_names.push_back(symbol(new_name.str().c_str()));
}
bv = m.mk_app(bfid, OP_MKBV, 0, 0, args.size(), args.c_ptr());
bv = m.mk_app(bfid, OP_MKBV, 0, nullptr, args.size(), args.c_ptr());
_subst_map.push_back(bv.get());
}
else {

18
src/ast/rewriter/bv_rewriter.cpp
View file

@ -630,13 +630,13 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re
const bool curr_is_conc = m_util.is_concat(curr);
if (curr_is_conc && to_app(curr)->get_num_args() == 0) continue;
expr * const curr_first = curr_is_conc ? to_app(curr)->get_arg(0) : curr;
expr * new_first = NULL;
expr * new_first = nullptr;
if (is_numeral(curr_first, val, curr_first_sz)) {
SASSERT(curr_first_sz >= removable);
const unsigned new_num_sz = curr_first_sz - removable;
new_first = new_num_sz ? mk_numeral(val, new_num_sz) : NULL;
new_first = new_num_sz ? mk_numeral(val, new_num_sz) : nullptr;
}
expr * new_arg = NULL;
expr * new_arg = nullptr;
if (curr_is_conc) {
const unsigned conc_num = to_app(curr)->get_num_args();
if (new_first) {
@ -650,7 +650,7 @@ unsigned bv_rewriter::propagate_extract(unsigned high, expr * arg, expr_ref & re
expr * const * const old_conc_args = to_app(curr)->get_args();
switch (conc_num) {
case 0: UNREACHABLE(); break;
case 1: new_arg = NULL; break;
case 1: new_arg = nullptr; break;
case 2: new_arg = to_app(curr)->get_arg(1); break;
default: new_arg = m_util.mk_concat(conc_num - 1, old_conc_args + 1);
}
@ -1458,10 +1458,10 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
bool fused_extract = false;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i];
expr * prev = 0;
expr * prev = nullptr;
if (i > 0)
prev = new_args.back();
if (is_numeral(arg, v1, sz1) && prev != 0 && is_numeral(prev, v2, sz2)) {
if (is_numeral(arg, v1, sz1) && prev != nullptr && is_numeral(prev, v2, sz2)) {
v2 *= rational::power_of_two(sz1);
v2 += v1;
new_args.pop_back();
@ -1476,7 +1476,7 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re
expanded = true;
}
else if (m_util.is_extract(arg) &&
prev != 0 &&
prev != nullptr &&
m_util.is_extract(prev) &&
to_app(arg)->get_arg(0) == to_app(prev)->get_arg(0) &&
m_util.get_extract_low(prev) == m_util.get_extract_high(arg) + 1) {
@ -1814,7 +1814,7 @@ br_status bv_rewriter::mk_bv_xor(unsigned num, expr * const * args, expr_ref & r
//
if (!v1.is_zero() && num_coeffs == num - 1) {
// find argument that is not a numeral
expr * t = 0;
expr * t = nullptr;
for (unsigned i = 0; i < num; i++) {
t = args[i];
if (!is_numeral(t))
@ -1937,7 +1937,7 @@ br_status bv_rewriter::mk_bv_not(expr * arg, expr_ref & result) {
}
if (m_bvnot_simpl) {
expr *s(0), *t(0);
expr *s(nullptr), *t(nullptr);
if (m_util.is_bv_mul(arg, s, t)) {
// ~(-1 * x) --> (x - 1)
bv_size = m_util.get_bv_size(s);

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

@ -39,7 +39,7 @@ struct bv_trailing::imp {
TRACE("bv-trailing", tout << "ctor\n";);
for (unsigned i = 0; i <= TRAILING_DEPTH; ++i)
m_count_cache[i] = NULL;
m_count_cache[i] = nullptr;
}
virtual ~imp() {
@ -116,7 +116,7 @@ struct bv_trailing::imp {
const unsigned sz = m_util.get_bv_size(a);
if (to_rm == sz) {
result = NULL;
result = nullptr;
return sz;
}
@ -155,7 +155,7 @@ struct bv_trailing::imp {
const unsigned new_sz = sz - retv;
if (!new_sz) {
result = NULL;
result = nullptr;
return retv;
}
@ -181,7 +181,7 @@ struct bv_trailing::imp {
const unsigned num = a->get_num_args();
unsigned retv = 0;
unsigned i = num;
expr_ref new_last(NULL, m);
expr_ref new_last(nullptr, m);
while (i && retv < n) {
i--;
expr * const curr = a->get_arg(i);
@ -197,7 +197,7 @@ struct bv_trailing::imp {
if (!i && !new_last) {// all args eaten completely
SASSERT(retv == m_util.get_bv_size(a));
result = NULL;
result = nullptr;
return retv;
}
@ -230,7 +230,7 @@ struct bv_trailing::imp {
if (m_util.is_numeral(e, e_val, sz)) {
retv = remove_trailing(std::min(n, sz), e_val);
const unsigned new_sz = sz - retv;
result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : NULL;
result = new_sz ? (retv ? m_util.mk_numeral(e_val, new_sz) : e) : nullptr;
return retv;
}
if (m_util.is_bv_mul(e))
@ -338,7 +338,7 @@ struct bv_trailing::imp {
void cache(unsigned depth, expr * e, unsigned min, unsigned max) {
SASSERT(depth <= TRAILING_DEPTH);
if (depth == 0) return;
if (m_count_cache[depth] == NULL)
if (m_count_cache[depth] == nullptr)
m_count_cache[depth] = alloc(map);
SASSERT(!m_count_cache[depth]->contains(e));
m.inc_ref(e);
@ -353,10 +353,10 @@ struct bv_trailing::imp {
max = m_util.get_bv_size(e);
return true;
}
if (m_count_cache[depth] == NULL)
if (m_count_cache[depth] == nullptr)
return false;
const map::obj_map_entry * const oe = m_count_cache[depth]->find_core(e);
if (oe == NULL) return false;
if (oe == nullptr) return false;
min = oe->get_data().m_value.first;
max = oe->get_data().m_value.second;
TRACE("bv-trailing", tout << "cached@" << depth << ": " << mk_ismt2_pp(e, m) << '[' << m_util.get_bv_size(e) << "]\n: " << min << '-' << max << "\n";);
@ -366,7 +366,7 @@ struct bv_trailing::imp {
void reset_cache(const unsigned condition) {
SASSERT(m_count_cache[0] == NULL);
for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
if (m_count_cache[i] == NULL) continue;
if (m_count_cache[i] == nullptr) continue;
TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition << "\n";);
if (condition && m_count_cache[i]->size() < condition) continue;
TRACE("bv-trailing", tout << "reset cache " << i << "\n";);
@ -374,7 +374,7 @@ struct bv_trailing::imp {
map::iterator end = m_count_cache[i]->end();
for (; it != end; ++it) m.dec_ref(it->m_key);
dealloc(m_count_cache[i]);
m_count_cache[i] = NULL;
m_count_cache[i] = nullptr;
}
}

14
src/ast/rewriter/der.cpp
View file

@ -118,7 +118,7 @@ bool der::is_var_diseq(expr * e, unsigned num_decls, var * & v, expr_ref & t) {
void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
bool reduced = false;
pr = 0;
pr = nullptr;
r = q;
TRACE("der", tout << mk_pp(q, m_manager) << "\n";);
@ -149,14 +149,14 @@ void der::operator()(quantifier * q, expr_ref & r, proof_ref & pr) {
void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
if (!is_forall(q)) {
pr = 0;
pr = nullptr;
r = q;
return;
}
expr * e = q->get_expr();
unsigned num_decls = q->get_num_decls();
var * v = 0;
var * v = nullptr;
expr_ref t(m_manager);
if (m_manager.is_or(e)) {
@ -211,7 +211,7 @@ void der::reduce1(quantifier * q, expr_ref & r, proof_ref & pr) {
r = q;
if (m_manager.proofs_enabled()) {
pr = r == q ? 0 : m_manager.mk_der(q, r);
pr = r == q ? nullptr : m_manager.mk_der(q, r);
}
}
@ -223,7 +223,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
for (unsigned i = 0; i < definitions.size(); i++) {
var * v = vars[i];
expr * t = definitions[i];
if (t == 0 || has_quantifiers(t) || occurs(v, t))
if (t == nullptr || has_quantifiers(t) || occurs(v, t))
definitions[i] = 0;
else
found = true; // found at least one candidate
@ -260,7 +260,7 @@ void der_sort_vars(ptr_vector<var> & vars, ptr_vector<expr> & definitions, unsig
vidx = to_var(t)->get_idx();
if (fr.second == 0) {
CTRACE("der_bug", vidx >= definitions.size(), tout << "vidx: " << vidx << "\n";);
// Remark: The size of definitions may be smaller than the number of variables occuring in the quantified formula.
// Remark: The size of definitions may be smaller than the number of variables occurring in the quantified formula.
if (definitions.get(vidx, 0) != 0) {
if (visiting.is_marked(t)) {
// cycle detected: remove t
@ -342,7 +342,7 @@ void der::get_elimination_order() {
void der::create_substitution(unsigned sz) {
m_subst_map.reset();
m_subst_map.resize(sz, 0);
m_subst_map.resize(sz, nullptr);
for(unsigned i = 0; i < m_order.size(); i++) {
expr_ref cur(m_map[m_order[i]], m_manager);

2
src/ast/rewriter/distribute_forall.h
View file

@ -71,7 +71,7 @@ protected:
void reduce1_app(app * a);
expr * get_cached(expr * n) const;
bool is_cached(expr * n) const { return get_cached(n) != 0; }
bool is_cached(expr * n) const { return get_cached(n) != nullptr; }
void cache_result(expr * n, expr * r);
void reset_cache() { m_cache.reset(); }
void flush_cache() { m_cache.cleanup(); }

22
src/ast/rewriter/elim_bounds.cpp
View file

@ -44,15 +44,15 @@ elim_bounds_cfg::elim_bounds_cfg(ast_manager & m):
It also detects >=, and the atom can be negated.
*/
bool elim_bounds_cfg::is_bound(expr * n, var * & lower, var * & upper) {
upper = 0;
lower = 0;
upper = nullptr;
lower = nullptr;
bool neg = false;
if (m.is_not(n)) {
n = to_app(n)->get_arg(0);
neg = true;
}
expr* l = 0, *r = 0;
expr* l = nullptr, *r = nullptr;
bool le = false;
if (m_util.is_le(n, l, r) && m_util.is_numeral(r)) {
n = l;
@ -139,14 +139,14 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
ptr_buffer<var> candidates;
#define ADD_CANDIDATE(V) if (!lowers.contains(V) && !uppers.contains(V)) { candidate_set.insert(V); candidates.push_back(V); }
for (expr * a : atoms) {
var * lower = 0;
var * upper = 0;
var * lower = nullptr;
var * upper = nullptr;
if (is_bound(a, lower, upper)) {
if (lower != 0 && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
if (lower != nullptr && !used_vars.contains(lower->get_idx()) && lower->get_idx() < num_vars) {
ADD_CANDIDATE(lower);
lowers.insert(lower);
}
if (upper != 0 && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
if (upper != nullptr && !used_vars.contains(upper->get_idx()) && upper->get_idx() < num_vars) {
ADD_CANDIDATE(upper);
uppers.insert(upper);
}
@ -167,9 +167,9 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
unsigned j = 0;
for (unsigned i = 0; i < atoms.size(); ++i) {
expr * a = atoms[i];
var * lower = 0;
var * upper = 0;
if (is_bound(a, lower, upper) && ((lower != 0 && candidate_set.contains(lower)) || (upper != 0 && candidate_set.contains(upper))))
var * lower = nullptr;
var * upper = nullptr;
if (is_bound(a, lower, upper) && ((lower != nullptr && candidate_set.contains(lower)) || (upper != nullptr && candidate_set.contains(upper))))
continue;
atoms[j] = a;
j++;
@ -178,7 +178,7 @@ bool elim_bounds_cfg::reduce_quantifier(quantifier * q,
return false;
}
atoms.resize(j);
expr * new_body = 0;
expr * new_body = nullptr;
switch (atoms.size()) {
case 0:
result = m.mk_false();

2
src/ast/rewriter/elim_bounds.h
View file

@ -70,7 +70,7 @@ public:
m_cfg(m)
{}
virtual ~elim_bounds_rw() {}
~elim_bounds_rw() override {}
};
#endif /* ELIM_BOUNDS2_H_ */

4
src/ast/rewriter/enum2bv_rewriter.cpp
View file

@ -194,7 +194,7 @@ struct enum2bv_rewriter::imp {
q->get_weight(), q->get_qid(), q->get_skid(),
q->get_num_patterns(), new_patterns,
q->get_num_no_patterns(), new_no_patterns);
result_pr = 0;
result_pr = nullptr;
return true;
}
@ -226,7 +226,7 @@ struct enum2bv_rewriter::imp {
m_enum_bvs(m),
m_enum_defs(m),
m_num_translated(0),
m_sort_pred(0),
m_sort_pred(nullptr),
m_rw(*this, m, p) {
}

34
src/ast/rewriter/expr_replacer.cpp
View file

@ -34,7 +34,7 @@ void expr_replacer::operator()(expr * t, expr_ref & result) {
struct expr_replacer::scoped_set_subst {
expr_replacer & m_r;
scoped_set_subst(expr_replacer & r, expr_substitution & s):m_r(r) { m_r.set_substitution(&s); }
~scoped_set_subst() { m_r.set_substitution(0); }
~scoped_set_subst() { m_r.set_substitution(nullptr); }
};
void expr_replacer::apply_substitution(expr * s, expr * def, proof * def_pr, expr_ref & t) {
@ -58,14 +58,14 @@ struct default_expr_replacer_cfg : public default_rewriter_cfg {
default_expr_replacer_cfg(ast_manager & _m):
m(_m),
m_subst(0),
m_subst(nullptr),
m_used_dependencies(_m) {
}
bool get_subst(expr * s, expr * & t, proof * & pr) {
if (m_subst == 0)
if (m_subst == nullptr)
return false;
expr_dependency * d = 0;
expr_dependency * d = nullptr;
if (m_subst->find(s, t, pr, d)) {
m_used_dependencies = m.mk_join(m_used_dependencies, d);
return true;
@ -90,29 +90,29 @@ public:
m_replacer(m, m.proofs_enabled(), m_cfg) {
}
virtual ast_manager & m() const { return m_replacer.m(); }
ast_manager & m() const override { return m_replacer.m(); }
virtual void set_substitution(expr_substitution * s) {
void set_substitution(expr_substitution * s) override {
m_replacer.cleanup();
m_replacer.cfg().m_subst = s;
}
virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) {
result_dep = 0;
void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
result_dep = nullptr;
m_replacer.operator()(t, result, result_pr);
if (m_cfg.m_used_dependencies != 0) {
result_dep = m_cfg.m_used_dependencies;
m_replacer.reset(); // reset cache
m_cfg.m_used_dependencies = 0;
m_cfg.m_used_dependencies = nullptr;
}
}
virtual unsigned get_num_steps() const {
unsigned get_num_steps() const override {
return m_replacer.get_num_steps();
}
virtual void reset() {
void reset() override {
m_replacer.reset();
}
};
@ -131,23 +131,23 @@ public:
m_r(m, p) {
}
virtual ~th_rewriter2expr_replacer() {}
~th_rewriter2expr_replacer() override {}
virtual ast_manager & m() const { return m_r.m(); }
ast_manager & m() const override { return m_r.m(); }
virtual void set_substitution(expr_substitution * s) { m_r.set_substitution(s); }
void set_substitution(expr_substitution * s) override { m_r.set_substitution(s); }
virtual void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) {
void operator()(expr * t, expr_ref & result, proof_ref & result_pr, expr_dependency_ref & result_dep) override {
m_r(t, result, result_pr);
result_dep = m_r.get_used_dependencies();
m_r.reset_used_dependencies();
}
virtual unsigned get_num_steps() const {
unsigned get_num_steps() const override {
return m_r.get_num_steps();
}
virtual void reset() {
void reset() override {
m_r.reset();
}

2
src/ast/rewriter/expr_safe_replace.cpp
View file

@ -61,7 +61,7 @@ void expr_safe_replace::operator()(expr* e, expr_ref& res) {
m_args.reset();
bool arg_differs = false;
for (unsigned i = 0; i < n; ++i) {
expr* d = 0, *arg = c->get_arg(i);
expr* d = nullptr, *arg = c->get_arg(i);
if (m_cache.find(arg, d)) {
m_args.push_back(d);
arg_differs |= arg != d;

2
src/ast/rewriter/factor_rewriter.h
View file

@ -61,7 +61,7 @@ struct factor_rewriter_cfg : public default_rewriter_cfg {
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
result_pr = nullptr;
return m_r.mk_app_core(f, num, args, result);
}
factor_rewriter_cfg(ast_manager & m):m_r(m) {}

6
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -48,17 +48,17 @@ br_status fpa_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
case OP_FPA_RM_TOWARD_POSITIVE:
case OP_FPA_RM_TOWARD_NEGATIVE:
case OP_FPA_RM_TOWARD_ZERO:
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
case OP_FPA_PLUS_INF:
case OP_FPA_MINUS_INF:
case OP_FPA_NAN:
case OP_FPA_PLUS_ZERO:
case OP_FPA_MINUS_ZERO:
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
case OP_FPA_NUM:
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)0); st = BR_DONE; break;
SASSERT(num_args == 0); result = m().mk_app(f, (expr * const *)nullptr); st = BR_DONE; break;
case OP_FPA_ADD: SASSERT(num_args == 3); st = mk_add(args[0], args[1], args[2], result); break;
case OP_FPA_SUB: SASSERT(num_args == 3); st = mk_sub(args[0], args[1], args[2], result); break;

8
src/ast/rewriter/inj_axiom.cpp
View file

@ -29,9 +29,9 @@ Revision History:
*/
bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
expr * n = q->get_expr();
expr* arg1 = 0, * arg2 = 0, *narg = 0;
expr* app1 = 0, * app2 = 0;
expr* var1 = 0, * var2 = 0;
expr* arg1 = nullptr, * arg2 = nullptr, *narg = nullptr;
expr* app1 = nullptr, * app2 = nullptr;
expr* var1 = nullptr, * var2 = nullptr;
if (q->is_forall() && m.is_or(n, arg1, arg2)) {
if (m.is_not(arg2))
std::swap(arg1, arg2);
@ -84,7 +84,7 @@ bool simplify_inj_axiom(ast_manager & m, quantifier * q, expr_ref & result) {
ptr_buffer<sort> decls;
buffer<symbol> names;
expr * var = 0;
expr * var = nullptr;
for (unsigned i = 0; i < num; i++) {
expr * c = f1->get_arg(i);
if (is_var(c)) {

4
src/ast/rewriter/maximize_ac_sharing.cpp
View file

@ -35,7 +35,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
if (std::find(m_kinds.begin(), m_kinds.end(), k) == m_kinds.end())
return BR_FAILED;
ptr_buffer<expr, 128> _args;
expr * numeral = 0;
expr * numeral = nullptr;
if (is_numeral(args[0])) {
numeral = args[0];
for (unsigned i = 1; i < num_args; i++)
@ -86,7 +86,7 @@ br_status maximize_ac_sharing::reduce_app(func_decl * f, unsigned num_args, expr
}
num_args = j;
if (num_args == 1) {
if (numeral == 0) {
if (numeral == nullptr) {
result = _args[0];
}
else {

6
src/ast/rewriter/maximize_ac_sharing.h
View file

@ -45,7 +45,7 @@ class maximize_ac_sharing : public default_rewriter_cfg {
expr * m_arg1;
expr * m_arg2;
entry(func_decl * d = 0, expr * arg1 = 0, expr * arg2 = 0):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
entry(func_decl * d = nullptr, expr * arg1 = nullptr, expr * arg2 = nullptr):m_decl(d), m_arg1(arg1), m_arg2(arg2) {
SASSERT((d == 0 && arg1 == 0 && arg2 == 0) || (d != 0 && arg1 != 0 && arg2 != 0));
if (arg1->get_id() > arg2->get_id())
std::swap(m_arg1, m_arg2);
@ -103,8 +103,8 @@ public:
class maximize_bv_sharing : public maximize_ac_sharing {
bv_util m_util;
protected:
virtual void init_core();
virtual bool is_numeral(expr * n) const;
void init_core() override;
bool is_numeral(expr * n) const override;
public:
maximize_bv_sharing(ast_manager & m);
};

4
src/ast/rewriter/mk_extract_proc.cpp
View file

@ -19,8 +19,8 @@ mk_extract_proc::mk_extract_proc(bv_util & u):
m_util(u),
m_high(0),
m_low(UINT_MAX),
m_domain(0),
m_f_cached(0) {
m_domain(nullptr),
m_f_cached(nullptr) {
}
mk_extract_proc::~mk_extract_proc() {

2
src/ast/rewriter/mk_simplified_app.cpp
View file

@ -98,7 +98,7 @@ br_status mk_simplified_app::mk_core(func_decl * decl, unsigned num, expr * cons
}
void mk_simplified_app::operator()(func_decl * decl, unsigned num, expr * const * args, expr_ref & result) {
result = 0;
result = nullptr;
mk_core(decl, num, args, result);
if (!result)
result = m_imp->m.mk_app(decl, num, args);

2
src/ast/rewriter/pb2bv_rewriter.cpp
View file

@ -403,7 +403,7 @@ struct pb2bv_rewriter::imp {
bool rewrite_patterns() const { return false; }
bool flat_assoc(func_decl * f) const { return false; }
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
result_pr = nullptr;
return m_r.mk_app_core(f, num, args, result);
}
card2bv_rewriter_cfg(imp& i, ast_manager & m):m_r(i, m) {}

2
src/ast/rewriter/poly_rewriter.h
View file

@ -96,7 +96,7 @@ protected:
public:
poly_rewriter(ast_manager & m, params_ref const & p = params_ref()):
Config(m),
m_curr_sort(0),
m_curr_sort(nullptr),
m_sort_sums(false) {
updt_params(p);
SASSERT(!m_som || m_flat); // som of monomials form requires flattening to be enabled.

22
src/ast/rewriter/poly_rewriter_def.h
View file

@ -206,7 +206,7 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
numeral c(1);
unsigned num_coeffs = 0;
unsigned num_add = 0;
expr * var = 0;
expr * var = nullptr;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i];
if (is_numeral(arg, a)) {
@ -290,13 +290,13 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
if (!m_som || num_add == 0) {
ptr_buffer<expr> new_args;
expr * prev = 0;
expr * prev = nullptr;
bool ordered = true;
for (unsigned i = 0; i < num_args; i++) {
expr * curr = args[i];
if (is_numeral(curr))
continue;
if (prev != 0 && lt(curr, prev))
if (prev != nullptr && lt(curr, prev))
ordered = false;
new_args.push_back(curr);
prev = curr;
@ -532,7 +532,7 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
expr_fast_mark1 visited; // visited.is_marked(power_product) if the power_product occurs in args
expr_fast_mark2 multiple; // multiple.is_marked(power_product) if power_product occurs more than once
bool has_multiple = false;
expr * prev = 0;
expr * prev = nullptr;
bool ordered = true;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = args[i];
@ -543,7 +543,7 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
ordered = !m_sort_sums || i == 0;
}
else if (m_sort_sums && ordered) {
if (prev != 0 && lt(arg, prev))
if (prev != nullptr && lt(arg, prev))
ordered = false;
prev = arg;
}
@ -874,8 +874,8 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
const bool insert_c_rhs = c_at_rhs && (new_rhs_monomials.size() == 1 || !c.is_zero());
const unsigned lhs_offset = insert_c_lhs ? 0 : 1;
const unsigned rhs_offset = insert_c_rhs ? 0 : 1;
new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : NULL;
new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : NULL;
new_rhs_monomials[0] = insert_c_rhs ? mk_numeral(c) : nullptr;
new_lhs_monomials[0] = insert_c_lhs ? mk_numeral(c) : nullptr;
lhs_result = mk_add_app(new_lhs_monomials.size() - lhs_offset, new_lhs_monomials.c_ptr() + lhs_offset);
rhs_result = mk_add_app(new_rhs_monomials.size() - rhs_offset, new_rhs_monomials.c_ptr() + rhs_offset);
TRACE("mk_le_bug", tout << lhs_result << " " << rhs_result << "\n";);
@ -994,7 +994,7 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
return false;
ptr_buffer<expr> args;
v = 0;
v = nullptr;
expr * curr = to_app(n);
bool stop = false;
inv = false;
@ -1013,12 +1013,12 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
args.push_back(arg);
}
else if (is_var(arg)) {
if (v != 0)
if (v != nullptr)
return false; // already found variable
v = to_var(arg);
}
else if (is_times_minus_one(arg, neg_arg) && is_var(neg_arg)) {
if (v != 0)
if (v != nullptr)
return false; // already found variable
v = to_var(neg_arg);
inv = true;
@ -1027,7 +1027,7 @@ bool poly_rewriter<Config>::is_var_plus_ground(expr * n, bool & inv, var * & v,
return false; // non ground term.
}
}
if (v == 0)
if (v == nullptr)
return false; // did not find variable
SASSERT(!args.empty());
mk_add(args.size(), args.c_ptr(), t);

34
src/ast/rewriter/pull_ite_tree.cpp
View file

@ -56,10 +56,10 @@ void pull_ite_tree::reduce(expr * n) {
expr * c = to_app(n)->get_arg(0);
expr * t_old = to_app(n)->get_arg(1);
expr * e_old = to_app(n)->get_arg(2);
expr * t = 0;
proof * t_pr = 0;
expr * e = 0;
proof * e_pr = 0;
expr * t = nullptr;
proof * t_pr = nullptr;
expr * e = nullptr;
proof * e_pr = nullptr;
get_cached(t_old, t, t_pr);
get_cached(e_old, e, e_pr);
expr_ref r(m_manager);
@ -67,7 +67,7 @@ void pull_ite_tree::reduce(expr * n) {
r = m_rewriter.mk_app(to_app(n)->get_decl(), 3, args);
if (!m_manager.proofs_enabled()) {
// expr * r = m_manager.mk_ite(c, t, e);
cache_result(n, r, 0);
cache_result(n, r, nullptr);
}
else {
// t_pr is a proof for (m_p ... t_old ...) == t
@ -83,15 +83,15 @@ void pull_ite_tree::reduce(expr * n) {
proof * pr1 = m_manager.mk_rewrite(old, tmp1); // proof for (m_p ... (ite c t_old e_old) ...) = (ite c (m_p ... t_old ...) (m_p ... e_old ...))
expr_ref tmp2(m_manager);
tmp2 = m_manager.mk_ite(c, t, e); // (ite c t e)
proof * pr2 = 0; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
proof * pr3 = 0; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = (ite c t e)
proof * pr2 = nullptr; // it will contain a proof for (ite c (m_p ... t_old ...) (m_p ... e_old ...)) = (ite c t e)
proof * pr3 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = (ite c t e)
proof * proofs[2];
unsigned num_proofs = 0;
if (t_pr != 0) {
if (t_pr != nullptr) {
proofs[num_proofs] = t_pr;
num_proofs++;
}
if (e_pr != 0) {
if (e_pr != nullptr) {
proofs[num_proofs] = e_pr;
num_proofs++;
}
@ -102,8 +102,8 @@ void pull_ite_tree::reduce(expr * n) {
else {
pr3 = pr1;
}
proof * pr4 = 0; // it will contain a proof for (ite c t e) = r
proof * pr5 = 0; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r
proof * pr4 = nullptr; // it will contain a proof for (ite c t e) = r
proof * pr5 = nullptr; // it will contain a proof for (m_p ... (ite c t_old e_old) ...) = r
if (tmp2 != r) {
pr4 = m_manager.mk_rewrite(tmp2, r);
pr5 = m_manager.mk_transitivity(pr3, pr4);
@ -120,14 +120,14 @@ void pull_ite_tree::reduce(expr * n) {
r = m_rewriter.mk_app(m_p, m_args.size(), m_args.c_ptr());
if (!m_manager.proofs_enabled()) {
// expr * r = m_manager.mk_app(m_p, m_args.size(), m_args.c_ptr());
cache_result(n, r, 0);
cache_result(n, r, nullptr);
}
else {
expr_ref old(m_manager);
proof * p;
old = mk_p_arg(n);
if (old == r)
p = 0;
p = nullptr;
else
p = m_manager.mk_rewrite(old, r);
cache_result(n, r, p);
@ -139,7 +139,7 @@ void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
unsigned num_args = n->get_num_args();
m_args.resize(num_args);
m_p = n->get_decl();
expr * ite = 0;
expr * ite = nullptr;
for (unsigned i = 0; i < num_args; i++) {
expr * arg = n->get_arg(i);
if (ite) {
@ -156,7 +156,7 @@ void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
}
if (!ite) {
r = n;
pr = 0;
pr = nullptr;
return;
}
m_todo.push_back(ite);
@ -170,8 +170,8 @@ void pull_ite_tree::operator()(app * n, app_ref & r, proof_ref & pr) {
}
}
SASSERT(is_cached(ite));
expr * _r = 0;
proof * _pr = 0;
expr * _r = nullptr;
proof * _pr = nullptr;
get_cached(ite, _r, _pr);
r = to_app(_r);
pr = _pr;

4
src/ast/rewriter/pull_ite_tree.h
View file

@ -96,8 +96,8 @@ public:
class pull_cheap_ite_tree_cfg : public pull_ite_tree_cfg {
public:
pull_cheap_ite_tree_cfg(ast_manager & m):pull_ite_tree_cfg(m) {}
virtual ~pull_cheap_ite_tree_cfg() {}
virtual bool is_target(app * n) const;
~pull_cheap_ite_tree_cfg() override {}
bool is_target(app * n) const override;
};
class pull_cheap_ite_tree_rw : public rewriter_tpl<pull_cheap_ite_tree_cfg> {

2
src/ast/rewriter/push_app_ite.cpp
View file

@ -63,7 +63,7 @@ br_status push_app_ite_cfg::reduce_app(func_decl * f, unsigned num, expr * const
return BR_FAILED;
}
app * ite = to_app(args[ite_arg_idx]);
expr * c = 0, * t = 0, * e = 0;
expr * c = nullptr, * t = nullptr, * e = nullptr;
VERIFY(m.is_ite(ite, c, t, e));
expr ** args_prime = const_cast<expr**>(args);
expr * old = args_prime[ite_arg_idx];

2
src/ast/rewriter/push_app_ite.h
View file

@ -45,7 +45,7 @@ struct push_app_ite_cfg : public default_rewriter_cfg {
*/
class ng_push_app_ite_cfg : public push_app_ite_cfg {
protected:
virtual bool is_target(func_decl * decl, unsigned num_args, expr * const * args);
bool is_target(func_decl * decl, unsigned num_args, expr * const * args) override;
public:
ng_push_app_ite_cfg(ast_manager& m, bool conservative = true): push_app_ite_cfg(m, conservative) {}
virtual ~ng_push_app_ite_cfg() {}

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

@ -34,11 +34,11 @@ void rewriter_core::init_cache_stack() {
void rewriter_core::del_cache_stack() {
std::for_each(m_cache_stack.begin(), m_cache_stack.end(), delete_proc<cache>());
m_cache_stack.finalize();
m_cache = 0;
m_cache = nullptr;
if (m_proof_gen) {
std::for_each(m_cache_pr_stack.begin(), m_cache_pr_stack.end(), delete_proc<cache>());
m_cache_pr_stack.finalize();
m_cache_pr = 0;
m_cache_pr = nullptr;
}
}
@ -161,7 +161,7 @@ void rewriter_core::elim_reflex_prs(unsigned spos) {
unsigned j = spos;
for (unsigned i = spos; i < sz; i++) {
proof * pr = m_result_pr_stack.get(i);
if (pr != 0) {
if (pr != nullptr) {
if (i != j)
m_result_pr_stack.set(j, pr);
j++;
@ -192,7 +192,7 @@ void rewriter_core::reset() {
m_result_stack.reset();
if (m_proof_gen)
m_result_pr_stack.reset();
m_root = 0;
m_root = nullptr;
m_num_qvars = 0;
m_scopes.reset();
}
@ -201,7 +201,7 @@ void rewriter_core::reset() {
void rewriter_core::cleanup() {
free_memory();
init_cache_stack();
m_root = 0;
m_root = nullptr;
m_num_qvars = 0;
}

6
src/ast/rewriter/rewriter.h
View file

@ -150,7 +150,7 @@ class var_shifter : public var_shifter_core {
unsigned m_bound;
unsigned m_shift1;
unsigned m_shift2;
virtual void process_var(var * v);
void process_var(var * v) override;
public:
var_shifter(ast_manager & m):var_shifter_core(m) {}
void operator()(expr * t, unsigned bound, unsigned shift1, unsigned shift2, expr_ref & r);
@ -183,7 +183,7 @@ public:
class inv_var_shifter : public var_shifter_core {
protected:
unsigned m_shift;
virtual void process_var(var * v);
void process_var(var * v) override;
public:
inv_var_shifter(ast_manager & m):var_shifter_core(m) {}
void operator()(expr * t, unsigned shift, expr_ref & r);
@ -339,7 +339,7 @@ public:
Config & cfg() { return m_cfg; }
Config const & cfg() const { return m_cfg; }
~rewriter_tpl();
~rewriter_tpl() override;
void reset();
void cleanup();

86
src/ast/rewriter/rewriter_def.h
View file

@ -28,11 +28,11 @@ void rewriter_tpl<Config>::process_var(var * v) {
SASSERT(v->get_sort() == m().get_sort(m_r));
if (ProofGen) {
result_pr_stack().push_back(m_pr);
m_pr = 0;
m_pr = nullptr;
}
set_new_child_flag(v);
TRACE("rewriter", tout << mk_ismt2_pp(v, m()) << " -> " << m_r << "\n";);
m_r = 0;
m_r = nullptr;
return;
}
if (!ProofGen) {
@ -41,7 +41,7 @@ void rewriter_tpl<Config>::process_var(var * v) {
if (idx < m_bindings.size()) {
unsigned index = m_bindings.size() - idx - 1;
var * r = (var*)(m_bindings[index]);
if (r != 0) {
if (r != nullptr) {
CTRACE("rewriter", v->get_sort() != m().get_sort(r),
tout << expr_ref(v, m()) << ":" << sort_ref(v->get_sort(), m()) << " != " << expr_ref(r, m()) << ":" << sort_ref(m().get_sort(r), m());
tout << "index " << index << " bindings " << m_bindings.size() << "\n";
@ -67,14 +67,14 @@ void rewriter_tpl<Config>::process_var(var * v) {
}
result_stack().push_back(v);
if (ProofGen)
result_pr_stack().push_back(0); // implicit reflexivity
result_pr_stack().push_back(nullptr); // implicit reflexivity
}
template<typename Config>
template<bool ProofGen>
void rewriter_tpl<Config>::process_const(app * t) {
SASSERT(t->get_num_args() == 0);
br_status st = m_cfg.reduce_app(t->get_decl(), 0, 0, m_r, m_pr);
br_status st = m_cfg.reduce_app(t->get_decl(), 0, nullptr, m_r, m_pr);
SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
SASSERT(st == BR_FAILED || st == BR_DONE);
if (st == BR_DONE) {
@ -84,15 +84,15 @@ void rewriter_tpl<Config>::process_const(app * t) {
result_pr_stack().push_back(m_pr);
else
result_pr_stack().push_back(m().mk_rewrite(t, m_r));
m_pr = 0;
m_pr = nullptr;
}
m_r = 0;
m_r = nullptr;
set_new_child_flag(t);
}
else {
result_stack().push_back(t);
if (ProofGen)
result_pr_stack().push_back(0); // implicit reflexivity
result_pr_stack().push_back(nullptr); // implicit reflexivity
}
}
@ -108,8 +108,8 @@ template<typename Config>
template<bool ProofGen>
bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
expr * new_t = 0;
proof * new_t_pr = 0;
expr * new_t = nullptr;
proof * new_t_pr = nullptr;
if (m_cfg.get_subst(t, new_t, new_t_pr)) {
TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";);
SASSERT(m().get_sort(t) == m().get_sort(new_t));
@ -122,7 +122,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
if (max_depth == 0) {
result_stack().push_back(t);
if (ProofGen)
result_pr_stack().push_back(0); // implicit reflexivity
result_pr_stack().push_back(nullptr); // implicit reflexivity
return true; // t is not going to be processed
}
SASSERT(max_depth > 0);
@ -150,7 +150,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
if (!pre_visit(t)) {
result_stack().push_back(t);
if (ProofGen)
result_pr_stack().push_back(0); // implicit reflexivity
result_pr_stack().push_back(nullptr); // implicit reflexivity
return true; // t is not going to be processed
}
switch (t->get_kind()) {
@ -183,7 +183,7 @@ template<typename Config>
bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
if (fr.m_i == 1 && m().is_ite(t)) {
expr * cond = result_stack()[fr.m_spos].get();
expr* arg = 0;
expr* arg = nullptr;
if (m().is_true(cond)) {
arg = t->get_arg(1);
}
@ -203,7 +203,7 @@ bool rewriter_tpl<Config>::constant_fold(app * t, frame & fr) {
frame_stack().pop_back();
set_new_child_flag(t);
}
m_r = 0;
m_r = nullptr;
return true;
}
}
@ -255,7 +255,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
unsigned num_prs = result_pr_stack().size() - fr.m_spos;
if (num_prs == 0) {
new_t = t;
m_pr = 0;
m_pr = nullptr;
}
else {
new_t = m().mk_app(f, new_num_args, new_args);
@ -278,16 +278,16 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (!m_pr2)
m_pr2 = m().mk_rewrite(new_t, m_r);
m_pr = m().mk_transitivity(m_pr, m_pr2);
m_pr2 = 0;
m_pr2 = nullptr;
result_pr_stack().push_back(m_pr);
}
if (st == BR_DONE) {
cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
frame_stack().pop_back();
set_new_child_flag(t);
m_r = 0;
m_r = nullptr;
if (ProofGen)
m_pr = 0;
m_pr = nullptr;
return;
}
else {
@ -318,16 +318,16 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
frame_stack().pop_back();
set_new_child_flag(t);
m_r = 0;
m_r = nullptr;
if (ProofGen)
m_pr = 0;
m_pr = nullptr;
return;
}
else {
// frame was created for processing m_r
m_r = 0;
m_r = nullptr;
if (ProofGen)
m_pr = 0;
m_pr = nullptr;
return;
}
}
@ -407,11 +407,11 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
if (ProofGen) {
result_pr_stack().shrink(fr.m_spos);
result_pr_stack().push_back(m_pr);
m_pr = 0;
m_pr = nullptr;
}
frame_stack().pop_back();
set_new_child_flag(t, m_r);
m_r = 0;
m_r = nullptr;
return;
}
case REWRITE_BUILTIN:
@ -497,23 +497,27 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
SASSERT(fr.m_spos + num_children == result_stack().size());
expr * const * it = result_stack().c_ptr() + fr.m_spos;
expr * new_body = *it;
expr * const * new_pats;
expr * const * new_no_pats;
unsigned num_pats = q->get_num_patterns();
unsigned num_no_pats = q->get_num_no_patterns();
expr_ref_vector new_pats(m_manager, num_pats, q->get_patterns());
expr_ref_vector new_no_pats(m_manager, num_no_pats, q->get_no_patterns());
if (rewrite_patterns()) {
TRACE("reduce_quantifier_bug", tout << "rewrite patterns\n";);
new_pats = it + 1;
new_no_pats = new_pats + q->get_num_patterns();
}
else {
new_pats = q->get_patterns();
new_no_pats = q->get_no_patterns();
expr * const * np = it + 1;
expr * const * nnp = np + num_pats;
for (unsigned i = 0; i < num_pats; i++)
if (m_manager.is_pattern(np[i]))
new_pats[i] = np[i];
for (unsigned i = 0; i < num_no_pats; i++)
if (m_manager.is_pattern(nnp[i]))
new_no_pats[i] = nnp[i];
}
if (ProofGen) {
quantifier_ref new_q(m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body), m());
m_pr = q == new_q ? 0 : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos));
quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body), m());
m_pr = q == new_q ? nullptr : m().mk_quant_intro(q, new_q, result_pr_stack().get(fr.m_spos));
m_r = new_q;
proof_ref pr2(m());
if (m_cfg.reduce_quantifier(new_q, new_body, new_pats, new_no_pats, m_r, pr2)) {
if (m_cfg.reduce_quantifier(new_q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, pr2)) {
m_pr = m().mk_transitivity(m_pr, pr2);
}
TRACE("reduce_quantifier_bug", tout << "m_pr is_null: " << (m_pr.get() == 0) << "\n";
@ -524,9 +528,9 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
else {
expr_ref tmp(m());
TRACE("reduce_quantifier_bug", tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";);
if (!m_cfg.reduce_quantifier(q, new_body, new_pats, new_no_pats, m_r, m_pr)) {
if (!m_cfg.reduce_quantifier(q, new_body, new_pats.c_ptr(), new_no_pats.c_ptr(), m_r, m_pr)) {
if (fr.m_new_child) {
m_r = m().update_quantifier(q, q->get_num_patterns(), new_pats, q->get_num_no_patterns(), new_no_pats, new_body);
m_r = m().update_quantifier(q, num_pats, new_pats.c_ptr(), num_no_pats, new_no_pats.c_ptr(), new_body);
}
else {
TRACE("rewriter_reuse", tout << "reusing:\n" << mk_ismt2_pp(q, m()) << "\n";);
@ -546,9 +550,9 @@ void rewriter_tpl<Config>::process_quantifier(quantifier * q, frame & fr) {
}
else {
cache_result<ProofGen>(q, m_r, m_pr, fr.m_cache_result);
m_pr = 0;
m_pr = nullptr;
}
m_r = 0;
m_r = nullptr;
frame_stack().pop_back();
set_new_child_flag(q, m_r);
}
@ -652,7 +656,7 @@ void rewriter_tpl<Config>::main_loop(expr * t, expr_ref & result, proof_ref & re
if (ProofGen) {
result_pr = result_pr_stack().back();
result_pr_stack().pop_back();
if (result_pr.get() == 0)
if (result_pr.get() == nullptr)
result_pr = m().mk_reflexivity(t);
SASSERT(result_pr_stack().empty());
}
@ -717,7 +721,7 @@ void rewriter_tpl<Config>::resume_core(expr_ref & result, proof_ref & result_pr)
if (ProofGen) {
result_pr = result_pr_stack().back();
result_pr_stack().pop_back();
if (result_pr.get() == 0)
if (result_pr.get() == nullptr)
result_pr = m().mk_reflexivity(m_root);
SASSERT(result_pr_stack().empty());
}

81
src/ast/rewriter/seq_rewriter.cpp
View file

@ -85,15 +85,15 @@ public:
sym_expr_boolean_algebra(ast_manager& m, expr_solver& s):
m(m), m_solver(s) {}
virtual T mk_false() {
T mk_false() override {
expr_ref fml(m.mk_false(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort()); // use of Bool sort for bound variable is arbitrary
}
virtual T mk_true() {
T mk_true() override {
expr_ref fml(m.mk_true(), m);
return sym_expr::mk_pred(fml, m.mk_bool_sort());
}
virtual T mk_and(T x, T y) {
T mk_and(T x, T y) override {
if (x->is_char() && y->is_char()) {
if (x->get_char() == y->get_char()) {
return x;
@ -118,7 +118,7 @@ public:
br.mk_and(fml1, fml2, fml);
return sym_expr::mk_pred(fml, x->get_sort());
}
virtual T mk_or(T x, T y) {
T mk_or(T x, T y) override {
if (x->is_char() && y->is_char() &&
x->get_char() == y->get_char()) {
return x;
@ -135,7 +135,7 @@ public:
return sym_expr::mk_pred(fml, x->get_sort());
}
virtual T mk_and(unsigned sz, T const* ts) {
T mk_and(unsigned sz, T const* ts) override {
switch (sz) {
case 0: return mk_true();
case 1: return ts[0];
@ -148,7 +148,7 @@ public:
}
}
}
virtual T mk_or(unsigned sz, T const* ts) {
T mk_or(unsigned sz, T const* ts) override {
switch (sz) {
case 0: return mk_false();
case 1: return ts[0];
@ -161,7 +161,7 @@ public:
}
}
}
virtual lbool is_sat(T x) {
lbool is_sat(T x) override {
if (x->is_char()) {
return l_true;
}
@ -178,7 +178,7 @@ public:
}
return m_solver.check_sat(fml);
}
virtual T mk_not(T x) {
T mk_not(T x) override {
var_ref v(m.mk_var(0, x->get_sort()), m);
expr_ref fml(m.mk_not(x->accept(v)), m);
return sym_expr::mk_pred(fml, x->get_sort());
@ -190,7 +190,7 @@ public:
}*/
};
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(0), m_sa(0) {}
re2automaton::re2automaton(ast_manager& m): m(m), u(m), bv(m), m_ba(nullptr), m_sa(nullptr) {}
re2automaton::~re2automaton() {}
@ -289,19 +289,28 @@ eautomaton* re2automaton::re2aut(expr* e) {
else if (u.re.is_empty(e)) {
return alloc(eautomaton, sm);
}
else if (u.re.is_full(e)) {
else if (u.re.is_full_seq(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = 0, *char_s = 0;
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(m.get_sort(e), seq_s));
VERIFY (u.is_seq(seq_s, char_s));
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
return eautomaton::mk_loop(sm, _true);
}
else if (u.re.is_full_char(e)) {
expr_ref tt(m.mk_true(), m);
sort *seq_s = nullptr, *char_s = nullptr;
VERIFY (u.is_re(m.get_sort(e), seq_s));
VERIFY (u.is_seq(seq_s, char_s));
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
a = alloc(eautomaton, sm, _true);
return a.detach();
}
else if (u.re.is_intersection(e, e1, e2) && m_sa && (a = re2aut(e1)) && (b = re2aut(e2))) {
return m_sa->mk_product(*a, *b);
}
return 0;
return nullptr;
}
eautomaton* re2automaton::seq2aut(expr* e) {
@ -329,7 +338,7 @@ eautomaton* re2automaton::seq2aut(expr* e) {
}
return alloc(eautomaton, sm, init, final, mvs);
}
return 0;
return nullptr;
}
br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@ -373,7 +382,9 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
return mk_re_loop(num_args, args, result);
case OP_RE_EMPTY_SET:
return BR_FAILED;
case OP_RE_FULL_SET:
case OP_RE_FULL_SEQ_SET:
return BR_FAILED;
case OP_RE_FULL_CHAR_SET:
return BR_FAILED;
case OP_RE_OF_PRED:
return BR_FAILED;
@ -985,14 +996,14 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
bool isc1 = false;
bool isc2 = false;
expr *a1 = 0, *a2 = 0, *b1 = 0, *b2 = 0;
expr *a1 = nullptr, *a2 = nullptr, *b1 = nullptr, *b2 = nullptr;
if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
isc1 = true;
}
else if (m_util.str.is_string(a, s1)) {
isc1 = true;
a2 = a;
a1 = 0;
a1 = nullptr;
}
if (m_util.str.is_concat(b, b1, b2) && m_util.str.is_string(b2, s2)) {
@ -1001,7 +1012,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
else if (m_util.str.is_string(b, s2)) {
isc2 = true;
b2 = b;
b1 = 0;
b1 = nullptr;
}
if (isc1 && isc2) {
if (s1.length() == s2.length()) {
@ -1011,7 +1022,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
}
else if (s1.length() < s2.length()) {
bool suffix = s1.suffixof(s2);
if (suffix && a1 == 0) {
if (suffix && a1 == nullptr) {
result = m().mk_true();
return BR_DONE;
}
@ -1028,7 +1039,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
}
else {
SASSERT(s1.length() > s2.length());
if (b1 == 0) {
if (b1 == nullptr) {
result = m().mk_false();
return BR_DONE;
}
@ -1220,7 +1231,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
result = m().mk_false();
return BR_DONE;
}
if (m_util.re.is_full(b)) {
if (m_util.re.is_full_seq(b)) {
result = m().mk_true();
return BR_DONE;
}
@ -1315,7 +1326,7 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
return BR_FAILED;
}
br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
if (m_util.re.is_full(a) && m_util.re.is_full(b)) {
if (m_util.re.is_full_seq(a) && m_util.re.is_full_seq(b)) {
result = a;
return BR_DONE;
}
@ -1355,11 +1366,11 @@ br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
result = a;
return BR_DONE;
}
if (m_util.re.is_full(a)) {
if (m_util.re.is_full_seq(a)) {
result = a;
return BR_DONE;
}
if (m_util.re.is_full(b)) {
if (m_util.re.is_full_seq(b)) {
result = b;
return BR_DONE;
}
@ -1385,10 +1396,10 @@ br_status seq_rewriter::mk_re_complement(expr* a, expr_ref& result) {
return BR_REWRITE2;
}
if (m_util.re.is_empty(a)) {
result = m_util.re.mk_full(m().get_sort(a));
result = m_util.re.mk_full_seq(m().get_sort(a));
return BR_DONE;
}
if (m_util.re.is_full(a)) {
if (m_util.re.is_full_seq(a)) {
result = m_util.re.mk_empty(m().get_sort(a));
return BR_DONE;
}
@ -1415,11 +1426,11 @@ br_status seq_rewriter::mk_re_inter(expr* a, expr* b, expr_ref& result) {
result = b;
return BR_DONE;
}
if (m_util.re.is_full(a)) {
if (m_util.re.is_full_seq(a)) {
result = b;
return BR_DONE;
}
if (m_util.re.is_full(b)) {
if (m_util.re.is_full_seq(b)) {
result = a;
return BR_DONE;
}
@ -1462,12 +1473,18 @@ br_status seq_rewriter::mk_re_loop(unsigned num_args, expr* const* args, expr_re
*/
br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
expr* b, *c, *b1, *c1;
if (m_util.re.is_star(a) || m_util.re.is_full(a)) {
if (m_util.re.is_star(a) || m_util.re.is_full_seq(a)) {
result = a;
return BR_DONE;
}
if (m_util.re.is_full_char(a)) {
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(a, seq_sort));
result = m_util.re.mk_full_seq(seq_sort);
return BR_DONE;
}
if (m_util.re.is_empty(a)) {
sort* seq_sort = 0;
sort* seq_sort = nullptr;
VERIFY(m_util.is_re(a, seq_sort));
result = m_util.re.mk_to_re(m_util.str.mk_empty(seq_sort));
return BR_DONE;
@ -1522,7 +1539,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
result = a;
return BR_DONE;
}
if (m_util.re.is_full(a)) {
if (m_util.re.is_full_seq(a)) {
result = a;
return BR_DONE;
}
@ -1545,7 +1562,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
}
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
sort* s = 0;
sort* s = nullptr;
VERIFY(m_util.is_re(a, s));
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
return BR_REWRITE1;
@ -1869,7 +1886,7 @@ expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) {
bool seq_rewriter::set_empty(unsigned sz, expr* const* es, bool all, expr_ref_vector& lhs, expr_ref_vector& rhs) {
zstring s;
expr* emp = 0;
expr* emp = nullptr;
for (unsigned i = 0; i < sz; ++i) {
if (m_util.str.is_unit(es[i])) {
if (all) return false;

28
src/ast/rewriter/th_rewriter.cpp
View file

@ -440,8 +440,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
if (num1 != num2 && num1 != num2 + 1 && num1 != num2 - 1)
return false;
new_t1 = 0;
new_t2 = 0;
new_t1 = nullptr;
new_t2 = nullptr;
expr_fast_mark1 visited1;
expr_fast_mark2 visited2;
for (unsigned i = 0; i < num1; i++) {
@ -533,7 +533,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr * c = args[0];
expr * t = args[1];
expr * e = args[2];
func_decl * f_prime = 0;
func_decl * f_prime = nullptr;
expr_ref new_t(m()), new_e(m()), common(m());
bool first;
TRACE("push_ite", tout << "unifying:\n" << mk_ismt2_pp(t, m()) << "\n" << mk_ismt2_pp(e, m()) << "\n";);
@ -559,7 +559,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
br_status reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) {
result_pr = 0;
result_pr = nullptr;
br_status st = reduce_app_core(f, num, args, result);
if (st != BR_DONE && st != BR_FAILED) {
CTRACE("th_rewriter_step", st != BR_FAILED,
@ -604,7 +604,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
expr_ref & result,
proof_ref & result_pr) {
quantifier_ref q1(m());
proof * p1 = 0;
proof * p1 = nullptr;
if (is_quantifier(new_body) &&
to_quantifier(new_body)->is_forall() == old_q->is_forall() &&
!old_q->has_patterns() &&
@ -627,7 +627,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
std::min(old_q->get_weight(), nested_q->get_weight()),
old_q->get_qid(),
old_q->get_skid(),
0, 0, 0, 0);
0, nullptr, 0, nullptr);
SASSERT(is_well_sorted(m(), q1));
@ -657,9 +657,9 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << mk_ismt2_pp(result, m()) << "\n";);
result_pr = 0;
result_pr = nullptr;
if (m().proofs_enabled()) {
proof * p2 = 0;
proof * p2 = nullptr;
if (q1.get() != result.get())
p2 = m().mk_elim_unused_vars(q1, result);
result_pr = m().mk_transitivity(p1, p2);
@ -680,7 +680,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_a_util(m),
m_bv_util(m),
m_used_dependencies(m),
m_subst(0) {
m_subst(nullptr) {
updt_local_params(p);
}
@ -690,13 +690,13 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
}
void reset() {
m_subst = 0;
m_subst = nullptr;
}
bool get_subst(expr * s, expr * & t, proof * & pr) {
if (m_subst == 0)
if (m_subst == nullptr)
return false;
expr_dependency * d = 0;
expr_dependency * d = nullptr;
if (m_subst->find(s, t, pr, d)) {
m_used_dependencies = m().mk_join(m_used_dependencies, d);
return true;
@ -798,9 +798,9 @@ expr_dependency * th_rewriter::get_used_dependencies() {
}
void th_rewriter::reset_used_dependencies() {
if (get_used_dependencies() != 0) {
if (get_used_dependencies() != nullptr) {
set_substitution(m_imp->cfg().m_subst); // reset cache preserving subst
m_imp->cfg().m_used_dependencies = 0;
m_imp->cfg().m_used_dependencies = nullptr;
}
}

4
src/ast/rewriter/var_subst.cpp
View file

@ -94,7 +94,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
}
else {
num_removed++;
var_mapping.push_back(0);
var_mapping.push_back(nullptr);
}
}
// (VAR 0) is in the first position of var_mapping.
@ -104,7 +104,7 @@ void unused_vars_eliminator::operator()(quantifier* q, expr_ref & result) {
if (s)
var_mapping.push_back(m.mk_var(i - num_removed, s));
else
var_mapping.push_back(0);
var_mapping.push_back(nullptr);
}