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

disable ackerman reduction when head contains a non-constant/non-variable. #947

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-03-17 10:12:32 -07:00
parent a0237ed2a6
commit d754aa2dc4
3 changed files with 11 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/muz/transforms/dl_mk_array_blast.cpp
View file

@ -126,6 +126,12 @@ namespace datalog {
app* s; app* s;
var* v; var* v;
// disable Ackerman reduction if head contains a non-variable or non-constant argument.
for (unsigned i = 0; i < to_app(head)->get_num_args(); ++i) {
expr* arg = to_app(head)->get_arg(i);
if (!is_var(arg) && !m.is_value(arg)) return false;
}
for (unsigned i = 0; i < conjs.size(); ++i) { for (unsigned i = 0; i < conjs.size(); ++i) {
expr* e = conjs[i].get(); expr* e = conjs[i].get();
if (is_select_eq_var(e, s, v)) { if (is_select_eq_var(e, s, v)) {
@ -281,6 +287,7 @@ namespace datalog {
m_rewriter(body); m_rewriter(body);
sub(head); sub(head);
m_rewriter(head); m_rewriter(head);
TRACE("dl", tout << body << " => " << head << "\n";);
change = ackermanize(r, body, head); change = ackermanize(r, body, head);
if (!change) { if (!change) {
rules.add_rule(&r); rules.add_rule(&r);

4
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
View file

@ -394,10 +394,6 @@ namespace datalog {
m_simp(a, simp1_res); m_simp(a, simp1_res);
(*m_rw)(simp1_res.get(), res); (*m_rw)(simp1_res.get(), res);
/*if (simp1_res.get()!=res.get()) {
std::cout<<"pre norm:\n"<<mk_pp(simp1_res.get(),m)<<"post norm:\n"<<mk_pp(res.get(),m)<<"\n";
}*/
m_simp(res.get(), res); m_simp(res.get(), res);
} }

6
src/smt/theory_arith_int.h
View file

@ -206,7 +206,8 @@ namespace smt {
numeral k = ceil(get_value(v)); numeral k = ceil(get_value(v));
rational _k = k.to_rational(); rational _k = k.to_rational();
expr_ref bound(get_manager()); expr_ref bound(get_manager());
bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(_k, true)); expr* e = get_enode(v)->get_owner();
bound = m_util.mk_ge(e, m_util.mk_numeral(_k, m_util.is_int(e)));
TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";); TRACE("arith_int", tout << mk_bounded_pp(bound, get_manager()) << "\n";);
context & ctx = get_context(); context & ctx = get_context();
ctx.internalize(bound, true); ctx.internalize(bound, true);
@ -371,7 +372,7 @@ namespace smt {
ctx.mk_th_axiom(get_id(), l1, l2); ctx.mk_th_axiom(get_id(), l1, l2);
TRACE("theory_arith_int", TRACE("arith_int",
tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n"; tout << "cut: (or " << mk_pp(p1, get_manager()) << " " << mk_pp(p2, get_manager()) << ")\n";
); );
@ -1407,6 +1408,7 @@ namespace smt {
if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) { if (m_params.m_arith_int_eq_branching && branch_infeasible_int_equality()) {
return FC_CONTINUE; return FC_CONTINUE;
} }
theory_var int_var = find_infeasible_int_base_var(); theory_var int_var = find_infeasible_int_base_var();
if (int_var != null_theory_var) { if (int_var != null_theory_var) {
TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";); TRACE("arith_int", tout << "v" << int_var << " does not have an integer assignment: " << get_value(int_var) << "\n";);