mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

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

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2018-04-05 20:28:44 +01:00
commit b0492659d6
816 changed files with 9880 additions and 10461 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/act_cache.cpp
View file

@ -187,8 +187,8 @@ void act_cache::insert(expr * k, expr * v) {
*/
expr * act_cache::find(expr * k) {
map::key_value * entry = m_table.find_core(k);
if (entry == 0)
return 0;
if (entry == nullptr)
return nullptr;
if (GET_TAG(entry->m_value) == 0) {
entry->m_value = TAG(expr*, entry->m_value, 1);
SASSERT(GET_TAG(entry->m_value) == 1);

114
src/ast/arith_decl_plugin.cpp
View file

@ -65,7 +65,7 @@ struct arith_decl_plugin::algebraic_numbers_wrapper {
};
arith_decl_plugin::algebraic_numbers_wrapper & arith_decl_plugin::aw() const {
if (m_aw == 0)
if (m_aw == nullptr)
const_cast<arith_decl_plugin*>(this)->m_aw = alloc(algebraic_numbers_wrapper, m_manager->limit());
return *m_aw;
}
@ -100,7 +100,7 @@ app * arith_decl_plugin::mk_numeral(sexpr const * p, unsigned i) {
void arith_decl_plugin::del(parameter const & p) {
SASSERT(p.is_external());
if (m_aw != 0) {
if (m_aw != nullptr) {
aw().recycle_id(p.get_ext_id());
}
}
@ -222,56 +222,56 @@ void arith_decl_plugin::set_manager(ast_manager * m, family_id id) {
}
arith_decl_plugin::arith_decl_plugin():
m_aw(0),
m_aw(nullptr),
m_intv_sym("Int"),
m_realv_sym("Real"),
m_rootv_sym("RootObject"),
m_real_decl(0),
m_int_decl(0),
m_r_le_decl(0),
m_r_ge_decl(0),
m_r_lt_decl(0),
m_r_gt_decl(0),
m_r_add_decl(0),
m_r_sub_decl(0),
m_r_uminus_decl(0),
m_r_mul_decl(0),
m_r_div_decl(0),
m_i_le_decl(0),
m_i_ge_decl(0),
m_i_lt_decl(0),
m_i_gt_decl(0),
m_i_add_decl(0),
m_i_sub_decl(0),
m_i_uminus_decl(0),
m_i_mul_decl(0),
m_i_div_decl(0),
m_i_mod_decl(0),
m_i_rem_decl(0),
m_to_real_decl(0),
m_to_int_decl(0),
m_is_int_decl(0),
m_r_power_decl(0),
m_i_power_decl(0),
m_r_abs_decl(0),
m_i_abs_decl(0),
m_sin_decl(0),
m_cos_decl(0),
m_tan_decl(0),
m_asin_decl(0),
m_acos_decl(0),
m_atan_decl(0),
m_sinh_decl(0),
m_cosh_decl(0),
m_tanh_decl(0),
m_asinh_decl(0),
m_acosh_decl(0),
m_atanh_decl(0),
m_pi(0),
m_e(0),
m_neg_root_decl(0),
m_u_asin_decl(0),
m_u_acos_decl(0),
m_real_decl(nullptr),
m_int_decl(nullptr),
m_r_le_decl(nullptr),
m_r_ge_decl(nullptr),
m_r_lt_decl(nullptr),
m_r_gt_decl(nullptr),
m_r_add_decl(nullptr),
m_r_sub_decl(nullptr),
m_r_uminus_decl(nullptr),
m_r_mul_decl(nullptr),
m_r_div_decl(nullptr),
m_i_le_decl(nullptr),
m_i_ge_decl(nullptr),
m_i_lt_decl(nullptr),
m_i_gt_decl(nullptr),
m_i_add_decl(nullptr),
m_i_sub_decl(nullptr),
m_i_uminus_decl(nullptr),
m_i_mul_decl(nullptr),
m_i_div_decl(nullptr),
m_i_mod_decl(nullptr),
m_i_rem_decl(nullptr),
m_to_real_decl(nullptr),
m_to_int_decl(nullptr),
m_is_int_decl(nullptr),
m_r_power_decl(nullptr),
m_i_power_decl(nullptr),
m_r_abs_decl(nullptr),
m_i_abs_decl(nullptr),
m_sin_decl(nullptr),
m_cos_decl(nullptr),
m_tan_decl(nullptr),
m_asin_decl(nullptr),
m_acos_decl(nullptr),
m_atan_decl(nullptr),
m_sinh_decl(nullptr),
m_cosh_decl(nullptr),
m_tanh_decl(nullptr),
m_asinh_decl(nullptr),
m_acosh_decl(nullptr),
m_atanh_decl(nullptr),
m_pi(nullptr),
m_e(nullptr),
m_neg_root_decl(nullptr),
m_u_asin_decl(nullptr),
m_u_acos_decl(nullptr),
m_convert_int_numerals_to_real(false) {
}
@ -335,7 +335,7 @@ sort * arith_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
switch (k) {
case REAL_SORT: return m_real_decl;
case INT_SORT: return m_int_decl;
default: return 0;
default: return nullptr;
}
}
@ -380,7 +380,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) {
//case OP_MOD_0: return m_mod_0_decl;
case OP_U_ASIN: return m_u_asin_decl;
case OP_U_ACOS: return m_u_acos_decl;
default: return 0;
default: return nullptr;
}
}
@ -408,7 +408,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
if (u_val < MAX_SMALL_NUM_TO_CACHE) {
if (is_int && !m_convert_int_numerals_to_real) {
app * r = m_small_ints.get(u_val, 0);
if (r == 0) {
if (r == nullptr) {
parameter p[2] = { parameter(val), parameter(1) };
r = m_manager->mk_const(m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
m_manager->inc_ref(r);
@ -418,7 +418,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
}
else {
app * r = m_small_reals.get(u_val, 0);
if (r == 0) {
if (r == nullptr) {
parameter p[2] = { parameter(val), parameter(0) };
r = m_manager->mk_const(m_manager->mk_const_decl(m_realv_sym, m_real_decl, func_decl_info(m_family_id, OP_NUM, 2, p)));
m_manager->inc_ref(r);
@ -440,7 +440,7 @@ app * arith_decl_plugin::mk_numeral(rational const & val, bool is_int) {
func_decl * arith_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity) {
if (!(num_parameters == 2 && arity == 0 && parameters[0].is_rational() && parameters[1].is_int())) {
m_manager->raise_exception("invalid numeral declaration");
return 0;
return nullptr;
}
if (parameters[1].get_int() != 0)
return m_manager->mk_const_decl(m_intv_sym, m_int_decl, func_decl_info(m_family_id, OP_NUM, num_parameters, parameters));
@ -480,7 +480,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_num_decl(num_parameters, parameters, arity);
if (arity == 0 && !is_const_op(k)) {
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
return nullptr;
}
if (m_manager->int_real_coercions() && use_coercion(k)) {
return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl));
@ -497,7 +497,7 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
return mk_num_decl(num_parameters, parameters, num_args);
if (num_args == 0 && !is_const_op(k)) {
m_manager->raise_exception("no arguments supplied to arithmetical operator");
return 0;
return nullptr;
}
if (m_manager->int_real_coercions() && use_coercion(k)) {
return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl));
@ -641,7 +641,7 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
arith_util::arith_util(ast_manager & m):
arith_recognizers(m.mk_family_id("arith")),
m_manager(m),
m_plugin(0) {
m_plugin(nullptr) {
}
void arith_util::init_plugin() {

38
src/ast/arith_decl_plugin.h
View file

@ -145,7 +145,7 @@ protected:
bool m_convert_int_numerals_to_real;
func_decl * mk_func_decl(decl_kind k, bool is_real);
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
decl_kind fix_kind(decl_kind k, unsigned arity);
void check_arity(unsigned arity, unsigned expected_arity);
func_decl * mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity);
@ -153,38 +153,38 @@ protected:
public:
arith_decl_plugin();
virtual ~arith_decl_plugin();
virtual void finalize();
~arith_decl_plugin() override;
void finalize() override;
algebraic_numbers::manager & am() const;
algebraic_numbers_wrapper & aw() const;
virtual void del(parameter const & p);
virtual parameter translate(parameter const & p, decl_plugin & target);
void del(parameter const & p) override;
parameter translate(parameter const & p, decl_plugin & target) override;
virtual decl_plugin * mk_fresh() {
decl_plugin * mk_fresh() override {
return alloc(arith_decl_plugin);
}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) override;
virtual bool is_value(app * e) const;
bool is_value(app * e) const override;
virtual bool is_unique_value(app * e) const;
bool is_unique_value(app * e) const override;
virtual bool are_equal(app * a, app * b) const;
bool are_equal(app * a, app * b) const override;
virtual bool are_distinct(app * a, app * b) const;
bool are_distinct(app * a, app * b) const override;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
app * mk_numeral(rational const & n, bool is_int);
@ -197,9 +197,9 @@ public:
app * mk_e() const { return m_e; }
virtual expr * get_some_value(sort * s);
expr * get_some_value(sort * s) override;
virtual bool is_considered_uninterpreted(func_decl * f) {
bool is_considered_uninterpreted(func_decl * f) override {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind())

82
src/ast/array_decl_plugin.cpp
View file

@ -44,7 +44,7 @@ sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
if (k == _SET_SORT) {
if (num_parameters != 1) {
m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
return 0;
return nullptr;
}
parameter params[2] = { parameters[0], parameter(m_manager->mk_bool_sort()) };
return mk_sort(ARRAY_SORT, 2, params);
@ -52,13 +52,13 @@ sort * array_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, paramete
SASSERT(k == ARRAY_SORT);
if (num_parameters < 2) {
m_manager->raise_exception("invalid array sort definition, invalid number of parameters");
return 0;
return nullptr;
}
for (unsigned i = 0; i < num_parameters; i++) {
if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) {
m_manager->raise_exception("invalid array sort definition, parameter is not a sort");
return 0;
return nullptr;
}
}
sort * range = to_sort(parameters[num_parameters - 1].get_ast());
@ -120,15 +120,15 @@ bool array_decl_plugin::is_array_sort(sort* s) const {
func_decl * array_decl_plugin::mk_const(sort * s, unsigned arity, sort * const * domain) {
if (arity != 1) {
m_manager->raise_exception("invalid const array definition, invalid domain size");
return 0;
return nullptr;
}
if (!is_array_sort(s)) {
m_manager->raise_exception("invalid const array definition, parameter is not an array sort");
return 0;
return nullptr;
}
if (!m_manager->compatible_sorts(get_array_range(s), domain[0])) {
m_manager->raise_exception("invalid const array definition, sort mismatch between array range and argument");
return 0;
return nullptr;
}
parameter param(s);
func_decl_info info(m_family_id, OP_CONST_ARRAY, 1, &param);
@ -142,11 +142,11 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
buffer << "map expects to take as many arguments as the function being mapped, "
<< "it was given " << arity << " but expects " << f->get_arity();
m_manager->raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
if (arity == 0) {
m_manager->raise_exception("don't use map on constants");
return 0;
return nullptr;
}
//
// check that each domain[i] is an array sort
@ -159,14 +159,14 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
std::ostringstream buffer;
buffer << "map expects an array sort as argument at position " << i;
m_manager->raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
if (get_array_arity(domain[i]) != dom_arity) {
std::ostringstream buffer;
buffer << "map expects all arguments to have the same array domain, "
<< "this is not the case for argument " << i;
m_manager->raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
for (unsigned j = 0; j < dom_arity; ++j) {
if (get_array_domain(domain[i],j) != get_array_domain(domain[0],j)) {
@ -174,7 +174,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
buffer << "map expects all arguments to have the same array domain, "
<< "this is not the case for argument " << i;
m_manager->raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
}
if (get_array_range(domain[i]) != f->get_domain(i)) {
@ -182,7 +182,7 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
buffer << "map expects the argument at position " << i
<< " to have the array range the same as the function";
m_manager->raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
}
vector<parameter> parameters;
@ -211,19 +211,19 @@ func_decl * array_decl_plugin::mk_map(func_decl* f, unsigned arity, sort* const*
func_decl * array_decl_plugin::mk_default(unsigned domain_size, sort * const * domain) {
if (domain_size != 1) {
m_manager->raise_exception("invalid default array definition, invalid domain size");
return 0;
return nullptr;
}
// check that domain[0] is an array sort.
unsigned num_parameters = domain[0]->get_num_parameters();
if (num_parameters <= 1) {
m_manager->raise_exception("parameter mismatch. There should be more than one parameter to defaults");
return 0;
return nullptr;
}
parameter param(domain[0]->get_parameter(num_parameters-1));
if (!param.is_ast() || !is_sort(param.get_ast())) {
m_manager->raise_exception("last parameter should be a sort");
return 0;
return nullptr;
}
sort * s = to_sort(param.get_ast());
@ -235,7 +235,7 @@ func_decl * array_decl_plugin::mk_default(unsigned domain_size, sort * const * d
func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
if (arity <= 1) {
m_manager->raise_exception("select takes at least two arguments");
return 0;
return nullptr;
}
sort * s = domain[0];
unsigned num_parameters = s->get_num_parameters();
@ -245,7 +245,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
std::stringstream strm;
strm << "select requires " << num_parameters << " arguments, but was provided with " << arity << " arguments";
m_manager->raise_exception(strm.str().c_str());
return 0;
return nullptr;
}
ptr_buffer<sort> new_domain; // we need this because of coercions.
new_domain.push_back(s);
@ -255,7 +255,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
!m_manager->compatible_sorts(domain[i+1], to_sort(parameters[i].get_ast()))) {
m_manager->raise_exception("domain sort and parameter do not match");
UNREACHABLE();
return 0;
return nullptr;
}
new_domain.push_back(to_sort(parameters[i].get_ast()));
}
@ -267,7 +267,7 @@ func_decl* array_decl_plugin::mk_select(unsigned arity, sort * const * domain) {
func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
if (arity < 3) {
m_manager->raise_exception("store takes at least 3 arguments");
return 0;
return nullptr;
}
sort * s = domain[0];
unsigned num_parameters = s->get_num_parameters();
@ -275,7 +275,7 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
if (!is_array_sort(s)) {
m_manager->raise_exception("store expects the first argument sort to be an array");
UNREACHABLE();
return 0;
return nullptr;
}
if (arity != num_parameters+1) {
std::ostringstream buffer;
@ -283,19 +283,19 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
<< ", instead it was passed " << (arity - 1) << "arguments";
m_manager->raise_exception(buffer.str().c_str());
UNREACHABLE();
return 0;
return nullptr;
}
ptr_buffer<sort> new_domain; // we need this because of coercions.
new_domain.push_back(s);
for (unsigned i = 0; i < num_parameters; ++i) {
if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) {
m_manager->raise_exception("expecting sort parameter");
return 0;
return nullptr;
}
if (!m_manager->compatible_sorts(to_sort(parameters[i].get_ast()), domain[i+1])) {
m_manager->raise_exception("domain sort and parameter do not match");
UNREACHABLE();
return 0;
return nullptr;
}
new_domain.push_back(to_sort(parameters[i].get_ast()));
}
@ -307,13 +307,13 @@ func_decl * array_decl_plugin::mk_store(unsigned arity, sort * const * domain) {
func_decl * array_decl_plugin::mk_array_ext(unsigned arity, sort * const * domain, unsigned i) {
if (arity != 2 || domain[0] != domain[1]) {
UNREACHABLE();
return 0;
return nullptr;
}
sort * s = domain[0];
unsigned num_parameters = s->get_num_parameters();
if (num_parameters == 0 || i >= num_parameters - 1) {
UNREACHABLE();
return 0;
return nullptr;
}
sort * r = to_sort(s->get_parameter(i).get_ast());
parameter param(i);
@ -362,11 +362,11 @@ func_decl * array_decl_plugin::mk_set_union(unsigned arity, sort * const * domai
if (arity == 0) {
m_manager->raise_exception("union takes at least one argument");
return 0;
return nullptr;
}
sort * s = domain[0];
if (!check_set_arguments(arity, domain)) {
return 0;
return nullptr;
}
parameter param(s);
func_decl_info info(m_family_id, OP_SET_UNION, 1, &param);
@ -381,10 +381,10 @@ func_decl * array_decl_plugin::mk_set_intersect(unsigned arity, sort * const * d
if (arity == 0) {
m_manager->raise_exception("intersection takes at least one argument");
return 0;
return nullptr;
}
if (!check_set_arguments(arity, domain)) {
return 0;
return nullptr;
}
func_decl_info info(m_family_id, OP_SET_INTERSECT);
info.set_associative();
@ -397,10 +397,10 @@ func_decl * array_decl_plugin::mk_set_intersect(unsigned arity, sort * const * d
func_decl * array_decl_plugin::mk_set_difference(unsigned arity, sort * const * domain) {
if (arity != 2) {
m_manager->raise_exception("set difference takes precisely two arguments");
return 0;
return nullptr;
}
if (!check_set_arguments(arity, domain)) {
return 0;
return nullptr;
}
return m_manager->mk_func_decl(m_set_difference_sym, arity, domain, domain[0],
func_decl_info(m_family_id, OP_SET_DIFFERENCE));
@ -409,10 +409,10 @@ func_decl * array_decl_plugin::mk_set_difference(unsigned arity, sort * const *
func_decl * array_decl_plugin::mk_set_complement(unsigned arity, sort * const * domain) {
if (arity != 1) {
m_manager->raise_exception("set complement takes one argument");
return 0;
return nullptr;
}
if (!check_set_arguments(arity, domain)) {
return 0;
return nullptr;
}
return m_manager->mk_func_decl(m_set_complement_sym, arity, domain, domain[0],
func_decl_info(m_family_id, OP_SET_COMPLEMENT));
@ -421,10 +421,10 @@ func_decl * array_decl_plugin::mk_set_complement(unsigned arity, sort * const *
func_decl * array_decl_plugin::mk_set_subset(unsigned arity, sort * const * domain) {
if (arity != 2) {
m_manager->raise_exception("subset takes two arguments");
return 0;
return nullptr;
}
if (!check_set_arguments(arity, domain)) {
return 0;
return nullptr;
}
sort * bool_sort = m_manager->mk_bool_sort();
return m_manager->mk_func_decl(m_set_subset_sym, arity, domain, bool_sort,
@ -456,20 +456,20 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
sort * s = to_sort(parameters[0].get_ast());
return mk_const(s, arity, domain);
}
else if (range != 0) {
else if (range != nullptr) {
return mk_const(range, arity, domain);
}
else {
m_manager->raise_exception("array operation requires one sort parameter (the array sort)");
UNREACHABLE();
return 0;
return nullptr;
}
}
case OP_ARRAY_MAP: {
if (num_parameters != 1 || !parameters[0].is_ast() || !is_func_decl(parameters[0].get_ast())) {
m_manager->raise_exception("array operation requires one function declaration parameter (the function to be mapped)");
UNREACHABLE();
return 0;
return nullptr;
}
func_decl * f = to_func_decl(parameters[0].get_ast());
return mk_map(f, arity, domain);
@ -480,7 +480,7 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
}
if (num_parameters != 1 || !parameters[0].is_int()) {
UNREACHABLE();
return 0;
return nullptr;
}
return mk_array_ext(arity, domain, parameters[0].get_int());
case OP_ARRAY_DEFAULT:
@ -506,12 +506,12 @@ func_decl * array_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
tout << "as-array-bug: " << to_func_decl(parameters[0].get_ast())->get_name() << " " << to_func_decl(parameters[0].get_ast())->get_arity() << std::endl;);
m_manager->raise_exception("as-array takes one parameter, a function declaration with arity greater than zero");
UNREACHABLE();
return 0;
return nullptr;
}
func_decl * f = to_func_decl(parameters[0].get_ast());
return mk_as_array(f);
}
default: return 0;
default: return nullptr;
}
}

24
src/ast/array_decl_plugin.h
View file

@ -98,9 +98,9 @@ class array_decl_plugin : public decl_plugin {
bool is_array_sort(sort* s) const;
public:
array_decl_plugin();
virtual ~array_decl_plugin() {}
~array_decl_plugin() override {}
virtual decl_plugin * mk_fresh() {
decl_plugin * mk_fresh() override {
return alloc(array_decl_plugin);
}
@ -111,23 +111,23 @@ class array_decl_plugin : public decl_plugin {
// parameters[n-1] - nth dimension
// parameters[n] - range
//
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
//
// Contract for func_decl:
// parameters[0] - array sort
// Contract for others:
// no parameters
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
virtual expr * get_some_value(sort * s);
expr * get_some_value(sort * s) override;
virtual bool is_fully_interp(sort * s) const;
bool is_fully_interp(sort * s) const override;
};
class array_recognizers {
@ -161,11 +161,11 @@ public:
bool is_as_array_tree(expr * n);
app * mk_store(unsigned num_args, expr * const * args) {
return m_manager.mk_app(m_fid, OP_STORE, 0, 0, num_args, args);
return m_manager.mk_app(m_fid, OP_STORE, 0, nullptr, num_args, args);
}
app * mk_select(unsigned num_args, expr * const * args) {
return m_manager.mk_app(m_fid, OP_SELECT, 0, 0, num_args, args);
return m_manager.mk_app(m_fid, OP_SELECT, 0, nullptr, num_args, args);
}
app * mk_map(func_decl * f, unsigned num_args, expr * const * args) {
@ -191,7 +191,7 @@ public:
app * mk_as_array(func_decl * f) {
parameter param(f);
return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, 0, 0);
return m_manager.mk_app(m_fid, OP_AS_ARRAY, 1, &param, 0, nullptr, nullptr);
}
};

310
src/ast/ast.cpp
View file

@ -405,7 +405,7 @@ sort * get_sort(expr const * n) {
break;
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
}
@ -434,18 +434,18 @@ bool compare_nodes(ast const * n1, ast const * n2) {
}
switch (n1->get_kind()) {
case AST_SORT:
if ((to_sort(n1)->get_info() == 0) != (to_sort(n2)->get_info() == 0)) {
if ((to_sort(n1)->get_info() == nullptr) != (to_sort(n2)->get_info() == nullptr)) {
return false;
}
if (to_sort(n1)->get_info() != 0 && !(*to_sort(n1)->get_info() == *to_sort(n2)->get_info())) {
if (to_sort(n1)->get_info() != nullptr && !(*to_sort(n1)->get_info() == *to_sort(n2)->get_info())) {
return false;
}
return to_sort(n1)->get_name() == to_sort(n2)->get_name();
case AST_FUNC_DECL:
if ((to_func_decl(n1)->get_info() == 0) != (to_func_decl(n2)->get_info() == 0)) {
if ((to_func_decl(n1)->get_info() == nullptr) != (to_func_decl(n2)->get_info() == nullptr)) {
return false;
}
if (to_func_decl(n1)->get_info() != 0 && !(*to_func_decl(n1)->get_info() == *to_func_decl(n2)->get_info())) {
if (to_func_decl(n1)->get_info() != nullptr && !(*to_func_decl(n1)->get_info() == *to_func_decl(n2)->get_info())) {
return false;
}
return
@ -549,13 +549,13 @@ unsigned get_node_hash(ast const * n) {
switch (n->get_kind()) {
case AST_SORT:
if (to_sort(n)->get_info() == 0)
if (to_sort(n)->get_info() == nullptr)
return to_sort(n)->get_name().hash();
else
return combine_hash(to_sort(n)->get_name().hash(), to_sort(n)->get_info()->hash());
case AST_FUNC_DECL:
return ast_array_hash(to_func_decl(n)->get_domain(), to_func_decl(n)->get_arity(),
to_func_decl(n)->get_info() == 0 ?
to_func_decl(n)->get_info() == nullptr ?
to_func_decl(n)->get_name().hash() : combine_hash(to_func_decl(n)->get_name().hash(), to_func_decl(n)->get_info()->hash()));
case AST_APP:
return ast_array_hash(to_app(n)->get_args(),
@ -587,13 +587,13 @@ void ast_table::erase(ast * n) {
unsigned idx = h & mask;
cell * c = m_table + idx;
SASSERT(!c->is_free());
cell * prev = 0;
cell * prev = nullptr;
while (true) {
if (c->m_data == n) {
m_size--;
if (prev == 0) {
if (prev == nullptr) {
cell * next = c->m_next;
if (next == 0) {
if (next == nullptr) {
m_used_slots--;
c->mark_free();
SASSERT(c->is_free());
@ -638,49 +638,48 @@ func_decl * decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, para
// -----------------------------------
basic_decl_plugin::basic_decl_plugin():
m_bool_sort(0),
m_true_decl(0),
m_false_decl(0),
m_and_decl(0),
m_or_decl(0),
m_iff_decl(0),
m_xor_decl(0),
m_not_decl(0),
m_interp_decl(0),
m_implies_decl(0),
m_bool_sort(nullptr),
m_true_decl(nullptr),
m_false_decl(nullptr),
m_and_decl(nullptr),
m_or_decl(nullptr),
m_iff_decl(nullptr),
m_xor_decl(nullptr),
m_not_decl(nullptr),
m_interp_decl(nullptr),
m_implies_decl(nullptr),
m_proof_sort(0),
m_undef_decl(0),
m_true_pr_decl(0),
m_asserted_decl(0),
m_goal_decl(0),
m_modus_ponens_decl(0),
m_reflexivity_decl(0),
m_symmetry_decl(0),
m_transitivity_decl(0),
m_quant_intro_decl(0),
m_and_elim_decl(0),
m_not_or_elim_decl(0),
m_rewrite_decl(0),
m_pull_quant_decl(0),
m_pull_quant_star_decl(0),
m_push_quant_decl(0),
m_elim_unused_vars_decl(0),
m_der_decl(0),
m_quant_inst_decl(0),
m_proof_sort(nullptr),
m_undef_decl(nullptr),
m_true_pr_decl(nullptr),
m_asserted_decl(nullptr),
m_goal_decl(nullptr),
m_modus_ponens_decl(nullptr),
m_reflexivity_decl(nullptr),
m_symmetry_decl(nullptr),
m_transitivity_decl(nullptr),
m_quant_intro_decl(nullptr),
m_and_elim_decl(nullptr),
m_not_or_elim_decl(nullptr),
m_rewrite_decl(nullptr),
m_pull_quant_decl(nullptr),
m_push_quant_decl(nullptr),
m_elim_unused_vars_decl(nullptr),
m_der_decl(nullptr),
m_quant_inst_decl(nullptr),
m_hypothesis_decl(0),
m_iff_true_decl(0),
m_iff_false_decl(0),
m_commutativity_decl(0),
m_def_axiom_decl(0),
m_lemma_decl(0),
m_hypothesis_decl(nullptr),
m_iff_true_decl(nullptr),
m_iff_false_decl(nullptr),
m_commutativity_decl(nullptr),
m_def_axiom_decl(nullptr),
m_lemma_decl(nullptr),
m_def_intro_decl(0),
m_iff_oeq_decl(0),
m_skolemize_decl(0),
m_mp_oeq_decl(0),
m_hyper_res_decl0(0) {
m_def_intro_decl(nullptr),
m_iff_oeq_decl(nullptr),
m_skolemize_decl(nullptr),
m_mp_oeq_decl(nullptr),
m_hyper_res_decl0(nullptr) {
}
bool basic_decl_plugin::check_proof_sorts(basic_op_kind k, unsigned arity, sort * const * domain) const {
@ -790,7 +789,7 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_param
}
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
@ -827,7 +826,6 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_REWRITE: return mk_proof_decl("rewrite", k, 0, m_rewrite_decl);
case PR_REWRITE_STAR: return mk_proof_decl("rewrite*", k, num_parents, m_rewrite_star_decls);
case PR_PULL_QUANT: return mk_proof_decl("pull-quant", k, 0, m_pull_quant_decl);
case PR_PULL_QUANT_STAR: return mk_proof_decl("pull-quant*", k, 0, m_pull_quant_star_decl);
case PR_PUSH_QUANT: return mk_proof_decl("push-quant", k, 0, m_push_quant_decl);
case PR_ELIM_UNUSED_VARS: return mk_proof_decl("elim-unused", k, 0, m_elim_unused_vars_decl);
case PR_DER: return mk_proof_decl("der", k, 0, m_der_decl);
@ -844,15 +842,13 @@ func_decl * basic_decl_plugin::mk_proof_decl(basic_op_kind k, unsigned num_paren
case PR_IFF_OEQ: return mk_proof_decl("iff~", k, 1, m_iff_oeq_decl);
case PR_NNF_POS: return mk_proof_decl("nnf-pos", k, num_parents, m_nnf_pos_decls);
case PR_NNF_NEG: return mk_proof_decl("nnf-neg", k, num_parents, m_nnf_neg_decls);
case PR_NNF_STAR: return mk_proof_decl("nnf*", k, num_parents, m_nnf_star_decls);
case PR_CNF_STAR: return mk_proof_decl("cnf*", k, num_parents, m_cnf_star_decls);
case PR_SKOLEMIZE: return mk_proof_decl("sk", k, 0, m_skolemize_decl);
case PR_MODUS_PONENS_OEQ: return mk_proof_decl("mp~", k, 2, m_mp_oeq_decl);
case PR_TH_LEMMA: return mk_proof_decl("th-lemma", k, num_parents, m_th_lemma_decls);
case PR_HYPER_RESOLVE: return mk_proof_decl("hyper-res", k, num_parents, m_hyper_res_decl0);
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
@ -949,7 +945,6 @@ void basic_decl_plugin::finalize() {
DEC_REF(m_not_or_elim_decl);
DEC_REF(m_rewrite_decl);
DEC_REF(m_pull_quant_decl);
DEC_REF(m_pull_quant_star_decl);
DEC_REF(m_push_quant_decl);
DEC_REF(m_elim_unused_vars_decl);
DEC_REF(m_der_decl);
@ -975,8 +970,6 @@ void basic_decl_plugin::finalize() {
DEC_ARRAY_REF(m_apply_def_decls);
DEC_ARRAY_REF(m_nnf_pos_decls);
DEC_ARRAY_REF(m_nnf_neg_decls);
DEC_ARRAY_REF(m_nnf_star_decls);
DEC_ARRAY_REF(m_cnf_star_decls);
DEC_ARRAY_REF(m_th_lemma_decls);
DEC_REF(m_hyper_res_decl0);
@ -1067,10 +1060,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
case OP_ITE: return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : 0;
case OP_ITE: return arity == 3 ? mk_ite_decl(join(domain[1], domain[2])) : nullptr;
// eq and oeq must have at least two arguments, they can have more since they are chainable
case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(arity, domain), m_eq_decls) : 0;
case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(arity, domain), m_oeq_decls) : 0;
case OP_EQ: return arity >= 2 ? mk_eq_decl_core("=", OP_EQ, join(arity, domain), m_eq_decls) : nullptr;
case OP_OEQ: return arity >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(arity, domain), m_oeq_decls) : nullptr;
case OP_DISTINCT: {
func_decl_info info(m_family_id, OP_DISTINCT);
info.set_pairwise();
@ -1110,10 +1103,10 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
case OP_IFF: return m_iff_decl;
case OP_IMPLIES: return m_implies_decl;
case OP_XOR: return m_xor_decl;
case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): 0;
case OP_ITE: return num_args == 3 ? mk_ite_decl(join(m_manager->get_sort(args[1]), m_manager->get_sort(args[2]))): nullptr;
// eq and oeq must have at least two arguments, they can have more since they are chainable
case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(num_args, args), m_eq_decls) : 0;
case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : 0;
case OP_EQ: return num_args >= 2 ? mk_eq_decl_core("=", OP_EQ, join(num_args, args), m_eq_decls) : nullptr;
case OP_OEQ: return num_args >= 2 ? mk_eq_decl_core("~", OP_OEQ, join(num_args, args), m_oeq_decls) : nullptr;
case OP_DISTINCT:
return decl_plugin::mk_func_decl(k, num_parameters, parameters, num_args, args, range);
default:
@ -1134,7 +1127,7 @@ func_decl * basic_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
expr * basic_decl_plugin::get_some_value(sort * s) {
if (s == m_bool_sort)
return m_manager->mk_false();
return 0;
return nullptr;
}
bool basic_recognizers::is_ite(expr const * n, expr * & t1, expr * & t2, expr * & t3) const {
@ -1168,7 +1161,7 @@ void label_decl_plugin::set_manager(ast_manager * m, family_id id) {
sort * label_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
UNREACHABLE();
return 0;
return nullptr;
}
func_decl * label_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -1176,12 +1169,12 @@ func_decl * label_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
if (k == OP_LABEL) {
if (arity != 1 || num_parameters < 2 || !parameters[0].is_int() || !parameters[1].is_symbol() || !m_manager->is_bool(domain[0])) {
m_manager->raise_exception("invalid label declaration");
return 0;
return nullptr;
}
for (unsigned i = 2; i < num_parameters; i++) {
if (!parameters[i].is_symbol()) {
m_manager->raise_exception("invalid label declaration");
return 0;
return nullptr;
}
}
return m_manager->mk_func_decl(parameters[0].get_int() ? m_lblpos : m_lblneg, arity, domain, domain[0],
@ -1191,15 +1184,15 @@ func_decl * label_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
SASSERT(k == OP_LABEL_LIT);
if (arity != 0) {
m_manager->raise_exception("invalid label literal declaration");
return 0;
return nullptr;
}
for (unsigned i = 0; i < num_parameters; i++) {
if (!parameters[i].is_symbol()) {
m_manager->raise_exception("invalid label literal declaration");
return 0;
return nullptr;
}
}
return m_manager->mk_func_decl(m_lbllit, 0, static_cast<sort * const *>(0), m_manager->mk_bool_sort(),
return m_manager->mk_func_decl(m_lbllit, 0, static_cast<sort * const *>(nullptr), m_manager->mk_bool_sort(),
func_decl_info(m_family_id, OP_LABEL_LIT, num_parameters, parameters));
}
}
@ -1212,7 +1205,7 @@ func_decl * label_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters
sort * pattern_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
UNREACHABLE();
return 0;
return nullptr;
}
func_decl * pattern_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -1230,7 +1223,7 @@ func_decl * pattern_decl_plugin::mk_func_decl(decl_kind k, unsigned num_paramete
sort * model_value_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
UNREACHABLE();
return 0;
return nullptr;
}
func_decl * model_value_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -1239,7 +1232,7 @@ func_decl * model_value_decl_plugin::mk_func_decl(decl_kind k, unsigned num_para
if (arity != 0 || num_parameters != 2 || !parameters[0].is_int() || !parameters[1].is_ast() || !is_sort(parameters[1].get_ast())) {
UNREACHABLE();
m_manager->raise_exception("invalid model value");
return 0;
return nullptr;
}
int idx = parameters[0].get_int();
sort * s = to_sort(parameters[1].get_ast());
@ -1247,7 +1240,7 @@ func_decl * model_value_decl_plugin::mk_func_decl(decl_kind k, unsigned num_para
buffer << s->get_name().bare_str() << "!val!" << idx;
func_decl_info info(m_family_id, k, num_parameters, parameters);
info.m_private_parameters = true;
return m_manager->mk_func_decl(symbol(buffer.c_str()), 0, static_cast<sort * const *>(0), s, info);
return m_manager->mk_func_decl(symbol(buffer.c_str()), 0, static_cast<sort * const *>(nullptr), s, info);
}
bool model_value_decl_plugin::is_value(app* n) const {
@ -1274,7 +1267,7 @@ sort * user_sort_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
func_decl * user_sort_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
UNREACHABLE();
return 0;
return nullptr;
}
decl_kind user_sort_plugin::register_name(symbol s) {
@ -1307,7 +1300,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
m_expr_dependency_manager(*this, m_alloc),
m_expr_dependency_array_manager(*this, m_alloc),
m_proof_mode(m),
m_trace_stream(0),
m_trace_stream(nullptr),
m_trace_stream_owner(false),
m_rec_fun(":rec-fun") {
@ -1319,7 +1312,7 @@ ast_manager::ast_manager(proof_gen_mode m, char const * trace_file, bool is_form
if (!is_format_manager)
m_format_manager = alloc(ast_manager, PGM_DISABLED, m_trace_stream, true);
else
m_format_manager = 0;
m_format_manager = nullptr;
init();
}
@ -1336,7 +1329,7 @@ ast_manager::ast_manager(proof_gen_mode m, std::fstream * trace_stream, bool is_
if (!is_format_manager)
m_format_manager = alloc(ast_manager, PGM_DISABLED, trace_stream, true);
else
m_format_manager = 0;
m_format_manager = nullptr;
init();
}
@ -1361,7 +1354,7 @@ void ast_manager::init() {
m_fresh_id = 0;
m_expr_id_gen.reset(0);
m_decl_id_gen.reset(c_first_decl_id);
m_some_value_proc = 0;
m_some_value_proc = nullptr;
m_basic_family_id = mk_family_id("basic");
m_label_family_id = mk_family_id("label");
m_pattern_family_id = mk_family_id("pattern");
@ -1427,14 +1420,14 @@ ast_manager::~ast_manager() {
switch (n->get_kind()) {
case AST_SORT: {
sort_info* info = to_sort(n)->get_info();
if (info != 0) {
if (info != nullptr) {
mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
}
break;
}
case AST_FUNC_DECL: {
func_decl_info* info = to_func_decl(n)->get_info();
if (info != 0) {
if (info != nullptr) {
mark_array_ref(mark, info->get_num_parameters(), info->get_parameters());
}
mark_array_ref(mark, to_func_decl(n)->get_arity(), to_func_decl(n)->get_domain());
@ -1476,14 +1469,14 @@ ast_manager::~ast_manager() {
delete_node(a);
}
}
if (m_format_manager != 0)
if (m_format_manager != nullptr)
dealloc(m_format_manager);
if (m_trace_stream_owner) {
std::fstream & tmp = * m_trace_stream;
tmp << "[eof]\n";
tmp.close();
dealloc(m_trace_stream);
m_trace_stream = 0;
m_trace_stream = nullptr;
}
}
@ -1532,32 +1525,39 @@ void ast_manager::copy_families_plugins(ast_manager const & from) {
tout << "fid: " << fid << " fidname: " << get_family_name(fid) << "\n";
});
ast_translation trans(const_cast<ast_manager&>(from), *this, false);
// Inheriting plugins can create new family ids. Since new family ids are
// assigned in the order that they are created, this can result in differing
// family ids. To avoid this, we first assign all family ids and only then inherit plugins.
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
symbol fid_name = from.get_family_name(fid);
TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
<< ", target has_family: " << m_family_manager.has_family(fid) << "\n";
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";);
SASSERT(fid == get_family_id(fid_name));
if (from.has_plugin(fid) && !has_plugin(fid)) {
decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
register_plugin(fid, new_p);
SASSERT(new_p->get_family_id() == fid);
SASSERT(has_plugin(fid));
}
if (from.has_plugin(fid)) {
get_plugin(fid)->inherit(from.get_plugin(fid), trans);
}
SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
SASSERT(!from.has_plugin(fid) || has_plugin(fid));
symbol fid_name = from.get_family_name(fid);
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";);
}
}
for (family_id fid = 0; from.m_family_manager.has_family(fid); fid++) {
SASSERT(from.is_builtin_family_id(fid) == is_builtin_family_id(fid));
SASSERT(!from.is_builtin_family_id(fid) || m_family_manager.has_family(fid));
symbol fid_name = from.get_family_name(fid);
(void)fid_name;
TRACE("copy_families_plugins", tout << "copying: " << fid_name << ", src fid: " << fid
<< ", target has_family: " << m_family_manager.has_family(fid) << "\n";
if (m_family_manager.has_family(fid)) tout << get_family_id(fid_name) << "\n";);
TRACE("copy_families_plugins", tout << "target fid: " << get_family_id(fid_name) << "\n";);
SASSERT(fid == get_family_id(fid_name));
if (from.has_plugin(fid) && !has_plugin(fid)) {
decl_plugin * new_p = from.get_plugin(fid)->mk_fresh();
register_plugin(fid, new_p);
SASSERT(new_p->get_family_id() == fid);
SASSERT(has_plugin(fid));
}
if (from.has_plugin(fid)) {
get_plugin(fid)->inherit(from.get_plugin(fid), trans);
}
SASSERT(from.m_family_manager.has_family(fid) == m_family_manager.has_family(fid));
SASSERT(from.get_family_id(fid_name) == get_family_id(fid_name));
SASSERT(!from.has_plugin(fid) || has_plugin(fid));
}
}
@ -1587,7 +1587,7 @@ decl_plugin * ast_manager::get_plugin(family_id fid) const {
bool ast_manager::is_value(expr* e) const {
decl_plugin const * p = 0;
decl_plugin const * p = nullptr;
if (is_app(e)) {
p = get_plugin(to_app(e)->get_family_id());
return p && p->is_value(to_app(e));
@ -1596,7 +1596,7 @@ bool ast_manager::is_value(expr* e) const {
}
bool ast_manager::is_unique_value(expr* e) const {
decl_plugin const * p = 0;
decl_plugin const * p = nullptr;
if (is_app(e)) {
p = get_plugin(to_app(e)->get_family_id());
return p && p->is_unique_value(to_app(e));
@ -1698,13 +1698,13 @@ ast * ast_manager::register_node_core(ast * n) {
// increment reference counters
switch (n->get_kind()) {
case AST_SORT:
if (to_sort(n)->m_info != 0) {
if (to_sort(n)->m_info != nullptr) {
to_sort(n)->m_info = alloc(sort_info, *(to_sort(n)->get_info()));
to_sort(n)->m_info->init_eh(*this);
}
break;
case AST_FUNC_DECL:
if (to_func_decl(n)->m_info != 0) {
if (to_func_decl(n)->m_info != nullptr) {
to_func_decl(n)->m_info = alloc(func_decl_info, *(to_func_decl(n)->get_info()));
to_func_decl(n)->m_info->init_eh(*this);
}
@ -1807,14 +1807,14 @@ void ast_manager::delete_node(ast * n) {
#endif
switch (n->get_kind()) {
case AST_SORT:
if (to_sort(n)->m_info != 0 && !m_debug_ref_count) {
if (to_sort(n)->m_info != nullptr && !m_debug_ref_count) {
sort_info * info = to_sort(n)->get_info();
info->del_eh(*this);
dealloc(info);
}
break;
case AST_FUNC_DECL:
if (to_func_decl(n)->m_info != 0 && !m_debug_ref_count) {
if (to_func_decl(n)->m_info != nullptr && !m_debug_ref_count) {
func_decl_info * info = to_func_decl(n)->get_info();
info->del_eh(*this);
dealloc(info);
@ -1849,7 +1849,7 @@ sort * ast_manager::mk_sort(family_id fid, decl_kind k, unsigned num_parameters,
decl_plugin * p = get_plugin(fid);
if (p)
return p->mk_sort(k, num_parameters, parameters);
return 0;
return nullptr;
}
func_decl * ast_manager::mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -1857,7 +1857,7 @@ func_decl * ast_manager::mk_func_decl(family_id fid, decl_kind k, unsigned num_p
decl_plugin * p = get_plugin(fid);
if (p)
return p->mk_func_decl(k, num_parameters, parameters, arity, domain, range);
return 0;
return nullptr;
}
func_decl * ast_manager::mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -1865,33 +1865,33 @@ func_decl * ast_manager::mk_func_decl(family_id fid, decl_kind k, unsigned num_p
decl_plugin * p = get_plugin(fid);
if (p)
return p->mk_func_decl(k, num_parameters, parameters, num_args, args, range);
return 0;
return nullptr;
}
app * ast_manager::mk_app(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) {
func_decl * decl = mk_func_decl(fid, k, num_parameters, parameters, num_args, args, range);
if (decl != 0)
if (decl != nullptr)
return mk_app(decl, num_args, args);
return 0;
return nullptr;
}
app * ast_manager::mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
return mk_app(fid, k, 0, 0, num_args, args);
return mk_app(fid, k, 0, nullptr, num_args, args);
}
app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg) {
return mk_app(fid, k, 0, 0, 1, &arg);
return mk_app(fid, k, 0, nullptr, 1, &arg);
}
app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2) {
expr * args[2] = { arg1, arg2 };
return mk_app(fid, k, 0, 0, 2, args);
return mk_app(fid, k, 0, nullptr, 2, args);
}
app * ast_manager::mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3) {
expr * args[3] = { arg1, arg2, arg3 };
return mk_app(fid, k, 0, 0, 3, args);
return mk_app(fid, k, 0, nullptr, 3, args);
}
sort * ast_manager::mk_sort(symbol const & name, sort_info * info) {
@ -2062,8 +2062,8 @@ bool ast_manager::coercion_needed(func_decl * decl, unsigned num_args, expr * co
}
app * ast_manager::mk_app_core(func_decl * decl, unsigned num_args, expr * const * args) {
app * r = 0;
app * new_node = 0;
app * r = nullptr;
app * new_node = nullptr;
unsigned sz = app::get_obj_size(num_args);
void * mem = allocate_node(sz);
@ -2171,7 +2171,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
<< ") passed to function " << mk_pp(decl, *this);
throw ast_exception(buffer.str().c_str());
}
app * r = 0;
app * r = nullptr;
if (num_args == 1 && decl->is_chainable() && decl->get_arity() == 2) {
r = mk_true();
}
@ -2200,7 +2200,7 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar
r = mk_and(new_args.size(), new_args.c_ptr());
}
}
if (r == 0) {
if (r == nullptr) {
r = mk_app_core(decl, num_args, args);
}
SASSERT(r != 0);
@ -2287,7 +2287,7 @@ app * ast_manager::mk_label_lit(unsigned num_names, symbol const * names) {
buffer<parameter> p;
for (unsigned i = 0; i < num_names; i++)
p.push_back(parameter(names[i]));
return mk_app(m_label_family_id, OP_LABEL_LIT, p.size(), p.c_ptr(), 0, 0);
return mk_app(m_label_family_id, OP_LABEL_LIT, p.size(), p.c_ptr(), 0, nullptr);
}
app * ast_manager::mk_label_lit(symbol const & name) {
@ -2309,7 +2309,7 @@ app * ast_manager::mk_pattern(unsigned num_exprs, app * const * exprs) {
for (unsigned i = 0; i < num_exprs; ++i) {
SASSERT(is_app(exprs[i]));
}});
return mk_app(m_pattern_family_id, OP_PATTERN, 0, 0, num_exprs, (expr*const*)exprs);
return mk_app(m_pattern_family_id, OP_PATTERN, 0, nullptr, num_exprs, (expr*const*)exprs);
}
bool ast_manager::is_pattern(expr const * n) const {
@ -2406,7 +2406,7 @@ quantifier * ast_manager::update_quantifier(quantifier * q, unsigned num_pattern
num_patterns,
patterns,
num_patterns == 0 ? q->get_num_no_patterns() : 0,
num_patterns == 0 ? q->get_no_patterns() : 0);
num_patterns == 0 ? q->get_no_patterns() : nullptr);
}
quantifier * ast_manager::update_quantifier(quantifier * q, unsigned num_patterns, expr * const * patterns, unsigned num_no_patterns, expr * const * no_patterns, expr * body) {
@ -2492,7 +2492,7 @@ quantifier * ast_manager::update_quantifier(quantifier * q, bool is_forall, unsi
num_patterns,
patterns,
num_patterns == 0 ? q->get_num_no_patterns() : 0,
num_patterns == 0 ? q->get_no_patterns() : 0);
num_patterns == 0 ? q->get_no_patterns() : nullptr);
}
app * ast_manager::mk_distinct(unsigned num_args, expr * const * args) {
@ -2524,14 +2524,14 @@ app * ast_manager::mk_distinct_expanded(unsigned num_args, expr * const * args)
// -----------------------------------
expr_dependency * ast_manager::mk_leaf(expr * t) {
if (t == 0)
return 0;
if (t == nullptr)
return nullptr;
else
return m_expr_dependency_manager.mk_leaf(t);
}
expr_dependency * ast_manager::mk_join(unsigned n, expr * const * ts) {
expr_dependency * d = 0;
expr_dependency * d = nullptr;
for (unsigned i = 0; i < n; i++)
d = mk_join(d, mk_leaf(ts[i]));
return d;
@ -2550,7 +2550,7 @@ void ast_manager::linearize(expr_dependency * d, ptr_vector<expr> & ts) {
app * ast_manager::mk_model_value(unsigned idx, sort * s) {
parameter p[2] = { parameter(idx), parameter(s) };
return mk_app(m_model_value_family_id, OP_MODEL_VALUE, 2, p, 0, static_cast<expr * const *>(0));
return mk_app(m_model_value_family_id, OP_MODEL_VALUE, 2, p, 0, static_cast<expr * const *>(nullptr));
}
expr * ast_manager::get_some_value(sort * s, some_value_proc * p) {
@ -2559,17 +2559,17 @@ expr * ast_manager::get_some_value(sort * s, some_value_proc * p) {
}
expr * ast_manager::get_some_value(sort * s) {
expr * v = 0;
expr * v = nullptr;
if (m_some_value_proc)
v = (*m_some_value_proc)(s);
if (v != 0)
if (v != nullptr)
return v;
family_id fid = s->get_family_id();
if (fid != null_family_id) {
decl_plugin * p = get_plugin(fid);
if (p != 0) {
if (p != nullptr) {
v = p->get_some_value(s);
if (v != 0)
if (v != nullptr)
return v;
}
}
@ -2582,7 +2582,7 @@ bool ast_manager::is_fully_interp(sort * s) const {
family_id fid = s->get_family_id();
SASSERT(fid != null_family_id);
decl_plugin * p = get_plugin(fid);
if (p != 0)
if (p != nullptr)
return p->is_fully_interp(s);
return false;
}
@ -2780,14 +2780,14 @@ proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proo
SASSERT(get_sort(f1) == get_sort(f2));
sort * s = get_sort(f1);
sort * d[2] = { s, s };
return mk_monotonicity(mk_func_decl(m_basic_family_id, get_eq_op(f1), 0, 0, 2, d), f1, f2, num_proofs, proofs);
return mk_monotonicity(mk_func_decl(m_basic_family_id, get_eq_op(f1), 0, nullptr, 2, d), f1, f2, num_proofs, proofs);
}
proof * ast_manager::mk_oeq_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {
SASSERT(get_sort(f1) == get_sort(f2));
sort * s = get_sort(f1);
sort * d[2] = { s, s };
return mk_monotonicity(mk_func_decl(m_basic_family_id, OP_OEQ, 0, 0, 2, d), f1, f2, num_proofs, proofs);
return mk_monotonicity(mk_func_decl(m_basic_family_id, OP_OEQ, 0, nullptr, 2, d), f1, f2, num_proofs, proofs);
}
proof * ast_manager::mk_quant_intro(quantifier * q1, quantifier * q2, proof * p) {
@ -2837,12 +2837,6 @@ proof * ast_manager::mk_pull_quant(expr * e, quantifier * q) {
return mk_app(m_basic_family_id, PR_PULL_QUANT, mk_iff(e, q));
}
proof * ast_manager::mk_pull_quant_star(expr * e, quantifier * q) {
if (proofs_disabled())
return nullptr;
return mk_app(m_basic_family_id, PR_PULL_QUANT_STAR, mk_iff(e, q));
}
proof * ast_manager::mk_push_quant(quantifier * q, expr * e) {
if (proofs_disabled())
return nullptr;
@ -3087,15 +3081,6 @@ proof * ast_manager::mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof *
return mk_app(m_basic_family_id, PR_NNF_NEG, args.size(), args.c_ptr());
}
proof * ast_manager::mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_oeq(s, t));
return mk_app(m_basic_family_id, PR_NNF_STAR, args.size(), args.c_ptr());
}
proof * ast_manager::mk_skolemization(expr * q, expr * e) {
if (proofs_disabled())
return nullptr;
@ -3104,15 +3089,6 @@ proof * ast_manager::mk_skolemization(expr * q, expr * e) {
return mk_app(m_basic_family_id, PR_SKOLEMIZE, mk_oeq(q, e));
}
proof * ast_manager::mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs) {
if (proofs_disabled())
return nullptr;
ptr_buffer<expr> args;
args.append(num_proofs, (expr**) proofs);
args.push_back(mk_oeq(s, t));
return mk_app(m_basic_family_id, PR_CNF_STAR, args.size(), args.c_ptr());
}
proof * ast_manager::mk_and_elim(proof * p, unsigned i) {
if (proofs_disabled())
return nullptr;

191
src/ast/ast.h
View file

@ -132,7 +132,7 @@ public:
case PARAM_INT: m_int = other.get_int(); break;
case PARAM_AST: m_ast = other.get_ast(); break;
case PARAM_SYMBOL: m_symbol = other.m_symbol; break;
case PARAM_RATIONAL: m_rational = 0; std::swap(m_rational, other.m_rational); break;
case PARAM_RATIONAL: m_rational = nullptr; std::swap(m_rational, other.m_rational); break;
case PARAM_DOUBLE: m_dval = other.m_dval; break;
case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break;
default:
@ -258,7 +258,7 @@ class decl_info {
public:
bool m_private_parameters;
decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind,
unsigned num_parameters = 0, parameter const * parameters = 0, bool private_params = false);
unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_params = false);
decl_info(decl_info const& other);
~decl_info() {}
@ -342,17 +342,17 @@ class sort_info : public decl_info {
sort_size m_num_elements;
public:
sort_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind,
unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false):
unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id, k, num_parameters, parameters, private_parameters) {
}
sort_info(family_id family_id, decl_kind k, uint64 num_elements,
unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false):
unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
}
sort_info(family_id family_id, decl_kind k, sort_size const& num_elements,
unsigned num_parameters = 0, parameter const * parameters = 0, bool private_parameters = false):
unsigned num_parameters = 0, parameter const * parameters = nullptr, bool private_parameters = false):
decl_info(family_id, k, num_parameters, parameters, private_parameters), m_num_elements(num_elements) {
}
sort_info(sort_info const& other) : decl_info(other), m_num_elements(other.m_num_elements) {
@ -390,7 +390,7 @@ struct func_decl_info : public decl_info {
bool m_idempotent:1;
bool m_skolem:1;
func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = 0);
func_decl_info(family_id family_id = null_family_id, decl_kind k = null_decl_kind, unsigned num_parameters = 0, parameter const * parameters = nullptr);
~func_decl_info() {}
bool is_associative() const { return m_left_assoc && m_right_assoc; }
@ -565,12 +565,12 @@ public:
unsigned get_decl_id() const { SASSERT(get_id() >= c_first_decl_id); return get_id() - c_first_decl_id; }
symbol const & get_name() const { return m_name; }
decl_info * get_info() const { return m_info; }
family_id get_family_id() const { return m_info == 0 ? null_family_id : m_info->get_family_id(); }
decl_kind get_decl_kind() const { return m_info == 0 ? null_decl_kind : m_info->get_decl_kind(); }
unsigned get_num_parameters() const { return m_info == 0 ? 0 : m_info->get_num_parameters(); }
family_id get_family_id() const { return m_info == nullptr ? null_family_id : m_info->get_family_id(); }
decl_kind get_decl_kind() const { return m_info == nullptr ? null_decl_kind : m_info->get_decl_kind(); }
unsigned get_num_parameters() const { return m_info == nullptr ? 0 : m_info->get_num_parameters(); }
parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
parameter const * get_parameters() const { return m_info == 0 ? 0 : m_info->get_parameters(); }
bool private_parameters() const { return m_info != 0 && m_info->private_parameters(); }
parameter const * get_parameters() const { return m_info == nullptr ? nullptr : m_info->get_parameters(); }
bool private_parameters() const { return m_info != nullptr && m_info->private_parameters(); }
};
// -----------------------------------
@ -587,8 +587,8 @@ class sort : public decl {
sort(symbol const & name, sort_info * info):decl(AST_SORT, name, info) {}
public:
sort_info * get_info() const { return static_cast<sort_info*>(m_info); }
bool is_infinite() const { return get_info() == 0 || get_info()->is_infinite(); }
bool is_very_big() const { return get_info() == 0 || get_info()->is_very_big(); }
bool is_infinite() const { return get_info() == nullptr || get_info()->is_infinite(); }
bool is_very_big() const { return get_info() == nullptr || get_info()->is_very_big(); }
bool is_sort_of(family_id fid, decl_kind k) const { return get_family_id() == fid && get_decl_kind() == k; }
sort_size const & get_num_elements() const { return get_info()->get_num_elements(); }
void set_num_elements(sort_size const& s) { get_info()->set_num_elements(s); }
@ -613,16 +613,16 @@ class func_decl : public decl {
func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range, func_decl_info * info);
public:
func_decl_info * get_info() const { return static_cast<func_decl_info*>(m_info); }
bool is_associative() const { return get_info() != 0 && get_info()->is_associative(); }
bool is_left_associative() const { return get_info() != 0 && get_info()->is_left_associative(); }
bool is_right_associative() const { return get_info() != 0 && get_info()->is_right_associative(); }
bool is_flat_associative() const { return get_info() != 0 && get_info()->is_flat_associative(); }
bool is_commutative() const { return get_info() != 0 && get_info()->is_commutative(); }
bool is_chainable() const { return get_info() != 0 && get_info()->is_chainable(); }
bool is_pairwise() const { return get_info() != 0 && get_info()->is_pairwise(); }
bool is_injective() const { return get_info() != 0 && get_info()->is_injective(); }
bool is_skolem() const { return get_info() != 0 && get_info()->is_skolem(); }
bool is_idempotent() const { return get_info() != 0 && get_info()->is_idempotent(); }
bool is_associative() const { return get_info() != nullptr && get_info()->is_associative(); }
bool is_left_associative() const { return get_info() != nullptr && get_info()->is_left_associative(); }
bool is_right_associative() const { return get_info() != nullptr && get_info()->is_right_associative(); }
bool is_flat_associative() const { return get_info() != nullptr && get_info()->is_flat_associative(); }
bool is_commutative() const { return get_info() != nullptr && get_info()->is_commutative(); }
bool is_chainable() const { return get_info() != nullptr && get_info()->is_chainable(); }
bool is_pairwise() const { return get_info() != nullptr && get_info()->is_pairwise(); }
bool is_injective() const { return get_info() != nullptr && get_info()->is_injective(); }
bool is_skolem() const { return get_info() != nullptr && get_info()->is_skolem(); }
bool is_idempotent() const { return get_info() != nullptr && get_info()->is_idempotent(); }
unsigned get_arity() const { return m_arity; }
sort * get_domain(unsigned idx) const { SASSERT(idx < get_arity()); return m_domain[idx]; }
sort * const * get_domain() const { return m_domain; }
@ -957,7 +957,7 @@ protected:
friend class ast_manager;
public:
decl_plugin():m_manager(0), m_family_id(null_family_id) {}
decl_plugin():m_manager(nullptr), m_family_id(null_family_id) {}
virtual ~decl_plugin() {}
virtual void finalize() {}
@ -1013,7 +1013,7 @@ public:
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic = symbol()) {}
virtual expr * get_some_value(sort * s) { return 0; }
virtual expr * get_some_value(sort * s) { return nullptr; }
// Return true if the interpreted sort s does not depend on uninterpreted sorts.
// This may be the case, for example, for array and datatype sorts.
@ -1042,11 +1042,11 @@ enum basic_op_kind {
PR_UNDEF, PR_TRUE, PR_ASSERTED, PR_GOAL, PR_MODUS_PONENS, PR_REFLEXIVITY, PR_SYMMETRY, PR_TRANSITIVITY, PR_TRANSITIVITY_STAR, PR_MONOTONICITY, PR_QUANT_INTRO,
PR_DISTRIBUTIVITY, PR_AND_ELIM, PR_NOT_OR_ELIM, PR_REWRITE, PR_REWRITE_STAR, PR_PULL_QUANT,
PR_PULL_QUANT_STAR, PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
PR_PUSH_QUANT, PR_ELIM_UNUSED_VARS, PR_DER, PR_QUANT_INST,
PR_HYPOTHESIS, PR_LEMMA, PR_UNIT_RESOLUTION, PR_IFF_TRUE, PR_IFF_FALSE, PR_COMMUTATIVITY, PR_DEF_AXIOM,
PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_NNF_STAR, PR_SKOLEMIZE, PR_CNF_STAR,
PR_DEF_INTRO, PR_APPLY_DEF, PR_IFF_OEQ, PR_NNF_POS, PR_NNF_NEG, PR_SKOLEMIZE,
PR_MODUS_PONENS_OEQ, PR_TH_LEMMA, PR_HYPER_RESOLVE, LAST_BASIC_PR
};
@ -1080,7 +1080,6 @@ protected:
func_decl * m_not_or_elim_decl;
func_decl * m_rewrite_decl;
func_decl * m_pull_quant_decl;
func_decl * m_pull_quant_star_decl;
func_decl * m_push_quant_decl;
func_decl * m_elim_unused_vars_decl;
func_decl * m_der_decl;
@ -1106,8 +1105,6 @@ protected:
ptr_vector<func_decl> m_apply_def_decls;
ptr_vector<func_decl> m_nnf_pos_decls;
ptr_vector<func_decl> m_nnf_neg_decls;
ptr_vector<func_decl> m_nnf_star_decls;
ptr_vector<func_decl> m_cnf_star_decls;
ptr_vector<func_decl> m_th_lemma_decls;
func_decl * m_hyper_res_decl0;
@ -1129,7 +1126,7 @@ protected:
unsigned num_parameters, parameter const* params, unsigned num_parents);
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
func_decl * mk_eq_decl_core(char const * name, decl_kind k, sort * s, ptr_vector<func_decl> & cache);
func_decl * mk_ite_decl(sort * s);
sort* join(sort* s1, sort* s2);
@ -1138,33 +1135,33 @@ protected:
public:
basic_decl_plugin();
virtual ~basic_decl_plugin() {}
virtual void finalize();
~basic_decl_plugin() override {}
void finalize() override;
virtual decl_plugin * mk_fresh() {
decl_plugin * mk_fresh() override {
return alloc(basic_decl_plugin);
}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) override;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
virtual bool is_value(app* a) const;
bool is_value(app* a) const override;
virtual bool is_unique_value(app* a) const;
bool is_unique_value(app* a) const override;
sort * mk_bool_sort() const { return m_bool_sort; }
sort * mk_proof_sort() const { return m_proof_sort; }
virtual expr * get_some_value(sort * s);
expr * get_some_value(sort * s) override;
};
typedef app proof; /* a proof is just an application */
@ -1188,15 +1185,15 @@ class label_decl_plugin : public decl_plugin {
symbol m_lblneg;
symbol m_lbllit;
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
public:
label_decl_plugin();
virtual ~label_decl_plugin();
~label_decl_plugin() override;
virtual decl_plugin * mk_fresh() { return alloc(label_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(label_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
/**
contract: when label
@ -1210,8 +1207,8 @@ public:
...
parameter[n-1] (symbol): label's tag.
*/
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
};
// -----------------------------------
@ -1230,12 +1227,12 @@ enum pattern_op_kind {
*/
class pattern_decl_plugin : public decl_plugin {
public:
virtual decl_plugin * mk_fresh() { return alloc(pattern_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(pattern_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
};
// -----------------------------------
@ -1263,21 +1260,21 @@ class model_value_decl_plugin : public decl_plugin {
public:
model_value_decl_plugin() {}
virtual decl_plugin * mk_fresh() { return alloc(model_value_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(model_value_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
/**
contract:
parameter[0]: (integer) value idx
parameter[1]: (ast) sort of the value.
*/
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual bool is_value(app* n) const;
bool is_value(app* n) const override;
virtual bool is_unique_value(app* a) const;
bool is_unique_value(app* a) const override;
};
// -----------------------------------
@ -1292,11 +1289,11 @@ class user_sort_plugin : public decl_plugin {
public:
user_sort_plugin() {}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
decl_kind register_name(symbol s);
virtual decl_plugin * mk_fresh();
decl_plugin * mk_fresh() override;
};
@ -1497,14 +1494,14 @@ protected:
public:
ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = 0, bool is_format_manager = false);
ast_manager(proof_gen_mode = PGM_DISABLED, char const * trace_file = nullptr, bool is_format_manager = false);
ast_manager(proof_gen_mode, std::fstream * trace_stream, bool is_format_manager = false);
ast_manager(ast_manager const & src, bool disable_proofs = false);
~ast_manager();
// propagate cancellation signal to decl_plugins
bool has_trace_stream() const { return m_trace_stream != 0; }
bool has_trace_stream() const { return m_trace_stream != nullptr; }
std::ostream & trace_stream() { SASSERT(has_trace_stream()); return *m_trace_stream; }
void enable_int_real_coercions(bool f) { m_int_real_coercions = f; }
@ -1523,7 +1520,7 @@ public:
// Equivalent to throw ast_exception(msg)
Z3_NORETURN void raise_exception(char const * msg);
bool is_format_manager() const { return m_format_manager == 0; }
bool is_format_manager() const { return m_format_manager == nullptr; }
ast_manager & get_format_manager() { return is_format_manager() ? *this : *m_format_manager; }
@ -1558,7 +1555,7 @@ public:
decl_plugin * get_plugin(family_id fid) const;
bool has_plugin(family_id fid) const { return get_plugin(fid) != 0; }
bool has_plugin(family_id fid) const { return get_plugin(fid) != nullptr; }
bool has_plugin(symbol const & s) const { return m_family_manager.has_family(s) && has_plugin(m_family_manager.get_family_id(s)); }
@ -1670,7 +1667,7 @@ private:
public:
sort * mk_uninterpreted_sort(symbol const & name, unsigned num_parameters, parameter const * parameters);
sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, 0); }
sort * mk_uninterpreted_sort(symbol const & name) { return mk_uninterpreted_sort(name, 0, nullptr); }
sort * mk_sort(symbol const & name, sort_info const & info) {
if (info.get_family_id() == null_family_id) {
@ -1681,7 +1678,7 @@ public:
}
}
sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0);
sort * mk_sort(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr);
sort * substitute(sort* s, unsigned n, sort * const * src, sort * const * dst);
@ -1700,13 +1697,13 @@ public:
bool is_fully_interp(sort * s) const;
func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range = 0);
unsigned arity, sort * const * domain, sort * range = nullptr);
func_decl * mk_func_decl(family_id fid, decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range = 0);
unsigned num_args, expr * const * args, sort * range = nullptr);
app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = 0,
unsigned num_args = 0, expr * const * args = 0, sort * range = 0);
app * mk_app(family_id fid, decl_kind k, unsigned num_parameters = 0, parameter const * parameters = nullptr,
unsigned num_args = 0, expr * const * args = nullptr, sort * range = nullptr);
app * mk_app(family_id fid, decl_kind k, unsigned num_args, expr * const * args);
@ -1716,7 +1713,7 @@ public:
app * mk_app(family_id fid, decl_kind k, expr * arg1, expr * arg2, expr * arg3);
app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast<expr * const *>(0)); }
app * mk_const(family_id fid, decl_kind k) { return mk_app(fid, k, 0, static_cast<expr * const *>(nullptr)); }
private:
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
func_decl_info * info);
@ -1727,13 +1724,13 @@ private:
public:
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range) {
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(0));
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
}
func_decl * mk_func_decl(symbol const & name, unsigned arity, sort * const * domain, sort * range,
func_decl_info const & info) {
if (info.is_null()) {
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(0));
return mk_func_decl(name, arity, domain, range, static_cast<func_decl_info *>(nullptr));
}
else {
return mk_func_decl(name, arity, domain, range, & const_cast<func_decl_info&>(info));
@ -1746,11 +1743,11 @@ public:
}
func_decl * mk_const_decl(symbol const & name, sort * s) {
return mk_func_decl(name, static_cast<unsigned>(0), 0, s);
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s);
}
func_decl * mk_const_decl(symbol const & name, sort * s, func_decl_info const & info) {
return mk_func_decl(name, static_cast<unsigned>(0), 0, s, info);
return mk_func_decl(name, static_cast<unsigned>(0), nullptr, s, info);
}
func_decl * mk_func_decl(symbol const & name, sort * domain, sort * range, func_decl_info const & info) {
@ -1804,7 +1801,7 @@ public:
app * mk_const(func_decl * decl) {
SASSERT(decl->get_arity() == 0);
return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(0));
return mk_app(decl, static_cast<unsigned>(0), static_cast<expr**>(nullptr));
}
app * mk_const(symbol const & name, sort * s) {
@ -1825,9 +1822,9 @@ public:
return mk_fresh_func_decl(symbol(prefix), symbol::null, arity, domain, range);
}
app * mk_fresh_const(char const * prefix, sort * s) { return mk_const(mk_fresh_func_decl(prefix, 0, 0, s)); }
app * mk_fresh_const(char const * prefix, sort * s) { return mk_const(mk_fresh_func_decl(prefix, 0, nullptr, s)); }
symbol mk_fresh_var_name(char const * prefix = 0);
symbol mk_fresh_var_name(char const * prefix = nullptr);
var * mk_var(unsigned idx, sort * ty);
@ -1879,21 +1876,21 @@ public:
quantifier * mk_quantifier(bool forall, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = 0,
unsigned num_no_patterns = 0, expr * const * no_patterns = 0);
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr);
quantifier * mk_forall(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = 0,
unsigned num_no_patterns = 0, expr * const * no_patterns = 0) {
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
return mk_quantifier(true, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
num_no_patterns, no_patterns);
}
quantifier * mk_exists(unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body,
int weight = 0, symbol const & qid = symbol::null, symbol const & skid = symbol::null,
unsigned num_patterns = 0, expr * const * patterns = 0,
unsigned num_no_patterns = 0, expr * const * no_patterns = 0) {
unsigned num_patterns = 0, expr * const * patterns = nullptr,
unsigned num_no_patterns = 0, expr * const * no_patterns = nullptr) {
return mk_quantifier(false, num_decls, decl_sorts, decl_names, body, weight, qid, skid, num_patterns, patterns,
num_no_patterns, no_patterns);
}
@ -2057,12 +2054,12 @@ public:
func_decl* mk_and_decl() {
sort* domain[2] = { m_bool_sort, m_bool_sort };
return mk_func_decl(m_basic_family_id, OP_AND, 0, 0, 2, domain);
return mk_func_decl(m_basic_family_id, OP_AND, 0, nullptr, 2, domain);
}
func_decl* mk_not_decl() { return mk_func_decl(m_basic_family_id, OP_NOT, 0, 0, 1, &m_bool_sort); }
func_decl* mk_not_decl() { return mk_func_decl(m_basic_family_id, OP_NOT, 0, nullptr, 1, &m_bool_sort); }
func_decl* mk_or_decl() {
sort* domain[2] = { m_bool_sort, m_bool_sort };
return mk_func_decl(m_basic_family_id, OP_OR, 0, 0, 2, domain);
return mk_func_decl(m_basic_family_id, OP_OR, 0, nullptr, 2, domain);
}
// -----------------------------------
@ -2182,7 +2179,6 @@ public:
proof * mk_oeq_rewrite(expr * s, expr * t);
proof * mk_rewrite_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_pull_quant(expr * e, quantifier * q);
proof * mk_pull_quant_star(expr * e, quantifier * q);
proof * mk_push_quant(quantifier * q, expr * e);
proof * mk_elim_unused_vars(quantifier * q, expr * r);
proof * mk_der(quantifier * q, expr * r);
@ -2201,16 +2197,15 @@ public:
proof * mk_nnf_pos(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_nnf_neg(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_nnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_skolemization(expr * q, expr * e);
proof * mk_cnf_star(expr * s, expr * t, unsigned num_proofs, proof * const * proofs);
proof * mk_and_elim(proof * p, unsigned i);
proof * mk_not_or_elim(proof * p, unsigned i);
proof * mk_th_lemma(family_id tid,
expr * fact, unsigned num_proofs, proof * const * proofs,
unsigned num_params = 0, parameter const* params = 0);
unsigned num_params = 0, parameter const* params = nullptr);
protected:
bool check_nnf_proof_parents(unsigned num_proofs, proof * const * proofs) const;
@ -2467,9 +2462,9 @@ class scoped_mark : public ast_mark {
unsigned_vector m_lim;
public:
scoped_mark(ast_manager& m): m_stack(m) {}
virtual ~scoped_mark() {}
virtual void mark(ast * n, bool flag);
virtual void reset();
~scoped_mark() override {}
void mark(ast * n, bool flag) override;
void reset() override;
void mark(ast * n);
void push_scope();
void pop_scope();

4
src/ast/ast_ll_pp.cpp
View file

@ -319,11 +319,11 @@ void ast_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited,
}
void ast_def_ll_pp(std::ostream & out, ast_manager & m, ast * n, ast_mark & visited, bool only_exprs, bool compact) {
ll_printer p(out, m, 0, only_exprs, compact);
ll_printer p(out, m, nullptr, only_exprs, compact);
p.pp(n, visited);
}
void ast_ll_bounded_pp(std::ostream & out, ast_manager & m, ast * n, unsigned depth) {
ll_printer p(out, m, 0, false, true);
ll_printer p(out, m, nullptr, false, true);
p.display_bounded(n, depth);
}

4
src/ast/ast_pp.h
View file

@ -24,10 +24,10 @@ Revision History:
#include "ast/ast_smt2_pp.h"
struct mk_pp : public mk_ismt2_pp {
mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr):
mk_ismt2_pp(t, m, p, indent, num_vars, var_prefix) {
}
mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0):
mk_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr):
mk_ismt2_pp(t, m, indent, num_vars, var_prefix) {
}
};

10
src/ast/ast_pp_util.cpp
View file

@ -38,20 +38,26 @@ void ast_pp_util::collect(expr_ref_vector const& es) {
void ast_pp_util::display_decls(std::ostream& out) {
smt2_pp_environment_dbg env(m);
ast_smt_pp pp(m);
coll.order_deps();
unsigned n = coll.get_num_sorts();
for (unsigned i = 0; i < n; ++i) {
pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, 0);
pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr);
}
n = coll.get_num_decls();
for (unsigned i = 0; i < n; ++i) {
func_decl* f = coll.get_func_decls()[i];
if (f->get_family_id() == null_family_id) {
if (f->get_family_id() == null_family_id && !m_removed.contains(f)) {
ast_smt2_pp(out, f, env);
out << "\n";
}
}
}
void ast_pp_util::remove_decl(func_decl* f) {
m_removed.insert(f);
}
void ast_pp_util::display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat) {
if (neat) {
smt2_pp_environment_dbg env(m);

4
src/ast/ast_pp_util.h
View file

@ -20,9 +20,11 @@ Revision History:
#define AST_PP_UTIL_H_
#include "ast/decl_collector.h"
#include "util/obj_hashtable.h"
class ast_pp_util {
ast_manager& m;
obj_hashtable<func_decl> m_removed;
public:
decl_collector coll;
@ -35,6 +37,8 @@ class ast_pp_util {
void collect(expr_ref_vector const& es);
void remove_decl(func_decl* f);
void display_decls(std::ostream& out);
void display_asserts(std::ostream& out, expr_ref_vector const& fmls, bool neat = true);

22
src/ast/ast_printer.cpp
View file

@ -25,24 +25,24 @@ class simple_ast_printer_context : public ast_printer_context {
smt2_pp_environment_dbg & env() const { return *(m_env.get()); }
public:
simple_ast_printer_context(ast_manager & m):m_manager(m) { m_env = alloc(smt2_pp_environment_dbg, m); }
virtual ~simple_ast_printer_context() {}
~simple_ast_printer_context() override {}
ast_manager & m() const { return m_manager; }
virtual ast_manager & get_ast_manager() { return m_manager; }
virtual void display(std::ostream & out, sort * s, unsigned indent = 0) const { out << mk_ismt2_pp(s, m(), indent); }
virtual void display(std::ostream & out, expr * n, unsigned indent = 0) const { out << mk_ismt2_pp(n, m(), indent); }
virtual void display(std::ostream & out, func_decl * f, unsigned indent = 0) const {
ast_manager & get_ast_manager() override { return m_manager; }
void display(std::ostream & out, sort * s, unsigned indent = 0) const override { out << mk_ismt2_pp(s, m(), indent); }
void display(std::ostream & out, expr * n, unsigned indent = 0) const override { out << mk_ismt2_pp(n, m(), indent); }
void display(std::ostream & out, func_decl * f, unsigned indent = 0) const override {
out << f->get_name();
}
virtual void pp(sort * s, format_ns::format_ref & r) const { mk_smt2_format(s, env(), params_ref(), r); }
virtual void pp(func_decl * f, format_ns::format_ref & r) const { mk_smt2_format(f, env(), params_ref(), r); }
virtual void pp(expr * n, format_ns::format_ref & r) const {
void pp(sort * s, format_ns::format_ref & r) const override { mk_smt2_format(s, env(), params_ref(), r); }
void pp(func_decl * f, format_ns::format_ref & r) const override { mk_smt2_format(f, env(), params_ref(), r); }
void pp(expr * n, format_ns::format_ref & r) const override {
sbuffer<symbol> buf;
mk_smt2_format(n, env(), params_ref(), 0, 0, r, buf);
mk_smt2_format(n, env(), params_ref(), 0, nullptr, r, buf);
}
virtual void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const {
void pp(expr * n, unsigned num_vars, char const * var_prefix, format_ns::format_ref & r, sbuffer<symbol> & var_names) const override {
mk_smt2_format(n, env(), params_ref(), num_vars, var_prefix, r, var_names);
}
virtual void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const {
void display(std::ostream & out, expr * n, unsigned indent, unsigned num_vars, char const * var_prefix, sbuffer<symbol> & var_names) const override {
NOT_IMPLEMENTED_YET();
}

2
src/ast/ast_printer.h
View file

@ -45,7 +45,7 @@ public:
class ast_printer_context : public ast_printer {
public:
virtual ~ast_printer_context() {}
~ast_printer_context() override {}
virtual ast_manager & get_ast_manager() = 0;
virtual std::ostream & regular_stream() { return std::cout; }
virtual std::ostream & diagnostic_stream() { return std::cerr; }

16
src/ast/ast_smt2_pp.cpp
View file

@ -236,7 +236,7 @@ format * smt2_pp_environment::pp_float_literal(app * t, bool use_bv_lits, bool u
mpf_manager & fm = get_futil().fm();
scoped_mpf v(fm);
ast_manager & m = get_manager();
format * body = 0;
format * body = nullptr;
string_buffer<> buf;
VERIFY(get_futil().is_numeral(t, v));
if (fm.is_nan(v)) {
@ -750,7 +750,7 @@ class smt2_printer {
}
buffer<symbol> labels;
bool is_pos;
format * f = 0;
format * f = nullptr;
format ** it = m_format_stack.c_ptr() + fr.m_spos;
format ** end = m_format_stack.c_ptr() + m_format_stack.size();
if (m().is_label(t, is_pos, labels)) {
@ -1004,7 +1004,7 @@ class smt2_printer {
void del_expr2alias_stack() {
std::for_each(m_expr2alias_stack.begin(), m_expr2alias_stack.end(), delete_proc<expr2alias>());
m_expr2alias_stack.reset();
m_expr2alias = 0;
m_expr2alias = nullptr;
}
void reset_expr2alias_stack() {
@ -1064,7 +1064,7 @@ public:
m_manager(env.get_manager()),
m_env(env),
m_soccs(m_manager),
m_root(0),
m_root(nullptr),
m_aliased_pps(fm()),
m_next_alias_idx(1),
m_format_stack(fm()) {
@ -1092,7 +1092,7 @@ public:
void operator()(expr * n, unsigned num, char const * var_prefix, format_ref & r, sbuffer<symbol> & var_names) {
reset_var_names();
if (var_prefix == 0)
if (var_prefix == nullptr)
var_prefix = "x";
if (strcmp(var_prefix, ALIAS_PREFIX) == 0) {
var_prefix = "_a";
@ -1228,7 +1228,7 @@ mk_ismt2_pp::mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent, unsigned num
std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p) {
smt2_pp_environment_dbg env(p.m_manager);
if (p.m_ast == 0) {
if (p.m_ast == nullptr) {
out << "null";
}
else if (is_expr(p.m_ast)) {
@ -1263,13 +1263,13 @@ std::ostream& operator<<(std::ostream& out, sort_ref const& e) {
std::ostream& operator<<(std::ostream& out, expr_ref_vector const& e) {
smt2_pp_environment_dbg env(e.get_manager());
params_ref p;
return ast_smt2_pp(out, e.size(), e.c_ptr(), env, p, 0, 0, 0);
return ast_smt2_pp(out, e.size(), e.c_ptr(), env, p, 0, 0, nullptr);
}
std::ostream& operator<<(std::ostream& out, app_ref_vector const& e) {
smt2_pp_environment_dbg env(e.get_manager());
params_ref p;
return ast_smt2_pp(out, e.size(), (expr*const*)e.c_ptr(), env, p, 0, 0, 0);
return ast_smt2_pp(out, e.size(), (expr*const*)e.c_ptr(), env, p, 0, 0, nullptr);
}
std::ostream& operator<<(std::ostream& out, func_decl_ref_vector const& e) {

24
src/ast/ast_smt2_pp.h
View file

@ -80,15 +80,15 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
datalog::dl_decl_util m_dlutil;
public:
smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dtutil(m), m_dlutil(m) {}
virtual ast_manager & get_manager() const { return m_manager; }
virtual arith_util & get_autil() { return m_autil; }
virtual bv_util & get_bvutil() { return m_bvutil; }
virtual seq_util & get_sutil() { return m_sutil; }
virtual array_util & get_arutil() { return m_arutil; }
virtual fpa_util & get_futil() { return m_futil; }
virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
virtual datatype_util& get_dtutil() { return m_dtutil; }
virtual bool uses(symbol const & s) const { return false; }
ast_manager & get_manager() const override { return m_manager; }
arith_util & get_autil() override { return m_autil; }
bv_util & get_bvutil() override { return m_bvutil; }
seq_util & get_sutil() override { return m_sutil; }
array_util & get_arutil() override { return m_arutil; }
fpa_util & get_futil() override { return m_futil; }
datalog::dl_decl_util& get_dlutil() override { return m_dlutil; }
datatype_util& get_dtutil() override { return m_dtutil; }
bool uses(symbol const & s) const override { return false; }
};
void mk_smt2_format(expr * n, smt2_pp_environment & env, params_ref const & p,
@ -98,7 +98,7 @@ void mk_smt2_format(sort * s, smt2_pp_environment & env, params_ref const & p, f
void mk_smt2_format(func_decl * f, smt2_pp_environment & env, params_ref const & p, format_ns::format_ref & r);
std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0,
unsigned num_vars = 0, char const * var_prefix = 0);
unsigned num_vars = 0, char const * var_prefix = nullptr);
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
@ -113,8 +113,8 @@ struct mk_ismt2_pp {
unsigned m_indent;
unsigned m_num_vars;
char const * m_var_prefix;
mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = 0);
mk_ismt2_pp(ast * t, ast_manager & m, params_ref const & p, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
mk_ismt2_pp(ast * t, ast_manager & m, unsigned indent = 0, unsigned num_vars = 0, char const * var_prefix = nullptr);
};
std::ostream& operator<<(std::ostream& out, mk_ismt2_pp const & p);

17
src/ast/ast_smt_pp.cpp
View file

@ -702,7 +702,7 @@ class smt_printer {
public:
smt_printer(std::ostream& out, ast_manager& m, ptr_vector<quantifier>& ql, smt_renaming& rn,
symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = 0) :
symbol logic, bool no_lets, bool simplify_implies, unsigned indent, unsigned num_var_names = 0, char const* const* var_names = nullptr) :
m_out(out),
m_manager(m),
m_qlists(ql),
@ -768,7 +768,7 @@ public:
}
m_mark.reset();
m_num_lets = 0;
m_top = 0;
m_top = nullptr;
}
void pp_dt(ast_mark& mark, sort* s) {
@ -952,6 +952,10 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
strm << "; " << m_attributes.c_str();
}
#if 0
decls.display_decls(strm);
#else
decls.order_deps();
ast_mark sort_mark;
for (unsigned i = 0; i < decls.get_num_sorts(); ++i) {
sort* s = decls.get_sorts()[i];
@ -978,18 +982,19 @@ void ast_smt_pp::display_smt2(std::ostream& strm, expr* n) {
strm << "\n";
}
}
#endif
for (unsigned i = 0; i < m_assumptions.size(); ++i) {
for (expr* a : m_assumptions) {
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
strm << "(assert\n ";
p(m_assumptions[i].get());
p(a);
strm << ")\n";
}
for (unsigned i = 0; i < m_assumptions_star.size(); ++i) {
for (expr* a : m_assumptions_star) {
smt_printer p(strm, m, ql, rn, m_logic, false, true, m_simplify_implies, 1);
strm << "(assert\n ";
p(m_assumptions_star[i].get());
p(a);
strm << ")\n";
}

6
src/ast/ast_smt_pp.h
View file

@ -76,8 +76,8 @@ public:
void set_is_declared(is_declared* id) { m_is_declared = id; }
void display_smt2(std::ostream& strm, expr* n);
void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0);
void display_expr_smt2(std::ostream& strm, expr* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
void display_ast_smt2(std::ostream& strm, ast* n, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr);
};
@ -87,7 +87,7 @@ struct mk_smt_pp {
unsigned m_indent;
unsigned m_num_var_names;
char const* const* m_var_names;
mk_smt_pp(ast* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = 0) :
mk_smt_pp(ast* e, ast_manager & m, unsigned indent = 0, unsigned num_var_names = 0, char const* const* var_names = nullptr) :
m_ast(e), m_manager(m), m_indent(indent), m_num_var_names(num_var_names), m_var_names(var_names) {}
};

2
src/ast/ast_trail.h
View file

@ -66,7 +66,7 @@ public:
m.insert(s,t);
}
virtual void undo(Ctx& ctx) {
void undo(Ctx& ctx) override {
m_map.pop();
}
};

8
src/ast/ast_translation.cpp
View file

@ -108,7 +108,7 @@ void ast_translation::copy_params(decl * d, unsigned rpos, buffer<parameter> & p
void ast_translation::mk_sort(sort * s, frame & fr) {
sort_info * si = s->get_info();
sort * new_s;
if (si == 0) {
if (si == nullptr) {
// TODO: investigate: this branch is probably unreachable.
// It became unreachable after we started using mk_uninterpreted_sort for creating uninterpreted sorts,
// and mk_uninterpreted_sort actually creates a user_sort.
@ -139,7 +139,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
sort ** new_domain = reinterpret_cast<sort**>(m_result_stack.c_ptr() + fr.m_rpos + num_extra);
sort * new_range = static_cast<sort*>(m_result_stack.back());
func_decl * new_f;
if (fi == 0) {
if (fi == nullptr) {
new_f = m_to_manager.mk_func_decl(f->get_name(),
f->get_arity(),
new_domain,
@ -182,7 +182,7 @@ void ast_translation::mk_func_decl(func_decl * f, frame & fr) {
}
ast * ast_translation::process(ast const * _n) {
if (!_n) return 0;
if (!_n) return nullptr;
SASSERT(m_result_stack.empty());
SASSERT(m_frame_stack.empty());
SASSERT(m_extra_children_stack.empty());
@ -320,7 +320,7 @@ ast * ast_translation::process(ast const * _n) {
}
expr_dependency * expr_dependency_translation::operator()(expr_dependency * d) {
if (d == 0)
if (d == nullptr)
return d;
m_buffer.reset();
m_translation.from().linearize(d, m_buffer);

2
src/ast/ast_util.cpp
View file

@ -38,7 +38,7 @@ app * mk_list_assoc_app(ast_manager & m, func_decl * f, unsigned num_args, expr
}
app * mk_list_assoc_app(ast_manager & m, family_id fid, decl_kind k, unsigned num_args, expr * const * args) {
func_decl * decl = m.mk_func_decl(fid, k, 0, 0, num_args, args, 0);
func_decl * decl = m.mk_func_decl(fid, k, 0, nullptr, num_args, args, nullptr);
SASSERT(decl != 0);
SASSERT(decl->is_associative());
return mk_list_assoc_app(m, decl, num_args, args);

50
src/ast/bv_decl_plugin.cpp
View file

@ -34,11 +34,11 @@ bv_decl_plugin::bv_decl_plugin():
m_repeat_sym("repeat"),
m_bit2bool_sym("bit2bool"),
m_mkbv_sym("mkbv"),
m_bit0(0),
m_bit1(0),
m_carry(0),
m_xor3(0),
m_int_sort(0) {
m_bit0(nullptr),
m_bit1(nullptr),
m_carry(nullptr),
m_xor3(nullptr),
m_int_sort(nullptr) {
}
void bv_decl_plugin::set_manager(ast_manager * m, family_id id) {
@ -218,7 +218,7 @@ func_decl * bv_decl_plugin::mk_int2bv(unsigned bv_size, unsigned num_parameters,
if (arity != 1) {
m_manager->raise_exception("expecting one argument to int2bv");
return 0;
return nullptr;
}
if (m_int2bv[bv_size] == 0) {
@ -237,7 +237,7 @@ func_decl * bv_decl_plugin::mk_bv2int(unsigned bv_size, unsigned num_parameters,
if (arity != 1) {
m_manager->raise_exception("expecting one argument to bv2int");
return 0;
return nullptr;
}
if (m_bv2int[bv_size] == 0) {
@ -341,7 +341,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned bv_size) {
case OP_EXT_ROTATE_LEFT: return mk_binary(m_ext_rotate_left, k, "ext_rotate_left", bv_size, false);
case OP_EXT_ROTATE_RIGHT: return mk_binary(m_ext_rotate_right, k, "ext_rotate_right", bv_size, false);
default: return 0;
default: return nullptr;
}
}
@ -417,7 +417,7 @@ bool bv_decl_plugin::get_int2bv_size(unsigned num_parameters, parameter const *
func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const * parameters, unsigned arity) {
if (!(num_parameters == 2 && arity == 0 && parameters[0].is_rational() && parameters[1].is_int())) {
m_manager->raise_exception("invalid bit-vector numeral declaration");
return 0;
return nullptr;
}
unsigned bv_size = parameters[1].get_int();
if (bv_size == 0) {
@ -437,7 +437,7 @@ func_decl * bv_decl_plugin::mk_bit2bool(unsigned bv_size, unsigned num_parameter
unsigned arity, sort * const * domain) {
if (!(num_parameters == 1 && parameters[0].is_int() && arity == 1 && parameters[0].get_int() < static_cast<int>(bv_size))) {
m_manager->raise_exception("invalid bit2bool declaration");
return 0;
return nullptr;
}
unsigned idx = parameters[0].get_int();
m_bit2bool.reserve(bv_size+1);
@ -455,7 +455,7 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) {
for (unsigned i = 0; i < arity; i++) {
if (!m_manager->is_bool(domain[i])) {
m_manager->raise_exception("invalid mkbv operator");
return 0;
return nullptr;
}
}
unsigned bv_size = arity;
@ -493,26 +493,26 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
else if (arity == 0) {
m_manager->raise_exception("no arguments supplied to bit-vector operator");
return 0;
return nullptr;
}
else if (!get_bv_size(domain[0], bv_size)) {
m_manager->raise_exception("could not extract bit-vector size");
return 0;
return nullptr;
}
func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) {
if (r != nullptr) {
if (arity != r->get_arity()) {
if (r->get_info()->is_associative())
arity = r->get_arity();
else {
m_manager->raise_exception("declared arity mismatches supplied arity");
return 0;
return nullptr;
}
}
for (unsigned i = 0; i < arity; ++i) {
if (domain[i] != r->get_domain(i)) {
m_manager->raise_exception("declared sorts do not match supplied sorts");
return 0;
return nullptr;
}
}
return r;
@ -565,7 +565,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()),
func_decl_info(m_family_id, k, num_parameters, parameters));
default:
return 0;
return nullptr;
}
}
@ -596,24 +596,24 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
else if (num_args == 0 || !get_bv_size(args[0], bv_size)) {
m.raise_exception("operator is applied to arguments of the wrong sort");
return 0;
return nullptr;
}
func_decl * r = mk_func_decl(k, bv_size);
if (r != 0) {
if (r != nullptr) {
if (num_args != r->get_arity()) {
if (r->get_info()->is_associative()) {
sort * fs = r->get_domain(0);
for (unsigned i = 0; i < num_args; ++i) {
if (m.get_sort(args[i]) != fs) {
m_manager->raise_exception("declared sorts do not match supplied sorts");
return 0;
return nullptr;
}
}
return r;
}
else {
m.raise_exception("declared arity mismatches supplied arity");
return 0;
return nullptr;
}
}
for (unsigned i = 0; i < num_args; ++i) {
@ -621,7 +621,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
std::ostringstream buffer;
buffer << "Argument " << mk_pp(args[i], m) << " at position " << i << " does not match declaration " << mk_pp(r, m);
m.raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
}
return r;
@ -747,7 +747,7 @@ expr * bv_decl_plugin::get_some_value(sort * s) {
SASSERT(s->is_sort_of(m_family_id, BV_SORT));
unsigned bv_size = s->get_parameter(0).get_int();
parameter p[2] = { parameter(rational(0)), parameter(static_cast<int>(bv_size)) };
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, 0);
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, nullptr);
}
rational bv_recognizers::norm(rational const & val, unsigned bv_size, bool is_signed) const {
@ -856,7 +856,7 @@ bv_util::bv_util(ast_manager & m):
app * bv_util::mk_numeral(rational const & val, sort* s) const {
if (!is_bv_sort(s)) {
return 0;
return nullptr;
}
unsigned bv_size = get_bv_size(s);
return mk_numeral(val, bv_size);
@ -864,7 +864,7 @@ app * bv_util::mk_numeral(rational const & val, sort* s) const {
app * bv_util::mk_numeral(rational const & val, unsigned bv_size) const {
parameter p[2] = { parameter(val), parameter(static_cast<int>(bv_size)) };
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, 0);
return m_manager.mk_app(get_fid(), OP_BV_NUM, 2, p, 0, nullptr);
}
sort * bv_util::mk_sort(unsigned bv_size) {

34
src/ast/bv_decl_plugin.h
View file

@ -122,7 +122,7 @@ inline bv_op_kind get_div0_op(bv_op_kind k) {
// models the value of "div" it is underspecified (i.e., when the denominator is zero).
inline func_decl * get_div0_decl(ast_manager & m, func_decl * decl) {
return m.mk_func_decl(decl->get_family_id(), get_div0_op(static_cast<bv_op_kind>(decl->get_decl_kind())),
0, 0, 1, decl->get_domain());
0, nullptr, 1, decl->get_domain());
}
class bv_decl_plugin : public decl_plugin {
@ -204,7 +204,7 @@ protected:
vector<ptr_vector<func_decl> > m_bit2bool;
ptr_vector<func_decl> m_mkbv;
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
void mk_bv_sort(unsigned bv_size);
sort * get_bv_sort(unsigned bv_size);
func_decl * mk_func_decl(decl_kind k, unsigned bv_size);
@ -241,34 +241,34 @@ protected:
public:
bv_decl_plugin();
virtual ~bv_decl_plugin() {}
virtual void finalize();
~bv_decl_plugin() override {}
void finalize() override;
virtual decl_plugin * mk_fresh() { return alloc(bv_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(bv_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) override;
virtual bool is_value(app * e) const;
bool is_value(app * e) const override;
virtual bool is_unique_value(app * e) const { return is_value(e); }
bool is_unique_value(app * e) const override { return is_value(e); }
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
virtual bool are_distinct(app* a, app* b) const;
bool are_distinct(app* a, app* b) const override;
virtual expr * get_some_value(sort * s);
expr * get_some_value(sort * s) override;
bool get_int2bv_size(unsigned num_parameters, parameter const * parameters, int & result);
virtual bool is_considered_uninterpreted(func_decl * f) {
bool is_considered_uninterpreted(func_decl * f) override {
if (f->get_family_id() != get_family_id())
return false;
switch (f->get_decl_kind()) {

62
src/ast/datatype_decl_plugin.cpp
View file

@ -157,13 +157,13 @@ namespace datatype {
dealloc(kv.m_value);
}
m_defs.reset();
m_util = 0; // force deletion
m_util = nullptr; // force deletion
}
util & plugin::u() const {
SASSERT(m_manager);
SASSERT(m_family_id != null_family_id);
if (m_util.get() == 0) {
if (m_util.get() == nullptr) {
m_util = alloc(util, *m_manager);
}
return *(m_util.get());
@ -215,7 +215,7 @@ namespace datatype {
sort* s = m_manager->mk_sort(name.get_symbol(),
sort_info(m_family_id, k, num_parameters, parameters, true));
def* d = 0;
def* d = nullptr;
if (m_defs.find(s->get_name(), d) && d->sort_size()) {
obj_map<sort, sort_size> S;
for (unsigned i = 0; i + 1 < num_parameters; ++i) {
@ -233,7 +233,7 @@ namespace datatype {
}
catch (invalid_datatype) {
m_manager->raise_exception("invalid datatype");
return 0;
return nullptr;
}
}
@ -245,35 +245,35 @@ namespace datatype {
if (num_parameters != 1 || !parameters[0].is_ast()) {
m.raise_exception("invalid parameters for datatype field update");
return 0;
return nullptr;
}
if (arity != 2) {
m.raise_exception("invalid number of arguments for datatype field update");
return 0;
return nullptr;
}
func_decl* acc = 0;
func_decl* acc = nullptr;
if (is_func_decl(parameters[0].get_ast())) {
acc = to_func_decl(parameters[0].get_ast());
}
if (acc && !u().is_accessor(acc)) {
acc = 0;
acc = nullptr;
}
if (!acc) {
m.raise_exception("datatype field update requires a datatype accessor as the second argument");
return 0;
return nullptr;
}
sort* dom = acc->get_domain(0);
sort* rng = acc->get_range();
if (dom != domain[0]) {
m.raise_exception("first argument to field update should be a data-type");
return 0;
return nullptr;
}
if (rng != domain[1]) {
std::ostringstream buffer;
buffer << "second argument to field update should be " << mk_ismt2_pp(rng, m)
<< " instead of " << mk_ismt2_pp(domain[1], m);
m.raise_exception(buffer.str().c_str());
return 0;
return nullptr;
}
range = domain[0];
func_decl_info info(m_family_id, k, num_parameters, parameters);
@ -345,7 +345,7 @@ namespace datatype {
return mk_update_field(num_parameters, parameters, arity, domain, range);
default:
m_manager->raise_exception("invalid datatype operator kind");
return 0;
return nullptr;
}
}
@ -386,7 +386,7 @@ namespace datatype {
bool plugin::mk_datatypes(unsigned num_datatypes, def * const * datatypes, unsigned num_params, sort* const* sort_params, sort_ref_vector & new_sorts) {
begin_def_block();
for (unsigned i = 0; i < num_datatypes; ++i) {
def* d = 0;
def* d = nullptr;
TRACE("datatype", tout << "declaring " << datatypes[i]->name() << "\n";);
if (m_defs.find(datatypes[i]->name(), d)) {
TRACE("datatype", tout << "delete previous version for " << datatypes[i]->name() << "\n";);
@ -404,7 +404,7 @@ namespace datatype {
}
void plugin::remove(symbol const& s) {
def* d = 0;
def* d = nullptr;
if (m_defs.find(s, d)) dealloc(d);
m_defs.remove(s);
}
@ -750,7 +750,7 @@ namespace datatype {
ptr_vector<func_decl> const * util::get_datatype_constructors(sort * ty) {
SASSERT(is_datatype(ty));
ptr_vector<func_decl> * r = 0;
ptr_vector<func_decl> * r = nullptr;
if (m_datatype2constructors.find(ty, r))
return r;
r = alloc(ptr_vector<func_decl>);
@ -768,7 +768,7 @@ namespace datatype {
ptr_vector<func_decl> const * util::get_constructor_accessors(func_decl * con) {
SASSERT(is_constructor(con));
ptr_vector<func_decl> * res = 0;
ptr_vector<func_decl> * res = nullptr;
if (m_constructor2accessors.find(con, res)) {
return res;
}
@ -791,9 +791,17 @@ namespace datatype {
return res;
}
func_decl * util::get_constructor_is(func_decl * con) {
SASSERT(is_constructor(con));
sort * datatype = con->get_range();
parameter ps[1] = { parameter(con)};
return m.mk_func_decl(m_family_id, OP_DT_IS, 1, ps, 1, &datatype);
}
func_decl * util::get_constructor_recognizer(func_decl * con) {
SASSERT(is_constructor(con));
func_decl * d = 0;
func_decl * d = nullptr;
if (m_constructor2recognizer.find(con, d))
return d;
sort * datatype = con->get_range();
@ -848,7 +856,7 @@ namespace datatype {
func_decl * util::get_accessor_constructor(func_decl * accessor) {
SASSERT(is_accessor(accessor));
func_decl * r = 0;
func_decl * r = nullptr;
if (m_accessor2constructor.find(accessor, r))
return r;
sort * datatype = accessor->get_domain(0);
@ -892,10 +900,10 @@ namespace datatype {
*/
func_decl * util::get_non_rec_constructor(sort * ty) {
SASSERT(is_datatype(ty));
func_decl * r = 0;
func_decl * r = nullptr;
if (m_datatype2nonrec_constructor.find(ty, r))
return r;
r = 0;
r = nullptr;
ptr_vector<sort> forbidden_set;
forbidden_set.push_back(ty);
TRACE("util_bug", tout << "invoke get-non-rec: " << sort_ref(ty, m) << "\n";);
@ -962,14 +970,14 @@ namespace datatype {
func_decl * nested_c = get_non_rec_constructor_core(T_i, forbidden_set);
SASSERT(forbidden_set.back() == T_i);
forbidden_set.pop_back();
if (nested_c == 0)
if (nested_c == nullptr)
break;
TRACE("util_bug", tout << "nested_c: " << nested_c->get_name() << "\n";);
}
if (i == num_args)
return c;
}
return 0;
return nullptr;
}
unsigned util::get_constructor_idx(func_decl * f) const {
@ -1040,15 +1048,11 @@ namespace datatype {
sort* s = todo.back();
todo.pop_back();
out << s->get_name() << " =\n";
ptr_vector<func_decl> const& cnstrs = *get_datatype_constructors(s);
for (unsigned i = 0; i < cnstrs.size(); ++i) {
func_decl* cns = cnstrs[i];
func_decl* rec = get_constructor_recognizer(cns);
out << " " << cns->get_name() << " :: " << rec->get_name() << " :: ";
for (func_decl * cns : cnstrs) {
out << " " << cns->get_name() << " :: ";
ptr_vector<func_decl> const & accs = *get_constructor_accessors(cns);
for (unsigned j = 0; j < accs.size(); ++j) {
func_decl* acc = accs[j];
for (func_decl* acc : accs) {
sort* s1 = acc->get_range();
out << "(" << acc->get_name() << ": " << s1->get_name() << ") ";
if (is_datatype(s1) && are_siblings(s1, s0) && !mark.is_marked(s1)) {

61
src/ast/datatype_decl_plugin.h
View file

@ -124,16 +124,16 @@ namespace datatype {
struct offset : public size {
sort_size m_offset;
offset(sort_size const& s): m_offset(s) {}
virtual ~offset() {}
virtual size* subst(obj_map<sort,size*>& S) { return this; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return m_offset; }
~offset() override {}
size* subst(obj_map<sort,size*>& S) override { return this; }
sort_size eval(obj_map<sort, sort_size> const& S) override { return m_offset; }
};
struct plus : public size {
size* m_arg1, *m_arg2;
plus(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref();}
virtual ~plus() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
~plus() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_plus(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
@ -147,9 +147,9 @@ namespace datatype {
struct times : public size {
size* m_arg1, *m_arg2;
times(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~times() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
~times() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_times(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
if (s1.is_infinite()) return s1;
@ -163,9 +163,9 @@ namespace datatype {
struct power : public size {
size* m_arg1, *m_arg2;
power(size* a1, size* a2): m_arg1(a1), m_arg2(a2) { a1->inc_ref(); a2->inc_ref(); }
virtual ~power() { m_arg1->dec_ref(); m_arg2->dec_ref(); }
virtual size* subst(obj_map<sort,size*>& S) { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
virtual sort_size eval(obj_map<sort, sort_size> const& S) {
~power() override { m_arg1->dec_ref(); m_arg2->dec_ref(); }
size* subst(obj_map<sort,size*>& S) override { return mk_power(m_arg1->subst(S), m_arg2->subst(S)); }
sort_size eval(obj_map<sort, sort_size> const& S) override {
sort_size s1 = m_arg1->eval(S);
sort_size s2 = m_arg2->eval(S);
// s1^s2
@ -183,9 +183,9 @@ namespace datatype {
struct sparam : public size {
sort_ref m_param;
sparam(sort_ref& p): m_param(p) {}
virtual ~sparam() {}
virtual size* subst(obj_map<sort,size*>& S) { return S[m_param]; }
virtual sort_size eval(obj_map<sort, sort_size> const& S) { return S[m_param]; }
~sparam() override {}
size* subst(obj_map<sort,size*>& S) override { return S[m_param]; }
sort_size eval(obj_map<sort, sort_size> const& S) override { return S[m_param]; }
};
};
@ -204,7 +204,7 @@ namespace datatype {
m_util(u),
m_name(n),
m_class_id(class_id),
m_sort_size(0),
m_sort_size(nullptr),
m_params(m, num_params, params),
m_sort(m)
{}
@ -228,7 +228,7 @@ namespace datatype {
sort_ref_vector const& params() const { return m_params; }
util& u() const { return m_util; }
param_size::size* sort_size() { return m_sort_size; }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = 0; }
void set_sort_size(param_size::size* p) { m_sort_size = p; p->inc_ref(); m_sort = nullptr; }
def* translate(ast_translation& tr, util& u);
};
@ -241,30 +241,30 @@ namespace datatype {
unsigned m_class_id;
util & u() const;
virtual void inherit(decl_plugin* other_p, ast_translation& tr);
void inherit(decl_plugin* other_p, ast_translation& tr) override;
public:
plugin(): m_class_id(0) {}
virtual ~plugin();
~plugin() override;
virtual void finalize();
void finalize() override;
virtual decl_plugin * mk_fresh() { return alloc(plugin); }
decl_plugin * mk_fresh() override { return alloc(plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual expr * get_some_value(sort * s);
expr * get_some_value(sort * s) override;
virtual bool is_fully_interp(sort * s) const;
bool is_fully_interp(sort * s) const override;
virtual bool is_value(app* e) const;
bool is_value(app* e) const override;
virtual bool is_unique_value(app * e) const { return is_value(e); }
bool is_unique_value(app * e) const override { return is_value(e); }
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
void begin_def_block() { m_class_id++; m_def_block.reset(); }
@ -368,6 +368,7 @@ namespace datatype {
sort* get_datatype_parameter_sort(sort * ty, unsigned idx);
func_decl * get_non_rec_constructor(sort * ty);
func_decl * get_constructor_recognizer(func_decl * constructor);
func_decl * get_constructor_is(func_decl * constructor);
ptr_vector<func_decl> const * get_constructor_accessors(func_decl * constructor);
func_decl * get_accessor_constructor(func_decl * accessor);
func_decl * get_recognizer_constructor(func_decl * recognizer) const;
@ -398,7 +399,7 @@ typedef datatype::util datatype_util;
class type_ref {
void * m_data;
public:
type_ref():m_data(TAG(void *, static_cast<void*>(0), 1)) {}
type_ref():m_data(TAG(void *, nullptr, 1)) {}
type_ref(int idx):m_data(BOXINT(void *, idx)) {}
type_ref(sort * s):m_data(TAG(void *, s, 1)) {}

78
src/ast/decl_collector.cpp
View file

@ -18,6 +18,7 @@ Revision History:
--*/
#include "ast/decl_collector.h"
#include "ast/ast_pp.h"
void decl_collector::visit_sort(sort * n) {
family_id fid = n->get_family_id();
@ -25,19 +26,21 @@ void decl_collector::visit_sort(sort * n) {
m_sorts.push_back(n);
if (fid == m_dt_fid) {
m_sorts.push_back(n);
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n);
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i);
m_decls.push_back(cnstr);
m_todo.push_back(cnstr);
ptr_vector<func_decl> const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr);
unsigned num_cas = cnstr_acc.size();
for (unsigned j = 0; j < num_cas; j++) {
func_decl * accsr = cnstr_acc.get(j);
m_decls.push_back(accsr);
m_todo.push_back(cnstr_acc.get(j));
}
}
}
for (unsigned i = n->get_num_parameters(); i-- > 0; ) {
parameter const& p = n->get_parameter(i);
if (p.is_ast()) m_todo.push_back(p.get_ast());
}
}
bool decl_collector::is_bool(sort * s) {
@ -63,43 +66,43 @@ decl_collector::decl_collector(ast_manager & m, bool preds):
}
void decl_collector::visit(ast* n) {
ptr_vector<ast> todo;
todo.push_back(n);
while (!todo.empty()) {
n = todo.back();
todo.pop_back();
datatype_util util(m());
m_todo.push_back(n);
while (!m_todo.empty()) {
n = m_todo.back();
m_todo.pop_back();
if (!m_visited.is_marked(n)) {
m_visited.mark(n, true);
switch(n->get_kind()) {
case AST_APP: {
app * a = to_app(n);
for (unsigned i = 0; i < a->get_num_args(); ++i) {
todo.push_back(a->get_arg(i));
for (expr* arg : *a) {
m_todo.push_back(arg);
}
todo.push_back(a->get_decl());
m_todo.push_back(a->get_decl());
break;
}
case AST_QUANTIFIER: {
quantifier * q = to_quantifier(n);
unsigned num_decls = q->get_num_decls();
for (unsigned i = 0; i < num_decls; ++i) {
todo.push_back(q->get_decl_sort(i));
m_todo.push_back(q->get_decl_sort(i));
}
todo.push_back(q->get_expr());
m_todo.push_back(q->get_expr());
for (unsigned i = 0; i < q->get_num_patterns(); ++i) {
todo.push_back(q->get_pattern(i));
m_todo.push_back(q->get_pattern(i));
}
break;
}
case AST_SORT:
case AST_SORT:
visit_sort(to_sort(n));
break;
case AST_FUNC_DECL: {
func_decl * d = to_func_decl(n);
for (unsigned i = 0; i < d->get_arity(); ++i) {
todo.push_back(d->get_domain(i));
m_todo.push_back(d->get_domain(i));
}
todo.push_back(d->get_range());
m_todo.push_back(d->get_range());
visit_func(d);
break;
}
@ -112,5 +115,44 @@ void decl_collector::visit(ast* n) {
}
}
void decl_collector::order_deps() {
top_sort<sort> st;
for (sort * s : m_sorts) st.insert(s, collect_deps(s));
st.topological_sort();
m_sorts.reset();
for (sort* s : st.top_sorted()) m_sorts.push_back(s);
}
decl_collector::sort_set* decl_collector::collect_deps(sort* s) {
sort_set* set = alloc(sort_set);
collect_deps(s, *set);
set->remove(s);
return set;
}
void decl_collector::collect_deps(sort* s, sort_set& set) {
if (set.contains(s)) return;
set.insert(s);
if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) {
unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s);
for (unsigned i = 0; i < num_sorts; ++i) {
set.insert(m_dt_util.get_datatype_parameter_sort(s, i));
}
unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s);
for (unsigned i = 0; i < num_cnstr; i++) {
func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i);
set.insert(cnstr->get_range());
for (unsigned j = 0; j < cnstr->get_arity(); ++j)
set.insert(cnstr->get_domain(j));
}
}
for (unsigned i = s->get_num_parameters(); i-- > 0; ) {
parameter const& p = s->get_parameter(i);
if (p.is_ast() && is_sort(p.get_ast())) {
set.insert(to_sort(p.get_ast()));
}
}
}

10
src/ast/decl_collector.h
View file

@ -20,6 +20,7 @@ Revision History:
#ifndef SMT_DECL_COLLECTOR_H_
#define SMT_DECL_COLLECTOR_H_
#include "util/top_sort.h"
#include "ast/ast.h"
#include "ast/datatype_decl_plugin.h"
@ -33,11 +34,17 @@ class decl_collector {
family_id m_basic_fid;
family_id m_dt_fid;
datatype_util m_dt_util;
ptr_vector<ast> m_todo;
void visit_sort(sort* n);
bool is_bool(sort* s);
void visit_func(func_decl* n);
typedef obj_hashtable<sort> sort_set;
sort_set* collect_deps(sort* s);
void collect_deps(top_sort<sort>& st);
void collect_deps(sort* s, sort_set& set);
public:
// if preds == true, then predicates are stored in a separate collection.
@ -48,9 +55,12 @@ public:
void visit(unsigned n, expr* const* es);
void visit(expr_ref_vector const& es);
void order_deps();
unsigned get_num_sorts() const { return m_sorts.size(); }
unsigned get_num_decls() const { return m_decls.size(); }
unsigned get_num_preds() const { return m_preds.size(); }
sort * const * get_sorts() const { return m_sorts.c_ptr(); }
func_decl * const * get_func_decls() const { return m_decls.c_ptr(); }
func_decl * const * get_pred_decls() const { return m_preds.c_ptr(); }

152
src/ast/dl_decl_plugin.cpp
View file

@ -72,7 +72,7 @@ namespace datalog {
for (unsigned i = 0; is_finite && i < num_parameters; ++i) {
if (!parameters[i].is_ast() || !is_sort(parameters[i].get_ast())) {
m_manager->raise_exception("expecting sort parameters");
return 0;
return nullptr;
}
sort* s = to_sort(parameters[i].get_ast());
sort_size sz1 = s->get_num_elements();
@ -97,16 +97,16 @@ namespace datalog {
sort * dl_decl_plugin::mk_finite_sort(unsigned num_params, parameter const* params) {
if (num_params != 2) {
m_manager->raise_exception("expecting two parameters");
return 0;
return nullptr;
}
if (!params[0].is_symbol()) {
m_manager->raise_exception("expecting symbol");
return 0;
return nullptr;
}
if (!params[1].is_rational() || !params[1].get_rational().is_uint64()) {
m_manager->raise_exception("expecting rational");
return 0;
return nullptr;
}
sort_size sz = sort_size::mk_finite(params[1].get_rational().get_uint64());
sort_info info(m_family_id, DL_FINITE_SORT, sz, num_params, params);
@ -115,7 +115,7 @@ namespace datalog {
sort* dl_decl_plugin::mk_rule_sort() {
sort_size sz(sort_size::mk_infinite());
sort_info info(m_family_id, DL_RULE_SORT, sz, 0, 0);
sort_info info(m_family_id, DL_RULE_SORT, sz, 0, nullptr);
return m_manager->mk_sort(m_rule_sym, info);
}
@ -130,7 +130,7 @@ namespace datalog {
default:
UNREACHABLE();
}
return 0;
return nullptr;
}
bool dl_decl_plugin::is_rel_sort(sort* r) {
@ -173,11 +173,11 @@ namespace datalog {
}
ptr_vector<sort> sorts;
if (!is_rel_sort(r, sorts)) {
return 0;
return nullptr;
}
if (sorts.size() + 1 != arity) {
m_manager->raise_exception("wrong arity supplied to relational access");
return 0;
return nullptr;
}
for (unsigned i = 0; i < sorts.size(); ++i) {
if (sorts[i] != domain[i+1]) {
@ -186,10 +186,10 @@ namespace datalog {
mk_pp(sorts[i], m) << "\n" <<
mk_pp(domain[i+1], m) << "\n";);
m_manager->raise_exception("sort miss-match for relational access");
return 0;
return nullptr;
}
}
func_decl_info info(m_family_id, k, 0, 0);
func_decl_info info(m_family_id, k, 0, nullptr);
return m.mk_func_decl(sym, arity, domain, r, info);
}
@ -197,14 +197,14 @@ namespace datalog {
ast_manager& m = *m_manager;
if (!p.is_ast() || !is_sort(p.get_ast())) {
m_manager->raise_exception("expected sort parameter");
return 0;
return nullptr;
}
sort* r = to_sort(p.get_ast());
if (!is_rel_sort(r)) {
return 0;
return nullptr;
}
func_decl_info info(m_family_id, OP_RA_EMPTY, 1, &p);
return m.mk_func_decl(m_empty_sym, 0, (sort*const*)0, r, info);
return m.mk_func_decl(m_empty_sym, 0, (sort*const*)nullptr, r, info);
}
func_decl* dl_decl_plugin::mk_project(unsigned num_params, parameter const* params, sort* r) {
@ -219,7 +219,7 @@ namespace datalog {
tout << "\n";
);
if (!is_rel_sort(r, sorts)) {
return 0;
return nullptr;
}
SASSERT(sorts.size() >= num_params);
// populate ps
@ -227,12 +227,12 @@ namespace datalog {
for (; i < num_params; ++i) {
if (!params[i].is_int()) {
m_manager->raise_exception("expecting integer parameter");
return 0;
return nullptr;
}
unsigned k = params[i].get_int();
if (j > k) {
m_manager->raise_exception("arguments to projection should be increasing");
return 0;
return nullptr;
}
while (j < k) {
ps.push_back(parameter(sorts[j]));
@ -253,13 +253,13 @@ namespace datalog {
ast_manager& m = *m_manager;
if (s1 != s2) {
m_manager->raise_exception("sort miss-match for arguments to union");
return 0;
return nullptr;
}
if (!is_rel_sort(s1)) {
return 0;
return nullptr;
}
sort* domain[2] = { s1, s2 };
func_decl_info info(m_family_id, k, 0, 0);
func_decl_info info(m_family_id, k, 0, nullptr);
return m.mk_func_decl(m_union_sym, 2, domain, s1, info);
}
@ -267,7 +267,7 @@ namespace datalog {
ast_manager& m = *m_manager;
ptr_vector<sort> sorts;
if (!is_rel_sort(r, sorts)) {
return 0;
return nullptr;
}
if (!p.is_ast() || !is_expr(p.get_ast())) {
m_manager->raise_exception("ast expression expected to filter");
@ -277,7 +277,7 @@ namespace datalog {
// 2. the free variables in f correspond to column types of r.
if (!m.is_bool(f)) {
m_manager->raise_exception("filter predicate should be of Boolean type");
return 0;
return nullptr;
}
ptr_vector<expr> todo;
todo.push_back(f);
@ -295,11 +295,11 @@ namespace datalog {
idx = to_var(e)->get_idx();
if (idx >= sorts.size()) {
m_manager->raise_exception("illegal index");
return 0;
return nullptr;
}
if (sorts[idx] != m.get_sort(e)) {
m_manager->raise_exception("sort miss-match in filter");
return 0;
return nullptr;
}
break;
case AST_APP:
@ -309,10 +309,10 @@ namespace datalog {
break;
case AST_QUANTIFIER:
m_manager->raise_exception("quantifiers are not allowed in filter expressions");
return 0;
return nullptr;
default:
m_manager->raise_exception("unexpected filter expression kind");
return 0;
return nullptr;
}
}
func_decl_info info(m_family_id, OP_RA_FILTER, 1, &p);
@ -322,23 +322,23 @@ namespace datalog {
func_decl * dl_decl_plugin::mk_rename(unsigned num_params, parameter const* params, sort* r) {
ptr_vector<sort> sorts;
if (!is_rel_sort(r, sorts)) {
return 0;
return nullptr;
}
unsigned index0 = 0;
sort* last_sort = 0;
sort* last_sort = nullptr;
SASSERT(num_params > 0);
for (unsigned i = 0; i < num_params; ++i) {
parameter const& p = params[i];
if (!p.is_int()) {
m_manager->raise_exception("expected integer parameter");
return 0;
return nullptr;
}
unsigned j = p.get_int();
if (j >= sorts.size()) {
// We should not use ast_pp anymore on error messages.
// m_manager->raise_exception("index %d out of bound %s : %d", j, ast_pp(r, *m_manager).c_str(), sorts.size());
m_manager->raise_exception("index out of bound");
return 0;
return nullptr;
}
if (i == 0) {
index0 = j;
@ -362,10 +362,10 @@ namespace datalog {
vector<parameter> params2;
ptr_vector<sort> sorts1, sorts2;
if (!is_rel_sort(r1, sorts1)) {
return 0;
return nullptr;
}
if (!is_rel_sort(r2, sorts2)) {
return 0;
return nullptr;
}
for (unsigned i = 0; i < sorts1.size(); ++i) {
params2.push_back(parameter(sorts1[i]));
@ -375,24 +375,24 @@ namespace datalog {
}
if (0 != num_params % 2) {
m_manager->raise_exception("expecting an even number of parameters to join");
return 0;
return nullptr;
}
for (unsigned i = 0; i + 1 < num_params; i += 2) {
parameter const& p1 = params[i];
parameter const& p2 = params[i+1];
if (!p1.is_int() || !p2.is_int()) {
m_manager->raise_exception("encountered non-integer parameter");
return 0;
return nullptr;
}
unsigned i1 = p1.get_int();
unsigned i2 = p2.get_int();
if (i1 >= sorts1.size() || i2 >= sorts2.size()) {
m_manager->raise_exception("index out of bounds");
return 0;
return nullptr;
}
if (sorts1[i1] != sorts2[i2]) {
m_manager->raise_exception("sort miss-match in join");
return 0;
return nullptr;
}
}
sort* args[2] = { r1, r2 };
@ -403,40 +403,40 @@ namespace datalog {
func_decl* dl_decl_plugin::mk_complement(sort* s) {
if (!is_rel_sort(s)) {
return 0;
return nullptr;
}
func_decl_info info(m_family_id, OP_RA_COMPLEMENT, 0, 0);
func_decl_info info(m_family_id, OP_RA_COMPLEMENT, 0, nullptr);
return m_manager->mk_func_decl(m_complement_sym, 1, &s, s, info);
}
func_decl * dl_decl_plugin::mk_negation_filter(unsigned num_params, parameter const* params, sort* r1, sort* r2) {
ptr_vector<sort> sorts1, sorts2;
if (!is_rel_sort(r1, sorts1)) {
return 0;
return nullptr;
}
if (!is_rel_sort(r2, sorts2)) {
return 0;
return nullptr;
}
if (0 != num_params % 2) {
m_manager->raise_exception("expecting an even number of parameters to negation filter");
return 0;
return nullptr;
}
for (unsigned i = 0; i + 1 < num_params; i += 2) {
parameter const& p1 = params[i];
parameter const& p2 = params[i+1];
if (!p1.is_int() || !p2.is_int()) {
m_manager->raise_exception("encountered non-integer parameter");
return 0;
return nullptr;
}
unsigned i1 = p1.get_int();
unsigned i2 = p2.get_int();
if (i1 >= sorts1.size() || i2 >= sorts2.size()) {
m_manager->raise_exception("index out of bounds");
return 0;
return nullptr;
}
if (sorts1[i1] != sorts2[i2]) {
m_manager->raise_exception("sort miss-match in join");
return 0;
return nullptr;
}
}
sort* args[2] = { r1, r2 };
@ -446,9 +446,9 @@ namespace datalog {
func_decl * dl_decl_plugin::mk_is_empty(sort* s) {
if (!is_rel_sort(s)) {
return 0;
return nullptr;
}
func_decl_info info(m_family_id, OP_RA_IS_EMPTY, 0, 0);
func_decl_info info(m_family_id, OP_RA_IS_EMPTY, 0, nullptr);
sort* rng = m_manager->mk_bool_sort();
return m_manager->mk_func_decl(m_is_empty_sym, 1, &s, rng, info);
}
@ -458,35 +458,35 @@ namespace datalog {
parameter const& ps = params[1];
if (!p.is_rational() || !p.get_rational().is_uint64()) {
m_manager->raise_exception("first parameter should be a rational");
return 0;
return nullptr;
}
if (!ps.is_ast() || !is_sort(ps.get_ast()) || !is_fin_sort(to_sort(ps.get_ast()))) {
m_manager->raise_exception("second parameter should be a finite domain sort");
return 0;
return nullptr;
}
sort* s = to_sort(ps.get_ast());
func_decl_info info(m_family_id, OP_DL_CONSTANT, 2, params);
return m_manager->mk_func_decl(m_num_sym, 0, (sort*const*)0, s, info);
return m_manager->mk_func_decl(m_num_sym, 0, (sort*const*)nullptr, s, info);
}
func_decl * dl_decl_plugin::mk_compare(decl_kind k, symbol const& sym, sort *const* domain) {
if (!is_sort_of(domain[0], m_family_id, DL_FINITE_SORT)) {
m_manager->raise_exception("expecting finite domain sort");
return 0;
return nullptr;
}
if (domain[0] != domain[1]) {
m_manager->raise_exception("expecting two identical finite domain sorts");
return 0;
return nullptr;
}
func_decl_info info(m_family_id, k, 0, 0);
func_decl_info info(m_family_id, k, 0, nullptr);
return m_manager->mk_func_decl(sym, 2, domain, m_manager->mk_bool_sort(), info);
}
func_decl * dl_decl_plugin::mk_clone(sort* s) {
if (!is_rel_sort(s)) {
return 0;
return nullptr;
}
func_decl_info info(m_family_id, OP_RA_CLONE, 0, 0);
func_decl_info info(m_family_id, OP_RA_CLONE, 0, nullptr);
return m_manager->mk_func_decl(m_clone_sym, 1, &s, s, info);
}
@ -494,14 +494,14 @@ namespace datalog {
func_decl * dl_decl_plugin::mk_func_decl(
decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
func_decl* result = 0;
func_decl* result = nullptr;
switch(k) {
case OP_RA_STORE:
case OP_RA_SELECT:
if (!check_params(0, 0, num_parameters) ||
!check_domain(1, UINT_MAX, arity)) {
return 0;
return nullptr;
}
result = mk_store_select(k, arity, domain);
break;
@ -509,7 +509,7 @@ namespace datalog {
case OP_RA_EMPTY:
if (!check_params( 1, 1, num_parameters) ||
!check_domain(0, 0, arity)) {
return 0;
return nullptr;
}
result = mk_empty(parameters[0]);
break;
@ -517,7 +517,7 @@ namespace datalog {
case OP_RA_JOIN:
if (!check_params(0, UINT_MAX, num_parameters) ||
!check_domain(2, 2, arity)) {
return 0;
return nullptr;
}
result = mk_join(num_parameters, parameters, domain[0], domain[1]);
break;
@ -526,7 +526,7 @@ namespace datalog {
case OP_RA_WIDEN:
if (!check_params( 0, 0, num_parameters) ||
!check_domain(2, 2, arity)) {
return 0;
return nullptr;
}
result = mk_unionw(k, domain[0], domain[1]);
break;
@ -534,7 +534,7 @@ namespace datalog {
case OP_RA_PROJECT:
if (!check_params( 1, UINT_MAX, num_parameters) ||
!check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_project(num_parameters, parameters, domain[0]);
break;
@ -542,7 +542,7 @@ namespace datalog {
case OP_RA_FILTER:
if (!check_params( 1, 1, num_parameters) ||
!check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_filter(parameters[0], domain[0]);
break;
@ -550,7 +550,7 @@ namespace datalog {
case OP_RA_IS_EMPTY:
if (!check_params( 0, 0, num_parameters) ||
!check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_is_empty(domain[0]);
break;
@ -558,7 +558,7 @@ namespace datalog {
case OP_RA_RENAME:
if (!check_params( 2, UINT_MAX, num_parameters) ||
!check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_rename(num_parameters, parameters, domain[0]);
break;
@ -566,7 +566,7 @@ namespace datalog {
case OP_RA_COMPLEMENT:
if (!check_params( 0, 0, num_parameters) ||
!check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_complement(domain[0]);
break;
@ -574,14 +574,14 @@ namespace datalog {
case OP_RA_NEGATION_FILTER:
if (!check_params(1, UINT_MAX, num_parameters) ||
!check_domain(2, 2, arity)) {
return 0;
return nullptr;
}
result = mk_negation_filter(num_parameters, parameters, domain[0], domain[1]);
break;
case OP_RA_CLONE:
if (!check_params(0, 0, num_parameters) || !check_domain(1, 1, arity)) {
return 0;
return nullptr;
}
result = mk_clone(domain[0]);
break;
@ -589,7 +589,7 @@ namespace datalog {
case OP_DL_CONSTANT:
if (!check_params( 2, 2, num_parameters) ||
!check_domain(0, 0, arity)) {
return 0;
return nullptr;
}
result = mk_constant(parameters);
break;
@ -597,23 +597,23 @@ namespace datalog {
case OP_DL_LT:
if (!check_params( 0, 0, num_parameters) ||
!check_domain(2, 2, arity)) {
return 0;
return nullptr;
}
result = mk_compare(OP_DL_LT, m_lt_sym, domain);
break;
case OP_DL_REP: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
!check_domain(1, 1, arity)) return nullptr;
func_decl_info info(m_family_id, k, 0, nullptr);
result = m_manager->mk_func_decl(symbol("rep"), 1, domain, range, info);
break;
}
case OP_DL_ABS: {
if (!check_domain(0, 0, num_parameters) ||
!check_domain(1, 1, arity)) return 0;
func_decl_info info(m_family_id, k, 0, 0);
!check_domain(1, 1, arity)) return nullptr;
func_decl_info info(m_family_id, k, 0, nullptr);
result = m_manager->mk_func_decl(symbol("abs"), 1, domain, range, info);
break;
}
@ -621,7 +621,7 @@ namespace datalog {
default:
m_manager->raise_exception("operator not recognized");
return 0;
return nullptr;
}
TRACE("dl_decl_plugin", tout << mk_pp(result, *m_manager) << "\n";);
@ -659,7 +659,7 @@ namespace datalog {
m.raise_exception("value is out of bounds");
}
parameter params[2] = { parameter(rational(value, rational::ui64())), parameter(s) };
return m.mk_const(m.mk_func_decl(m_fid, OP_DL_CONSTANT, 2, params, 0, (sort*const*)0));
return m.mk_const(m.mk_func_decl(m_fid, OP_DL_CONSTANT, 2, params, 0, (sort*const*)nullptr));
}
if (m_arith.is_int(s) || m_arith.is_real(s)) {
return m_arith.mk_numeral(rational(value, rational::ui64()), s);
@ -677,7 +677,7 @@ namespace datalog {
std::stringstream strm;
strm << "sort '" << mk_pp(s, m) << "' is not recognized as a sort that contains numeric values.\nUse Bool, BitVec, Int, Real, or a Finite domain sort";
m.raise_exception(strm.str().c_str());
return 0;
return nullptr;
}
bool dl_decl_util::is_numeral(const expr* e, uint64& v) const {
@ -745,12 +745,12 @@ namespace datalog {
app* dl_decl_util::mk_lt(expr* a, expr* b) {
expr* args[2] = { a, b };
return m.mk_app(m_fid, OP_DL_LT, 0, 0, 2, args);
return m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args);
}
app* dl_decl_util::mk_le(expr* a, expr* b) {
expr* args[2] = { b, a };
return m.mk_not(m.mk_app(m_fid, OP_DL_LT, 0, 0, 2, args));
return m.mk_not(m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args));
}
sort* dl_decl_util::mk_rule_sort() {

22
src/ast/dl_decl_plugin.h
View file

@ -102,9 +102,9 @@ namespace datalog {
public:
dl_decl_plugin();
virtual ~dl_decl_plugin() {}
~dl_decl_plugin() override {}
virtual decl_plugin * mk_fresh() { return alloc(dl_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(dl_decl_plugin); }
//
// Contract for sort DL_RELATION_SORT
@ -116,7 +116,7 @@ namespace datalog {
// parameters[0] - name
// parameters[1] - uint64
//
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
//
// Contract for func_decl:
@ -126,15 +126,15 @@ namespace datalog {
// parameters[1] - a DL_FINITE_SORT sort of the constant
// Contract for others:
// no parameters
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
virtual bool is_value(app * e) const { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
virtual bool is_unique_value(app * e) const { return is_value(e); }
bool is_value(app * e) const override { return is_app_of(e, m_family_id, OP_DL_CONSTANT); }
bool is_unique_value(app * e) const override { return is_value(e); }
};
@ -204,9 +204,9 @@ namespace datalog {
sort* mk_rule_sort();
app* mk_rule(symbol const& name, unsigned num_args = 0, expr* const* args = 0);
app* mk_rule(symbol const& name, unsigned num_args = 0, expr* const* args = nullptr);
app* mk_fact(symbol const& name) { return mk_rule(name, 0, 0); }
app* mk_fact(symbol const& name) { return mk_rule(name, 0, nullptr); }
ast_manager& get_manager() const { return m; }

10
src/ast/expr2polynomial.cpp
View file

@ -29,7 +29,7 @@ struct expr2polynomial::imp {
struct frame {
app * m_curr;
unsigned m_idx;
frame():m_curr(0), m_idx(0) {}
frame():m_curr(nullptr), m_idx(0) {}
frame(app * t):m_curr(t), m_idx(0) {}
};
@ -59,8 +59,8 @@ struct expr2polynomial::imp {
m_am(am),
m_autil(am),
m_pm(pm),
m_expr2var(e2v == 0 && !use_var_idxs ? alloc(expr2var, am) : e2v),
m_expr2var_owner(e2v == 0 && !use_var_idxs),
m_expr2var(e2v == nullptr && !use_var_idxs ? alloc(expr2var, am) : e2v),
m_expr2var_owner(e2v == nullptr && !use_var_idxs),
m_var2expr(am),
m_cached_domain(am),
m_cached_polynomials(pm),
@ -156,7 +156,7 @@ struct expr2polynomial::imp {
x = m_wrapper.mk_var(is_int);
m_expr2var->insert(t, x);
if (x >= m_var2expr.size())
m_var2expr.resize(x+1, 0);
m_var2expr.resize(x+1, nullptr);
m_var2expr.set(x, t);
}
}
@ -502,7 +502,7 @@ void expr2polynomial::set_cancel(bool f) {
}
default_expr2polynomial::default_expr2polynomial(ast_manager & am, polynomial::manager & pm):
expr2polynomial(am, pm, 0) {
expr2polynomial(am, pm, nullptr) {
}
default_expr2polynomial::~default_expr2polynomial() {

6
src/ast/expr2polynomial.h
View file

@ -103,10 +103,10 @@ class default_expr2polynomial : public expr2polynomial {
svector<bool> m_is_int;
public:
default_expr2polynomial(ast_manager & am, polynomial::manager & pm);
virtual ~default_expr2polynomial();
virtual bool is_int(polynomial::var x) const;
~default_expr2polynomial() override;
bool is_int(polynomial::var x) const override;
protected:
virtual polynomial::var mk_var(bool is_int);
polynomial::var mk_var(bool is_int) override;
};
#endif

2
src/ast/expr2var.cpp
View file

@ -64,7 +64,7 @@ void expr2var::mk_inv(expr_ref_vector & var2expr) const {
expr * t = it->m_key;
var x = it->m_value;
if (x >= var2expr.size())
var2expr.resize(x+1, 0);
var2expr.resize(x+1, nullptr);
var2expr.set(x, t);
}
}

2
src/ast/expr_abstract.cpp
View file

@ -27,7 +27,7 @@ void expr_abstractor::operator()(unsigned base, unsigned num_bound, expr* const*
result = n;
return;
}
expr * curr = 0, *b = 0;
expr * curr = nullptr, *b = nullptr;
SASSERT(n->get_ref_count() > 0);
m_stack.push_back(n);

2
src/ast/expr_delta_pair.h
View file

@ -26,7 +26,7 @@ struct expr_delta_pair {
expr * m_node;
unsigned m_delta;
expr_delta_pair():m_node(0), m_delta(0) {}
expr_delta_pair():m_node(nullptr), m_delta(0) {}
expr_delta_pair(expr * n, unsigned d):m_node(n), m_delta(d) {}
unsigned hash() const { return hash_u_u(m_node->hash(), m_delta); }
bool operator==(const expr_delta_pair & e) const { return m_node == e.m_node && m_delta == e.m_delta; }

10
src/ast/expr_functors.cpp
View file

@ -121,22 +121,22 @@ void map_proc::reconstruct(app* a) {
}
if (is_new) {
expr* b = m.mk_app(a->get_decl(), m_args.size(), m_args.c_ptr());
m_map.insert(a, b, 0);
m_map.insert(a, b, nullptr);
}
else {
m_map.insert(a, a, 0);
m_map.insert(a, a, nullptr);
}
}
void map_proc::visit(quantifier* e) {
expr_ref q(m);
q = m.update_quantifier(e, get_expr(e->get_expr()));
m_map.insert(e, q, 0);
m_map.insert(e, q, nullptr);
}
expr* map_proc::get_expr(expr* e) {
expr* result = 0;
proof* p = 0;
expr* result = nullptr;
proof* p = nullptr;
m_map.get(e, result, p);
return result;
}

4
src/ast/expr_functors.h
View file

@ -73,7 +73,7 @@ class contains_app {
app* m_x;
public:
pred(app* x) : m_x(x) {}
virtual bool operator()(expr* e) {
bool operator()(expr* e) override {
return m_x == e;
}
};
@ -115,7 +115,7 @@ public:
void reset() { m_map.reset(); }
void visit(var* e) { m_map.insert(e, e, 0); }
void visit(var* e) { m_map.insert(e, e, nullptr); }
void visit(quantifier* e);

6
src/ast/expr_map.cpp
View file

@ -38,7 +38,7 @@ expr_map::~expr_map() {
void expr_map::insert(expr * k, expr * d, proof * p) {
m_manager.inc_ref(d);
obj_map<expr, expr*>::obj_map_entry * entry = m_expr2expr.find_core(k);
if (entry != 0) {
if (entry != nullptr) {
m_manager.dec_ref(entry->get_data().m_value);
entry->get_data().m_value = d;
if (m_store_proofs) {
@ -61,7 +61,7 @@ void expr_map::insert(expr * k, expr * d, proof * p) {
void expr_map::get(expr * k, expr * & d, proof * & p) const {
if (m_expr2expr.find(k, d)) {
p = 0;
p = nullptr;
if (m_store_proofs)
m_expr2pr.find(k, p);
}
@ -73,7 +73,7 @@ void expr_map::erase(expr * k) {
m_expr2expr.erase(k);
m_manager.dec_ref(v);
if (m_store_proofs) {
proof * pr = 0;
proof * pr = nullptr;
m_expr2pr.find(k, pr);
m_expr2pr.erase(k);
m_manager.dec_ref(pr);

6
src/ast/expr_substitution.cpp
View file

@ -106,20 +106,20 @@ void expr_substitution::insert(expr * c, expr * def, proof * def_pr, expr_depend
void expr_substitution::erase(expr * c) {
if (proofs_enabled()) {
proof * pr = 0;
proof * pr = nullptr;
if (m_subst_pr->find(c, pr)) {
m_manager.dec_ref(pr);
m_subst_pr->erase(c);
}
}
if (unsat_core_enabled()) {
expr_dependency * dep = 0;
expr_dependency * dep = nullptr;
if (m_subst_dep->find(c, dep)) {
m_manager.dec_ref(dep);
m_subst_dep->erase(c);
}
}
expr * def = 0;
expr * def = nullptr;
if (m_subst.find(c, def)) {
m_manager.dec_ref(c);
m_manager.dec_ref(def);

6
src/ast/expr_substitution.h
View file

@ -43,7 +43,7 @@ public:
bool unsat_core_enabled() const { return m_cores_enabled; }
bool empty() const { return m_subst.empty(); }
void insert(expr * s, expr * def, proof * def_pr = 0, expr_dependency * def_dep = 0);
void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr);
void erase(expr * s);
bool find(expr * s, expr * & def, proof * & def_pr);
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep);
@ -63,7 +63,7 @@ public:
scoped_expr_substitution(expr_substitution& s): m_subst(s), m_trail(s.m()) {}
~scoped_expr_substitution() {}
void insert(expr * s, expr * def, proof * def_pr = 0, expr_dependency * def_dep = 0) {
void insert(expr * s, expr * def, proof * def_pr = nullptr, expr_dependency * def_dep = nullptr) {
if (!m_subst.contains(s)) {
m_subst.insert(s, def, def_pr, def_dep);
m_trail.push_back(s);
@ -82,7 +82,7 @@ public:
}
unsigned scope_level() const { return m_trail_lim.size(); }
bool empty() const { return m_subst.empty(); }
expr* find(expr * e) { proof* pr; expr* d = 0; if (find(e, d, pr)) return d; else return e; }
expr* find(expr * e) { proof* pr; expr* d = nullptr; if (find(e, d, pr)) return d; else return e; }
bool find(expr * s, expr * & def, proof * & def_pr) { return m_subst.find(s, def, def_pr); }
bool find(expr * s, expr * & def, proof * & def_pr, expr_dependency * & def_dep) { return m_subst.find(s, def, def_pr, def_dep); }
bool contains(expr * s) { return m_subst.contains(s); }

4
src/ast/factor_equivs.cpp
View file

@ -34,7 +34,7 @@ Revision History:
void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
ast_manager &m = v.get_manager();
arith_util arith(m);
expr *e1 = 0, *e2 = 0;
expr *e1 = nullptr, *e2 = nullptr;
flatten_and(v);
unsigned j = 0;
@ -45,7 +45,7 @@ void factor_eqs(expr_ref_vector &v, expr_equiv_class &equiv) {
}
// y + -1*x == 0
expr* a0 = 0, *a1 = 0, *x = 0;
expr* a0 = nullptr, *a1 = nullptr, *x = nullptr;
if (arith.is_zero(e2) && arith.is_add(e1, a0, a1)) {
if (arith.is_times_minus_one(a1, x)) {
e1 = a0;

24
src/ast/format.cpp
View file

@ -32,7 +32,7 @@ namespace format_ns {
symbol m_line_break;
symbol m_line_break_ext;
virtual void set_manager(ast_manager * m, family_id id) {
void set_manager(ast_manager * m, family_id id) override {
SASSERT(m->is_format_manager());
decl_plugin::set_manager(m, id);
@ -42,7 +42,7 @@ namespace format_ns {
public:
format_decl_plugin():
m_format_sort(0),
m_format_sort(nullptr),
m_nil("nil"),
m_string("string"),
m_indent("indent"),
@ -52,24 +52,24 @@ namespace format_ns {
m_line_break_ext("cr++") {
}
virtual ~format_decl_plugin() {}
~format_decl_plugin() override {}
virtual void finalize() {
void finalize() override {
if (m_format_sort)
m_manager->dec_ref(m_format_sort);
}
virtual decl_plugin * mk_fresh() {
decl_plugin * mk_fresh() override {
return alloc(format_decl_plugin);
}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) {
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override {
SASSERT(k == FORMAT_SORT);
return m_format_sort;
}
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override {
switch (k) {
case OP_NIL:
return m_manager->mk_func_decl(m_nil, arity, domain, m_format_sort,
@ -94,7 +94,7 @@ namespace format_ns {
return m_manager->mk_func_decl(m_line_break_ext, arity, domain, m_format_sort,
func_decl_info(m_family_id, OP_LINE_BREAK_EXT, num_parameters, parameters));
default:
return 0;
return nullptr;
}
}
};
@ -124,8 +124,8 @@ namespace format_ns {
SASSERT(m_manager.is_format_manager());
}
format * visit(var *) { UNREACHABLE(); return 0; }
format * visit(quantifier * q, format *, format * const *, format * const *) { UNREACHABLE(); return 0; }
format * visit(var *) { UNREACHABLE(); return nullptr; }
format * visit(quantifier * q, format *, format * const *, format * const *) { UNREACHABLE(); return nullptr; }
format * visit(format * n, format * const * children) {
if (is_app_of(n, m_fid, OP_LINE_BREAK))
return mk_string(m_manager, " ");
@ -147,7 +147,7 @@ namespace format_ns {
format * mk_string(ast_manager & m, char const * str) {
symbol s(str);
parameter p(s);
return fm(m).mk_app(fid(m), OP_STRING, 1, &p, 0, 0);
return fm(m).mk_app(fid(m), OP_STRING, 1, &p, 0, nullptr);
}
format * mk_int(ast_manager & m, int i) {

10
src/ast/fpa/bv2fpa_converter.cpp
View file

@ -198,7 +198,7 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) {
tout << std::endl; );
if (m_fpa_util.is_float(s)) {
if (e == 0)
if (e == nullptr)
result = m_fpa_util.mk_pzero(s);
else if (m_fpa_util.is_numeral(e))
result = e;
@ -208,7 +208,7 @@ expr_ref bv2fpa_converter::rebuild_floats(model_core * mc, sort * s, app * e) {
}
}
else if (m_fpa_util.is_rm(s)) {
if (e == 0)
if (e == nullptr)
result = m_fpa_util.mk_round_toward_zero();
else if (m_fpa_util.is_rm_numeral(e))
result = e;
@ -256,7 +256,7 @@ bv2fpa_converter::array_model bv2fpa_converter::convert_array_func_interp(model_
func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl * f, func_decl * bv_f) {
SASSERT(f->get_arity() > 0);
func_interp * result = 0;
func_interp * result = nullptr;
sort * rng = f->get_range();
sort * const * dmn = f->get_domain();
@ -291,7 +291,7 @@ func_interp * bv2fpa_converter::convert_func_interp(model_core * mc, func_decl *
mk_ismt2_pp(new_args[i], m) << std::endl;
tout << mk_ismt2_pp(bv_fres, m) << " == " << mk_ismt2_pp(ft_fres, m) << std::endl;);
func_entry * fe = result->get_entry(new_args.c_ptr());
if (fe == 0)
if (fe == nullptr)
result->insert_new_entry(new_args.c_ptr(), ft_fres);
else {
// The BV model may have multiple equivalent entries using different
@ -338,7 +338,7 @@ void bv2fpa_converter::convert_consts(model_core * mc, model_core * target_model
v2 = mc->get_const_interp(a2->get_decl());
#else
expr * bv = mc->get_const_interp(to_app(to_app(a0)->get_arg(0))->get_decl());
if (bv == 0) {
if (bv == nullptr) {
v0 = m_bv_util.mk_numeral(0, 1);
v1 = m_bv_util.mk_numeral(0, ebits);
v2 = m_bv_util.mk_numeral(0, sbits-1);

2
src/ast/fpa/bv2fpa_converter.h
View file

@ -64,7 +64,7 @@ public:
func_interp * new_float_fi;
func_decl * bv_fd;
expr_ref result;
array_model(ast_manager & m) : new_float_fd(0), new_float_fi(0), bv_fd(0), result(m) {}
array_model(ast_manager & m) : new_float_fd(nullptr), new_float_fi(nullptr), bv_fd(nullptr), result(m) {}
};
array_model convert_array_func_interp(model_core * mc, func_decl * f, func_decl * bv_f);

24
src/ast/fpa/fpa2bv_converter.cpp
View file

@ -25,7 +25,7 @@ Notes:
#include "ast/fpa/fpa2bv_converter.h"
#include "ast/rewriter/fpa_rewriter.h"
#define BVULT(X,Y,R) { expr_ref bvult_eq(m), bvult_not(m); m_simp.mk_eq(X, Y, bvult_eq); m_simp.mk_not(bvult_eq, bvult_not); expr_ref t(m); t = m_bv_util.mk_ule(X,Y); m_simp.mk_and(t, bvult_not, R); }
#define BVULT(X,Y,R) { expr_ref t(m); t = m_bv_util.mk_ule(Y,X); m_simp.mk_not(t, R); }
fpa2bv_converter::fpa2bv_converter(ast_manager & m) :
m(m),
@ -197,7 +197,7 @@ void fpa2bv_converter::mk_const(func_decl * f, expr_ref & result) {
#else
app_ref bv(m);
unsigned bv_sz = 1 + ebits + (sbits - 1);
bv = mk_fresh_const(0, bv_sz);
bv = mk_fresh_const(nullptr, bv_sz);
sgn = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv);
e = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv);
@ -288,7 +288,7 @@ void fpa2bv_converter::mk_rm_const(func_decl * f, expr_ref & result) {
#ifdef Z3DEBUG
"fpa2bv_rm"
#else
0
nullptr
#endif
, m_bv_util.mk_sort(3));
@ -1274,8 +1274,8 @@ expr_ref fpa2bv_converter::mk_min_max_unspecified(func_decl * f, expr * x, expr
std::pair<app*, app*> decls(0, 0);
if (!m_min_max_ufs.find(f, decls)) {
decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1));
decls.first = m.mk_fresh_const(nullptr, m_bv_util.mk_sort(1));
decls.second = m.mk_fresh_const(nullptr, m_bv_util.mk_sort(1));
m_min_max_ufs.insert(f, decls);
m.inc_ref(f);
m.inc_ref(decls.first);
@ -2681,11 +2681,11 @@ void fpa2bv_converter::mk_to_fp_real_int(func_decl * f, unsigned num, expr * con
a_tz = m_plugin->mk_numeral(tz);
expr_ref bv_nte(m), bv_nta(m), bv_tp(m), bv_tn(m), bv_tz(m);
mk_numeral(a_nte->get_decl(), 0, 0, bv_nte);
mk_numeral(a_nta->get_decl(), 0, 0, bv_nta);
mk_numeral(a_tp->get_decl(), 0, 0, bv_tp);
mk_numeral(a_tn->get_decl(), 0, 0, bv_tn);
mk_numeral(a_tz->get_decl(), 0, 0, bv_tz);
mk_numeral(a_nte->get_decl(), 0, nullptr, bv_nte);
mk_numeral(a_nta->get_decl(), 0, nullptr, bv_nta);
mk_numeral(a_tp->get_decl(), 0, nullptr, bv_tp);
mk_numeral(a_tn->get_decl(), 0, nullptr, bv_tn);
mk_numeral(a_tz->get_decl(), 0, nullptr, bv_tz);
expr_ref c1(m), c2(m), c3(m), c4(m);
c1 = m.mk_eq(bv_rm, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3));
@ -4097,7 +4097,7 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref &
TRACE("fpa2bv_round", tout << "ROUND = " << mk_ismt2_pp(result, m) << std::endl; );
}
void fpa2bv_converter::reset(void) {
void fpa2bv_converter::reset() {
dec_ref_map_key_values(m, m_const2bv);
dec_ref_map_key_values(m, m_rm_const2bv);
dec_ref_map_key_values(m, m_uf2bvuf);
@ -4115,7 +4115,7 @@ void fpa2bv_converter::reset(void) {
func_decl * fpa2bv_converter::mk_bv_uf(func_decl * f, sort * const * domain, sort * range) {
func_decl * res;
if (!m_uf2bvuf.find(f, res)) {
res = m.mk_fresh_func_decl(0, f->get_arity(), domain, range);
res = m.mk_fresh_func_decl(nullptr, f->get_arity(), domain, range);
m_uf2bvuf.insert(f, res);
m.inc_ref(f);
m.inc_ref(res);

2
src/ast/fpa/fpa2bv_converter.h
View file

@ -150,7 +150,7 @@ public:
void mk_max(func_decl * f, unsigned num, expr * const * args, expr_ref & result);
expr_ref mk_min_max_unspecified(func_decl * f, expr * x, expr * y);
void reset(void);
void reset();
void dbg_decouple(const char * prefix, expr_ref & e);
expr_ref_vector m_extra_assertions;

4
src/ast/fpa/fpa2bv_rewriter.cpp
View file

@ -220,7 +220,7 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q,
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);
TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " <<
mk_ismt2_pp(old_q->get_expr(), m()) << std::endl <<
@ -249,7 +249,7 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res
new_exp = m().mk_var(t->get_idx(), s);
result = new_exp;
result_pr = 0;
result_pr = nullptr;
TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;);
return true;
}

26
src/ast/fpa_decl_plugin.cpp
View file

@ -23,9 +23,9 @@ Revision History:
fpa_decl_plugin::fpa_decl_plugin():
m_values(m_fm),
m_value_table(mpf_hash_proc(m_values), mpf_eq_proc(m_values)) {
m_real_sort = 0;
m_int_sort = 0;
m_bv_plugin = 0;
m_real_sort = nullptr;
m_int_sort = nullptr;
m_bv_plugin = nullptr;
}
void fpa_decl_plugin::set_manager(ast_manager * m, family_id id) {
@ -70,7 +70,7 @@ void fpa_decl_plugin::recycled_id(unsigned id) {
func_decl * fpa_decl_plugin::mk_numeral_decl(mpf const & v) {
sort * s = mk_float_sort(v.get_ebits(), v.get_sbits());
func_decl * r = 0;
func_decl * r = nullptr;
if (m_fm.is_nan(v))
r = m_manager->mk_const_decl(symbol("NaN"), s, func_decl_info(m_family_id, OP_FPA_NAN));
else if (m_fm.is_pinf(v))
@ -160,7 +160,7 @@ bool fpa_decl_plugin::is_rm_numeral(expr * n, mpf_rounding_mode & val) {
return true;
}
return 0;
return false;
}
bool fpa_decl_plugin::is_rm_numeral(expr * n) {
@ -223,7 +223,7 @@ sort * fpa_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
return mk_float_sort(15, 113);
default:
m_manager->raise_exception("unknown floating point theory sort");
return 0;
return nullptr;
}
}
@ -248,20 +248,20 @@ func_decl * fpa_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_paramete
return m_manager->mk_const_decl(symbol("roundTowardZero"), s, finfo);
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
sort * s = 0;
sort * s = nullptr;
if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {
s = to_sort(parameters[0].get_ast());
}
else if (num_parameters == 2 && parameters[0].is_int() && parameters[1].is_int()) {
s = mk_float_sort(parameters[0].get_int(), parameters[1].get_int());
}
else if (range != 0 && is_float_sort(range)) {
else if (range != nullptr && is_float_sort(range)) {
s = range;
}
else {
@ -561,7 +561,7 @@ func_decl * fpa_decl_plugin::mk_to_fp(decl_kind k, unsigned num_parameters, para
);
}
return 0;
return nullptr;
}
func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_parameters, parameter const * parameters,
@ -779,7 +779,7 @@ func_decl * fpa_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
default:
m_manager->raise_exception("unsupported floating point operator");
return 0;
return nullptr;
}
}
@ -862,12 +862,12 @@ expr * fpa_decl_plugin::get_some_value(sort * s) {
return res;
}
else if (s->is_sort_of(m_family_id, ROUNDING_MODE_SORT)) {
func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, 0, 0, 0, s);
func_decl * f = mk_rm_const_decl(OP_FPA_RM_TOWARD_ZERO, 0, nullptr, 0, nullptr, s);
return m_manager->mk_const(f);
}
UNREACHABLE();
return 0;
return nullptr;
}
bool fpa_decl_plugin::is_value(app * e) const {

32
src/ast/fpa_decl_plugin.h
View file

@ -159,11 +159,11 @@ class fpa_decl_plugin : public decl_plugin {
func_decl * mk_bv_wrap(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
unsigned mk_id(mpf const & v);
void recycled_id(unsigned id);
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
bool is_considered_uninterpreted(func_decl * f) override { return false; }
public:
fpa_decl_plugin();
@ -171,18 +171,18 @@ public:
bool is_float_sort(sort * s) const { return is_sort_of(s, m_family_id, FLOATING_POINT_SORT); }
bool is_rm_sort(sort * s) const { return is_sort_of(s, m_family_id, ROUNDING_MODE_SORT); }
virtual ~fpa_decl_plugin();
virtual void finalize();
~fpa_decl_plugin() override;
void finalize() override;
virtual decl_plugin * mk_fresh();
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
virtual expr * get_some_value(sort * s);
virtual bool is_value(app* e) const;
virtual bool is_unique_value(app* e) const;
decl_plugin * mk_fresh() override;
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override;
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
expr * get_some_value(sort * s) override;
bool is_value(app* e) const override;
bool is_unique_value(app* e) const override;
mpf_manager & fm() { return m_fm; }
func_decl * mk_numeral_decl(mpf const & v);
@ -197,8 +197,8 @@ public:
return m_values[id];
}
virtual void del(parameter const & p);
virtual parameter translate(parameter const & p, decl_plugin & target);
void del(parameter const & p) override;
parameter translate(parameter const & p, decl_plugin & target) override;
};
class fpa_util {
@ -342,7 +342,7 @@ public:
app * mk_bv2rm(expr * bv3) {
SASSERT(m_bv_util.is_bv(bv3) && m_bv_util.get_bv_size(bv3) == 3);
return m().mk_app(m_fid, OP_FPA_BV2RM, 0, 0, 1, &bv3, mk_rm_sort());
return m().mk_app(m_fid, OP_FPA_BV2RM, 0, nullptr, 1, &bv3, mk_rm_sort());
}
bool is_bvwrap(expr const * e) const { return is_app_of(e, get_family_id(), OP_FPA_BVWRAP); }

4
src/ast/func_decl_dependencies.cpp
View file

@ -86,7 +86,7 @@ class func_decl_dependencies::top_sort {
ptr_vector<func_decl> m_todo;
func_decl_set * definition(func_decl * f) const {
func_decl_set * r = 0;
func_decl_set * r = nullptr;
m_deps.find(f, r);
return r;
}
@ -210,7 +210,7 @@ bool func_decl_dependencies::insert(func_decl * f, func_decl_set * s) {
}
void func_decl_dependencies::erase(func_decl * f) {
func_decl_set * s = 0;
func_decl_set * s = nullptr;
if (m_deps.find(f, s)) {
m_manager.dec_ref(f);
dec_ref(m_manager, *s);

2
src/ast/func_decl_dependencies.h
View file

@ -96,7 +96,7 @@ public:
*/
bool contains(func_decl * f) const { return m_deps.contains(f); }
func_decl_set * get_dependencies(func_decl * f) const { func_decl_set * r = 0; m_deps.find(f, r); return r; }
func_decl_set * get_dependencies(func_decl * f) const { func_decl_set * r = nullptr; m_deps.find(f, r); return r; }
/**
\brief Erase \c f (and its dependencies) from the manager.

6
src/ast/macro_substitution.cpp
View file

@ -123,20 +123,20 @@ void macro_substitution::insert(func_decl * f, quantifier * q, proof * pr, expr_
void macro_substitution::erase(func_decl * f) {
if (proofs_enabled()) {
proof * pr = 0;
proof * pr = nullptr;
if (m_decl2macro_pr->find(f, pr)) {
m_manager.dec_ref(pr);
m_decl2macro_pr->erase(f);
}
}
if (unsat_core_enabled()) {
expr_dependency * dep = 0;
expr_dependency * dep = nullptr;
if (m_decl2macro_dep->find(f, dep)) {
m_manager.dec_ref(dep);
m_decl2macro_dep->erase(f);
}
}
quantifier * q = 0;
quantifier * q = nullptr;
if (m_decl2macro.find(f, q)) {
m_manager.dec_ref(f);
m_manager.dec_ref(q);

2
src/ast/macro_substitution.h
View file

@ -45,7 +45,7 @@ public:
bool empty() const { return m_decl2macro.empty(); }
void insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = 0);
void insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr);
void erase(func_decl * f);
bool contains(func_decl * f) { return m_decl2macro.contains(f); }
bool find(func_decl * f, quantifier * & q, proof * & pr);

18
src/ast/macros/macro_finder.cpp
View file

@ -71,7 +71,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, expr_dependency * dep, e
quantifier_ref new_q(m);
new_q = m.update_quantifier(to_quantifier(n), new_body);
proof * new_pr = 0;
proof * new_pr = nullptr;
if (m.proofs_enabled()) {
proof * rw = m.mk_rewrite(n, new_q);
new_pr = m.mk_modus_ponens(pr, rw);
@ -142,7 +142,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
quantifier_ref new_q(m);
new_q = m.update_quantifier(to_quantifier(n), new_body);
proof * new_pr = 0;
proof * new_pr = nullptr;
if (m.proofs_enabled()) {
proof * rw = m.mk_rewrite(n, new_q);
new_pr = m.mk_modus_ponens(pr, rw);
@ -163,7 +163,7 @@ bool macro_finder::is_arith_macro(expr * n, proof * pr, vector<justified_expr>&
quantifier * q1 = m.update_quantifier(new_q, body1);
expr * patterns[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(new_q, 1, patterns, body2);
proof* pr1 = 0, *pr2 = 0;
proof* pr1 = nullptr, *pr2 = nullptr;
if (m.proofs_enabled()) {
// new_pr : new_q
// rw : [rewrite] new_q ~ q1 & q2
@ -233,7 +233,7 @@ static void pseudo_predicate_macro2macro(ast_manager & m, app * head, app * t, e
app * body_1 = m.mk_eq(head, ite);
app * body_2 = m.mk_not(m.mk_eq(k_app, t));
quantifier * q1 = m.update_quantifier(q, body_1);
proof * pr1 = 0, *pr2 = 0;
proof * pr1 = nullptr, *pr2 = nullptr;
expr * pats[1] = { m.mk_pattern(k_app) };
quantifier * q2 = m.update_quantifier(q, 1, pats, body_2); // erase patterns
if (m.proofs_enabled()) {
@ -268,8 +268,8 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
bool found_new_macro = false;
for (unsigned i = 0; i < num; i++) {
expr * n = exprs[i];
proof * pr = m.proofs_enabled() ? prs[i] : 0;
expr_dependency * depi = deps != 0 ? deps[i] : 0;
proof * pr = m.proofs_enabled() ? prs[i] : nullptr;
expr_dependency * depi = deps != nullptr ? deps[i] : nullptr;
expr_ref new_n(m), def(m);
proof_ref new_pr(m);
expr_dependency_ref new_dep(m);
@ -292,7 +292,7 @@ bool macro_finder::expand_macros(unsigned num, expr * const * exprs, proof * con
new_exprs.push_back(new_n);
if (m.proofs_enabled())
new_prs.push_back(new_pr);
if (deps != 0)
if (deps != nullptr)
new_deps.push_back(new_dep);
}
}
@ -333,11 +333,11 @@ bool macro_finder::expand_macros(unsigned num, justified_expr const * fmls, vect
bool found_new_macro = false;
for (unsigned i = 0; i < num; i++) {
expr * n = fmls[i].get_fml();
proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : 0;
proof * pr = m.proofs_enabled() ? fmls[i].get_proof() : nullptr;
expr_ref new_n(m), def(m);
proof_ref new_pr(m);
expr_dependency_ref new_dep(m);
m_macro_manager.expand_macros(n, pr, 0, new_n, new_pr, new_dep);
m_macro_manager.expand_macros(n, pr, nullptr, new_n, new_pr, new_dep);
app_ref head(m), t(m);
if (is_macro(new_n, head, def) && m_macro_manager.insert(head->get_decl(), to_quantifier(new_n.get()), new_pr)) {
TRACE("macro_finder_found", tout << "found new macro: " << head->get_decl()->get_name() << "\n" << new_n << "\n";);

16
src/ast/macros/macro_manager.cpp
View file

@ -188,7 +188,7 @@ void macro_manager::display(std::ostream & out) {
unsigned sz = m_decls.size();
for (unsigned i = 0; i < sz; i++) {
func_decl * f = m_decls.get(i);
quantifier * q = 0;
quantifier * q = nullptr;
m_decl2macro.find(f, q);
app * head;
expr * def;
@ -226,7 +226,7 @@ struct macro_manager::macro_expander_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 BR_FAILED;
}
@ -255,7 +255,7 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
erase_patterns = true;
}
if (erase_patterns) {
result = m.update_quantifier(old_q, 0, 0, 0, 0, new_body);
result = m.update_quantifier(old_q, 0, nullptr, 0, nullptr, new_body);
}
return erase_patterns;
}
@ -264,13 +264,13 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
if (!is_app(_n))
return false;
app * n = to_app(_n);
quantifier * q = 0;
quantifier * q = nullptr;
func_decl * d = n->get_decl();
TRACE("macro_manager", tout << "trying to expand:\n" << mk_pp(n, m) << "\nd:\n" << d->get_name() << "\n";);
if (mm.m_decl2macro.find(d, q)) {
TRACE("macro_manager", tout << "expanding: " << mk_pp(n, m) << "\n";);
app * head = 0;
expr * def = 0;
app * head = nullptr;
expr * def = nullptr;
mm.get_head_def(q, d, head, def);
unsigned num = n->get_num_args();
SASSERT(head && def);
@ -292,14 +292,14 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg {
expr_ref instance(m);
s(q->get_expr(), num, subst_args.c_ptr(), instance);
proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.c_ptr());
proof * q_pr = 0;
proof * q_pr = nullptr;
mm.m_decl2macro_pr.find(d, q_pr);
SASSERT(q_pr != 0);
proof * prs[2] = { qi_pr, q_pr };
p = m.mk_unit_resolution(2, prs);
}
else {
p = 0;
p = nullptr;
}
expr_dependency * ed = mm.m_decl2macro_dep.find(d);
m_used_macro_dependencies = m.mk_join(m_used_macro_dependencies, ed);

4
src/ast/macros/macro_manager.h
View file

@ -67,7 +67,7 @@ public:
~macro_manager();
ast_manager & get_manager() const { return m; }
macro_util & get_util() { return m_util; }
bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = 0);
bool insert(func_decl * f, quantifier * m, proof * pr, expr_dependency * dep = nullptr);
bool has_macros() const { return !m_macros.empty(); }
void push_scope();
void pop_scope(unsigned num_scopes);
@ -82,7 +82,7 @@ public:
unsigned get_first_macro_last_level() const { return m_scopes.empty() ? 0 : m_scopes.back().m_decls_lim; }
func_decl * get_macro_func_decl(unsigned i) const { return m_decls.get(i); }
func_decl * get_macro_interpretation(unsigned i, expr_ref & interp) const;
quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = 0; m_decl2macro.find(f, q); return q; }
quantifier * get_macro_quantifier(func_decl * f) const { quantifier * q = nullptr; m_decl2macro.find(f, q); return q; }
void get_head_def(quantifier * q, func_decl * d, app * & head, expr * & def) const;
void expand_macros(expr * n, proof * pr, expr_dependency * dep, expr_ref & r, proof_ref & new_pr, expr_dependency_ref & new_dep);

32
src/ast/macros/macro_util.cpp
View file

@ -33,8 +33,8 @@ macro_util::macro_util(ast_manager & m):
m_arith(m),
m_arith_rw(m),
m_bv_rw(m),
m_forbidden_set(0),
m_curr_clause(0) {
m_forbidden_set(nullptr),
m_curr_clause(nullptr) {
}
@ -256,7 +256,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
inv = false;
ptr_buffer<expr> args;
expr * h = 0;
expr * h = nullptr;
unsigned lhs_num_args;
expr * const * lhs_args;
if (is_add(lhs)) {
@ -270,13 +270,13 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
for (unsigned i = 0; i < lhs_num_args; i++) {
expr * arg = lhs_args[i];
expr * neg_arg;
if (h == 0 &&
if (h == nullptr &&
is_macro_head(arg, num_decls) &&
!is_forbidden(to_app(arg)->get_decl()) &&
!poly_contains_head(lhs, to_app(arg)->get_decl(), arg)) {
h = arg;
}
else if (h == 0 && m_arith_rw.is_times_minus_one(arg, neg_arg) &&
else if (h == nullptr && m_arith_rw.is_times_minus_one(arg, neg_arg) &&
is_macro_head(neg_arg, num_decls) &&
!is_forbidden(to_app(neg_arg)->get_decl()) &&
!poly_contains_head(lhs, to_app(neg_arg)->get_decl(), arg)) {
@ -287,7 +287,7 @@ bool macro_util::is_arith_macro(expr * n, unsigned num_decls, app_ref & head, ex
args.push_back(arg);
}
}
if (h == 0)
if (h == nullptr)
return false;
head = to_app(h);
expr_ref tmp(m_manager);
@ -666,7 +666,7 @@ void macro_util::insert_macro(app * head, unsigned num_decls, expr * def, expr *
expr_ref norm_def(m_manager);
expr_ref norm_cond(m_manager);
normalize_expr(head, num_decls, def, norm_def);
if (cond != 0)
if (cond != nullptr)
normalize_expr(head, num_decls, cond, norm_cond);
else if (!hint)
norm_cond = m_manager.mk_true();
@ -682,7 +682,7 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def,
expr_ref new_cond(m_manager);
if (!hint) {
quasi_macro_head_to_macro_head(head, num_decls, new_head, extra_cond);
if (cond == 0)
if (cond == nullptr)
new_cond = extra_cond;
else
bool_rewriter(m_manager).mk_and(cond, extra_cond, new_cond);
@ -701,7 +701,7 @@ void macro_util::insert_quasi_macro(app * head, unsigned num_decls, expr * def,
}
bool macro_util::rest_contains_decl(func_decl * f, expr * except_lit) {
if (m_curr_clause == 0)
if (m_curr_clause == nullptr)
return false;
SASSERT(is_clause(m_manager, m_curr_clause));
unsigned num_lits = get_clause_num_literals(m_manager, m_curr_clause);
@ -714,7 +714,7 @@ bool macro_util::rest_contains_decl(func_decl * f, expr * except_lit) {
}
void macro_util::get_rest_clause_as_cond(expr * except_lit, expr_ref & extra_cond) {
if (m_curr_clause == 0)
if (m_curr_clause == nullptr)
return;
SASSERT(is_clause(m_manager, m_curr_clause));
expr_ref_buffer neg_other_lits(m_manager);
@ -795,7 +795,7 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a
mk_sub(rhs, rest, def);
// If is_poly_hint, rhs may contain variables that do not occur in to_app(arg).
// So, we should re-check.
if (!_is_poly_hint || is_poly_hint(def, to_app(arg), 0))
if (!_is_poly_hint || is_poly_hint(def, to_app(arg), nullptr))
add_arith_macro_candidate(to_app(arg), num_decls, def, atom, is_ineq, _is_poly_hint, r);
}
else if (is_times_minus_one(arg, neg_arg) && is_app(neg_arg)) {
@ -816,7 +816,7 @@ void macro_util::collect_arith_macro_candidates(expr * lhs, expr * rhs, expr * a
mk_sub(rest, rhs, def);
// If is_poly_hint, rhs may contain variables that do not occur in to_app(neg_arg).
// So, we should re-check.
if (!_is_poly_hint || is_poly_hint(def, to_app(neg_arg), 0))
if (!_is_poly_hint || is_poly_hint(def, to_app(neg_arg), nullptr))
add_arith_macro_candidate(to_app(neg_arg), num_decls, def, atom, is_ineq, _is_poly_hint, r);
}
}
@ -885,7 +885,7 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
insert_quasi_macro(to_app(lhs), num_decls, rhs, cond, false, true, false, r);
}
else if (is_hint_atom(lhs, rhs)) {
insert_quasi_macro(to_app(lhs), num_decls, rhs, 0, false, true, true, r);
insert_quasi_macro(to_app(lhs), num_decls, rhs, nullptr, false, true, true, r);
}
if (is_quasi_macro_head(rhs, num_decls) &&
@ -897,7 +897,7 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
insert_quasi_macro(to_app(rhs), num_decls, lhs, cond, false, true, false, r);
}
else if (is_hint_atom(rhs, lhs)) {
insert_quasi_macro(to_app(rhs), num_decls, lhs, 0, false, true, true, r);
insert_quasi_macro(to_app(rhs), num_decls, lhs, nullptr, false, true, true, r);
}
}
@ -905,7 +905,7 @@ void macro_util::collect_macro_candidates_core(expr * atom, unsigned num_decls,
}
void macro_util::collect_macro_candidates(expr * atom, unsigned num_decls, macro_candidates & r) {
m_curr_clause = 0;
m_curr_clause = nullptr;
r.reset();
collect_macro_candidates_core(atom, num_decls, r);
}
@ -922,7 +922,7 @@ void macro_util::collect_macro_candidates(quantifier * q, macro_candidates & r)
unsigned num_lits = get_clause_num_literals(m_manager, n);
for (unsigned i = 0; i < num_lits; i++)
collect_macro_candidates_core(get_clause_literal(m_manager, n, i), num_decls, r);
m_curr_clause = 0;
m_curr_clause = nullptr;
}
else {
collect_macro_candidates_core(n, num_decls, r);

2
src/ast/macros/macro_util.h
View file

@ -64,7 +64,7 @@ private:
mutable bv_rewriter m_bv_rw;
obj_hashtable<func_decl> * m_forbidden_set;
bool is_forbidden(func_decl * f) const { return m_forbidden_set != 0 && m_forbidden_set->contains(f); }
bool is_forbidden(func_decl * f) const { return m_forbidden_set != nullptr && m_forbidden_set->contains(f); }
bool poly_contains_head(expr * n, func_decl * f, expr * exception) const;
void collect_arith_macros(expr * n, unsigned num_decls, unsigned max_macros, bool allow_cond_macros,

14
src/ast/macros/quasi_macros.cpp
View file

@ -91,7 +91,7 @@ public:
void operator()(var * n) { m_bitset.set(n->get_idx(), true); }
void operator()(quantifier * n) {}
void operator()(app * n) {}
bool all_used(void) {
bool all_used() {
for (unsigned i = 0; i < m_bitset.size() ; i++)
if (!m_bitset.get(i))
return false;
@ -281,10 +281,10 @@ bool quasi_macros::find_macros(unsigned n, expr * const * exprs) {
quasi_macro_to_macro(to_quantifier(exprs[i]), a, t, macro);
TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i], m_manager) << std::endl;
tout << "Macro: " << mk_pp(macro, m_manager) << std::endl; );
proof * pr = 0;
proof * pr = nullptr;
if (m_manager.proofs_enabled())
pr = m_manager.mk_def_axiom(macro);
expr_dependency * dep = 0;
expr_dependency * dep = nullptr;
if (m_macro_manager.insert(a->get_decl(), macro, pr, dep))
res = true;
}
@ -320,7 +320,7 @@ bool quasi_macros::find_macros(unsigned n, justified_expr const * exprs) {
quasi_macro_to_macro(to_quantifier(exprs[i].get_fml()), a, t, macro);
TRACE("quasi_macros", tout << "Found quasi macro: " << mk_pp(exprs[i].get_fml(), m_manager) << std::endl;
tout << "Macro: " << mk_pp(macro, m_manager) << std::endl; );
proof * pr = 0;
proof * pr = nullptr;
if (m_manager.proofs_enabled())
pr = m_manager.mk_def_axiom(macro);
if (m_macro_manager.insert(a->get_decl(), macro, pr))
@ -336,7 +336,7 @@ void quasi_macros::apply_macros(unsigned n, expr * const * exprs, proof * const
expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager);
expr_dependency_ref dep(m_manager);
proof * p = m_manager.proofs_enabled() ? prs[i] : 0;
proof * p = m_manager.proofs_enabled() ? prs[i] : nullptr;
m_macro_manager.expand_macros(exprs[i], p, deps[i], r, pr, dep);
m_rewriter(r);
@ -366,9 +366,9 @@ void quasi_macros::apply_macros(unsigned n, justified_expr const* fmls, vector<j
for ( unsigned i = 0 ; i < n ; i++ ) {
expr_ref r(m_manager), rs(m_manager);
proof_ref pr(m_manager), ps(m_manager);
proof * p = m_manager.proofs_enabled() ? fmls[i].get_proof() : 0;
proof * p = m_manager.proofs_enabled() ? fmls[i].get_proof() : nullptr;
expr_dependency_ref dep(m_manager);
m_macro_manager.expand_macros(fmls[i].get_fml(), p, 0, r, pr, dep);
m_macro_manager.expand_macros(fmls[i].get_fml(), p, nullptr, r, pr, dep);
m_rewriter(r);
new_fmls.push_back(justified_expr(m_manager, r, pr));
}

4
src/ast/normal_forms/defined_names.cpp
View file

@ -74,7 +74,7 @@ struct defined_names::impl {
struct defined_names::pos_impl : public defined_names::impl {
pos_impl(ast_manager & m, char const * fresh_prefix):impl(m, fresh_prefix) {}
virtual void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def);
void mk_definition(expr * e, app * n, sort_ref_buffer & var_sorts, buffer<symbol> const & var_names, expr_ref & new_def) override;
};
@ -210,7 +210,7 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
n = n_ptr;
if (m_manager.proofs_enabled()) {
proof * pr_ptr = 0;
proof * pr_ptr = nullptr;
m_expr2proof.find(e, pr_ptr);
SASSERT(pr_ptr);
pr = pr_ptr;

22
src/ast/normal_forms/name_exprs.cpp
View file

@ -38,8 +38,8 @@ class name_exprs_core : public name_exprs {
m_pred(pred),
m_r(m),
m_pr(m),
m_def_exprs(0),
m_def_proofs(0) {
m_def_exprs(nullptr),
m_def_proofs(nullptr) {
}
void gen_name_for_expr(expr * n, expr * & t, proof * & t_pr) {
@ -77,10 +77,10 @@ public:
m_rw(m, m.proofs_enabled(), m_cfg) {
}
virtual ~name_exprs_core() {
~name_exprs_core() override {
}
virtual void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
m_cfg.m_def_exprs = &new_defs;
m_cfg.m_def_proofs = &new_def_proofs;
m_rw(n, r, p);
@ -88,7 +88,7 @@ public:
}
virtual void reset() {
void reset() override {
m_rw.reset();
}
};
@ -102,7 +102,7 @@ class name_quantifier_labels : public name_exprs_core {
ast_manager & m_manager;
public:
pred(ast_manager & m):m_manager(m) {}
virtual bool operator()(expr * t) {
bool operator()(expr * t) override {
return is_quantifier(t) || m_manager.is_label(t);
}
};
@ -114,7 +114,7 @@ public:
m_pred(m) {
}
virtual ~name_quantifier_labels() {
~name_quantifier_labels() override {
}
};
@ -127,9 +127,9 @@ class name_nested_formulas : public name_exprs_core {
ast_manager & m_manager;
expr * m_root;
pred(ast_manager & m):m_manager(m), m_root(0) {}
pred(ast_manager & m):m_manager(m), m_root(nullptr) {}
virtual bool operator()(expr * t) {
bool operator()(expr * t) override {
TRACE("name_exprs", tout << "name_nested_formulas::pred:\n" << mk_ismt2_pp(t, m_manager) << "\n";);
if (is_app(t))
return to_app(t)->get_family_id() == m_manager.get_basic_family_id() && to_app(t)->get_num_args() > 0 && t != m_root;
@ -145,10 +145,10 @@ public:
m_pred(m) {
}
virtual ~name_nested_formulas() {
~name_nested_formulas() override {
}
virtual void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) {
void operator()(expr * n, expr_ref_vector & new_defs, proof_ref_vector & new_def_proofs, expr_ref & r, proof_ref & p) override {
m_pred.m_root = n;
TRACE("name_exprs", tout << "operator()\n";);
name_exprs_core::operator()(n, new_defs, new_def_proofs, r, p);

26
src/ast/normal_forms/nnf.cpp
View file

@ -82,7 +82,7 @@ class skolemizer {
expr_ref_vector args(m());
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
if (s != 0) {
if (s != nullptr) {
sorts.push_back(s);
args.push_back(m().mk_var(i, s));
}
@ -105,10 +105,10 @@ class skolemizer {
//
for (unsigned i = 0; i < sz; i++) {
sort * s = uv.get(i);
if (s != 0)
if (s != nullptr)
substitution.push_back(m().mk_var(i, s));
else
substitution.push_back(0);
substitution.push_back(nullptr);
}
//
// (VAR num_decls) ... (VAR num_decls+sz-1)
@ -137,7 +137,7 @@ class skolemizer {
}
}
s(body, substitution.size(), substitution.c_ptr(), r);
p = 0;
p = nullptr;
if (m().proofs_enabled()) {
if (q->is_forall())
p = m().mk_skolemization(m().mk_not(q), m().mk_not(r));
@ -163,8 +163,8 @@ public:
void operator()(quantifier * q, expr_ref & r, proof_ref & p) {
r = m_cache.find(q);
if (r.get() != 0) {
p = 0;
if (r.get() != nullptr) {
p = nullptr;
if (m().proofs_enabled())
p = static_cast<proof*>(m_cache_pr.find(q));
}
@ -496,7 +496,7 @@ struct nnf::imp {
return false;
}
expr * r = m_result_stack.back();
proof * pr = 0;
proof * pr = nullptr;
if (proofs_enabled()) {
pr = m_result_pr_stack.back();
if (!fr.m_pol) {
@ -673,7 +673,7 @@ struct nnf::imp {
}
expr * arg = m_result_stack.back();
proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
proof * arg_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr;
if (m_ignore_labels && !proofs_enabled())
return true; // the result is already on the stack
@ -765,7 +765,7 @@ struct nnf::imp {
if (q->is_forall() == fr.m_pol || !m_skolemize) {
expr * new_expr = m_result_stack.back();
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : 0;
proof * new_expr_pr = proofs_enabled() ? m_result_pr_stack.back() : nullptr;
ptr_buffer<expr> new_patterns;
@ -783,8 +783,8 @@ struct nnf::imp {
// So, ignore patterns
}
quantifier * new_q = 0;
proof * new_q_pr = 0;
quantifier * new_q = nullptr;
proof * new_q_pr = nullptr;
if (fr.m_pol) {
new_q = m().update_quantifier(q, new_patterns.size(), new_patterns.c_ptr(), new_expr);
if (proofs_enabled())
@ -827,7 +827,7 @@ struct nnf::imp {
if (proofs_enabled()) {
result_pr = m_result_pr_stack.back();
m_result_pr_stack.pop_back();
if (result_pr.get() == 0)
if (result_pr.get() == nullptr)
result_pr = m().mk_reflexivity(t);
SASSERT(m_result_pr_stack.empty());
}
@ -870,7 +870,7 @@ struct nnf::imp {
if (status) {
if (fr.m_cache_result)
cache_result(fr.m_curr, fr.m_pol, fr.m_in_q, m_result_stack.back(), proofs_enabled() ? m_result_pr_stack.back() : 0);
cache_result(fr.m_curr, fr.m_pol, fr.m_in_q, m_result_stack.back(), proofs_enabled() ? m_result_pr_stack.back() : nullptr);
m_frame_stack.pop_back();
}
}

12
src/ast/normal_forms/pull_quant.cpp
View file

@ -85,7 +85,7 @@ struct pull_quant::imp {
var_sorts.push_back(nested_q->get_decl_sort(j));
symbol s = nested_q->get_decl_name(j);
if (std::find(var_names.begin(), var_names.end(), s) != var_names.end())
var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? 0 : s.bare_str()));
var_names.push_back(m_manager.mk_fresh_var_name(s.is_numerical() ? nullptr : s.bare_str()));
else
var_names.push_back(s);
}
@ -215,7 +215,7 @@ struct pull_quant::imp {
// Code for proof generation...
void pull_quant2(expr * n, expr_ref & r, proof_ref & pr) {
pr = 0;
pr = nullptr;
if (is_app(n)) {
expr_ref_buffer new_args(m_manager);
expr_ref new_arg(m_manager);
@ -231,8 +231,8 @@ struct pull_quant::imp {
pull_quant1(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr(), r);
if (m_manager.proofs_enabled()) {
app * r1 = m_manager.mk_app(to_app(n)->get_decl(), new_args.size(), new_args.c_ptr());
proof * p1 = proofs.empty() ? 0 : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
proof * p2 = r1 == r ? 0 : m_manager.mk_pull_quant(r1, to_quantifier(r));
proof * p1 = proofs.empty() ? nullptr : m_manager.mk_congruence(to_app(n), r1, proofs.size(), proofs.c_ptr());
proof * p2 = r1 == r ? nullptr : m_manager.mk_pull_quant(r1, to_quantifier(r));
pr = m_manager.mk_transitivity(p1, p2);
}
}
@ -242,12 +242,12 @@ struct pull_quant::imp {
pull_quant1(to_quantifier(n), new_expr, r);
if (m_manager.proofs_enabled()) {
quantifier * q1 = m_manager.update_quantifier(to_quantifier(n), new_expr);
proof * p1 = 0;
proof * p1 = nullptr;
if (n != q1) {
proof * p0 = m_manager.mk_pull_quant(n, to_quantifier(new_expr));
p1 = m_manager.mk_quant_intro(to_quantifier(n), q1, p0);
}
proof * p2 = q1 == r ? 0 : m_manager.mk_pull_quant(q1, to_quantifier(r));
proof * p2 = q1 == r ? nullptr : m_manager.mk_pull_quant(q1, to_quantifier(r));
pr = m_manager.mk_transitivity(p1, p2);
}
}

2
src/ast/pattern/expr_pattern_match.cpp
View file

@ -83,7 +83,7 @@ expr_pattern_match::instantiate(expr* a, unsigned num_bound, subst& s, expr_ref&
inst_proc proc(m_manager, s, b, m_regs);
for_each_ast(proc, a);
expr* v = 0;
expr* v = nullptr;
proc.m_memoize.find(a, v);
SASSERT(v);
result = v;

4
src/ast/pattern/expr_pattern_match.h
View file

@ -80,7 +80,7 @@ class expr_pattern_match {
}
void operator()(var* v) {
var* b = 0;
var* b = nullptr;
if (m_bound.find(v, b)) {
m_memoize.insert(v, b);
}
@ -99,7 +99,7 @@ class expr_pattern_match {
decl = to_app(m_regs[r])->get_decl();
}
for (unsigned i = 0; i < num_args; ++i) {
expr* arg = 0;
expr* arg = nullptr;
if (m_memoize.find(n->get_arg(i), arg)) {
SASSERT(arg);
args.push_back(arg);

22
src/ast/pattern/pattern_inference.cpp
View file

@ -168,7 +168,7 @@ bool pattern_inference_cfg::collect::visit_children(expr * n, unsigned delta) {
inline void pattern_inference_cfg::collect::save(expr * n, unsigned delta, info * i) {
m_cache.insert(entry(n, delta), i);
if (i != 0)
if (i != nullptr)
m_info.push_back(i);
}
@ -181,7 +181,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
uint_set free_vars;
if (idx < m_num_bindings)
free_vars.insert(idx);
info * i = 0;
info * i = nullptr;
if (delta == 0)
i = alloc(info, m, n, free_vars, 1);
else
@ -189,7 +189,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
save(n, delta, i);
}
else {
save(n, delta, 0);
save(n, delta, nullptr);
}
return;
}
@ -197,7 +197,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
app * c = to_app(n);
func_decl * decl = c->get_decl();
if (m_owner.is_forbidden(c)) {
save(n, delta, 0);
save(n, delta, nullptr);
return;
}
@ -213,14 +213,14 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
unsigned num = c->get_num_args();
for (unsigned i = 0; i < num; i++) {
expr * child = c->get_arg(i);
info * child_info = 0;
info * child_info = nullptr;
#ifdef Z3DEBUG
bool found =
#endif
m_cache.find(entry(child, delta), child_info);
SASSERT(found);
if (child_info == 0) {
save(n, delta, 0);
if (child_info == nullptr) {
save(n, delta, nullptr);
return;
}
buffer.push_back(child_info->m_node.get());
@ -230,7 +230,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
changed = true;
}
app * new_node = 0;
app * new_node = nullptr;
if (changed)
new_node = m.mk_app(decl, buffer.size(), buffer.c_ptr());
else
@ -254,7 +254,7 @@ void pattern_inference_cfg::collect::save_candidate(expr * n, unsigned delta) {
return;
}
default:
save(n, delta, 0);
save(n, delta, nullptr);
return;
}
}
@ -630,7 +630,7 @@ bool pattern_inference_cfg::reduce_quantifier(
if (new_patterns.empty() && num_no_patterns > 0) {
if (new_patterns.empty()) {
mk_patterns(q->get_num_decls(), new_body, 0, 0, new_patterns);
mk_patterns(q->get_num_decls(), new_body, 0, nullptr, new_patterns);
if (m_params.m_pi_warnings && !new_patterns.empty()) {
warning_msg("ignoring nopats annotation because Z3 couldn't find any other pattern (quantifier id: %s)", q->get_qid().str().c_str());
}
@ -683,7 +683,7 @@ bool pattern_inference_cfg::reduce_quantifier(
pull(new_q, new_expr, new_pr);
quantifier * result2 = to_quantifier(new_expr);
if (result2 != new_q) {
mk_patterns(result2->get_num_decls(), result2->get_expr(), 0, 0, new_patterns);
mk_patterns(result2->get_num_decls(), result2->get_expr(), 0, nullptr, new_patterns);
if (!new_patterns.empty()) {
if (m_params.m_pi_warnings) {
warning_msg("pulled nested quantifier to be able to find an useable pattern (quantifier id: %s)", q->get_qid().str().c_str());

2
src/ast/pattern/pattern_inference.h
View file

@ -118,7 +118,7 @@ class pattern_inference_cfg : public default_rewriter_cfg {
struct entry {
expr * m_node;
unsigned m_delta;
entry():m_node(0), m_delta(0) {}
entry():m_node(nullptr), m_delta(0) {}
entry(expr * n, unsigned d):m_node(n), m_delta(d) {}
unsigned hash() const {
return hash_u_u(m_node->get_id(), m_delta);

6
src/ast/pb_decl_plugin.cpp
View file

@ -86,7 +86,7 @@ func_decl * pb_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p
}
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
@ -299,6 +299,6 @@ bool pb_util::has_unit_coefficients(func_decl* f) const {
app* pb_util::mk_fresh_bool() {
symbol name = m.mk_fresh_var_name("pb");
func_decl_info info(m_fid, OP_PB_AUX_BOOL, 0, 0);
return m.mk_const(m.mk_func_decl(name, 0, (sort *const*)0, m.mk_bool_sort(), info));
func_decl_info info(m_fid, OP_PB_AUX_BOOL, 0, nullptr);
return m.mk_const(m.mk_func_decl(name, 0, (sort *const*)nullptr, m.mk_bool_sort(), info));
}

16
src/ast/pb_decl_plugin.h
View file

@ -53,14 +53,14 @@ class pb_decl_plugin : public decl_plugin {
func_decl * mk_eq(unsigned arity, rational const* coeffs, int k);
public:
pb_decl_plugin();
virtual ~pb_decl_plugin() {}
~pb_decl_plugin() override {}
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) override {
UNREACHABLE();
return 0;
return nullptr;
}
virtual decl_plugin * mk_fresh() {
decl_plugin * mk_fresh() override {
return alloc(pb_decl_plugin);
}
@ -69,11 +69,11 @@ public:
// parameters[0] - integer (at most k elements)
// all sorts are Booleans
// parameters[1] .. parameters[arity] - coefficients
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
virtual bool is_considered_uninterpreted(func_decl * f) { return false; }
bool is_considered_uninterpreted(func_decl * f) override { return false; }
};

99
src/ast/proofs/proof_checker.cpp
View file

@ -17,10 +17,10 @@ Copyright (c) 2015 Microsoft Corporation
#define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
proof_checker::hyp_decl_plugin::hyp_decl_plugin() :
m_cons(0),
m_atom(0),
m_nil(0),
m_cell(0) {
m_cons(nullptr),
m_atom(nullptr),
m_nil(nullptr),
m_cell(nullptr) {
}
void proof_checker::hyp_decl_plugin::finalize() {
@ -54,7 +54,7 @@ func_decl * proof_checker::hyp_decl_plugin::mk_func_decl(decl_kind k) {
case OP_NIL: return m_nil;
default:
UNREACHABLE();
return 0;
return nullptr;
}
}
@ -440,16 +440,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_PULL_QUANT_STAR: {
if (match_proof(p) &&
match_fact(p, fact) &&
match_iff(fact.get(), t1, t2)) {
// TBD: check the enchilada.
return true;
}
IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m););
return false;
}
case PR_PUSH_QUANT: {
if (match_proof(p) &&
match_fact(p, fact) &&
@ -730,16 +720,12 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
// TBD:
return true;
}
case PR_NNF_STAR: {
// TBD:
return true;
}
case PR_SKOLEMIZE: {
// (exists ?x (p ?x y)) -> (p (sk y) y)
// (not (forall ?x (p ?x y))) -> (not (p (sk y) y))
if (match_fact(p, fact) &&
match_oeq(fact.get(), t1, t2)) {
quantifier* q = 0;
quantifier* q = nullptr;
expr* e = t1.get();
bool is_forall = false;
if (match_not(t1.get(), s1)) {
@ -755,19 +741,6 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
UNREACHABLE();
return false;
}
case PR_CNF_STAR: {
for (unsigned i = 0; i < proofs.size(); ++i) {
if (match_op(proofs[i].get(), PR_DEF_INTRO, terms)) {
// ok
}
else {
UNREACHABLE();
return false;
}
}
// coarse grain CNF conversion.
return true;
}
case PR_MODUS_PONENS_OEQ: {
if (match_fact(p, fact) &&
match_proof(p, p0, p1) &&
@ -823,7 +796,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
premise0 = fmls[0].get();
for (unsigned i = 1; i < fmls.size(); ++i) {
expr_ref lit1(m), lit2(m);
expr* lit3 = 0;
expr* lit3 = nullptr;
std::pair<unsigned, unsigned> pos = positions[i-1];
premise1 = fmls[i].get();
set_false(premise0, pos.first, lit1);
@ -922,7 +895,7 @@ void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
}
}
bool proof_checker::match_fact(proof* p, expr_ref& fact) {
bool proof_checker::match_fact(proof const* p, expr_ref& fact) const {
if (m.is_proof(p) &&
m.has_fact(p)) {
fact = m.get_fact(p);
@ -938,13 +911,13 @@ void proof_checker::add_premise(proof* p) {
}
}
bool proof_checker::match_proof(proof* p) {
bool proof_checker::match_proof(proof const* p) const {
return
m.is_proof(p) &&
m.get_num_parents(p) == 0;
}
bool proof_checker::match_proof(proof* p, proof_ref& p0) {
bool proof_checker::match_proof(proof const* p, proof_ref& p0) const {
if (m.is_proof(p) &&
m.get_num_parents(p) == 1) {
p0 = m.get_parent(p, 0);
@ -953,7 +926,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0) {
return false;
}
bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
bool proof_checker::match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const {
if (m.is_proof(p) &&
m.get_num_parents(p) == 2) {
p0 = m.get_parent(p, 0);
@ -963,7 +936,7 @@ bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
return false;
}
bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
bool proof_checker::match_proof(proof const* p, proof_ref_vector& parents) const {
if (m.is_proof(p)) {
for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
parents.push_back(m.get_parent(p, i));
@ -974,7 +947,7 @@ bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
}
bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_num_args() == 2) {
d = to_app(e)->get_decl();
@ -986,7 +959,7 @@ bool proof_checker::match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_r
}
bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms) {
bool proof_checker::match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP) {
d = to_app(e)->get_decl();
for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
@ -997,9 +970,9 @@ bool proof_checker::match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms)
return false;
}
bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) {
bool proof_checker::match_quantifier(expr const* e, bool& is_univ, sort_ref_vector& sorts, expr_ref& body) const {
if (is_quantifier(e)) {
quantifier* q = to_quantifier(e);
quantifier const* q = to_quantifier(e);
is_univ = q->is_forall();
body = q->get_expr();
for (unsigned i = 0; i < q->get_num_decls(); ++i) {
@ -1010,7 +983,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
return false;
}
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
@ -1022,7 +995,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
return false;
}
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k) {
@ -1035,7 +1008,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
}
bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
bool proof_checker::match_op(expr const* e, decl_kind k, expr_ref& t) const {
if (e->get_kind() == AST_APP &&
to_app(e)->get_family_id() == m.get_basic_family_id() &&
to_app(e)->get_decl_kind() == k &&
@ -1046,39 +1019,39 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
return false;
}
bool proof_checker::match_not(expr* e, expr_ref& t) {
bool proof_checker::match_not(expr const* e, expr_ref& t) const {
return match_op(e, OP_NOT, t);
}
bool proof_checker::match_or(expr* e, expr_ref_vector& terms) {
bool proof_checker::match_or(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_OR, terms);
}
bool proof_checker::match_and(expr* e, expr_ref_vector& terms) {
bool proof_checker::match_and(expr const* e, expr_ref_vector& terms) const {
return match_op(e, OP_AND, terms);
}
bool proof_checker::match_iff(expr* e, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IFF, t1, t2);
}
bool proof_checker::match_equiv(expr* e, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_equiv(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_oeq(e, t1, t2) || match_eq(e, t1, t2);
}
bool proof_checker::match_implies(expr* e, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_IMPLIES, t1, t2);
}
bool proof_checker::match_eq(expr* e, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_EQ, t1, t2) || match_iff(e, t1, t2);
}
bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
bool proof_checker::match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const {
return match_op(e, OP_OEQ, t1, t2);
}
bool proof_checker::match_negated(expr* a, expr* b) {
bool proof_checker::match_negated(expr const* a, expr* b) const {
expr_ref t(m);
return
(match_not(a, t) && t.get() == b) ||
@ -1099,7 +1072,7 @@ void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
ptr_vector<proof> stack;
expr* h = 0;
expr* h = nullptr;
expr_ref hyp(m);
stack.push_back(p);
@ -1186,14 +1159,14 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
}
bool proof_checker::match_nil(expr* e) const {
bool proof_checker::match_nil(expr const* e) const {
return
is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_NIL;
}
bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
bool proof_checker::match_cons(expr const* e, expr_ref& a, expr_ref& b) const {
if (is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_CONS) {
@ -1205,7 +1178,7 @@ bool proof_checker::match_cons(expr* e, expr_ref& a, expr_ref& b) const {
}
bool proof_checker::match_atom(expr* e, expr_ref& a) const {
bool proof_checker::match_atom(expr const* e, expr_ref& a) const {
if (is_app(e) &&
to_app(e)->get_family_id() == m_hyp_fid &&
to_app(e)->get_decl_kind() == OP_ATOM) {
@ -1227,14 +1200,14 @@ expr* proof_checker::mk_nil() {
return m_nil.get();
}
bool proof_checker::is_hypothesis(proof* p) const {
bool proof_checker::is_hypothesis(proof const* p) const {
return
m.is_proof(p) &&
p->get_decl_kind() == PR_HYPOTHESIS;
}
expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
expr* result = 0;
expr* result = nullptr;
for (unsigned i = 0; i < num_hyps; ++i) {
if (!match_nil(hyps[i])) {
if (result) {
@ -1245,7 +1218,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
}
}
}
if (result == 0) {
if (result == nullptr) {
return mk_nil();
}
else {
@ -1253,7 +1226,7 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
}
}
void proof_checker::dump_proof(proof * pr) {
void proof_checker::dump_proof(proof const* pr) {
if (!m_dump_lemmas)
return;
SASSERT(m.has_fact(pr));

72
src/ast/proofs/proof_checker.h
View file

@ -48,24 +48,24 @@ class proof_checker {
func_decl* m_atom;
func_decl* m_nil;
sort* m_cell;
virtual void set_manager(ast_manager * m, family_id id);
void set_manager(ast_manager * m, family_id id) override;
func_decl * mk_func_decl(decl_kind k);
public:
hyp_decl_plugin();
virtual ~hyp_decl_plugin() {}
~hyp_decl_plugin() override {}
virtual void finalize();
void finalize() override;
virtual decl_plugin * mk_fresh() { return alloc(hyp_decl_plugin); }
decl_plugin * mk_fresh() override { return alloc(hyp_decl_plugin); }
virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range);
virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range);
virtual void get_op_names(svector<builtin_name> & op_names, symbol const & logic);
virtual void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic);
sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const* parameters) override;
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) override;
func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned num_args, expr * const * args, sort * range) override;
void get_op_names(svector<builtin_name> & op_names, symbol const & logic) override;
void get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) override;
};
public:
proof_checker(ast_manager& m);
@ -77,39 +77,39 @@ private:
bool check1_spc(proof* p, expr_ref_vector& side_conditions);
bool check_arith_proof(proof* p);
bool check_arith_literal(bool is_pos, app* lit, rational const& coeff, expr_ref& sum, bool& is_strict);
bool match_fact(proof* p, expr_ref& fact);
bool match_fact(proof const* p, expr_ref& fact) const;
void add_premise(proof* p);
bool match_proof(proof* p);
bool match_proof(proof* p, proof_ref& p0);
bool match_proof(proof* p, proof_ref& p0, proof_ref& p1);
bool match_proof(proof* p, proof_ref_vector& parents);
bool match_binary(expr* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2);
bool match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2);
bool match_op(expr* e, decl_kind k, expr_ref& t);
bool match_op(expr* e, decl_kind k, expr_ref_vector& terms);
bool match_iff(expr* e, expr_ref& t1, expr_ref& t2);
bool match_implies(expr* e, expr_ref& t1, expr_ref& t2);
bool match_eq(expr* e, expr_ref& t1, expr_ref& t2);
bool match_oeq(expr* e, expr_ref& t1, expr_ref& t2);
bool match_not(expr* e, expr_ref& t);
bool match_or(expr* e, expr_ref_vector& terms);
bool match_and(expr* e, expr_ref_vector& terms);
bool match_app(expr* e, func_decl_ref& d, expr_ref_vector& terms);
bool match_quantifier(expr*, bool& is_univ, sort_ref_vector&, expr_ref& body);
bool match_negated(expr* a, expr* b);
bool match_equiv(expr* a, expr_ref& t1, expr_ref& t2);
bool match_proof(proof const* p) const;
bool match_proof(proof const* p, proof_ref& p0) const;
bool match_proof(proof const* p, proof_ref& p0, proof_ref& p1) const;
bool match_proof(proof const* p, proof_ref_vector& parents) const;
bool match_binary(expr const* e, func_decl_ref& d, expr_ref& t1, expr_ref& t2) const;
bool match_op(expr const* e, decl_kind k, expr_ref& t1, expr_ref& t2) const;
bool match_op(expr const* e, decl_kind k, expr_ref& t) const;
bool match_op(expr const* e, decl_kind k, expr_ref_vector& terms) const;
bool match_iff(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_implies(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_eq(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_oeq(expr const* e, expr_ref& t1, expr_ref& t2) const;
bool match_not(expr const* e, expr_ref& t) const;
bool match_or(expr const* e, expr_ref_vector& terms) const;
bool match_and(expr const* e, expr_ref_vector& terms) const;
bool match_app(expr const* e, func_decl_ref& d, expr_ref_vector& terms) const;
bool match_quantifier(expr const*, bool& is_univ, sort_ref_vector&, expr_ref& body) const;
bool match_negated(expr const* a, expr* b) const;
bool match_equiv(expr const* a, expr_ref& t1, expr_ref& t2) const;
void get_ors(expr* e, expr_ref_vector& ors);
void get_hypotheses(proof* p, expr_ref_vector& ante);
bool match_nil(expr* e) const;
bool match_cons(expr* e, expr_ref& a, expr_ref& b) const;
bool match_atom(expr* e, expr_ref& a) const;
bool match_nil(expr const* e) const;
bool match_cons(expr const* e, expr_ref& a, expr_ref& b) const;
bool match_atom(expr const* e, expr_ref& a) const;
expr* mk_nil();
expr* mk_cons(expr* a, expr* b);
expr* mk_atom(expr* e);
bool is_hypothesis(proof* p) const;
bool is_hypothesis(proof const* p) const;
expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
void dump_proof(proof * pr);
void dump_proof(proof const* pr);
void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
void set_false(expr_ref& e, unsigned idx, expr_ref& lit);

10
src/ast/proofs/proof_utils.cpp
View file

@ -143,7 +143,7 @@ class reduce_hypotheses {
void reduce(proof* pf, proof_ref &out)
{
proof *res = NULL;
proof *res = nullptr;
m_todo.reset();
m_todo.push_back(pf);
@ -392,7 +392,7 @@ class reduce_hypotheses0 {
}
void add_hypotheses(proof* p) {
expr_set* hyps = 0;
expr_set* hyps = nullptr;
bool inherited = false;
if (p->get_decl_kind() == PR_HYPOTHESIS) {
hyps = alloc(expr_set);
@ -509,7 +509,7 @@ public:
// eliminate hypothesis recursively in the proof of the lemma
elim(tmp);
expr_set* hyps = m_hypmap.find(tmp);
expr_set* new_hyps = 0;
expr_set* new_hyps = nullptr;
// XXX if the proof is correct, the hypotheses of the tmp
// XXX should be exactly those of the consequence of the lemma
// XXX but if this code actually eliminates hypotheses, the set might be a subset
@ -567,7 +567,7 @@ public:
}
if (new_hyps && new_hyps->empty()) {
dealloc(new_hyps);
new_hyps = 0;
new_hyps = nullptr;
}
m_hypmap.insert(result, new_hyps);
// might push 0 into m_hyprefs. No reason for that
@ -822,7 +822,7 @@ bool proof_utils::is_closed(ast_manager& m, proof* p) {
static void permute_unit_resolution(expr_ref_vector& refs, obj_map<proof,proof*>& cache, proof_ref& pr) {
ast_manager& m = pr.get_manager();
proof* pr2 = 0;
proof* pr2 = nullptr;
proof_ref_vector parents(m);
proof_ref prNew(pr);
if (cache.find(pr, pr2)) {

2
src/ast/recurse_expr_def.h
View file

@ -72,7 +72,7 @@ void recurse_expr<T, Visitor, IgnorePatterns, CallDestructors>::process(expr * n
break;
case AST_QUANTIFIER:
if (IgnorePatterns) {
cache_result(n, this->Visitor::visit(to_quantifier(n), get_cached(to_quantifier(n)->get_expr()), 0, 0));
cache_result(n, this->Visitor::visit(to_quantifier(n), get_cached(to_quantifier(n)->get_expr()), nullptr, nullptr));
}
else {
m_results1.reset();

1
src/ast/rewriter/CMakeLists.txt
View file

@ -25,7 +25,6 @@ z3_add_component(rewriter
pb_rewriter.cpp
pb2bv_rewriter.cpp
push_app_ite.cpp
pull_ite_tree.cpp
quant_hoist.cpp
rewriter.cpp
seq_rewriter.cpp

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);

Some files were not shown because too many files have changed in this diff Show more