1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     aig.h
7 
8 Abstract:
9 
10     And-inverted graphs
11 
12 Author:
13 
14     Leonardo (leonardo) 2011-05-13
15 
16 Notes:
17 
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "tactic/tactic_exception.h"
23 
24 class goal;
25 class aig_lit;
26 class aig_manager;
27 
28 class aig_exception : public tactic_exception {
29 public:
aig_exception(char const * msg)30     aig_exception(char const * msg):tactic_exception(msg) {}
31 };
32 
33 class aig_ref {
34     friend class aig_lit;
35     friend class aig_manager;
36     aig_manager * m_manager;
37     void *        m_ref;
38     aig_ref(aig_manager & m, aig_lit const & l);
39 public:
40     aig_ref();
41     ~aig_ref();
42     aig_ref & operator=(aig_ref const & r);
43     bool operator==(aig_ref const & r) const { return m_ref == r.m_ref; }
44     bool operator!=(aig_ref const & r) const { return m_ref != r.m_ref; }
45 };
46 
47 class aig_manager {
48     struct imp;
49     imp *  m_imp;
50     friend class aig_ref;
51 public:
52     // If default_gate_encoding == true, then
53     // ite(a, b, c) is encoded as (NOT a OR b) AND (a OR c)
54     // iff(a, b)    is encoded as (NOT a OR b) AND (a OR NOT b)
55     //
56     // If default_gate_encoding == false, then
57     // ite(a, b, c) is encoded as (a AND b) OR (NOT a AND c)
58     // iff(a, b)    is encoded as (a AND b) OR (NOT a AND NOT b)
59     aig_manager(ast_manager & m, unsigned long long max_memory = UINT64_MAX, bool default_gate_encoding = true);
60     ~aig_manager();
61     void set_max_memory(unsigned long long max);
62     aig_ref mk_aig(expr * n);
63     aig_ref mk_aig(goal const & g);
64     aig_ref mk_not(aig_ref const & r);
65     aig_ref mk_and(aig_ref const & r1, aig_ref const & r2);
66     aig_ref mk_or(aig_ref const & r1, aig_ref const & r2);
67     aig_ref mk_iff(aig_ref const & r1, aig_ref const & r2);
68     aig_ref mk_ite(aig_ref const & r1, aig_ref const & r2, aig_ref const & r3);
69     void max_sharing(aig_ref & r);
70     void to_formula(aig_ref const & r, expr_ref & result);
71     void to_formula(aig_ref const & r, goal & result);
72     void display(std::ostream & out, aig_ref const & r) const;
73     void display_smt2(std::ostream & out, aig_ref const & r) const;
74     unsigned get_num_aigs() const;
75 };
76 
77