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

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

Browse source
This commit is contained in:
Nikolaj Bjorner 2018-07-13 07:52:40 -07:00
parent 167969d6c2 ca12a8482f
commit 1d408c1955
11 changed files with 87 additions and 49 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/ast/ast.cpp
View file

@ -1934,8 +1934,7 @@ sort * ast_manager::substitute(sort* s, unsigned n, sort * const * src, sort * c
vector<parameter> ps;
bool change = false;
sort_ref_vector sorts(*this);
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast()) {
SASSERT(is_sort(p.get_ast()));
change = true;
@ -2330,8 +2329,8 @@ bool ast_manager::is_label_lit(expr const * n, buffer<symbol> & names) const {
return false;
}
func_decl const * decl = to_app(n)->get_decl();
for (unsigned i = 0; i < decl->get_num_parameters(); i++)
names.push_back(decl->get_parameter(i).get_symbol());
for (parameter const& p : decl->parameters())
names.push_back(p.get_symbol());
return true;
}
@ -2928,8 +2927,8 @@ bool ast_manager::is_quant_inst(expr const* e, expr*& not_q_or_i, ptr_vector<exp
not_q_or_i = to_app(e)->get_arg(0);
func_decl* d = to_app(e)->get_decl();
SASSERT(binding.empty());
for (unsigned i = 0; i < d->get_num_parameters(); ++i) {
binding.push_back(to_expr(d->get_parameter(i).get_ast()));
for (parameter const& p : d->parameters()) {
binding.push_back(to_expr(p.get_ast()));
}
return true;
}

24
src/ast/ast.h
View file

@ -273,6 +273,14 @@ public:
parameter const * get_parameters() const { return m_parameters.begin(); }
bool private_parameters() const { return m_private_parameters; }
struct iterator {
decl_info const& d;
iterator(decl_info const& d) : d(d) {}
parameter const* begin() const { return d.get_parameters(); }
parameter const* end() const { return begin() + d.get_num_parameters(); }
};
iterator parameters() const { return iterator(*this); }
unsigned hash() const;
bool operator==(decl_info const & info) const;
};
@ -571,6 +579,16 @@ public:
parameter const & get_parameter(unsigned idx) const { return m_info->get_parameter(idx); }
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(); }
struct iterator {
decl const& d;
iterator(decl const& d) : d(d) {}
parameter const* begin() const { return d.get_parameters(); }
parameter const* end() const { return begin() + d.get_num_parameters(); }
};
iterator parameters() const { return iterator(*this); }
};
// -----------------------------------
@ -2401,11 +2419,7 @@ public:
}
void reset() {
ptr_buffer<ast>::iterator it = m_to_unmark.begin();
ptr_buffer<ast>::iterator end = m_to_unmark.end();
for (; it != end; ++it) {
reset_mark(*it);
}
for (ast* a : m_to_unmark) reset_mark(a);
m_to_unmark.reset();
}

6
src/ast/bv_decl_plugin.cpp
View file

@ -401,7 +401,7 @@ bool bv_decl_plugin::get_int2bv_size(unsigned num_parameters, parameter const *
m_manager->raise_exception("int2bv expects one parameter");
return false;
}
parameter p(parameters[0]);
const parameter &p = parameters[0];
if (p.is_int()) {
result = p.get_int();
return true;
@ -428,7 +428,7 @@ func_decl * bv_decl_plugin::mk_num_decl(unsigned num_parameters, parameter const
// After SMT-COMP, I should find all offending modules.
// For now, I will just simplify the numeral here.
parameter p0(mod(parameters[0].get_rational(), rational::power_of_two(bv_size)));
parameter ps[2] = { p0, parameters[1] };
parameter ps[2] = { std::move(p0), parameters[1] };
sort * bv = get_bv_sort(bv_size);
return m_manager->mk_const_decl(m_bv_sym, bv, func_decl_info(m_family_id, OP_BV_NUM, num_parameters, ps));
}
@ -746,7 +746,7 @@ void bv_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const
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)) };
parameter p[2] = { parameter(rational::zero()), parameter(static_cast<int>(bv_size)) };
return m_manager->mk_app(m_family_id, OP_BV_NUM, 2, p, 0, nullptr);
}

