mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-10-01 19:32:52 -07:00
commit 096a6c088d
47 changed files with 98 additions and 183 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/smt/smt_context.h
View file

@ -565,7 +565,7 @@ namespace smt {
return m_asserted_formulas.has_quantifiers();
}
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = 0) {
fingerprint * add_fingerprint(void * data, unsigned data_hash, unsigned num_args, enode * const * args, expr* def = nullptr) {
return m_fingerprints.insert(data, data_hash, num_args, args, def);
}

2
src/smt/smt_model_checker.cpp
View file

@ -577,7 +577,7 @@ namespace smt {
}
if (inst.m_def) {
m_context->internalize_assertion(inst.m_def, 0, gen);
m_context->internalize_assertion(inst.m_def, nullptr, gen);
}
TRACE("model_checker_bug_detail", tout << "instantiating... q:\n" << mk_pp(q, m) << "\n";

4
src/smt/tactic/smt_tactic.cpp
View file

@ -217,7 +217,7 @@ public:
model_ref md;
m_ctx->get_model(md);
buffer<symbol> r;
m_ctx->get_relevant_labels(0, r);
m_ctx->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.c_ptr());
model_converter_ref mc;
@ -270,7 +270,7 @@ public:
model_ref md;
m_ctx->get_model(md);
buffer<symbol> r;
m_ctx->get_relevant_labels(0, r);
m_ctx->get_relevant_labels(nullptr, r);
labels_vec rv;
rv.append(r.size(), r.c_ptr());
in->add(model_and_labels2model_converter(md.get(), rv));

14
src/smt/theory_lra.cpp
View file

@ -1054,7 +1054,7 @@ public:
// to_int (to_real x) = x
// to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
void mk_to_int_axiom(app* n) {
expr* x = 0, *y = 0;
expr* x = nullptr, *y = nullptr;
VERIFY (a.is_to_int(n, x));
if (a.is_to_real(x, y)) {
mk_axiom(th.mk_eq(y, n, false));
@ -1070,7 +1070,7 @@ public:
// is_int(x) <=> to_real(to_int(x)) = x
void mk_is_int_axiom(app* n) {
expr* x = 0;
expr* x = nullptr;
VERIFY(a.is_is_int(n, x));
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
literal is_int = ctx().get_literal(n);
@ -1450,7 +1450,7 @@ public:
st = FC_GIVEUP;
break;
}
if (m_not_handled != 0) {
if (m_not_handled != nullptr) {
TRACE("arith", tout << "unhandled operator " << mk_pp(m_not_handled, m) << "\n";);
st = FC_GIVEUP;
}
@ -2080,12 +2080,12 @@ public:
m_core2.push_back(~c);
}
m_core2.push_back(lit);
justification * js = 0;
justification * js = nullptr;
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx(), m_core2.size(), m_core2.c_ptr(),
m_params.size(), m_params.c_ptr());
}
ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx().mk_clause(m_core2.size(), m_core2.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
else {
ctx().assign(
@ -2140,7 +2140,7 @@ public:
rational const& k1 = b.get_value();
lp_bounds & bounds = m_bounds[v];
lp_api::bound* end = 0;
lp_api::bound* end = nullptr;
lp_api::bound* lo_inf = end, *lo_sup = end;
lp_api::bound* hi_inf = end, *hi_sup = end;
@ -2798,7 +2798,7 @@ public:
justification* js =
ctx().mk_justification(
ext_theory_eq_propagation_justification(
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, 0));
get_id(), ctx().get_region(), m_core.size(), m_core.c_ptr(), m_eqs.size(), m_eqs.c_ptr(), x, y, 0, nullptr));
TRACE("arith",
for (unsigned i = 0; i < m_core.size(); ++i) {

32
src/smt/theory_pb.cpp
View file

@ -897,7 +897,7 @@ namespace smt {
void theory_pb::watch_literal(literal lit, card* c) {
init_watch(lit.var());
ptr_vector<card>* cards = m_var_infos[lit.var()].m_lit_cwatch[lit.sign()];
if (cards == 0) {
if (cards == nullptr) {
cards = alloc(ptr_vector<card>);
m_var_infos[lit.var()].m_lit_cwatch[lit.sign()] = cards;
}
@ -961,13 +961,13 @@ namespace smt {
void theory_pb::add_clause(card& c, literal_vector const& lits) {
m_stats.m_num_conflicts++;
context& ctx = get_context();
justification* js = 0;
justification* js = nullptr;
c.inc_propagations(*this);
if (!resolve_conflict(c, lits)) {
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
SASSERT(ctx.inconsistent());
}
@ -1027,7 +1027,7 @@ namespace smt {
}
void theory_pb::assign_eh(bool_var v, bool is_true) {
ptr_vector<ineq>* ineqs = 0;
ptr_vector<ineq>* ineqs = nullptr;
context& ctx = get_context();
literal nlit(v, is_true);
init_watch(v);
@ -1060,7 +1060,7 @@ namespace smt {
}
ptr_vector<card>* cards = m_var_infos[v].m_lit_cwatch[nlit.sign()];
if (cards != 0 && !cards->empty() && !ctx.inconsistent()) {
if (cards != nullptr && !cards->empty() && !ctx.inconsistent()) {
ptr_vector<card>::iterator it = cards->begin(), it2 = it, end = cards->end();
for (; it != end; ++it) {
if (ctx.get_assignment((*it)->lit()) != l_true) {
@ -1088,7 +1088,7 @@ namespace smt {
}
card* crd = m_var_infos[v].m_card;
if (crd != 0 && !ctx.inconsistent()) {
if (crd != nullptr && !ctx.inconsistent()) {
crd->init_watch(*this, is_true);
}
@ -1527,7 +1527,7 @@ namespace smt {
else {
z++;
clear_watch(*c);
m_var_infos[v].m_card = 0;
m_var_infos[v].m_card = nullptr;
dealloc(c);
m_card_trail[i] = null_bool_var;
ctx.remove_watch(v);
@ -1671,7 +1671,7 @@ namespace smt {
if (v != null_bool_var) {
card* c = m_var_infos[v].m_card;
clear_watch(*c);
m_var_infos[v].m_card = 0;
m_var_infos[v].m_card = nullptr;
dealloc(c);
}
}
@ -1774,11 +1774,11 @@ namespace smt {
context& ctx = get_context();
TRACE("pb", tout << "#prop:" << c.m_num_propagations << " - " << lits << "\n";
display(tout, c, true););
justification* js = 0;
justification* js = nullptr;
if (proofs_enabled()) {
js = alloc(theory_lemma_justification, get_id(), ctx, lits.size(), lits.c_ptr());
}
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx.mk_clause(lits.size(), lits.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
@ -1894,11 +1894,11 @@ namespace smt {
break;
case b_justification::JUSTIFICATION: {
justification* j = js.get_justification();
card_justification* pbj = 0;
card_justification* pbj = nullptr;
if (j->get_from_theory() == get_id()) {
pbj = dynamic_cast<card_justification*>(j);
}
if (pbj != 0) {
if (pbj != nullptr) {
card& c2 = pbj->get_card();
result = card2expr(c2);
}
@ -2170,11 +2170,11 @@ namespace smt {
VERIFY(internalize_card(atl, false));
bool_var abv = ctx.get_bool_var(atl);
m_antecedents.push_back(literal(abv));
justification* js = 0;
justification* js = nullptr;
if (proofs_enabled()) {
js = 0; //
js = nullptr;
}
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, 0);
ctx.mk_clause(m_antecedents.size(), m_antecedents.c_ptr(), js, CLS_AUX_LEMMA, nullptr);
}
bool theory_pb::resolve_conflict(card& c, literal_vector const& confl) {
@ -2403,7 +2403,7 @@ namespace smt {
}
#endif
SASSERT(validate_antecedents(m_antecedents));
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, 0)));
ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr)));
DEBUG_CODE(
m_antecedents.push_back(~alit);

2
src/smt/theory_pb.h
View file

@ -258,7 +258,7 @@ namespace smt {
card_watch* m_lit_cwatch[2];
card* m_card;
var_info(): m_var_watch(0), m_ineq(0), m_card(0)
var_info(): m_var_watch(nullptr), m_ineq(nullptr), m_card(nullptr)
{
m_lit_watch[0] = nullptr;
m_lit_watch[1] = nullptr;

4
src/smt/theory_seq.cpp
View file

@ -1120,7 +1120,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
break;
}
if (flag) {
expr* nl_fst = 0;
expr* nl_fst = nullptr;
if (e.rs().size()>1 && is_var(e.rs().get(0)))
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst) {
@ -1173,7 +1173,7 @@ bool theory_seq::find_better_rep(expr_ref_vector const& ls, expr_ref_vector cons
break;
}
if (flag) {
expr* nl_fst = 0;
expr* nl_fst = nullptr;
if (e.rs().size()>1 && is_var(e.rs().get(0)))
nl_fst = e.rs().get(0);
if (nl_fst && nl_fst != r_fst) {

26
src/smt/theory_str.cpp
View file

@ -6745,8 +6745,8 @@ namespace smt {
}
unsigned theory_str::estimate_automata_intersection_difficulty(eautomaton * aut1, eautomaton * aut2) {
ENSURE(aut1 != NULL);
ENSURE(aut2 != NULL);
ENSURE(aut1 != nullptr);
ENSURE(aut2 != nullptr);
return _qmul(aut1->num_states(), aut2->num_states());
}
@ -6999,7 +6999,7 @@ namespace smt {
* and the equality with 0 is based on whether solutions of length 0 are allowed.
*/
void theory_str::find_automaton_initial_bounds(expr * str_in_re, eautomaton * aut) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
context & ctx = get_context();
ast_manager & m = get_manager();
@ -7051,7 +7051,7 @@ namespace smt {
* if it exists, or -1 otherwise.
*/
bool theory_str::refine_automaton_lower_bound(eautomaton * aut, rational current_lower_bound, rational & refined_lower_bound) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
if (aut->final_states().size() < 1) {
// no solutions at all
@ -7161,7 +7161,7 @@ namespace smt {
* if a shorter solution exists, or -1 otherwise.
*/
bool theory_str::refine_automaton_upper_bound(eautomaton * aut, rational current_upper_bound, rational & refined_upper_bound) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
if (aut->final_states().empty()) {
// no solutions at all!
@ -7280,7 +7280,7 @@ namespace smt {
return retval;
} else {
TRACE("str", tout << "ERROR: unrecognized automaton path constraint " << mk_pp(cond, m) << ", cannot translate" << std::endl;);
retval = NULL;
retval = nullptr;
return retval;
}
}
@ -7293,7 +7293,7 @@ namespace smt {
* are returned in `characterConstraints`.
*/
expr_ref theory_str::generate_regex_path_constraints(expr * stringTerm, eautomaton * aut, rational lenVal, expr_ref & characterConstraints) {
ENSURE(aut != NULL);
ENSURE(aut != nullptr);
context & ctx = get_context();
ast_manager & m = get_manager();
@ -10582,12 +10582,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);
@ -10637,7 +10637,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;);
@ -10668,7 +10668,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)) {
@ -10686,7 +10686,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);
@ -12231,7 +12231,7 @@ namespace smt {
// - in the same EQC as freeVar
if (term_appears_as_subterm(freeVar, re_str)) {
TRACE("str", tout << "prevent value testing on free var " << mk_pp(freeVar, m) << " as it belongs to one or more regex constraints." << std::endl;);
return NULL;
return nullptr;
}
}
}

2
src/smt/theory_str.h
View file

@ -164,7 +164,7 @@ protected:
rational upper_bound;
public:
regex_automaton_under_assumptions() :
re_term(NULL), aut(NULL), polarity(false),
re_term(nullptr), aut(nullptr), polarity(false),
assume_lower_bound(false), assume_upper_bound(false) {}
regex_automaton_under_assumptions(expr * re_term, eautomaton * aut, bool polarity) :