mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix #2164 address some of simplification shortcommings from #2151 #2152 #2153

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-03-03 11:33:44 -08:00
parent ccc170a06e
commit 3ee5c0e7d9
11 changed files with 120 additions and 107 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_tactic.cpp
View file

@ -52,7 +52,9 @@ extern "C" {
RESET_ERROR_CODE();
tactic_cmd * t = mk_c(c)->find_tactic_cmd(symbol(name));
if (t == nullptr) {
SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);
std::stringstream err;
err << "unknown tactic " << name;
SET_ERROR_CODE(Z3_INVALID_ARG, err.str().c_str());
RETURN_Z3(nullptr);
}
tactic * new_t = t->mk(mk_c(c)->m());

2
src/api/c++/z3++.h
View file

@ -2387,7 +2387,7 @@ namespace z3 {
return *this;
}
void add(expr const & f) { check_context(*this, f); Z3_goal_assert(ctx(), m_goal, f); check_error(); }
// void add(expr_vector const& v) { check_context(*this, v); for (expr e : v) add(e); }
void add(expr_vector const& v) { check_context(*this, v); for (unsigned i = 0; i < v.size(); ++i) add(v[i]); }
unsigned size() const { return Z3_goal_size(ctx(), m_goal); }
expr operator[](int i) const { assert(0 <= i); Z3_ast r = Z3_goal_formula(ctx(), m_goal, i); check_error(); return expr(ctx(), r); }
Z3_goal_prec precision() const { return Z3_goal_precision(ctx(), m_goal); }

4
src/ast/array_decl_plugin.cpp
View file

@ -576,6 +576,10 @@ func_decl * array_recognizers::get_as_array_func_decl(func_decl * f) const {
return to_func_decl(f->get_parameter(0).get_ast());
}
bool array_recognizers::is_const(expr* e, expr*& v) const {
return is_const(e) && (v = to_app(e)->get_arg(0), true);
}
array_util::array_util(ast_manager& m):
array_recognizers(m.mk_family_id("array")),
m_manager(m) {

7
src/ast/array_decl_plugin.h
View file

@ -152,6 +152,8 @@ public:
bool is_as_array(func_decl* f, func_decl*& g) const { return is_decl_of(f, m_fid, OP_AS_ARRAY) && (g = get_as_array_func_decl(f), true); }
func_decl * get_as_array_func_decl(expr * n) const;
func_decl * get_as_array_func_decl(func_decl* f) const;
bool is_const(expr* e, expr*& v) const;
};
class array_util : public array_recognizers {
@ -178,6 +180,11 @@ public:
parameter param(s);
return m_manager.mk_app(m_fid, OP_CONST_ARRAY, 1, &param, 1, &v);
}
app * mk_const_array(unsigned n, sort * const* s, expr * v) {
vector<parameter> ps;
for (unsigned i = 0; i < n; ++i) ps.push_back(parameter(s[i]));
return m_manager.mk_app(m_fid, OP_CONST_ARRAY, n, ps.c_ptr(), 1, &v);
}
app * mk_empty_set(sort * s) {
return mk_const_array(s, m_manager.mk_false());
}

161
src/ast/rewriter/array_rewriter.cpp
View file