28
src/ast/datatype_decl_plugin.cpp
View file

@ -692,6 +692,7 @@ namespace datatype {
}
unsigned num_well_founded = 0, id = 0;
bool changed;
ptr_vector<sort> subsorts;
do {
changed = false;
for (unsigned tid = 0; tid < num_types; tid++) {
@ -701,23 +702,25 @@ namespace datatype {
sort* s = sorts[tid];
def const& d = get_def(s);
for (constructor const* c : d) {
bool found_nonwf = false;
for (accessor const* a : *c) {
if (sort2id.find(a->range(), id) && !well_founded[id]) {
found_nonwf = true;
break;
subsorts.reset();
get_subsorts(a->range(), subsorts);
for (sort* srt : subsorts) {
if (sort2id.find(srt, id) && !well_founded[id]) {
goto next_constructor;
}
}
}
if (!found_nonwf) {
changed = true;
well_founded[tid] = true;
num_well_founded++;
break;
}
changed = true;
well_founded[tid] = true;
num_well_founded++;
break;
next_constructor:
;
}
}
}
while(changed && num_well_founded < num_types);
while (changed && num_well_founded < num_types);
return num_well_founded == num_types;
}
@ -727,8 +730,7 @@ namespace datatype {
void util::get_subsorts(sort* s, ptr_vector<sort>& sorts) const {
sorts.push_back(s);
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast() && is_sort(p.get_ast())) {
get_subsorts(to_sort(p.get_ast()), sorts);
}

3
src/ast/seq_decl_plugin.cpp
View file

@ -376,8 +376,7 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
if (s->get_family_id() == sP->get_family_id() &&
s->get_decl_kind() == sP->get_decl_kind() &&
s->get_num_parameters() == sP->get_num_parameters()) {
for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
parameter const& p = s->get_parameter(i);
for (parameter const& p : s->parameters()) {
if (p.is_ast() && is_sort(p.get_ast())) {
parameter const& p2 = sP->get_parameter(i);
if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;

4
src/util/lp/general_matrix.h
View file

@ -105,12 +105,12 @@ public:
}
template <typename T>
void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix) {
void init_row_from_container(int i, const T & c, std::function<unsigned (unsigned)> column_fix, const mpq& sign) {
auto & row = m_data[adjust_row(i)];
lp_assert(row_is_initialized_correctly(row));
for (const auto & p : c) {
unsigned j = adjust_column(column_fix(p.var()));
row[j] = p.coeff();
row[j] = sign * p.coeff();
}
}

15
src/util/lp/hnf_cutter.h
View file

@ -29,6 +29,7 @@ class hnf_cutter {
var_register m_var_register;
general_matrix m_A;
vector<const lar_term*> m_terms;
vector<bool> m_terms_upper;
svector<constraint_index> m_constraints_for_explanation;
vector<mpq> m_right_sides;
lp_settings & m_settings;
@ -54,15 +55,22 @@ public:
// m_A will be filled from scratch in init_matrix_A
m_var_register.clear();
m_terms.clear();
m_terms_upper.clear();
m_constraints_for_explanation.clear();
m_right_sides.clear();
m_abs_max = zero_of_type<mpq>();
m_overflow = false;
}
void add_term(const lar_term* t, const mpq &rs, constraint_index ci) {
void add_term(const lar_term* t, const mpq &rs, constraint_index ci, bool upper_bound) {
m_terms.push_back(t);
m_right_sides.push_back(rs);
m_terms_upper.push_back(upper_bound);
if (upper_bound)
m_right_sides.push_back(rs);
else
m_right_sides.push_back(-rs);
m_constraints_for_explanation.push_back(ci);
for (const auto &p : *t) {
m_var_register.add_var(p.var());
mpq t = abs(ceil(p.coeff()));
@ -76,7 +84,8 @@ public:
}
void initialize_row(unsigned i) {
m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);});
mpq sign = m_terms_upper[i]? one_of_type<mpq>(): - one_of_type<mpq>();
m_A.init_row_from_container(i, * m_terms[i], [this](unsigned j) { return m_var_register.add_var(j);}, sign);
}
void init_matrix_A() {

5
src/util/lp/int_solver.cpp
View file

@ -537,8 +537,9 @@ void int_solver::try_add_term_to_A_for_hnf(unsigned i) {
mpq rs;
const lar_term* t = m_lar_solver->terms()[i];
constraint_index ci;
if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci)) {
m_hnf_cutter.add_term(t, rs, ci);
bool upper_bound;
if (!hnf_cutter_is_full() && m_lar_solver->get_equality_and_right_side_for_term_on_current_x(i, rs, ci, upper_bound)) {
m_hnf_cutter.add_term(t, rs, ci, upper_bound);
}
}

36
src/util/lp/lar_solver.cpp
View file

@ -2227,8 +2227,19 @@ void lar_solver::round_to_integer_solution() {
update_delta_for_terms(del, j, vars_to_terms[j]);
}
}
// return true if all y coords are zeroes
bool lar_solver::sum_first_coords(const lar_term& t, mpq & val) const {
val = zero_of_type<mpq>();
for (const auto & c : t) {
const auto & x = m_mpq_lar_core_solver.m_r_x[c.var()];
if (!is_zero(x.y))
return false;
val += x.x * c.coeff();
}
return true;
}
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci) const {
bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term_index, mpq & rs, constraint_index& ci, bool &upper_bound) const {
unsigned tj = term_index + m_terms_start_index;
unsigned j;
bool is_int;
@ -2236,26 +2247,29 @@ bool lar_solver::get_equality_and_right_side_for_term_on_current_x(unsigned term
return false; // the term does not have a bound because it does not correspond to a column
if (!is_int) // todo - allow for the next version of hnf
return false;
impq term_val;
bool term_val_ready = false;
bool rs_is_calculated = false;
mpq b;
bool is_strict;
const lar_term& t = *terms()[term_index];
if (has_upper_bound(j, ci, b, is_strict) && !is_strict) {
lp_assert(b.is_int());
term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x);
term_val_ready = true;
if (term_val.x == b) {
rs = b;
if (!sum_first_coords(t, rs))
return false;
rs_is_calculated = true;
if (rs == b) {
upper_bound = true;
return true;
}
}
if (has_lower_bound(j, ci, b, is_strict) && !is_strict) {
if (!term_val_ready)
term_val = terms()[term_index]->apply(m_mpq_lar_core_solver.m_r_x);
if (!rs_is_calculated){
if (!sum_first_coords(t, rs))
return false;
}
lp_assert(b.is_int());
if (term_val.x == b) {
rs = b;
if (rs == b) {
upper_bound = false;
return true;
}
}

3
src/util/lp/lar_solver.h
View file

@ -573,9 +573,10 @@ public:
unsigned column_count() const { return A_r().column_count(); }
const vector<unsigned> & r_basis() const { return m_mpq_lar_core_solver.r_basis(); }
const vector<unsigned> & r_nbasis() const { return m_mpq_lar_core_solver.r_nbasis(); }
bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci) const;
bool get_equality_and_right_side_for_term_on_current_x(unsigned i, mpq &rs, constraint_index& ci, bool &upper_bound) const;
bool remove_from_basis(unsigned);
lar_term get_term_to_maximize(unsigned ext_j) const;
void set_cut_strategy(unsigned cut_frequency);
bool sum_first_coords(const lar_term& t, mpq & val) const;
};
}

1
src/util/trace.h
View file

@ -51,7 +51,6 @@ void finalize_trace();
static inline void enable_trace(const char * tag) {}
static inline void enable_all_trace(bool flag) {}
static inline void disable_trace(const char * tag) {}
// On a default Visual C++ build on Windows, a non-void function either needs to return a value, or we have to add: #pragma warning(default:4716)
static inline bool is_trace_enabled(const char * tag) { return false; }
static inline void close_trace() {}
static inline void open_trace() {}