From 110fa0b7fb711418fe2be67f033e8ed70b354972 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 5 Jun 2013 13:50:22 -0700 Subject: [PATCH 1/3] Fix issue http://z3.codeplex.com/workitem/45 Signed-off-by: Leonardo de Moura --- src/ast/simplifier/bv_simplifier_plugin.cpp | 40 +++++++++++++++---- src/ast/simplifier/poly_simplifier_plugin.cpp | 1 + 2 files changed, 33 insertions(+), 8 deletions(-) diff --git a/src/ast/simplifier/bv_simplifier_plugin.cpp b/src/ast/simplifier/bv_simplifier_plugin.cpp index 3ef55baba..8ee353a76 100644 --- a/src/ast/simplifier/bv_simplifier_plugin.cpp +++ b/src/ast/simplifier/bv_simplifier_plugin.cpp @@ -636,7 +636,31 @@ bool bv_simplifier_plugin::try_mk_extract(unsigned high, unsigned low, expr * ar if (!all_found) { return false; } - result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr()); + // We should not use mk_app because it does not guarantee that the result would be in simplified form. + // result = m_manager.mk_app(m_fid, a->get_decl_kind(), new_args.size(), new_args.c_ptr()); + if (is_app_of(a, m_fid, OP_BAND)) + mk_bv_and(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BOR)) + mk_bv_or(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BXOR)) + mk_bv_xor(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNOR)) + mk_bv_nor(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNAND)) + mk_bv_nand(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BNOT)) { + SASSERT(new_args.size() == 1); + mk_bv_not(new_args[0], result); + } + else if (is_app_of(a, m_fid, OP_BADD)) + mk_add(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BMUL)) + mk_mul(new_args.size(), new_args.c_ptr(), result); + else if (is_app_of(a, m_fid, OP_BSUB)) + mk_sub(new_args.size(), new_args.c_ptr(), result); + else { + UNREACHABLE(); + } return true; } else if (m_manager.is_ite(a)) { @@ -747,16 +771,16 @@ void bv_simplifier_plugin::mk_bv_eq(expr* a1, expr* a2, expr_ref& result) { expr * arg1 = *it1; expr * arg2 = *it2; TRACE("expr_bv_util", tout << "low1: " << low1 << " low2: " << low2 << "\n"; - ast_ll_pp(tout, m_manager, arg1); - ast_ll_pp(tout, m_manager, arg2);); + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n";); unsigned sz1 = get_bv_size(arg1); unsigned sz2 = get_bv_size(arg2); SASSERT(low1 < sz1 && low2 < sz2); unsigned rsz1 = sz1 - low1; unsigned rsz2 = sz2 - low2; TRACE("expr_bv_util", tout << "rsz1: " << rsz1 << " rsz2: " << rsz2 << "\n"; - ast_ll_pp(tout, m_manager, arg1); ast_ll_pp(tout, m_manager, arg2);); - + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n";); if (rsz1 == rsz2) { mk_extract(sz1 - 1, low1, arg1, lhs); @@ -826,9 +850,9 @@ void bv_simplifier_plugin::mk_eq_core(expr * arg1, expr * arg2, expr_ref & resul } m_bsimp.mk_and(tmps.size(), tmps.c_ptr(), result); TRACE("mk_eq_bb", - ast_ll_pp(tout, m_manager, arg1); - ast_ll_pp(tout, m_manager, arg2); - ast_ll_pp(tout, m_manager, result);); + tout << mk_pp(arg1, m_manager) << "\n"; + tout << mk_pp(arg2, m_manager) << "\n"; + tout << mk_pp(result, m_manager) << "\n";); return; } #endif diff --git a/src/ast/simplifier/poly_simplifier_plugin.cpp b/src/ast/simplifier/poly_simplifier_plugin.cpp index 402b078a8..d64123e7b 100644 --- a/src/ast/simplifier/poly_simplifier_plugin.cpp +++ b/src/ast/simplifier/poly_simplifier_plugin.cpp @@ -285,6 +285,7 @@ bool poly_simplifier_plugin::merge_monomials(bool inv, expr * n1, expr * n2, exp else result = m_manager.mk_app(m_fid, m_MUL, mk_numeral(k1), b); } + TRACE("merge_monomials", tout << mk_pp(n1, m_manager) << "\n" << mk_pp(n2, m_manager) << "\n" << mk_pp(result, m_manager) << "\n";); return true; } From f4f1c63abb4a6fd0df908e376b0ab014bce3d9da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Jun 2013 13:20:43 -0700 Subject: [PATCH 2/3] Fix issue https://z3.codeplex.com/workitem/38 Signed-off-by: Leonardo de Moura --- src/sat/sat_clause_use_list.h | 20 +++++++++++++++++--- src/sat/sat_simplifier.cpp | 27 +++++++++++++++++---------- src/sat/sat_simplifier.h | 4 ++-- 3 files changed, 36 insertions(+), 15 deletions(-) diff --git a/src/sat/sat_clause_use_list.h b/src/sat/sat_clause_use_list.h index ccf4b4a5b..0859439d5 100644 --- a/src/sat/sat_clause_use_list.h +++ b/src/sat/sat_clause_use_list.h @@ -20,6 +20,7 @@ Revision History: #define _SAT_CLAUSE_USE_LIST_H_ #include"sat_types.h" +#include"trace.h" namespace sat { @@ -35,6 +36,7 @@ namespace sat { #endif public: clause_use_list() { + STRACE("clause_use_list_bug", tout << "[cul_created] " << this << "\n";); #ifdef LAZY_USE_LIST m_size = 0; #endif @@ -51,22 +53,33 @@ namespace sat { bool empty() const { return size() == 0; } void insert(clause & c) { - SASSERT(!m_clauses.contains(&c)); SASSERT(!c.was_removed()); + STRACE("clause_use_list_bug", tout << "[cul_insert] " << this << " " << &c << "\n";); + SASSERT(!m_clauses.contains(&c)); + SASSERT(!c.was_removed()); m_clauses.push_back(&c); #ifdef LAZY_USE_LIST m_size++; #endif } + void erase_not_removed(clause & c) { + STRACE("clause_use_list_bug", tout << "[cul_erase_not_removed] " << this << " " << &c << "\n";); #ifdef LAZY_USE_LIST - SASSERT(m_clauses.contains(&c)); SASSERT(!c.was_removed()); m_clauses.erase(&c); m_size--; + SASSERT(m_clauses.contains(&c)); + SASSERT(!c.was_removed()); + m_clauses.erase(&c); + m_size--; #else m_clauses.erase(&c); #endif } + void erase(clause & c) { + STRACE("clause_use_list_bug", tout << "[cul_erase] " << this << " " << &c << "\n";); #ifdef LAZY_USE_LIST - SASSERT(m_clauses.contains(&c)); SASSERT(c.was_removed()); m_size--; + SASSERT(m_clauses.contains(&c)); + SASSERT(c.was_removed()); + m_size--; #else m_clauses.erase(&c); #endif @@ -80,6 +93,7 @@ namespace sat { } bool check_invariant() const; + // iterate & compress class iterator { clause_vector & m_clauses; diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 623c73758..51006b2c9 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -146,8 +146,11 @@ namespace sat { m_need_cleanup = false; m_use_list.init(s.num_vars()); init_visited(); - if (learned) + bool learned_in_use_lists = false; + if (learned) { register_clauses(s.m_learned); + learned_in_use_lists = true; + } register_clauses(s.m_clauses); if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls)) @@ -179,7 +182,7 @@ namespace sat { if (!m_need_cleanup) { if (vars_eliminated) { // must remove learned clauses with eliminated variables - cleanup_clauses(s.m_learned, true, true); + cleanup_clauses(s.m_learned, true, true, learned_in_use_lists); } CASSERT("sat_solver", s.check_invariant()); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); @@ -187,8 +190,8 @@ namespace sat { return; } cleanup_watches(); - cleanup_clauses(s.m_learned, true, vars_eliminated); - cleanup_clauses(s.m_clauses, false, vars_eliminated); + cleanup_clauses(s.m_learned, true, vars_eliminated, learned_in_use_lists); + cleanup_clauses(s.m_clauses, false, vars_eliminated, true); TRACE("after_simplifier", s.display(tout); tout << "model_converter:\n"; s.m_mc.display(tout);); CASSERT("sat_solver", s.check_invariant()); free_memory(); @@ -221,7 +224,7 @@ namespace sat { } } - void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated) { + void simplifier::cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists) { clause_vector::iterator it = cs.begin(); clause_vector::iterator it2 = it; clause_vector::iterator end = cs.end(); @@ -245,7 +248,7 @@ namespace sat { } } - if (cleanup_clause(c)) { + if (cleanup_clause(c, in_use_lists)) { s.del_clause(c); continue; } @@ -516,7 +519,7 @@ namespace sat { Return true if the clause is satisfied */ - bool simplifier::cleanup_clause(clause & c) { + bool simplifier::cleanup_clause(clause & c, bool in_use_list) { bool r = false; unsigned sz = c.size(); unsigned j = 0; @@ -529,7 +532,11 @@ namespace sat { break; case l_false: m_need_cleanup = true; - m_use_list.get(l).erase_not_removed(c); + if (in_use_list && !c.frozen()) { + // Remark: if in_use_list is false, then the given clause was not added to the use lists. + // Remark: frozen clauses are not added to the use lists. + m_use_list.get(l).erase_not_removed(c); + } break; case l_true: r = true; @@ -611,7 +618,7 @@ namespace sat { clause_use_list & occurs = m_use_list.get(l); occurs.erase_not_removed(c); m_sub_counter -= occurs.size()/2; - if (cleanup_clause(c)) { + if (cleanup_clause(c, true /* clause is in the use lists */)) { // clause was satisfied TRACE("elim_lit", tout << "clause was satisfied\n";); remove_clause(c); @@ -805,7 +812,7 @@ namespace sat { m_sub_counter--; TRACE("subsumption", tout << "next: " << c << "\n";); if (s.m_trail.size() > m_last_sub_trail_sz) { - if (cleanup_clause(c)) { + if (cleanup_clause(c, true /* clause is in the use_lists */)) { remove_clause(c); continue; } diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h index 44e2f0dee..96d346598 100644 --- a/src/sat/sat_simplifier.h +++ b/src/sat/sat_simplifier.h @@ -125,7 +125,7 @@ namespace sat { void collect_subsumed0(clause const & c1, clause_vector & out); void back_subsumption0(clause & c1); - bool cleanup_clause(clause & c); + bool cleanup_clause(clause & c, bool in_use_list); bool cleanup_clause(literal_vector & c); void propagate_unit(literal l); void elim_lit(clause & c, literal l); @@ -136,7 +136,7 @@ namespace sat { void subsume(); void cleanup_watches(); - void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated); + void cleanup_clauses(clause_vector & cs, bool learned, bool vars_eliminated, bool in_use_lists); bool is_external(bool_var v) const; bool was_eliminated(bool_var v) const; From 2b59f2ecc2b0cb7621c8558cd635a2b930b71097 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 6 Jun 2013 18:29:29 -0700 Subject: [PATCH 3/3] Fix issue https://z3.codeplex.com/workitem/37 Signed-off-by: Leonardo de Moura --- src/tactic/core/ctx_simplify_tactic.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 2c2afab6f..71f4771a9 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -21,7 +21,7 @@ Notes: #include"goal_num_occurs.h" #include"cooperate.h" #include"ast_ll_pp.h" -#include"ast_smt2_pp.h" +#include"ast_pp.h" struct ctx_simplify_tactic::imp { struct cached_result { @@ -105,6 +105,7 @@ struct ctx_simplify_tactic::imp { } bool shared(expr * t) const { + TRACE("ctx_simplify_tactic_bug", tout << mk_pp(t, m) << "\n";); return t->get_ref_count() > 1 && m_occs.get_num_occs(t) > 1; } @@ -242,12 +243,13 @@ struct ctx_simplify_tactic::imp { } void assert_expr(expr * t, bool sign) { + expr * p = t; if (m.is_not(t)) { t = to_app(t)->get_arg(0); sign = !sign; } bool mk_scope = true; - if (shared(t)) { + if (shared(t) || shared(p)) { push(); mk_scope = false; assert_eq_core(t, sign ? m.mk_false() : m.mk_true()); @@ -457,7 +459,7 @@ struct ctx_simplify_tactic::imp { if (visit.is_marked(s)) { continue; } - visit.mark(s, true); + visit.mark(s, true); ++sz; for (unsigned i = 0; is_app(s) && i < to_app(s)->get_num_args(); ++i) { todo.push_back(to_app(s)->get_arg(i));