mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix clause check in goal2dimacs, redo rewriting of mod to avoid deeply nested mod

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-06 21:33:53 -07:00
parent 0b30ddb769
commit c4e4139ab6
2 changed files with 30 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -927,30 +927,29 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul
return BR_DONE;
}
// propagate mod inside only if not all arguments are not already mod.
// propagate mod inside only if there is something to reduce.
if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) {
TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";);
unsigned num_args = to_app(arg1)->get_num_args();
unsigned i;
rational arg_v;
for (i = 0; i < num_args; i++) {
expr * arg = to_app(arg1)->get_arg(i);
if (m_util.is_mod(arg))
continue;
if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) == arg_v)
continue;
if (m().is_ite(arg))
continue;
// found target for rewriting
break;
expr_ref_buffer args(m());
bool change = false;
for (expr* arg : *to_app(arg1)) {
rational arg_v;
if (m_util.is_numeral(arg, arg_v) && mod(arg_v, v2) != arg_v) {
change = true;
args.push_back(m_util.mk_numeral(mod(arg_v, v2), true));
}
else if (m_util.is_mod(arg, t1, t2) && t2 == arg2) {
change = true;
args.push_back(t1);
}
else {
args.push_back(arg);
}
}
TRACE("mod_bug", tout << "mk_mod target: " << i << "\n";);
if (i == num_args)
if (!change) {
return BR_FAILED; // did not find any target for applying simplification
ptr_buffer<expr> new_args;
for (unsigned i = 0; i < num_args; i++)
new_args.push_back(m_util.mk_mod(to_app(arg1)->get_arg(i), arg2));
result = m_util.mk_mod(m().mk_app(to_app(arg1)->get_decl(), new_args.size(), new_args.c_ptr()), arg2);
}
result = m_util.mk_mod(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.c_ptr()), arg2);
TRACE("mod_bug", tout << "mk_mod result: " << mk_ismt2_pp(result, m()) << "\n";);
return BR_REWRITE3;
}

15
src/tactic/goal.cpp
View file

@ -721,11 +721,16 @@ bool goal::is_cnf() const {
for (unsigned i = 0; i < size(); i++) {
expr * f = form(i);
if (m_manager.is_or(f)) {
for (expr* l : *to_app(f)) {
if (!is_literal(f)) return false;
for (expr* lit : *to_app(f)) {
if (!is_literal(lit)) {
return false;
}
}
return true;
}
if (!is_literal(f)) {
return false;
}
if (!is_literal(f)) return false;
}
return true;
}
@ -735,7 +740,9 @@ bool goal::is_literal(expr* f) const {
if (!is_app(f)) return false;
if (to_app(f)->get_family_id() == m_manager.get_basic_family_id()) {
for (expr* arg : *to_app(f))
if (m_manager.is_bool(arg)) return false;
if (m_manager.is_bool(arg)) {
return false;
}
}
return true;
}