From c24d445886360b117f226fea438311103a9e6331 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Sep 2022 17:05:00 -0500 Subject: [PATCH] fix #6355 conversion from AIG to expressions should always use the optimized conversion function. the aig-tactic should throttle regarding output bloat from AIG. If the expression after AIG simpification, for whatever reason, is bloated the rewrite does not take place. --- src/tactic/aig/aig.cpp | 54 +++++++++++----------------- src/tactic/aig/aig_tactic.cpp | 46 ++++++++++++++++-------- src/tactic/smtlogics/qfbv_tactic.cpp | 8 +---- 3 files changed, 53 insertions(+), 55 deletions(-) diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index b689a53e2..433120b48 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -18,7 +18,8 @@ Notes: --*/ #include "tactic/aig/aig.h" #include "tactic/goal.h" -#include "ast/ast_smt2_pp.h" +#include "ast/ast_ll_pp.h" +#include "ast/ast_util.h" #define USE_TWO_LEVEL_RULES #define FIRST_NODE_ID (UINT_MAX/2) @@ -431,13 +432,8 @@ struct aig_manager::imp { expr2aig(imp & _m):m(_m) {} ~expr2aig() { - obj_map::iterator it = m_cache.begin(); - obj_map::iterator end = m_cache.end(); - for (; it != end; ++it) { - TRACE("expr2aig", tout << "dec-ref: "; m.display_ref(tout, it->m_value); - tout << " ref-count: " << ref_count(it->m_value) << "\n";); - m.dec_ref(it->m_value); - } + for (auto& [k,v] : m_cache) + m.dec_ref(v); restore_result_stack(0); } @@ -447,7 +443,7 @@ struct aig_manager::imp { } void cache_result(expr * t, aig_lit const & r) { - TRACE("expr2aig", tout << "caching:\n" << mk_ismt2_pp(t, m.m()) << "\n---> "; m.display_ref(tout, r); tout << "\n";); + TRACE("expr2aig", tout << "caching:\n" << mk_bounded_pp(t, m.m()) << "\n---> "; m.display_ref(tout, r); tout << "\n";); SASSERT(!m_cache.contains(t)); m.inc_ref(r); m_cache.insert(t, r); @@ -1009,33 +1005,34 @@ struct aig_manager::imp { r = invert(r); } - void operator()(aig_lit const & l, expr_ref & r) { - naive(l, r); - } - - void operator()(aig_lit const & l, goal & g) { - g.reset(); + void not_naive(aig_lit const& l, expr_ref & r) { sbuffer roots; + expr_ref_vector rs(r.m()); roots.push_back(l); while (!roots.empty()) { aig_lit n = roots.back(); roots.pop_back(); if (n.is_inverted()) { - g.assert_expr(invert(process_root(n.ptr())), nullptr, nullptr); + rs.push_back(invert(process_root(n.ptr()))); continue; } aig * p = n.ptr(); if (m.is_ite(p)) { - g.assert_expr(process_root(p), nullptr, nullptr); + rs.push_back(process_root(p)); continue; } if (is_var(p)) { - g.assert_expr(m.var2expr(p), nullptr, nullptr); + rs.push_back(m.var2expr(p)); continue; } roots.push_back(left(p)); roots.push_back(right(p)); } + r = ::mk_and(rs); + } + + void operator()(aig_lit const & l, expr_ref & r) { + not_naive(l, r); } }; @@ -1534,18 +1531,14 @@ public: } SASSERT(ref_count(r) >= 1); } - catch (const aig_exception & ex) { - dec_ref(r); - throw ex; - } + catch (const aig_exception & ex) { + dec_ref(r); + throw ex; + } dec_ref_result(r); return r; } - void to_formula(aig_lit const & r, goal & g) { - aig2expr proc(*this); - proc(r, g); - } void to_formula(aig_lit const & r, expr_ref & result) { aig2expr proc(*this); @@ -1581,7 +1574,7 @@ public: qhead++; display_ref(out, n); out << ": "; if (is_var(n)) { - out << mk_ismt2_pp(m_var2exprs[n->m_id], m()) << "\n"; + out << mk_bounded_pp(m_var2exprs[n->m_id], m()) << "\n"; } else { display_ref(out, n->m_children[0]); @@ -1607,7 +1600,7 @@ public: if (r.is_inverted()) out << "(not "; if (is_var(r)) { - out << mk_ismt2_pp(var2expr(r.ptr()), m()); + out << mk_bounded_pp(var2expr(r.ptr()), m()); } else { out << "aig" << to_idx(r.ptr()); @@ -1738,11 +1731,6 @@ void aig_manager::max_sharing(aig_ref & r) { r = aig_ref(*this, m_imp->max_sharing(aig_lit(r))); } -void aig_manager::to_formula(aig_ref const & r, goal & g) { - SASSERT(!g.proofs_enabled()); - SASSERT(!g.unsat_core_enabled()); - return m_imp->to_formula(aig_lit(r), g); -} void aig_manager::to_formula(aig_ref const & r, expr_ref & res) { return m_imp->to_formula(aig_lit(r), res); diff --git a/src/tactic/aig/aig_tactic.cpp b/src/tactic/aig/aig_tactic.cpp index 5ffc0dc20..9c5390c16 100644 --- a/src/tactic/aig/aig_tactic.cpp +++ b/src/tactic/aig/aig_tactic.cpp @@ -16,6 +16,9 @@ Author: Notes: --*/ +#include "ast/ast_util.h" +#include "ast/ast_ll_pp.h" +#include "ast/for_each_expr.h" #include "tactic/tactical.h" #include "tactic/aig/aig.h" @@ -24,7 +27,6 @@ class aig_manager; class aig_tactic : public tactic { unsigned long long m_max_memory; bool m_aig_gate_encoding; - bool m_aig_per_assertion; aig_manager * m_aig_manager; struct mk_aig_manager { @@ -52,40 +54,54 @@ public: aig_tactic * t = alloc(aig_tactic); t->m_max_memory = m_max_memory; t->m_aig_gate_encoding = m_aig_gate_encoding; - t->m_aig_per_assertion = m_aig_per_assertion; return t; } void updt_params(params_ref const & p) override { m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true); - m_aig_per_assertion = p.get_bool("aig_per_assertion", true); } void collect_param_descrs(param_descrs & r) override { insert_max_memory(r); - r.insert("aig_per_assertion", CPK_BOOL, "(default: true) process one assertion at a time."); } void operator()(goal_ref const & g) { + ast_manager& m = g->m(); + mk_aig_manager mk(*this, m); - mk_aig_manager mk(*this, g->m()); - if (m_aig_per_assertion) { - for (unsigned i = 0; i < g->size(); i++) { + expr_ref_vector nodeps(m); + + for (unsigned i = 0; i < g->size(); i++) { + expr_dependency * ed = g->dep(i); + if (!ed) { + nodeps.push_back(g->form(i)); + g->update(i, m.mk_true()); + } + else { aig_ref r = m_aig_manager->mk_aig(g->form(i)); m_aig_manager->max_sharing(r); - expr_ref new_f(g->m()); + expr_ref new_f(m); m_aig_manager->to_formula(r, new_f); - expr_dependency * ed = g->dep(i); - g->update(i, new_f, nullptr, ed); + unsigned old_sz = get_num_exprs(g->form(i)); + unsigned new_sz = get_num_exprs(new_f); + if (new_sz <= 1.2*old_sz) + g->update(i, new_f, nullptr, ed); } } - else { - fail_if_unsat_core_generation("aig", g); - aig_ref r = m_aig_manager->mk_aig(*(g.get())); - g->reset(); // save memory + + if (!nodeps.empty()) { + expr_ref conj(::mk_and(nodeps)); + aig_ref r = m_aig_manager->mk_aig(conj); m_aig_manager->max_sharing(r); - m_aig_manager->to_formula(r, *(g.get())); + expr_ref new_f(m); + m_aig_manager->to_formula(r, new_f); + unsigned old_sz = get_num_exprs(conj); + unsigned new_sz = get_num_exprs(new_f); + + if (new_sz > 1.2*old_sz) + new_f = conj; + g->assert_expr(new_f); } } diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index af20eae3e..b242d86cf 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -90,9 +90,6 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat params_ref solver_p; solver_p.set_bool("preprocess", false); // preprocessor of smt::context is not needed. - params_ref big_aig_p; - big_aig_p.set_bool("aig_per_assertion", false); - tactic* preamble_st = mk_qfbv_preamble(m, p); tactic * st = main_p(and_then(preamble_st, // If the user sets HI_DIV0=false, then the formula may contain uninterpreted function @@ -107,10 +104,7 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat and_then(using_params(and_then(mk_simplify_tactic(m), mk_solve_eqs_tactic(m)), local_ctx_p), - if_no_proofs(cond(mk_produce_unsat_cores_probe(), - mk_aig_tactic(), - using_params(mk_aig_tactic(), - big_aig_p))))), + if_no_proofs(mk_aig_tactic()))), sat), smt))));