abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
rpo.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [rpo.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [RPO]
8 
9  Synopsis [Performs read polarity once factorization.]
10 
11  Author [Mayler G. A. Martins / Vinicius Callegaro]
12 
13  Affiliation [UFRGS]
14 
15  Date [Ver. 1.0. Started - May 08, 2013.]
16 
17  Revision [$Id: rpo.c,v 1.00 2013/05/08 00:00:00 mgamartins Exp $]
18 
19  ***********************************************************************/
20 
21 #include <stdio.h>
22 
23 #include "literal.h"
24 #include "rpo.h"
25 #include "bool/kit/kit.h"
26 #include "misc/util/abc_global.h"
27 #include "misc/vec/vec.h"
28 
29 
31 
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// DECLARATIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 
38 typedef struct Rpo_Man_t_ Rpo_Man_t;
39 
40 struct Rpo_Man_t_ {
41  unsigned * target;
42  int nVars;
43 
45  int nLits;
46  int nLitsMax;
47 
49  int nLCIElems;
50 
52 
53 };
54 
55 
56 ////////////////////////////////////////////////////////////////////////
57 /// FUNCTION DEFINITIONS ///
58 ////////////////////////////////////////////////////////////////////////
59 
60 /**Function*************************************************************
61 
62  Synopsis [Check if two literals are AND-grouped]
63 
64  Description []
65 
66  SideEffects []
67 
68  SeeAlso []
69 
70  ***********************************************************************/
71 int Rpo_CheckANDGroup(Literal_t* lit1, Literal_t* lit2, int nVars) {
72  unsigned* notLit1Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
73  unsigned* notLit2Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
74  unsigned* and1;
75  unsigned* and2;
76  int isZero;
77 
78  Kit_TruthNot(notLit1Func, lit1->function, nVars);
79  Kit_TruthNot(notLit2Func, lit2->function, nVars);
80  and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
81  and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
82  Kit_TruthAnd(and1, lit1->transition, notLit2Func, nVars);
83  isZero = Kit_TruthIsConst0(and1, nVars);
84  if (isZero) {
85  Kit_TruthAnd(and2, lit2->transition, notLit1Func, nVars);
86  isZero = Kit_TruthIsConst0(and2, nVars);
87  }
88  ABC_FREE(notLit1Func);
89  ABC_FREE(notLit2Func);
90  ABC_FREE(and1);
91  ABC_FREE(and2);
92  return isZero;
93 }
94 
95 /**Function*************************************************************
96 
97  Synopsis [Check if two literals are AND-grouped]
98 
99  Description []
100 
101  SideEffects []
102 
103  SeeAlso []
104 
105  ***********************************************************************/
106 int Rpo_CheckORGroup(Literal_t* lit1, Literal_t* lit2, int nVars) {
107  unsigned* and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
108  unsigned* and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars));
109  int isZero;
110  Kit_TruthAnd(and1, lit1->transition, lit2->function, nVars);
111  isZero = Kit_TruthIsConst0(and1, nVars);
112  if (isZero) {
113  Kit_TruthAnd(and2, lit2->transition, lit1->function, nVars);
114  isZero = Kit_TruthIsConst0(and2, nVars);
115  }
116  ABC_FREE(and1);
117  ABC_FREE(and2);
118  return isZero;
119 }
120 
121 Rpo_LCI_Edge_t* Rpo_CreateEdge(Operator_t op, int i, int j, int* vertexDegree) {
123  edge->connectionType = op;
124  edge->idx1 = i;
125  edge->idx2 = j;
126  edge->visited = 0;
127  vertexDegree[i]++;
128  vertexDegree[j]++;
129  return edge;
130 }
131 
132 int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t** edges, int edgeCount, int* vertexDegree) {
133  int minCostIndex = -1;
134  int minVertexIndex = -1;
135  unsigned int minCost = ~0;
136  Rpo_LCI_Edge_t* edge;
137  unsigned int edgeCost;
138  int minVertex;
139  int i;
140  for (i = 0; i < edgeCount; ++i) {
141  edge = edges[i];
142  if (!edge->visited) {
143  edgeCost = vertexDegree[edge->idx1] + vertexDegree[edge->idx2];
144  minVertex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2;
145  if (edgeCost < minCost) {
146  minCost = edgeCost;
147  minCostIndex = i;
148  minVertexIndex = minVertex;
149  } else if ((edgeCost == minCost) && minVertex < minVertexIndex) {
150  minCost = edgeCost;
151  minCostIndex = i;
152  minVertexIndex = minVertex;
153  }
154  }
155  }
156  return minCostIndex;
157 }
158 
160  Abc_Print(-2, "Edge (%d,%d)/%d\n", edge->idx1, edge->idx2, edge->connectionType);
161 }
162 
163 /**Function*************************************************************
164 
165  Synopsis [Test]
166 
167  Description []
168 
169  SideEffects []
170 
171  SeeAlso []
172 
173  ***********************************************************************/
174 Literal_t* Rpo_Factorize(unsigned* target, int nVars, int nThreshold, int verbose) {
175 
176  int nLitCap = nVars * 2;
177  int nLit = 0;
178  int w;
179  Literal_t** vecLit;
180  Literal_t* lit;
181  Literal_t* result;
182  int thresholdCount = 0;
183 
184  if (Kit_TruthIsConst0(target, nVars)) {
185  return Lit_CreateLiteralConst(target, nVars, 0);
186  } else if (Kit_TruthIsConst1(target, nVars)) {
187  return Lit_CreateLiteralConst(target, nVars, 1);
188  }
189 
190  // if (nThreshold == -1) {
191  // nThreshold = nLitCap + nVars;
192  // }
193  if (verbose) {
194  Abc_Print(-2, "Target: ");
195  Lit_PrintTT(target, nVars);
196  Abc_Print(-2, "\n");
197  }
198  vecLit = ABC_ALLOC(Literal_t*, nLitCap);
199 
200  for (w = nVars - 1; w >= 0; w--) {
201  lit = Lit_Alloc(target, nVars, w, '+');
202  if (lit != NULL) {
203  vecLit[nLit] = lit;
204  nLit++;
205  }
206  lit = Lit_Alloc(target, nVars, w, '-');
207  if (lit != NULL) {
208  vecLit[nLit] = lit;
209  nLit++;
210  }
211  }
212  if (verbose) {
213  Abc_Print(-2, "Allocated %d literal clusters\n", nLit);
214  }
215 
216  result = Rpo_Recursion(target, vecLit, nLit, nLit, nVars, &thresholdCount, nThreshold, verbose);
217 
218  //freeing the memory
219  for (w = 0; w < nLit; ++w) {
220  Lit_Free(vecLit[w]);
221  }
222  ABC_FREE(vecLit);
223 
224  return result;
225 
226 }
227 
228 Literal_t* Rpo_Recursion(unsigned* target, Literal_t** vecLit, int nLit, int nLitCount, int nVars, int* thresholdCount, int thresholdMax, int verbose) {
229  int i, j, k;
230  Literal_t* copyResult;
231  int* vertexDegree;
232  int v;
233  int edgeSize;
234  Rpo_LCI_Edge_t** edges;
235  int edgeCount = 0;
236  int isAnd;
237  int isOr;
238  Rpo_LCI_Edge_t* edge;
239  Literal_t* result = NULL;
240  int edgeIndex;
241  int minLitIndex;
242  int maxLitIndex;
243  Literal_t* oldLit1;
244  Literal_t* oldLit2;
245  Literal_t* newLit;
246 
247  *thresholdCount = *thresholdCount + 1;
248  if (*thresholdCount == thresholdMax) {
249  return NULL;
250  }
251  if (verbose) {
252  Abc_Print(-2, "Entering recursion %d\n", *thresholdCount);
253  }
254  // verify if solution is the target or not
255  if (nLitCount == 1) {
256  if (verbose) {
257  Abc_Print(-2, "Checking solution: ");
258  }
259  for (k = 0; k < nLit; ++k) {
260  if (vecLit[k] != NULL) {
261  if (Kit_TruthIsEqual(target, vecLit[k]->function, nVars)) {
262  copyResult = Lit_Copy(vecLit[k], nVars);
263  if (verbose) {
264  Abc_Print(-2, "FOUND!\n", thresholdCount);
265  }
266  thresholdCount = 0; //??
267  return copyResult;
268  }
269  }
270  }
271  if (verbose) {
272  Abc_Print(-2, "FAILED!\n", thresholdCount);
273  }
274  return NULL;
275  }
276 
277  vertexDegree = ABC_ALLOC(int, nLit);
278  // if(verbose) {
279  // Abc_Print(-2,"Allocating vertexDegree...\n");
280  // }
281  for (v = 0; v < nLit; v++) {
282  vertexDegree[v] = 0;
283  }
284  // building edges
285  edgeSize = (nLit * (nLit - 1)) / 2;
286  edges = ABC_ALLOC(Rpo_LCI_Edge_t*, edgeSize);
287  if (verbose) {
288  Abc_Print(-2, "Creating Edges: \n");
289  }
290 
291  for (i = 0; i < nLit; ++i) {
292  if (vecLit[i] == NULL) {
293  continue;
294  }
295  for (j = i; j < nLit; ++j) {
296  if (vecLit[j] == NULL) {
297  continue;
298  }
299  isAnd = Rpo_CheckANDGroup(vecLit[i], vecLit[j], nVars);
300  isOr = Rpo_CheckORGroup(vecLit[i], vecLit[j], nVars);
301  if (isAnd) {
302  if (verbose) {
303  Abc_Print(-2, "Grouped: ");
304  Lit_PrintExp(vecLit[j]);
305  Abc_Print(-2, " AND ");
306  Lit_PrintExp(vecLit[i]);
307  Abc_Print(-2, "\n");
308  }
309  // add edge
310  edge = Rpo_CreateEdge(LIT_AND, i, j, vertexDegree);
311  edges[edgeCount++] = edge;
312  }
313  if (isOr) {
314  if (verbose) {
315  Abc_Print(-2, "Grouped: ");
316  Lit_PrintExp(vecLit[j]);
317  Abc_Print(-2, " OR ");
318  Lit_PrintExp(vecLit[i]);
319  Abc_Print(-2, "\n");
320  }
321  // add edge
322  edge = Rpo_CreateEdge(LIT_OR, i, j, vertexDegree);
323  edges[edgeCount++] = edge;
324  }
325  }
326  }
327  if (verbose) {
328  Abc_Print(-2, "%d edges created.\n", edgeCount);
329  }
330 
331 
332  //traverse the edges, grouping new Literal Clusters
333  do {
334  edgeIndex = Rpo_computeMinEdgeCost(edges, edgeCount, vertexDegree);
335  if (edgeIndex < 0) {
336  if (verbose) {
337  Abc_Print(-2, "There is no edges unvisited... Exiting recursion.\n");
338  //exit(-1);
339  }
340  break;
341  //return NULL; // the graph does not have unvisited edges
342  }
343  edge = edges[edgeIndex];
344  edge->visited = 1;
345  //Rpo_PrintEdge(edge);
346  minLitIndex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2;
347  maxLitIndex = (edge->idx1 > edge->idx2) ? edge->idx1 : edge->idx2;
348  oldLit1 = vecLit[minLitIndex];
349  oldLit2 = vecLit[maxLitIndex];
350  newLit = Lit_GroupLiterals(oldLit1, oldLit2, (Operator_t)edge->connectionType, nVars);
351  vecLit[minLitIndex] = newLit;
352  vecLit[maxLitIndex] = NULL;
353 
354  if (verbose) {
355  Abc_Print(-2, "New Literal Cluster found: ");
356  Lit_PrintExp(newLit);
357  Abc_Print(-2, " -> ");
358  Lit_PrintTT(newLit->function, nVars);
359  Abc_Print(-2, "\n");
360  }
361  result = Rpo_Recursion(target, vecLit, nLit, (nLitCount - 1), nVars, thresholdCount, thresholdMax, verbose);
362  //independent of result, free the newLit and restore the vector of Literal Clusters
363  Lit_Free(newLit);
364  vecLit[minLitIndex] = oldLit1;
365  vecLit[maxLitIndex] = oldLit2;
366  if (*thresholdCount == thresholdMax) {
367  break;
368  }
369  } while (result == NULL);
370  //freeing memory
371  // if(verbose) {
372  // Abc_Print(-2,"Freeing vertexDegree...\n");
373  // }
374  ABC_FREE(vertexDegree);
375  for (i = 0; i < edgeCount; ++i) {
376  //Abc_Print(-2, "%p ", edges[i]);
377  ABC_FREE(edges[i]);
378  }
379  ABC_FREE(edges);
380  return result;
381 }
382 
int nLitsMax
Definition: rpo.c:46
typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
INCLUDES ///.
Definition: rpo.h:36
Definition: literal.h:45
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
int nVars
Definition: rpo.c:42
int Rpo_CheckORGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
Definition: rpo.c:106
static Literal_t * Lit_Alloc(unsigned *pTruth, int nVars, int varIdx, char pol)
Definition: literal.h:131
static Literal_t * Lit_Copy(Literal_t *lit, int nVars)
Definition: literal.h:249
Literal_t * Rpo_Recursion(unsigned *target, Literal_t **vecLit, int nLit, int nLitCount, int nVars, int *thresholdCount, int thresholdMax, int verbose)
Definition: rpo.c:228
Literal_t ** literals
Definition: rpo.c:44
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
unsigned * target
Definition: rpo.c:41
static void Lit_PrintExp(Literal_t *lit)
Definition: literal.h:267
static void Lit_Free(Literal_t *lit)
Definition: literal.h:283
int lit
Definition: satVec.h:130
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Rpo_LCI_Edge_t * lci
Definition: rpo.c:48
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Literal_t * Rpo_Factorize(unsigned *target, int nVars, int nThreshold, int verbose)
Definition: rpo.c:174
static Literal_t * Lit_CreateLiteralConst(unsigned *pTruth, int nVars, int constant)
Definition: literal.h:237
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void Rpo_PrintEdge(Rpo_LCI_Edge_t *edge)
Definition: rpo.c:159
static Literal_t * Lit_GroupLiterals(Literal_t *lit1, Literal_t *lit2, Operator_t op, int nVars)
Definition: literal.h:178
if(last==0)
Definition: sparse_int.h:34
typedefABC_NAMESPACE_IMPL_START struct Rpo_Man_t_ Rpo_Man_t
DECLARATIONS ///.
Definition: rpo.c:38
int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t **edges, int edgeCount, int *vertexDegree)
Definition: rpo.c:132
int nLits
Definition: rpo.c:45
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
unsigned * function
Definition: literal.h:54
int thresholdMax
Definition: rpo.c:51
Definition: rpo.c:40
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
unsigned * transition
Definition: literal.h:53
#define ABC_FREE(obj)
Definition: abc_global.h:232
static void Lit_PrintTT(unsigned *tt, int nVars)
Definition: literal.h:260
int nLCIElems
Definition: rpo.c:49
static int result
Definition: cuddGenetic.c:125
Operator_t
INCLUDES ///.
Definition: literal.h:42
int Rpo_CheckANDGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
FUNCTION DEFINITIONS ///.
Definition: rpo.c:71
Rpo_LCI_Edge_t * Rpo_CreateEdge(Operator_t op, int i, int j, int *vertexDegree)
Definition: rpo.c:121