From 6e0369036ea1fe38d11990854593e8a49c8050d2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 3 Nov 2016 17:13:02 +0000 Subject: [PATCH 1/4] fixed log output typo --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 84931b47e..868f9b9c1 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1591,7 +1591,7 @@ class DotNetDLLComponent(Component): elif os.path.isfile(os.path.join(self.src_dir, self.key_file)): self.key_file = os.path.abspath(os.path.join(self.src_dir, self.key_file)) else: - print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.dll_name, self.key_file)) + print("Keyfile '%s' could not be found; %s.dll will be unsigned." % (self.key_file, self.dll_name)) self.key_file = None if not self.key_file is None: From 7bbdb7714fa5cd6d82f573a0f14292b5543f9aea Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 3 Nov 2016 17:20:39 +0000 Subject: [PATCH 2/4] Added signed .NET assemblies in unix builds --- scripts/mk_util.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 868f9b9c1..873af8432 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -82,7 +82,7 @@ Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False DOTNET_ENABLED=False -DOTNET_KEY_FILE=None +DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False ML_ENABLED=False PYTHON_INSTALL_ENABLED=False From a3e915fbea00c30d6614824405086d7fc348905e Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Nov 2016 13:37:14 +0000 Subject: [PATCH 3/4] Whitespace --- src/ast/rewriter/bool_rewriter.cpp | 6 +-- src/tactic/core/ctx_simplify_tactic.cpp | 58 ++++++++++++------------- 2 files changed, 32 insertions(+), 32 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 66c5e66bc..a914d6a0a 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -581,15 +581,15 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) TRACE("try_ite_value", tout << mk_ismt2_pp(t, m()) << " " << mk_ismt2_pp(e, m()) << " " << mk_ismt2_pp(val, m()) << "\n"; tout << t << " " << e << " " << val << "\n";); result = m().mk_false(); - } + } else if (t == val && e == val) { result = m().mk_true(); - } + } else if (t == val) { result = cond; } else { - SASSERT(e == val); + SASSERT(e == val); mk_not(cond, result); } return BR_DONE; diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 1cda9cc6f..5258f8c5c 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -46,7 +46,7 @@ public: ctx_propagate_assertions::ctx_propagate_assertions(ast_manager& m): m(m), m_trail(m) {} bool ctx_propagate_assertions::assert_expr(expr * t, bool sign) { - + expr * p = t; while (m.is_not(t, t)) { sign = !sign; @@ -83,8 +83,8 @@ void ctx_propagate_assertions::assert_eq_core(expr * t, app * val) { // because the simplifier stopped at depth m_max_depth return; } - - CTRACE("assert_eq_bug", m_assertions.contains(t), + + CTRACE("assert_eq_bug", m_assertions.contains(t), tout << "t:\n" << mk_ismt2_pp(t, m) << "\nval:\n" << mk_ismt2_pp(val, m) << "\n"; expr * old_val = 0; m_assertions.find(t, old_val); @@ -114,11 +114,11 @@ void ctx_propagate_assertions::pop(unsigned num_scopes) { m_trail.pop_back(); } SASSERT(m_trail.size() == old_trail_size); - m_scopes.shrink(scope_lvl - num_scopes); + m_scopes.shrink(scope_lvl - num_scopes); } -bool ctx_simplify_tactic::simplifier::shared(expr * t) const { +bool ctx_simplify_tactic::simplifier::shared(expr * t) const { SASSERT(m_occs); return t->get_ref_count() > 1 && m_occs->get_num_occs(t) > 1; } @@ -139,7 +139,7 @@ struct ctx_simplify_tactic::imp { unsigned m_lvl; cached_result * m_next; cached_result(expr * t, unsigned lvl, cached_result * next): - m_to(t), + m_to(t), m_lvl(lvl), m_next(next) { } @@ -156,7 +156,7 @@ struct ctx_simplify_tactic::imp { small_object_allocator m_allocator; svector m_cache; vector > m_cache_undo; - unsigned m_depth; + unsigned m_depth; unsigned m_num_steps; goal_num_occurs m_occs; mk_simplified_app m_mk_app; @@ -183,7 +183,7 @@ struct ctx_simplify_tactic::imp { dealloc(m_simp); DEBUG_CODE({ for (unsigned i = 0; i < m_cache.size(); i++) { - CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, + CTRACE("ctx_simplify_tactic_bug", m_cache[i].m_from, tout << "i: " << i << "\n" << mk_ismt2_pp(m_cache[i].m_from, m) << "\n"; tout << "m_result: " << m_cache[i].m_result << "\n"; if (m_cache[i].m_result) tout << "lvl: " << m_cache[i].m_result->m_lvl << "\n";); @@ -209,7 +209,7 @@ struct ctx_simplify_tactic::imp { throw tactic_exception(m.limit().get_cancel_msg()); } - bool shared(expr * t) const { + 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; } @@ -233,7 +233,7 @@ struct ctx_simplify_tactic::imp { unsigned id = from->get_id(); TRACE("ctx_simplify_tactic_cache", tout << "caching " << id << " @ " << scope_level() << "\n" << mk_ismt2_pp(from, m) << "\n--->\n" << mk_ismt2_pp(to, m) << "\n";); m_cache.reserve(id+1); - cache_cell & cell = m_cache[id]; + cache_cell & cell = m_cache[id]; void * mem = m_allocator.allocate(sizeof(cached_result)); if (cell.m_from == 0) { // new_entry @@ -243,7 +243,7 @@ struct ctx_simplify_tactic::imp { m.inc_ref(to); } else { - // update + // update cell.m_result = new (mem) cached_result(to, scope_level(), cell.m_result); m.inc_ref(to); } @@ -255,7 +255,7 @@ struct ctx_simplify_tactic::imp { if (shared(from)) cache_core(from, to); } - + unsigned scope_level() const { return m_simp->scope_level(); } @@ -276,7 +276,7 @@ struct ctx_simplify_tactic::imp { m.dec_ref(cell.m_result->m_to); cached_result * to_delete = cell.m_result; SASSERT(to_delete->m_lvl == lvl); - TRACE("ctx_simplify_tactic_cache", tout << "uncaching: " << to_delete->m_lvl << "\n" << + TRACE("ctx_simplify_tactic_cache", tout << "uncaching: " << to_delete->m_lvl << "\n" << mk_ismt2_pp(key, m) << "\n--->\n" << mk_ismt2_pp(to_delete->m_to, m) << "\nrestoring:\n"; if (to_delete->m_next) tout << mk_ismt2_pp(to_delete->m_next->m_to, m); else tout << ""; tout << "\n";); @@ -287,7 +287,7 @@ struct ctx_simplify_tactic::imp { } m_allocator.deallocate(sizeof(cached_result), to_delete); } - keys.reset(); + keys.reset(); } void pop(unsigned num_scopes) { @@ -295,7 +295,7 @@ struct ctx_simplify_tactic::imp { return; SASSERT(num_scopes <= scope_level()); - unsigned lvl = scope_level(); + unsigned lvl = scope_level(); m_simp->pop(num_scopes); // restore cache @@ -339,7 +339,7 @@ struct ctx_simplify_tactic::imp { } m_num_steps++; m_depth++; - if (m.is_or(t)) + if (m.is_or(t)) simplify_or_and(to_app(t), r); else if (m.is_and(t)) simplify_or_and(to_app(t), r); @@ -351,7 +351,7 @@ struct ctx_simplify_tactic::imp { SASSERT(r.get() != 0); TRACE("ctx_simplify_tactic_detail", tout << "result:\n" << mk_bounded_pp(t, m) << "\n---->\n" << mk_bounded_pp(r, m) << "\n";); } - + template void simplify_or_and(app * t, expr_ref & r) { // go forwards @@ -374,7 +374,7 @@ struct ctx_simplify_tactic::imp { continue; } if ((OR && m.is_true(new_arg)) || - (!OR && m.is_false(new_arg))) { + (!OR && m.is_false(new_arg))) { r = new_arg; pop(scope_level() - old_lvl); cache(t, r); @@ -403,7 +403,7 @@ struct ctx_simplify_tactic::imp { continue; } if ((OR && m.is_true(new_arg)) || - (!OR && m.is_false(new_arg))) { + (!OR && m.is_false(new_arg))) { r = new_arg; pop(scope_level() - old_lvl); cache(t, r); @@ -428,7 +428,7 @@ struct ctx_simplify_tactic::imp { } cache(t, r); } - + void simplify_ite(app * ite, expr_ref & r) { expr * c = ite->get_arg(0); expr * t = ite->get_arg(1); @@ -467,8 +467,8 @@ struct ctx_simplify_tactic::imp { } else { expr * args[3] = { new_c.get(), new_t.get(), new_e.get() }; - TRACE("ctx_simplify_tactic_ite_bug", - tout << "mk_ite\n" << mk_ismt2_pp(new_c.get(), m) << "\n" << mk_ismt2_pp(new_t.get(), m) + TRACE("ctx_simplify_tactic_ite_bug", + tout << "mk_ite\n" << mk_ismt2_pp(new_c.get(), m) << "\n" << mk_ismt2_pp(new_t.get(), m) << "\n" << mk_ismt2_pp(new_e.get(), m) << "\n";); m_mk_app(ite->get_decl(), 3, args, r); } @@ -529,7 +529,7 @@ struct ctx_simplify_tactic::imp { unsigned sz = g.size(); expr_ref r(m); for (unsigned i = 0; !g.inconsistent() && i < sz; ++i) { - m_depth = 0; + m_depth = 0; simplify(g.form(i), r); if (i < sz - 1 && !m.is_true(r) && !m.is_false(r) && !g.dep(i) && !assert_expr(r, false)) { r = m.mk_false(); @@ -590,7 +590,7 @@ struct ctx_simplify_tactic::imp { IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-simplify :num-steps " << m_num_steps << ")\n";); SASSERT(g.is_well_sorted()); } - + }; ctx_simplify_tactic::ctx_simplify_tactic(ast_manager & m, simplifier* simp, params_ref const & p): @@ -618,9 +618,9 @@ void ctx_simplify_tactic::get_param_descrs(param_descrs & r) { r.insert("propagate_eq", CPK_BOOL, "(default: false) enable equality propagation from bounds."); } -void ctx_simplify_tactic::operator()(goal_ref const & in, - goal_ref_buffer & result, - model_converter_ref & mc, +void ctx_simplify_tactic::operator()(goal_ref const & in, + goal_ref_buffer & result, + model_converter_ref & mc, proof_converter_ref & pc, expr_dependency_ref & core) { mc = 0; pc = 0; core = 0; @@ -628,12 +628,12 @@ void ctx_simplify_tactic::operator()(goal_ref const & in, in->inc_depth(); result.push_back(in.get()); } - + void ctx_simplify_tactic::cleanup() { ast_manager & m = m_imp->m; imp * d = alloc(imp, m, m_imp->m_simp->translate(m), m_params); - std::swap(d, m_imp); + std::swap(d, m_imp); dealloc(d); } From 824ba1497744f0c646d4a6d9056b2d3108828854 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 4 Nov 2016 13:39:53 +0000 Subject: [PATCH 4/4] Disabled some ITE rewrite rules that were applied by default, but too expensive. Added re-computation of subterm occurrences in ctx_simplify_tactic. (Performance fixes for QF_LIA benchmarks). --- src/ast/rewriter/bool_rewriter.cpp | 36 +++++++++++++------------ src/tactic/core/ctx_simplify_tactic.cpp | 2 ++ 2 files changed, 21 insertions(+), 17 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index a914d6a0a..ce3eb5844 100644 --- a/src/ast/rewriter/bool_rewriter.cpp +++ b/src/ast/rewriter/bool_rewriter.cpp @@ -594,25 +594,27 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) } return BR_DONE; } - if (m().is_value(t)) { - if (val == t) { - result = m().mk_or(cond, m().mk_eq(val, e)); + if (m_ite_extra_rules) { + if (m().is_value(t)) { + if (val == t) { + result = m().mk_or(cond, m().mk_eq(val, e)); + } + else { + mk_not(cond, result); + result = m().mk_and(result, m().mk_eq(val, e)); + } + return BR_REWRITE2; } - else { - mk_not(cond, result); - result = m().mk_and(result, m().mk_eq(val, e)); + if (m().is_value(e)) { + if (val == e) { + mk_not(cond, result); + result = m().mk_or(result, m().mk_eq(val, t)); + } + else { + result = m().mk_and(cond, m().mk_eq(val, t)); + } + return BR_REWRITE2; } - return BR_REWRITE2; - } - if (m().is_value(e)) { - if (val == e) { - mk_not(cond, result); - result = m().mk_or(result, m().mk_eq(val, t)); - } - else { - result = m().mk_and(cond, m().mk_eq(val, t)); - } - return BR_REWRITE2; } expr* cond2, *t2, *e2; if (m().is_ite(t, cond2, t2, e2) && m().is_value(t2) && m().is_value(e2)) { diff --git a/src/tactic/core/ctx_simplify_tactic.cpp b/src/tactic/core/ctx_simplify_tactic.cpp index 5258f8c5c..3e2790fe3 100644 --- a/src/tactic/core/ctx_simplify_tactic.cpp +++ b/src/tactic/core/ctx_simplify_tactic.cpp @@ -538,6 +538,8 @@ struct ctx_simplify_tactic::imp { } pop(scope_level() - old_lvl); + m_occs(g); + // go backwards sz = g.size(); for (unsigned i = sz; !g.inconsistent() && i > 0; ) {