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