mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

update rewriting of equalities and monomials for regressions

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-09-03 14:36:03 -07:00
parent 7fbb938474
commit c6722859c2
9 changed files with 102 additions and 95 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/ast/justified_expr.h
View file

@ -21,12 +21,12 @@ public:
justified_expr& operator=(justified_expr const& other) {
SASSERT(&m == &other.m);
if (this != &other) {
m.inc_ref(other.get_fml());
m.inc_ref(other.get_proof());
m.dec_ref(m_fml);
m.dec_ref(m_proof);
m_fml = other.get_fml();
m_proof = other.get_proof();
m.inc_ref(m_fml);
m.inc_ref(m_proof);
}
return *this;
}

20
src/ast/rewriter/arith_rewriter.cpp
View file

@ -26,7 +26,6 @@ void arith_rewriter::updt_local_params(params_ref const & _p) {
arith_rewriter_params p(_p);
m_arith_lhs = p.arith_lhs();
m_gcd_rounding = p.gcd_rounding();
m_eq2ineq = p.eq2ineq();
m_elim_to_real = p.elim_to_real();
m_push_to_real = p.push_to_real();
m_anum_simp = p.algebraic_number_evaluator();
@ -371,7 +370,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
if ((is_zero(arg1) && is_reduce_power_target(arg2, kind == EQ)) ||
(is_zero(arg2) && is_reduce_power_target(arg1, kind == EQ)))
return reduce_power(arg1, arg2, kind, result);
br_status st = cancel_monomials(arg1, arg2, m_arith_lhs, new_arg1, new_arg2);
br_status st = cancel_monomials(arg1, arg2, true, new_arg1, new_arg2);
TRACE("mk_le_bug", tout << "st: " << st << " " << new_arg1 << " " << new_arg2 << "\n";);
if (st != BR_FAILED) {
arg1 = new_arg1;
@ -455,11 +454,7 @@ br_status arith_rewriter::mk_le_ge_eq_core(expr * arg1, expr * arg2, op_kind kin
st = BR_DONE;
}
}
if (kind == EQ && m_expand_eqs) {
result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
return BR_REWRITE2;
}
else if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
if (is_numeral(arg2, a2) && is_neg_poly(arg1, new_arg1)) {
a2.neg();
new_arg2 = m_util.mk_numeral(a2, m_util.is_int(new_arg1));
switch (kind) {
@ -500,12 +495,19 @@ br_status arith_rewriter::mk_gt_core(expr * arg1, expr * arg2, expr_ref & result
return BR_REWRITE2;
}
bool arith_rewriter::is_arith_term(expr * n) const {
return n->get_kind() == AST_APP && to_app(n)->get_family_id() == get_fid();
}
br_status arith_rewriter::mk_eq_core(expr * arg1, expr * arg2, expr_ref & result) {
if (m_eq2ineq) {
if (m_expand_eqs) {
result = m().mk_and(m_util.mk_le(arg1, arg2), m_util.mk_ge(arg1, arg2));
return BR_REWRITE2;
}
return mk_le_ge_eq_core(arg1, arg2, EQ, result);
if (m_arith_lhs || is_arith_term(arg1) || is_arith_term(arg2)) {
return mk_le_ge_eq_core(arg1, arg2, EQ, result);
}
return BR_FAILED;
}
expr_ref arith_rewriter::neg_monomial(expr* e) const {

4
src/ast/rewriter/arith_rewriter.h
View file

@ -50,12 +50,12 @@ public:
class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
bool m_arith_lhs;
bool m_gcd_rounding;
bool m_eq2ineq;
bool m_elim_to_real;
bool m_push_to_real;
bool m_anum_simp;
bool m_elim_rem;
bool m_expand_eqs;
bool m_process_all_eqs;
unsigned m_max_degree;
void get_coeffs_gcd(expr * t, numeral & g, bool & first, unsigned & num_consts);
@ -83,6 +83,8 @@ class arith_rewriter : public poly_rewriter<arith_rewriter_core> {
expr * reduce_power(expr * arg, bool is_eq);
br_status reduce_power(expr * arg1, expr * arg2, op_kind kind, expr_ref & result);
bool is_arith_term(expr * n) const;
bool is_pi_multiple(expr * t, rational & k);
bool is_pi_offset(expr * t, rational & k, expr * & m);
bool is_2_pi_integer(expr * t);

1
src/ast/rewriter/arith_rewriter_params.pyg
View file

@ -6,7 +6,6 @@ def_module_params(module_name='rewriter',
("expand_power", BOOL, False, "expand (^ t k) into (* t ... t) if 1 < k <= max_degree."),
("expand_tan", BOOL, False, "replace (tan x) with (/ (sin x) (cos x))."),
("max_degree", UINT, 64, "max degree of algebraic numbers (and power operators) processed by simplifier."),
("eq2ineq", BOOL, False, "split arithmetic equalities into two inequalities."),
("sort_sums", BOOL, False, "sort the arguments of + application."),
("gcd_rounding", BOOL, False, "use gcd rounding on integer arithmetic atoms."),
("arith_lhs", BOOL, False, "all monomials are moved to the left-hand-side, and the right-hand-side is just a constant."),

1
src/ast/rewriter/bv_rewriter.cpp
View file

@ -20,6 +20,7 @@ Notes:
#include "ast/rewriter/bv_rewriter_params.hpp"
#include "ast/rewriter/poly_rewriter_def.h"
#include "ast/ast_smt2_pp.h"
#include "ast/ast_lt.h"
void bv_rewriter::updt_local_params(params_ref const & _p) {

9
src/ast/rewriter/poly_rewriter.h
View file

@ -48,7 +48,6 @@ protected:
decl_kind power_decl_kind() const { return Config::power_decl_kind(); }
bool is_power(expr * t) const { return is_app_of(t, get_fid(), power_decl_kind()); }
expr * get_power_body(expr * t, rational & k);
struct mon_pw_lt; // functor used to sort monomial elements when use_power() == true
expr * mk_mul_app(unsigned num_args, expr * const * args);
expr * mk_mul_app(numeral const & c, expr * arg);
@ -85,6 +84,14 @@ protected:
bool is_mul(expr * t, numeral & c, expr * & pp);
void hoist_cmul(expr_ref_buffer & args);
class mon_lt {
poly_rewriter& rw;
int ordinal(expr* e) const;
public:
mon_lt(poly_rewriter& rw): rw(rw) {}
bool operator()(expr* e1, expr * e2) const;
};
public:
poly_rewriter(ast_manager & m, params_ref const & p = params_ref()):
Config(m),

71
src/ast/rewriter/poly_rewriter_def.h
View file

@ -18,7 +18,7 @@ Notes:
--*/
#include "ast/rewriter/poly_rewriter.h"
#include "ast/rewriter/poly_rewriter_params.hpp"
#include "ast/ast_lt.h"
// include "ast/ast_lt.h"
#include "ast/ast_ll_pp.h"
#include "ast/ast_smt2_pp.h"
@ -191,21 +191,9 @@ br_status poly_rewriter<Config>::mk_flat_mul_core(unsigned num_args, expr * cons
}
template<typename Config>
struct poly_rewriter<Config>::mon_pw_lt {
poly_rewriter<Config> & m_owner;
mon_pw_lt(poly_rewriter<Config> & o):m_owner(o) {}
bool operator()(expr * n1, expr * n2) const {
rational k;
return lt(m_owner.get_power_body(n1, k),
m_owner.get_power_body(n2, k));
}
};
template<typename Config>
br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * const * args, expr_ref & result) {
mon_lt lt(*this);
SASSERT(num_args >= 2);
// cheap case
numeral a;
@ -320,11 +308,8 @@ br_status poly_rewriter<Config>::mk_nflat_mul_core(unsigned num_args, expr * con
if (ordered && num_coeffs == 0 && !use_power())
return BR_FAILED;
if (!ordered) {
if (use_power())
std::sort(new_args.begin(), new_args.end(), mon_pw_lt(*this));
else
std::sort(new_args.begin(), new_args.end(), ast_to_lt());
TRACE("poly_rewriter",
std::sort(new_args.begin(), new_args.end(), lt);
TRACE("poly_rewriter",
tout << "after sorting:\n";
for (unsigned i = 0; i < new_args.size(); i++) {
if (i > 0)
@ -498,8 +483,43 @@ void poly_rewriter<Config>::hoist_cmul(expr_ref_buffer & args) {
args.resize(j);
}
template<typename Config>
bool poly_rewriter<Config>::mon_lt::operator()(expr* e1, expr * e2) const {
return ordinal(e1) < ordinal(e2);
}
inline bool is_essentially_var(expr * n, family_id fid) {
SASSERT(is_var(n) || is_app(n));
return is_var(n) || to_app(n)->get_family_id() != fid;
}
template<typename Config>
int poly_rewriter<Config>::mon_lt::ordinal(expr* e) const {
rational k;
if (is_essentially_var(e, rw.get_fid())) {
return e->get_id();
}
else if (rw.is_mul(e)) {
if (rw.is_numeral(to_app(e)->get_arg(0)))
return to_app(e)->get_arg(1)->get_id();
else
return e->get_id();
}
else if (rw.is_numeral(e)) {
return -1;
}
else if (rw.use_power() && rw.is_power(e) && rw.is_numeral(to_app(e)->get_arg(1), k) && k > rational(1)) {
return to_app(e)->get_arg(0)->get_id();
}
else {
return e->get_id();
}
}
template<typename Config>
br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * const * args, expr_ref & result) {
mon_lt lt(*this);
SASSERT(num_args >= 2);
numeral c;
unsigned num_coeffs = 0;
@ -591,9 +611,9 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
else if (m_sort_sums) {
TRACE("rewriter_bug", tout << "new_args.size(): " << new_args.size() << "\n";);
if (c.is_zero())
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), mon_lt(*this));
else
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), mon_lt(*this));
}
result = mk_add_app(new_args.size(), new_args.c_ptr());
TRACE("rewriter", tout << result << "\n";);
@ -624,10 +644,10 @@ br_status poly_rewriter<Config>::mk_nflat_add_core(unsigned num_args, expr * con
}
else if (!ordered) {
if (c.is_zero())
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), ast_to_lt());
std::sort(new_args.c_ptr(), new_args.c_ptr() + new_args.size(), lt);
else
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), ast_to_lt());
}
std::sort(new_args.c_ptr() + 1, new_args.c_ptr() + new_args.size(), lt);
}
result = mk_add_app(new_args.size(), new_args.c_ptr());
if (hoist_multiplication(result)) {
return BR_REWRITE_FULL;
@ -681,6 +701,7 @@ br_status poly_rewriter<Config>::mk_sub(unsigned num_args, expr * const * args,
template<typename Config>
br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool move, expr_ref & lhs_result, expr_ref & rhs_result) {
set_curr_sort(m().get_sort(lhs));
mon_lt lt(*this);
unsigned lhs_sz;
expr * const * lhs_monomials = get_monomials(lhs, lhs_sz);
unsigned rhs_sz;
@ -831,7 +852,7 @@ br_status poly_rewriter<Config>::cancel_monomials(expr * lhs, expr * rhs, bool m
if (move) {
if (m_sort_sums) {
// + 1 to skip coefficient
std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), ast_to_lt());
std::sort(new_lhs_monomials.begin() + 1, new_lhs_monomials.end(), lt);
}
c_at_rhs = true;
}

79
src/cmd_context/cmd_context.cpp
View file

@ -585,10 +585,8 @@ void cmd_context::register_builtin_sorts(decl_plugin * p) {
svector<builtin_name> names;
p->get_sort_names(names, m_logic);
family_id fid = p->get_family_id();
svector<builtin_name>::const_iterator it = names.begin();
svector<builtin_name>::const_iterator end = names.end();
for (; it != end; ++it) {
psort_decl * d = pm().mk_psort_builtin_decl((*it).m_name, fid, (*it).m_kind);
for (builtin_name const& n : names) {
psort_decl * d = pm().mk_psort_builtin_decl(n.m_name, fid, n.m_kind);
insert(d);
}
}
@ -597,17 +595,15 @@ void cmd_context::register_builtin_ops(decl_plugin * p) {
svector<builtin_name> names;
p->get_op_names(names, m_logic);
family_id fid = p->get_family_id();
svector<builtin_name>::const_iterator it = names.begin();
svector<builtin_name>::const_iterator end = names.end();
for (; it != end; ++it) {
if (m_builtin_decls.contains((*it).m_name)) {
builtin_decl & d = m_builtin_decls.find((*it).m_name);
builtin_decl * new_d = alloc(builtin_decl, fid, (*it).m_kind, d.m_next);
for (builtin_name const& n : names) {
if (m_builtin_decls.contains(n.m_name)) {
builtin_decl & d = m_builtin_decls.find(n.m_name);
builtin_decl * new_d = alloc(builtin_decl, fid, n.m_kind, d.m_next);
d.m_next = new_d;
m_extra_builtin_decls.push_back(new_d);
}
else {
m_builtin_decls.insert((*it).m_name, builtin_decl(fid, (*it).m_kind));
m_builtin_decls.insert(n.m_name, builtin_decl(fid, n.m_kind));
}
}
}
@ -693,10 +689,8 @@ void cmd_context::init_manager_core(bool new_manager) {
load_plugin(symbol("seq"), logic_has_seq(), fids);
load_plugin(symbol("fpa"), logic_has_fpa(), fids);
load_plugin(symbol("pb"), logic_has_pb(), fids);
svector<family_id>::iterator it = fids.begin();
svector<family_id>::iterator end = fids.end();
for (; it != end; ++it) {
decl_plugin * p = m_manager->get_plugin(*it);
for (family_id fid : fids) {
decl_plugin * p = m_manager->get_plugin(fid);
if (p) {
register_builtin_sorts(p);
register_builtin_ops(p);
@ -1148,11 +1142,8 @@ void cmd_context::erase_object_ref(symbol const & s) {
}
void cmd_context::reset_func_decls() {
dictionary<func_decls>::iterator it = m_func_decls.begin();
dictionary<func_decls>::iterator end = m_func_decls.end();
for (; it != end; ++it) {
func_decls fs = (*it).m_value;
fs.finalize(m());
for (auto & kv : m_func_decls) {
kv.m_value.finalize(m());
}
m_func_decls.reset();
m_func_decls_stack.reset();
@ -1160,10 +1151,8 @@ void cmd_context::reset_func_decls() {
}
void cmd_context::reset_psort_decls() {
dictionary<psort_decl*>::iterator it = m_psort_decls.begin();
dictionary<psort_decl*>::iterator end = m_psort_decls.end();
for (; it != end; ++it) {
psort_decl * p = (*it).m_value;
for (auto & kv : m_psort_decls) {
psort_decl * p = kv.m_value;
pm().dec_ref(p);
}
m_psort_decls.reset();
@ -1179,19 +1168,14 @@ void cmd_context::reset_macros() {
}
void cmd_context::reset_cmds() {
dictionary<cmd*>::iterator it = m_cmds.begin();
dictionary<cmd*>::iterator end = m_cmds.end();
for (; it != end; ++it) {
cmd * c = (*it).m_value;
c->reset(*this);
for (auto& kv : m_cmds) {
kv.m_value->reset(*this);
}
}
void cmd_context::finalize_cmds() {
dictionary<cmd*>::iterator it = m_cmds.begin();
dictionary<cmd*>::iterator end = m_cmds.end();
for (; it != end; ++it) {
cmd * c = (*it).m_value;
for (auto& kv : m_cmds) {
cmd * c = kv.m_value;
c->finalize(*this);
dealloc(c);
}
@ -1204,10 +1188,8 @@ void cmd_context::reset_user_tactics() {
}
void cmd_context::reset_object_refs() {
dictionary<object_ref*>::iterator it = m_object_refs.begin();
dictionary<object_ref*>::iterator end = m_object_refs.end();
for (; it != end; ++it) {
object_ref * r = (*it).m_value;
for (auto& kv : m_object_refs) {
object_ref * r = kv.m_value;
r->dec_ref(*this);
}
m_object_refs.reset();
@ -1541,10 +1523,8 @@ void cmd_context::reset_assertions() {
mk_solver();
}
restore_assertions(0);
svector<scope>::iterator it = m_scopes.begin();
svector<scope>::iterator end = m_scopes.end();
for (; it != end; ++it) {
it->m_assertions_lim = 0;
for (scope& s : m_scopes) {
s.m_assertions_lim = 0;
if (m_solver) m_solver->push();
}
}
@ -1717,10 +1697,7 @@ void cmd_context::set_solver_factory(solver_factory * f) {
mk_solver();
// assert formulas and create scopes in the new solver.
unsigned lim = 0;
svector<scope>::iterator it = m_scopes.begin();
svector<scope>::iterator end = m_scopes.end();
for (; it != end; ++it) {
scope & s = *it;
for (scope& s : m_scopes) {
for (unsigned i = lim; i < s.m_assertions_lim; i++) {
m_solver->assert_expr(m_assertions[i]);
}
@ -1757,11 +1734,9 @@ void cmd_context::display_statistics(bool show_total_time, double total_time) {
void cmd_context::display_assertions() {
if (!m_interactive_mode)
throw cmd_exception("command is only available in interactive mode, use command (set-option :interactive-mode true)");
std::vector<std::string>::const_iterator it = m_assertion_strings.begin();
std::vector<std::string>::const_iterator end = m_assertion_strings.end();
regular_stream() << "(";
for (bool first = true; it != end; ++it) {
std::string const & s = *it;
bool first = true;
for (std::string const& s : m_assertion_strings) {
if (first)
first = false;
else
@ -1837,10 +1812,8 @@ void cmd_context::display(std::ostream & out, func_decl * d, unsigned indent) co
}
void cmd_context::dump_assertions(std::ostream & out) const {
ptr_vector<expr>::const_iterator it = m_assertions.begin();
ptr_vector<expr>::const_iterator end = m_assertions.end();
for (; it != end; ++it) {
display(out, *it);
for (expr * e : m_assertions) {
display(out, e);
out << std::endl;
}
}

8
src/smt/asserted_formulas.cpp
View file

@ -120,7 +120,7 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, vector<justified_ex
void asserted_formulas::set_eliminate_and(bool flag) {
params_ref p;
p.set_bool("elim_and", flag);
p.set_bool("arith_lhs", true);
// p.set_bool("arith_lhs", true);
p.set_bool("sort_sums", true);
p.set_bool("rewrite_patterns", true);
p.set_bool("expand_eqs", m_params.m_arith_expand_eqs);
@ -429,7 +429,6 @@ void asserted_formulas::commit(unsigned new_qhead) {
}
void asserted_formulas::propagate_values() {
TRACE("propagate_values", tout << "before:\n"; display(tout););
flush_cache();
unsigned num_prop = 0;
@ -466,7 +465,7 @@ void asserted_formulas::propagate_values() {
}
unsigned asserted_formulas::propagate_values(unsigned i) {
expr * n = m_formulas[i].get_fml();
expr_ref n(m_formulas[i].get_fml(), m);
expr_ref new_n(m);
proof_ref new_pr(m);
m_rewriter(n, new_n, new_pr);
@ -476,6 +475,9 @@ unsigned asserted_formulas::propagate_values(unsigned i) {
}
justified_expr j(m, new_n, new_pr);
m_formulas[i] = j;
if (m_formulas[i].get_fml() != new_n) {
std::cout << "NOT updated\n";
}
if (m.is_false(j.get_fml())) {
m_inconsistent = true;
}