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