mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

overhead with push-ite on shared terms

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-02-14 19:36:14 +02:00
parent 3d26b501e7
commit 9a4d6cee6c
3 changed files with 8 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/ast/rewriter/poly_rewriter_def.h
View file

@ -979,9 +979,8 @@ expr* poly_rewriter<Config>::merge_muls(expr* x, expr* y) {
template<typename Config>
bool poly_rewriter<Config>::hoist_ite(expr_ref& e) {
if (!m_hoist_ite) {
if (!m_hoist_ite)
return false;
}
obj_hashtable<expr> shared;
ptr_buffer<expr> adds;
expr_ref_vector bs(m()), pinned(m());

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

@ -295,6 +295,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
bool is_ite_value_tree(expr * t) {
if (!m().is_ite(t))
return false;
if (t->get_ref_count() != 1)
return false;
ptr_buffer<app> todo;
todo.push_back(to_app(t));
while (!todo.empty()) {
@ -319,7 +321,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
br_status pull_ite(func_decl * f, unsigned num, expr * const * args, expr_ref & result) {
if (num == 2 && m().is_bool(f->get_range()) && !m().is_bool(args[0])) {
if (m().is_ite(args[0])) {
if (m().is_value(args[1]))
if (m().is_value(args[1]) && args[0]->get_ref_count() == 1)
return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) {
// (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2))
@ -329,17 +331,17 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
return BR_REWRITE2;
}
}
if (m().is_ite(args[1]) && m().is_value(args[0]))
if (m().is_ite(args[1]) && m().is_value(args[0]) && args[1]->get_ref_count() == 1)
return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
}
family_id fid = f->get_family_id();
if (num == 2 && (fid == m().get_basic_family_id() || fid == m_a_rw.get_fid() || fid == m_bv_rw.get_fid())) {
// (f v3 (ite c v1 v2)) --> (ite v (f v3 v1) (f v3 v2))
if (m().is_value(args[0]) && is_ite_value_tree(args[1]))
if (m().is_value(args[0]) && is_ite_value_tree(args[1]))
return pull_ite_core<true>(f, to_app(args[1]), to_app(args[0]), result);
// (f (ite c v1 v2) v3) --> (ite v (f v1 v3) (f v2 v3))
if (m().is_value(args[1]) && is_ite_value_tree(args[0]))
if (m().is_value(args[1]) && is_ite_value_tree(args[0]))
return pull_ite_core<false>(f, to_app(args[0]), to_app(args[1]), result);
}
return BR_FAILED;

1
src/tactic/tactic.cpp
View file

@ -52,6 +52,7 @@ struct tactic_report::imp {
<< " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
<< " :after-memory " << std::fixed << std::setprecision(2) << end_memory
<< ")" << std::endl);
IF_VERBOSE(20, m_goal.display(verbose_stream() << m_id << "\n"));
SASSERT(m_goal.is_well_formed());
}
};