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

add rewrites for moduli as exercised in example from #2319

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-24 19:02:28 -08:00
parent fad4356159
commit 84025d5c11
4 changed files with 61 additions and 39 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -988,6 +988,12 @@ void arith_rewriter::remove_divisor(expr* d, ptr_buffer<expr>& args) {
}
UNREACHABLE();
}
static rational symmod(rational const& a, rational const& b) {
rational r = mod(a, b);
if (2*r > b) r -= b;
return r;
}
br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & result) {
set_curr_sort(m().get_sort(arg1));
@ -1031,6 +1037,10 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
change = true;
args.push_back(t1);
}
else if (m_util.is_mul(arg, t1, t2) && m_util.is_numeral(t1, arg_v) && symmod(arg_v, v2) != arg_v) {
change = true;
args.push_back(m_util.mk_mul(m_util.mk_numeral(symmod(arg_v, v2), true), t2));
}
else {
args.push_back(arg);
}

35
src/tactic/arith/bound_propagator.cpp
View file

@ -84,10 +84,8 @@ bound_propagator::~bound_propagator() {
}
void bound_propagator::del_constraints_core() {
constraint_vector::iterator it = m_constraints.begin();
constraint_vector::iterator end = m_constraints.end();
for (; it != end; ++it) {
del_constraint(*it);
for (auto & c : m_constraints) {
del_constraint(c);
}
m_constraints.reset();
}
@ -98,10 +96,9 @@ void bound_propagator::del_constraints() {
return;
del_constraints_core();
m_constraints.finalize();
vector<wlist>::iterator it = m_watches.begin();
vector<wlist>::iterator end = m_watches.end();
for (; it != end; ++it)
it->finalize();
for (auto& wl : m_watches) {
wl.finalize();
}
}
void bound_propagator::del_constraint(constraint & c) {
@ -164,10 +161,8 @@ void bound_propagator::del_var(var x) {
m_dead[x] = true;
// mark constraints containing x as dead.
wlist & wl = m_watches[x];
wlist::iterator it = wl.begin();
wlist::iterator end = wl.end();
for (; it != end; ++it) {
m_constraints[*it].m_dead = true;
for (auto c : wl) {
m_constraints[c].m_dead = true;
}
}
@ -473,10 +468,7 @@ void bound_propagator::propagate() {
TRACE("bound_propagator_detail", tout << "propagating x" << x << "\n";);
m_qhead++;
wlist const & wl = m_watches[x];
wlist::const_iterator it = wl.begin();
wlist::const_iterator end = wl.end();
for (; it != end; ++it) {
unsigned c_idx = *it;
for (unsigned c_idx : wl) {
constraint & c = m_constraints[c_idx];
// We don't need to visit c if it was already propagated using b.
// Whenever we visit c we store in c.m_timestamp the current timestamp
@ -490,10 +482,8 @@ void bound_propagator::propagate() {
}
}
unsigned_vector::iterator it = m_to_reset_ts.begin();
unsigned_vector::iterator end = m_to_reset_ts.end();
for (; it != end; ++it)
m_constraints[*it].m_timestamp = 0;
for (unsigned c : m_to_reset_ts)
m_constraints[c].m_timestamp = 0;
}
bool bound_propagator::propagate(unsigned c_idx) {
@ -936,10 +926,7 @@ void bound_propagator::display_bounds(std::ostream & out, bool approx, bool prec
}
void bound_propagator::display_constraints(std::ostream & out) const {
constraint_vector::const_iterator it = m_constraints.begin();
constraint_vector::const_iterator end = m_constraints.end();
for (; it != end; ++it) {
constraint const & c = *it;
for (constraint const& c : m_constraints) {
if (c.m_kind == LINEAR) {
m_eq_manager.display(out, *(c.m_eq));
out << "\n";

51
src/tactic/core/solve_eqs_tactic.cpp
View file

@ -327,28 +327,53 @@ class solve_eqs_tactic : public tactic {
pr = m().mk_rewrite(eq, m().mk_eq(var, def));
return true;
}
bool solve_mod(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
rational r1, r2;
expr* arg1, *arg2, *arg3, *arg4;
if (m_produce_proofs) {
return false;
}
VERIFY(m_a_util.is_mod(lhs, arg1, arg2));
if (!m_a_util.is_numeral(arg2, r1) || !r1.is_pos()) {
return false;
}
if (m_a_util.is_mod(rhs, arg3, arg4) && m_a_util.is_numeral(arg4, r2) && r1 == r2) {
rhs = arg3;
}
else if (!m_a_util.is_numeral(rhs, r2) || !r2.is_zero()) {
return false;
}
if (solve_eq(arg1, rhs, eq, var, def, pr)) {
def = m_a_util.mk_add(def, m_a_util.mk_mul(m().mk_fresh_const("mod", m_a_util.mk_int()), m_a_util.mk_int(r1)));
return true;
}
return false;
}
bool solve_arith(expr * lhs, expr * rhs, expr * eq, app_ref & var, expr_ref & def, proof_ref & pr) {
return
(m_a_util.is_add(lhs) && solve_arith_core(to_app(lhs), rhs, eq, var, def, pr)) ||
(m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr));
#if 0
// better done inside of nlsat
(m_a_util.is_add(lhs) && solve_nl(to_app(lhs), rhs, eq, var, def, pr)) ||
(m_a_util.is_add(rhs) && solve_nl(to_app(rhs), lhs, eq, var, def, pr));
#endif
(m_a_util.is_add(rhs) && solve_arith_core(to_app(rhs), lhs, eq, var, def, pr)) ||
(m_a_util.is_mod(lhs) && solve_mod(lhs, rhs, eq, var, def, pr)) ||
(m_a_util.is_mod(rhs) && solve_mod(rhs, lhs, eq, var, def, pr));
}
bool solve_eq(expr* arg1, expr* arg2, expr* eq, app_ref& var, expr_ref & def, proof_ref& pr) {
if (trivial_solve(arg1, arg2, var, def, pr))
return true;
if (m_theory_solver) {
if (solve_arith(arg1, arg2, eq, var, def, pr))
return true;
}
return false;
}
bool solve(expr * f, app_ref & var, expr_ref & def, proof_ref & pr) {
expr* arg1 = nullptr, *arg2 = nullptr;
if (m().is_eq(f, arg1, arg2)) {
if (trivial_solve(arg1, arg2, var, def, pr))
return true;
if (m_theory_solver) {
if (solve_arith(arg1, arg2, f, var, def, pr))
return true;
}
return false;
return solve_eq(arg1, arg2, f, var, def, pr);
}
#if 0

4
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -54,7 +54,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
return r;
}
static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) {
params_ref pull_ite_p = p_ref;
pull_ite_p.set_bool("pull_cheap_ite", true);
pull_ite_p.set_bool("local_ctx", true);
@ -115,7 +115,7 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) {
return and_then(
mk_report_verbose_tactic("(qfnia-tactic)", 10),
mk_qfnia_premable(m, p),
mk_qfnia_preamble(m, p),
or_else(mk_qfnia_sat_solver(m, p),
try_for(mk_qfnia_smt_solver(m, p), 2000),