@ -230,105 +230,92 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
}
br_status array_rewriter::mk_map_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
SASSERT(num_args >= 0);
bool is_store0 = m_util.is_store(args[0]);
bool is_const0 = m_util.is_const(args[0]);
if (num_args == 1) {
//
// map_f (store a j v) = (store (map_f a) j (f v))
//
if (is_store0) {
app * store_expr = to_app(args[0]);
unsigned num_args = store_expr->get_num_args();
SASSERT(num_args >= 3);
expr * a = store_expr->get_arg(0);
expr * v = store_expr->get_arg(num_args-1);
ptr_buffer<expr> new_args;
new_args.push_back(m_util.mk_map(f, 1, &a)); // (map_f a)
new_args.append(num_args - 2, store_expr->get_args() + 1); // j
new_args.push_back(m().mk_app(f, v)); // (f v)
result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
return BR_REWRITE2;
}
//
// map_f (const v) = (const (f v))
//
if (is_const0) {
expr * fv = m().mk_app(f, to_app(args[0])->get_arg(0));
result = m_util.mk_const_array(m().get_sort(args[0]), fv);
return BR_REWRITE2;
}
return BR_FAILED;
}
SASSERT(num_args > 1);
if (is_store0) {
unsigned num_indices = to_app(args[0])->get_num_args() - 2;
unsigned i;
for (i = 1; i < num_args; i++) {
if (!m_util.is_store(args[i]))
break;
unsigned j;
for (j = 1; j < num_indices+1; j++) {
if (to_app(args[0])->get_arg(j) != to_app(args[i])->get_arg(j))
break;
}
if (j < num_indices+1)
break;
app* store_expr = nullptr;
unsigned num_indices = 0;
bool same_store = true;
for (unsigned i = 0; same_store && i < num_args; i++) {
expr* a = args[i];
if (m_util.is_const(a)) {
continue;
}
//
// map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
//
if (i == num_args) {
ptr_buffer<expr> arrays;
ptr_buffer<expr> values;
for (unsigned i = 0; i < num_args; i++) {
arrays.push_back(to_app(args[i])->get_arg(0));
values.push_back(to_app(args[i])->get_arg(num_indices+1));
else if (!m_util.is_store(a)) {
same_store = false;
}
else if (!store_expr) {
num_indices = to_app(a)->get_num_args() - 2;
store_expr = to_app(a);
}
else {
for (unsigned j = 1; same_store && j < num_indices + 1; j++) {
same_store = (store_expr->get_arg(j) == to_app(a)->get_arg(j));
}
ptr_buffer<expr> new_args;
new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
}
}
//
// map_f (store a_1 j v_1) ... (store a_n j v_n) --> (store (map_f a_1 ... a_n) j (f v_1 ... v_n))
//
if (same_store) {
ptr_buffer<expr> arrays;
ptr_buffer<expr> values;
for (unsigned i = 0; i < num_args; i++) {
expr* a = args[i];
if (m_util.is_const(a)) {
arrays.push_back(a);
values.push_back(to_app(a)->get_arg(0));
}
else {
arrays.push_back(to_app(a)->get_arg(0));
values.push_back(to_app(a)->get_arg(num_indices+1));
}
}
ptr_buffer<expr> new_args;
new_args.push_back(m_util.mk_map(f, arrays.size(), arrays.c_ptr()));
if (store_expr) {
new_args.append(num_indices, to_app(args[0])->get_args() + 1);
new_args.push_back(m().mk_app(f, values.size(), values.c_ptr()));
result = m().mk_app(get_fid(), OP_STORE, new_args.size(), new_args.c_ptr());
return BR_REWRITE2;
}
return BR_FAILED;
else {
result = m_util.mk_const_array(m().get_sort(args[0]), new_args.back());
}
return BR_REWRITE2;
}
if (is_const0) {
unsigned i;
for (i = 1; i < num_args; i++) {
if (!m_util.is_const(args[i]))
break;
//
// map_f (lambda x1 b1) ... (lambda x1 bn) -> lambda x1 (f b1 .. bn)
//
quantifier* lam = nullptr;
for (unsigned i = 0; i < num_args; ++i) {
if (is_lambda(args[i])) {
lam = to_quantifier(args[i]);
}
if (i == num_args) {
//
// map_f (const v_1) ... (const v_n) = (const (f v_1 ... v_n))
//
ptr_buffer<expr> values;
for (unsigned i = 0; i < num_args; i++) {
values.push_back(to_app(args[i])->get_arg(0));
}
if (lam) {
expr_ref_vector args1(m());
for (unsigned i = 0; i < num_args; ++i) {
expr* a = args[i];
if (m_util.is_const(a)) {
args1.push_back(to_app(a)->get_arg(0));
}
else if (is_lambda(a)) {
lam = to_quantifier(a);
args1.push_back(lam->get_expr());
}
else {
expr_ref_vector sel(m());
sel.push_back(a);
unsigned n = lam->get_num_decls();
for (unsigned i = 0; i < n; ++i) {
sel.push_back(m().mk_var(n - i - 1, lam->get_decl_sort(i)));
}
args1.push_back(m_util.mk_select(sel.size(), sel.c_ptr()));
}
expr * fv = m().mk_app(f, values.size(), values.c_ptr());
sort * in_s = get_sort(args[0]);
ptr_vector<sort> domain;
unsigned domain_sz = get_array_arity(in_s);
for (unsigned i = 0; i < domain_sz; i++)
domain.push_back(get_array_domain(in_s, i));
sort_ref out_s(m());
out_s = m_util.mk_array_sort(domain_sz, domain.c_ptr(), f->get_range());
parameter p(out_s.get());
result = m().mk_app(get_fid(), OP_CONST_ARRAY, 1, &p, 1, &fv);
return BR_REWRITE2;
}
return BR_FAILED;
result = m().mk_app(f, args1.size(), args1.c_ptr());
result = m().update_quantifier(lam, result);
return BR_REWRITE3;
}
return BR_FAILED;

1
src/cmd_context/eval_cmd.cpp
View file

@ -71,6 +71,7 @@ public:
expr_ref r(ctx.m());
unsigned timeout = m_params.get_uint("timeout", UINT_MAX);
unsigned rlimit = m_params.get_uint("rlimit", 0);
md->compress();
model_evaluator ev(*(md.get()), m_params);
ev.set_solver(alloc(th_solver, ctx));
cancel_eh<reslimit> eh(ctx.m().limit());

1
src/parsers/smt2/smt2parser.cpp
View file

@ -2677,6 +2677,7 @@ namespace smt2 {
m_ctx.regular_stream() << "(";
expr ** expr_it = expr_stack().c_ptr() + spos;
expr ** expr_end = expr_it + m_cached_strings.size();
md->compress();
for (unsigned i = 0; expr_it < expr_end; expr_it++, i++) {
model::scoped_model_completion _scm(md, true);
expr_ref v = (*md)(*expr_it);

5
src/smt/theory_lra.cpp
View file

@ -3329,13 +3329,12 @@ public:
st = lp::lp_status::UNBOUNDED;
}
else {
vi = m_theory_var2var_index[v];
st = m_solver->maximize_term(vi, term_max);
st = m_solver->maximize_term(v, term_max);
}
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
switch (st) {
case lp::lp_status::OPTIMAL: {
init_variable_values();
TRACE("arith", display(tout << st << " v" << v << " vi: " << vi << "\n"););
inf_rational val = get_value(v);
// inf_rational val(term_max.x, term_max.y);
blocker = mk_gt(v);

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

@ -85,6 +85,15 @@ std::ostream& lar_solver::print_implied_bound(const implied_bound& be, std::ostr
out << "end of implied bound" << std::endl;
return out;
}
std::ostream& lar_solver::print_values(std::ostream& out) const {
for (unsigned i = 0; i < m_mpq_lar_core_solver.m_r_x.size(); i++ ) {
const numeric_pair<mpq> & rp = m_mpq_lar_core_solver.m_r_x[i];
out << this->get_column_name(i) << " -> " << rp << "\n";
}
return out;
}
bool lar_solver::implied_bound_is_correctly_explained(implied_bound const & be, const vector<std::pair<mpq, unsigned>> & explanation) const {
std::unordered_map<unsigned, mpq> coeff_map;
@ -463,29 +472,28 @@ void lar_solver::prepare_costs_for_r_solver(const lar_term & term) {
bool lar_solver::maximize_term_on_corrected_r_solver(lar_term & term,
impq &term_max) {
settings().backup_costs = false;
bool ret = false;
switch (settings().simplex_strategy()) {
case simplex_strategy_enum::tableau_rows:
prepare_costs_for_r_solver(term);
settings().simplex_strategy() = simplex_strategy_enum::tableau_costs;
{
bool ret = maximize_term_on_tableau(term, term_max);
settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
}
ret = maximize_term_on_tableau(term, term_max);
settings().simplex_strategy() = simplex_strategy_enum::tableau_rows;
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
case simplex_strategy_enum::tableau_costs:
prepare_costs_for_r_solver(term);
{
bool ret = maximize_term_on_tableau(term, term_max);
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
}
ret = maximize_term_on_tableau(term, term_max);
set_costs_to_zero(term);
m_mpq_lar_core_solver.m_r_solver.set_status(lp_status::OPTIMAL);
return ret;
case simplex_strategy_enum::lu:
lp_assert(false); // not implemented
return false;
default:
lp_unreachable(); // wrong mode
}
@ -511,6 +519,7 @@ lar_term lar_solver::get_term_to_maximize(unsigned ext_j) const {
lp_status lar_solver::maximize_term(unsigned ext_j,
impq &term_max) {
TRACE("lar_solver", print_values(tout););
bool was_feasible = m_mpq_lar_core_solver.m_r_solver.calc_current_x_is_feasible_include_non_basis();
impq prev_value;
lar_term term = get_term_to_maximize(ext_j);
@ -559,6 +568,7 @@ lp_status lar_solver::maximize_term(unsigned ext_j,
term_max = prev_value;
m_mpq_lar_core_solver.m_r_x = backup;
}
TRACE("lar_solver", print_values(tout););
return term_max == opt_val? lp_status::OPTIMAL :lp_status::FEASIBLE;
}
@ -1185,6 +1195,7 @@ void lar_solver::get_model(std::unordered_map<var_index, mpq> & variable_values)
break;
}
TRACE("get_model", tout << get_column_name(i) << " := " << x << "\n";);
variable_values[i] = x;
}
} while (i != m_mpq_lar_core_solver.m_r_x.size());

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

@ -457,6 +457,7 @@ public:
std::ostream& print_implied_bound(const implied_bound& be, std::ostream & out) const;
std::ostream& print_values(std::ostream& out) const;
mpq get_left_side_val(const lar_base_constraint & cns, const std::unordered_map<var_index, mpq> & var_map) const;

2
src/util/mpz.cpp
View file

@ -1784,7 +1784,7 @@ void display_binary_data(std::ostream &out, unsigned val, unsigned numBits) {
template<bool SYNCH>
void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned num_bits) const {
if (is_small(a)) {
display_binary_data(out, get_uint64(a), num_bits);
display_binary_data(out, static_cast<unsigned>(get_uint64(a)), num_bits);
} else {
#ifndef _MP_GMP
digit_t *ds = digits(a);