1 /* Boolector: Satisfiability Modulo Theories (SMT) solver.
2 *
3 * Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4 *
5 * This file is part of Boolector.
6 * See COPYING for more information on using this software.
7 */
8
9 #ifndef BTORAIG_H_INCLUDED
10 #define BTORAIG_H_INCLUDED
11
12 #include "btoropt.h"
13 #include "btorsat.h"
14 #include "btortypes.h"
15 #include "utils/btorhashptr.h"
16 #include "utils/btormem.h"
17 #include "utils/btorstack.h"
18
19 #include <stdint.h>
20 #include <stdio.h>
21
22 struct BtorAIGMap;
23
24 /*------------------------------------------------------------------------*/
25
26 struct BtorAIG
27 {
28 int32_t id;
29 int32_t cnf_id;
30 uint32_t refs;
31 int32_t next; /* next AIG id for unique table */
32 uint8_t mark : 2;
33 uint8_t is_var : 1; /* is it an AIG variable or an AND? */
34 uint32_t local;
35 int32_t children[]; /* only allocated for AIG AND */
36 };
37
38 typedef struct BtorAIG BtorAIG;
39
40 BTOR_DECLARE_STACK (BtorAIGPtr, BtorAIG *);
41
42 struct BtorAIGUniqueTable
43 {
44 uint32_t size;
45 uint32_t num_elements;
46 int32_t *chains;
47 };
48
49 typedef struct BtorAIGUniqueTable BtorAIGUniqueTable;
50
51 struct BtorAIGMgr
52 {
53 Btor *btor;
54 BtorAIGUniqueTable table;
55 BtorSATMgr *smgr;
56 BtorAIGPtrStack id2aig; /* id to AIG node */
57 BtorIntStack cnfid2aig; /* cnf id to AIG id */
58
59 uint_least64_t cur_num_aigs; /* current number of ANDs */
60 uint_least64_t cur_num_aig_vars; /* current number of AIG variables */
61
62 /* statistics */
63 uint_least64_t max_num_aigs;
64 uint_least64_t max_num_aig_vars;
65 uint_least64_t num_cnf_vars;
66 uint_least64_t num_cnf_clauses;
67 uint_least64_t num_cnf_literals;
68 };
69
70 typedef struct BtorAIGMgr BtorAIGMgr;
71
72 /*------------------------------------------------------------------------*/
73
74 #define BTOR_AIG_FALSE ((BtorAIG *) (uintptr_t) 0)
75
76 #define BTOR_AIG_TRUE ((BtorAIG *) (uintptr_t) 1)
77
78 #define BTOR_INVERT_AIG(aig) ((BtorAIG *) ((uintptr_t) 1 ^ (uintptr_t) (aig)))
79
80 #define BTOR_IS_INVERTED_AIG(aig) ((uintptr_t) 1 & (uintptr_t) (aig))
81
82 #define BTOR_REAL_ADDR_AIG(aig) \
83 ((BtorAIG *) ((~(uintptr_t) 1) & (uintptr_t) (aig)))
84
85 #define BTOR_IS_REGULAR_AIG(aig) (!((uintptr_t) 1 & (uintptr_t) (aig)))
86
87 /*------------------------------------------------------------------------*/
88
89 static inline bool
btor_aig_is_const(const BtorAIG * aig)90 btor_aig_is_const (const BtorAIG *aig)
91 {
92 return aig == BTOR_AIG_TRUE || aig == BTOR_AIG_FALSE;
93 }
94
95 static inline bool
btor_aig_is_false(const BtorAIG * aig)96 btor_aig_is_false (const BtorAIG *aig)
97 {
98 return aig == BTOR_AIG_FALSE;
99 }
100
101 static inline bool
btor_aig_is_true(const BtorAIG * aig)102 btor_aig_is_true (const BtorAIG *aig)
103 {
104 return aig == BTOR_AIG_TRUE;
105 }
106
107 static inline bool
btor_aig_is_var(const BtorAIG * aig)108 btor_aig_is_var (const BtorAIG *aig)
109 {
110 if (btor_aig_is_const (aig)) return false;
111 return aig->is_var;
112 }
113
114 static inline bool
btor_aig_is_and(const BtorAIG * aig)115 btor_aig_is_and (const BtorAIG *aig)
116 {
117 if (btor_aig_is_const (aig)) return false;
118 return !aig->is_var;
119 }
120
121 static inline int32_t
btor_aig_get_id(const BtorAIG * aig)122 btor_aig_get_id (const BtorAIG *aig)
123 {
124 assert (aig);
125 assert (!btor_aig_is_const (aig));
126 return BTOR_IS_INVERTED_AIG (aig) ? -BTOR_REAL_ADDR_AIG (aig)->id : aig->id;
127 }
128
129 static inline BtorAIG *
btor_aig_get_by_id(BtorAIGMgr * amgr,int32_t id)130 btor_aig_get_by_id (BtorAIGMgr *amgr, int32_t id)
131 {
132 assert (amgr);
133
134 return id < 0 ? BTOR_INVERT_AIG (BTOR_PEEK_STACK (amgr->id2aig, -id))
135 : BTOR_PEEK_STACK (amgr->id2aig, id);
136 }
137
138 static inline int32_t
btor_aig_get_cnf_id(const BtorAIG * aig)139 btor_aig_get_cnf_id (const BtorAIG *aig)
140 {
141 if (btor_aig_is_true (aig)) return 1;
142 if (btor_aig_is_false (aig)) return -1;
143 return BTOR_IS_INVERTED_AIG (aig) ? -BTOR_REAL_ADDR_AIG (aig)->cnf_id
144 : aig->cnf_id;
145 }
146
147 static inline BtorAIG *
btor_aig_get_left_child(BtorAIGMgr * amgr,const BtorAIG * aig)148 btor_aig_get_left_child (BtorAIGMgr *amgr, const BtorAIG *aig)
149 {
150 assert (amgr);
151 assert (aig);
152 assert (!btor_aig_is_const (aig));
153 return btor_aig_get_by_id (amgr, BTOR_REAL_ADDR_AIG (aig)->children[0]);
154 }
155
156 static inline BtorAIG *
btor_aig_get_right_child(BtorAIGMgr * amgr,const BtorAIG * aig)157 btor_aig_get_right_child (BtorAIGMgr *amgr, const BtorAIG *aig)
158 {
159 assert (amgr);
160 assert (aig);
161 assert (!btor_aig_is_const (aig));
162 return btor_aig_get_by_id (amgr, BTOR_REAL_ADDR_AIG (aig)->children[1]);
163 }
164
165 /*------------------------------------------------------------------------*/
166 BtorAIGMgr *btor_aig_mgr_new (Btor *btor);
167 BtorAIGMgr *btor_aig_mgr_clone (Btor *btor, BtorAIGMgr *amgr);
168 void btor_aig_mgr_delete (BtorAIGMgr *amgr);
169
170 BtorSATMgr *btor_aig_get_sat_mgr (const BtorAIGMgr *amgr);
171
172 /* Variable representing 1 bit. */
173 BtorAIG *btor_aig_var (BtorAIGMgr *amgr);
174
175 /* Inverter. */
176 BtorAIG *btor_aig_not (BtorAIGMgr *amgr, BtorAIG *aig);
177
178 /* Logical AND. */
179 BtorAIG *btor_aig_and (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
180
181 /* Logical OR. */
182 BtorAIG *btor_aig_or (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
183
184 /* Logical EQUIVALENCE. */
185 BtorAIG *btor_aig_eq (BtorAIGMgr *amgr, BtorAIG *left, BtorAIG *right);
186
187 /* If then Else. */
188 BtorAIG *btor_aig_cond (BtorAIGMgr *amgr,
189 BtorAIG *aig_cond,
190 BtorAIG *aig_if,
191 BtorAIG *aig_else);
192
193 /* Copies AIG (increments reference counter). */
194 BtorAIG *btor_aig_copy (BtorAIGMgr *amgr, BtorAIG *aig);
195
196 /* Releases AIG (decrements reference counter).
197 * If reference counter reaches 0,
198 * then also the children are released
199 * and AIG is deleted from memory.
200 */
201 void btor_aig_release (BtorAIGMgr *amgr, BtorAIG *aig);
202
203 /* Translates AIG into SAT instance. */
204 void btor_aig_to_sat (BtorAIGMgr *amgr, BtorAIG *aig);
205
206 /* As 'btor_aig_to_sat' but also add the argument as new SAT constraint.
207 * Actually this will result in less constraints being generated.
208 */
209 void btor_aig_add_toplevel_to_sat (BtorAIGMgr *, BtorAIG *);
210
211 /* Translates AIG into SAT instance in both phases.
212 * The function guarantees that after finishing every reachable AIG
213 * has a CNF id.
214 */
215 void btor_aig_to_sat_tseitin (BtorAIGMgr *amgr, BtorAIG *aig);
216
217 /* Gets current assignment of AIG aig (in the SAT case).
218 */
219 int32_t btor_aig_get_assignment (BtorAIGMgr *amgr, BtorAIG *aig);
220
221 /* Orders AIGs (actually assume left child of an AND node is smaller
222 * than right child
223 */
224 int32_t btor_aig_compare (const BtorAIG *aig0, const BtorAIG *aig1);
225
226 /* hash AIG by id */
227 uint32_t btor_aig_hash_by_id (const BtorAIG *aig);
228
229 /* compare AIG by id */
230 int32_t btor_aig_compare_by_id (const BtorAIG *aig0, const BtorAIG *aig1);
231 int32_t btor_compare_aig_by_id_qsort_asc (const void *aig0, const void *aig1);
232 #endif
233