mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Use nullptr rather than 0/NULL.

Browse source
This commit is contained in:
Bruce Mitchener 2018-11-28 14:57:01 +07:00
parent eea9b79035
commit b83d6d77c9
9 changed files with 30 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -628,7 +628,7 @@ bool bv_bounds::is_sat_core(app * v) {
numeral new_hi = lower - one;
numeral ptr = lower;
if (has_neg_intervals) {
SASSERT(negative_intervals != NULL);
SASSERT(negative_intervals != nullptr);
std::sort(negative_intervals->begin(), negative_intervals->end(), interval_comp);
intervals::const_iterator e = negative_intervals->end();
for (intervals::const_iterator i = negative_intervals->begin(); i != e; ++i) {

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

@ -364,7 +364,7 @@ struct bv_trailing::imp {
}
void reset_cache(const unsigned condition) {
SASSERT(m_count_cache[0] == NULL);
SASSERT(m_count_cache[0] == nullptr);
for (unsigned i = 1; i <= TRAILING_DEPTH; ++i) {
if (m_count_cache[i] == nullptr) continue;
TRACE("bv-trailing", tout << "may reset cache " << i << " " << condition << "\n";);

2
src/muz/fp/datalog_parser.cpp
View file

@ -101,7 +101,7 @@ public:
resize_data(0);
#if _WINDOWS
errno_t err = fopen_s(&m_file, fname, "rb");
m_ok = (m_file != NULL) && (err == 0);
m_ok = (m_file != nullptr) && (err == 0);
#else
m_file = fopen(fname, "rb");
m_ok = (m_file != nullptr);

2
src/smt/theory_recfun.h
View file

@ -69,7 +69,7 @@ namespace smt {
recfun::case_def const * m_cdef;
ptr_vector<expr> m_args;
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(0), m_args() {
body_expansion(recfun::util& u, app * n) : m_pred(n), m_cdef(nullptr), m_args() {
m_cdef = &u.get_case_def(n);
m_args.append(n->get_num_args(), n->get_args());
}

34
src/smt/theory_str.cpp
View file

@ -505,7 +505,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), int_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
ctx.mark_as_relevant(a);
// I'm assuming that this combination will do the correct thing in the integer theory.
@ -544,7 +544,7 @@ namespace smt {
// I have a hunch that this may not get internalized for free...
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
// this might help??
mk_var(ctx.get_enode(a));
@ -566,7 +566,7 @@ namespace smt {
m_trail.push_back(a);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
SASSERT(ctx.e_internalized(a));
mk_var(ctx.get_enode(a));
m_basicstr_axiom_todo.push_back(ctx.get_enode(a));
@ -617,7 +617,7 @@ namespace smt {
app * a = mk_fresh_const(name.c_str(), string_sort);
ctx.internalize(a, false);
SASSERT(ctx.get_enode(a) != NULL);
SASSERT(ctx.get_enode(a) != nullptr);
// this might help??
mk_var(ctx.get_enode(a));
@ -710,7 +710,7 @@ namespace smt {
* Returns the simplified concatenation of two expressions,
* where either both expressions are constant strings
* or one expression is the empty string.
* If this precondition does not hold, the function returns NULL.
* If this precondition does not hold, the function returns nullptr.
* (note: this function was strTheory::Concat())
*/
expr * theory_str::mk_concat_const_str(expr * n1, expr * n2) {
@ -2148,7 +2148,7 @@ namespace smt {
// Evaluates the concatenation (n1 . n2) with respect to
// the current equivalence classes of n1 and n2.
// Returns a constant string expression representing this concatenation
// if one can be determined, or NULL if this is not possible.
// if one can be determined, or nullptr if this is not possible.
expr * theory_str::eval_concat(expr * n1, expr * n2) {
bool n1HasEqcValue = false;
bool n2HasEqcValue = false;
@ -2222,7 +2222,7 @@ namespace smt {
for (enode_vector::iterator parent_it = current_parents.begin(); parent_it != current_parents.end(); ++parent_it) {
enode * e_parent = *parent_it;
SASSERT(e_parent != NULL);
SASSERT(e_parent != nullptr);
app * a_parent = e_parent->get_owner();
TRACE("str", tout << "considering parent " << mk_ismt2_pp(a_parent, m) << std::endl;);
@ -5575,7 +5575,7 @@ namespace smt {
tout << " " << mk_pp(el, m);
}
tout << std::endl;
if (constStrAst == NULL) {
if (constStrAst == nullptr) {
tout << "constStrAst = NULL" << std::endl;
} else {
tout << "constStrAst = " << mk_pp(constStrAst, m) << std::endl;
@ -7787,7 +7787,7 @@ namespace smt {
generate_mutual_exclusion(arrangement_disjunction);
}
} /* (arg1Len != 1 || arg2Len != 1) */
} /* if (Concat(arg1, arg2) == NULL) */
} /* if (Concat(arg1, arg2) == nullptr) */
}
}
}
@ -10417,12 +10417,12 @@ namespace smt {
}
} // foreach(term in str_in_re_terms)
eautomaton * aut_inter = NULL;
eautomaton * aut_inter = nullptr;
CTRACE("str", !intersect_constraints.empty(), tout << "check intersection of automata constraints for " << mk_pp(str, m) << std::endl;);
for (svector<regex_automaton_under_assumptions>::iterator aut_it = intersect_constraints.begin();
aut_it != intersect_constraints.end(); ++aut_it) {
regex_automaton_under_assumptions aut = *aut_it;
if (aut_inter == NULL) {
if (aut_inter == nullptr) {
// start somewhere
aut_inter = aut.get_automaton();
used_intersect_constraints.push_back(aut);
@ -10472,7 +10472,7 @@ namespace smt {
}
}
} // foreach(entry in intersect_constraints)
if (aut_inter != NULL) {
if (aut_inter != nullptr) {
aut_inter->compress();
}
TRACE("str", tout << "intersected " << used_intersect_constraints.size() << " constraints" << std::endl;);
@ -10503,7 +10503,7 @@ namespace smt {
}
conflict_lhs = mk_and(conflict_terms);
if (used_intersect_constraints.size() > 1 && aut_inter != NULL) {
if (used_intersect_constraints.size() > 1 && aut_inter != nullptr) {
// check whether the intersection is only the empty string
unsigned initial_state = aut_inter->init();
if (aut_inter->final_states().size() == 1 && aut_inter->is_final_state(initial_state)) {
@ -10521,7 +10521,7 @@ namespace smt {
}
}
if (aut_inter != NULL && aut_inter->is_empty()) {
if (aut_inter != nullptr && aut_inter->is_empty()) {
TRACE("str", tout << "product automaton is empty; asserting conflict clause" << std::endl;);
expr_ref conflict_clause(m.mk_not(mk_and(conflict_terms)), m);
assert_axiom(conflict_clause);
@ -11809,7 +11809,7 @@ namespace smt {
expr_ref assertL(mk_and(and_items_LHS), m);
SASSERT(assertL);
expr * finalAxiom = m.mk_or(m.mk_not(assertL), lenTestAssert.get());
SASSERT(finalAxiom != NULL);
SASSERT(finalAxiom != nullptr);
TRACE("str", tout << "crash avoidance finalAxiom: " << mk_pp(finalAxiom, m) << std::endl;);
return finalAxiom;
} else {
@ -12095,7 +12095,7 @@ namespace smt {
lenTester_fvar_map.insert(indicator, freeVar);
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
TRACE("str", tout << "found previous in-scope length assertions" << std::endl;);
@ -12201,7 +12201,7 @@ namespace smt {
testNum = i + 1;
}
expr * lenTestAssert = gen_len_test_options(freeVar, indicator, testNum);
SASSERT(lenTestAssert != NULL);
SASSERT(lenTestAssert != nullptr);
return lenTestAssert;
} else {
// if we are performing automata-based reasoning and the term associated with

2
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -121,7 +121,7 @@ private:
tactic_ref t = mk_qfaufbv_tactic(m_m, m_p);
sat = mk_tactic2solver(m_m, t.get(), m_p);
}
SASSERT(sat != NULL);
SASSERT(sat != nullptr);
sat->set_produce_models(true);
return sat;
}

2
src/util/array.h
View file

@ -154,7 +154,7 @@ public:
return static_cast<unsigned>(reinterpret_cast<size_t *>(m_data)[SIZE_IDX]);
}
bool empty() const { return m_data == 0; }
bool empty() const { return m_data == nullptr; }
T & operator[](unsigned idx) {
SASSERT(idx < size());

12
src/util/scoped_timer.cpp
View file

@ -146,7 +146,7 @@ struct scoped_timer::imp {
#if defined(_WINDOWS) || defined(_CYGWIN)
m_first = true;
CreateTimerQueueTimer(&m_timer,
NULL,
nullptr,
abort_proc,
this,
0,
@ -180,9 +180,9 @@ struct scoped_timer::imp {
m_ms = ms;
m_initialized = false;
m_signal_sent = false;
ENSURE(pthread_mutex_init(&m_mutex, NULL) == 0);
ENSURE(pthread_cond_init(&m_cond, NULL) == 0);
ENSURE(pthread_create(&m_thread_id, NULL, &thread_func, this) == 0);
ENSURE(pthread_mutex_init(&m_mutex, nullptr) == 0);
ENSURE(pthread_cond_init(&m_cond, nullptr) == 0);
ENSURE(pthread_create(&m_thread_id, nullptr, &thread_func, this) == 0);
#else
// Other platforms
#endif
@ -190,7 +190,7 @@ struct scoped_timer::imp {
~imp() {
#if defined(_WINDOWS) || defined(_CYGWIN)
DeleteTimerQueueTimer(NULL,
DeleteTimerQueueTimer(nullptr,
m_timer,
INVALID_HANDLE_VALUE);
#elif defined(__APPLE__) && defined(__MACH__)
@ -242,7 +242,7 @@ struct scoped_timer::imp {
// Perform signal outside of lock to avoid waking timing thread twice.
pthread_cond_signal(&m_cond);
pthread_join(m_thread_id, NULL);
pthread_join(m_thread_id, nullptr);
pthread_cond_destroy(&m_cond);
pthread_mutex_destroy(&m_mutex);
#else

2
src/util/warning.cpp
View file

@ -88,7 +88,7 @@ void format2ostream(std::ostream & out, char const* msg, va_list args) {
#ifdef _WINDOWS
size_t msg_len = _vscprintf(msg, args_copy);
#else
size_t msg_len = vsnprintf(NULL, 0, msg, args_copy);
size_t msg_len = vsnprintf(nullptr, 0, msg, args_copy);
#endif
va_end(args_copy);