1 /*++ 2 Copyright (c) 2011 Microsoft Corporation 3 4 Module Name: 5 6 aig_tactic.cpp 7 8 Abstract: 9 10 Tactic for minimizing circuits using AIGs. 11 12 Author: 13 14 Leonardo (leonardo) 2011-10-24 15 16 Notes: 17 18 --*/ 19 #include "tactic/tactical.h" 20 #include "tactic/aig/aig.h" 21 22 class aig_manager; 23 24 class aig_tactic : public tactic { 25 unsigned long long m_max_memory; 26 bool m_aig_gate_encoding; 27 bool m_aig_per_assertion; 28 aig_manager * m_aig_manager; 29 30 struct mk_aig_manager { 31 aig_tactic & m_owner; 32 33 mk_aig_manager(aig_tactic & o, ast_manager & m):m_owner(o) { 34 aig_manager * mng = alloc(aig_manager, m, o.m_max_memory, o.m_aig_gate_encoding); 35 m_owner.m_aig_manager = mng; 36 } 37 38 ~mk_aig_manager() { 39 dealloc(m_owner.m_aig_manager); 40 m_owner.m_aig_manager = nullptr; 41 } 42 }; 43 44 public: 45 aig_tactic(params_ref const & p = params_ref()):m_aig_manager(nullptr) { 46 updt_params(p); 47 } 48 49 tactic * translate(ast_manager & m) override { 50 aig_tactic * t = alloc(aig_tactic); 51 t->m_max_memory = m_max_memory; 52 t->m_aig_gate_encoding = m_aig_gate_encoding; 53 t->m_aig_per_assertion = m_aig_per_assertion; 54 return t; 55 } 56 57 void updt_params(params_ref const & p) override { 58 m_max_memory = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX)); 59 m_aig_gate_encoding = p.get_bool("aig_default_gate_encoding", true); 60 m_aig_per_assertion = p.get_bool("aig_per_assertion", true); 61 } 62 63 void collect_param_descrs(param_descrs & r) override { 64 insert_max_memory(r); 65 r.insert("aig_per_assertion", CPK_BOOL, "(default: true) process one assertion at a time."); 66 } 67 68 void operator()(goal_ref const & g) { 69 70 mk_aig_manager mk(*this, g->m()); 71 if (m_aig_per_assertion) { 72 for (unsigned i = 0; i < g->size(); i++) { 73 aig_ref r = m_aig_manager->mk_aig(g->form(i)); 74 m_aig_manager->max_sharing(r); 75 expr_ref new_f(g->m()); 76 m_aig_manager->to_formula(r, new_f); 77 expr_dependency * ed = g->dep(i); 78 g->update(i, new_f, nullptr, ed); 79 } 80 } 81 else { 82 fail_if_unsat_core_generation("aig", g); 83 aig_ref r = m_aig_manager->mk_aig(*(g.get())); 84 g->reset(); // save memory 85 m_aig_manager->max_sharing(r); 86 m_aig_manager->to_formula(r, *(g.get())); 87 } 88 } 89 90 void operator()(goal_ref const & g, goal_ref_buffer & result) override { 91 fail_if_proof_generation("aig", g); 92 tactic_report report("aig", *g); 93 operator()(g); 94 g->inc_depth(); 95 result.push_back(g.get()); 96 } 97 98 void cleanup() override {} 99 100 }; 101 102 tactic * mk_aig_tactic(params_ref const & p) { 103 return clean(alloc(aig_tactic, p)); 104 } 105