abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Data Structures | Typedefs | Functions
rpo.c File Reference
#include <stdio.h>
#include "literal.h"
#include "rpo.h"
#include "bool/kit/kit.h"
#include "misc/util/abc_global.h"
#include "misc/vec/vec.h"

Go to the source code of this file.

Data Structures

struct  Rpo_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Rpo_Man_t_ 		Rpo_Man_t
 DECLARATIONS ///. More...
 

Functions

int Rpo_CheckANDGroup (Literal_t *lit1, Literal_t *lit2, int nVars)
 FUNCTION DEFINITIONS ///. More...
 
int Rpo_CheckORGroup (Literal_t *lit1, Literal_t *lit2, int nVars)
 
Rpo_LCI_Edge_t * Rpo_CreateEdge (Operator_t op, int i, int j, int *vertexDegree)
 
int Rpo_computeMinEdgeCost (Rpo_LCI_Edge_t **edges, int edgeCount, int *vertexDegree)
 
void Rpo_PrintEdge (Rpo_LCI_Edge_t *edge)
 
Literal_t * Rpo_Factorize (unsigned *target, int nVars, int nThreshold, int verbose)
 
Literal_t * Rpo_Recursion (unsigned *target, Literal_t **vecLit, int nLit, int nLitCount, int nVars, int *thresholdCount, int thresholdMax, int verbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Rpo_Man_t_ Rpo_Man_t

DECLARATIONS ///.

CFile****************************************************************

FileName [rpo.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [RPO]

Synopsis [Performs read polarity once factorization.]

Author [Mayler G. A. Martins / Vinicius Callegaro]

Affiliation [UFRGS]

Date [Ver. 1.0. Started - May 08, 2013.]

Revision [

Id:
rpo.c,v 1.00 2013/05/08 00:00:00 mgamartins Exp

]

Definition at line 38 of file rpo.c.

Function Documentation

int Rpo_CheckANDGroup ( Literal_t *  lit1,
Literal_t *  lit2,
int  nVars 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Check if two literals are AND-grouped]

Description []

SideEffects []

SeeAlso []

Definition at line 71 of file rpo.c.

71  {
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 }
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_TruthAnd
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Kit_TruthNot
static void Kit_TruthNot(unsigned *pOut, unsigned *pIn, int nVars)
Definition: kit.h:373
Literal_t_::function
unsigned * function
Definition: literal.h:54
Literal_t_::transition
unsigned * transition
Definition: literal.h:53
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
int Rpo_CheckORGroup ( Literal_t *  lit1,
Literal_t *  lit2,
int  nVars 
)

Function*************************************************************

Synopsis [Check if two literals are AND-grouped]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file rpo.c.

106  {
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 }
Kit_TruthWordNum
static int Kit_TruthWordNum(int nVars)
Definition: kit.h:224
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Kit_TruthAnd
static void Kit_TruthAnd(unsigned *pOut, unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:379
Literal_t_::function
unsigned * function
Definition: literal.h:54
Literal_t_::transition
unsigned * transition
Definition: literal.h:53
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
int Rpo_computeMinEdgeCost ( Rpo_LCI_Edge_t **  edges,
int  edgeCount,
int *  vertexDegree 
)

Definition at line 132 of file rpo.c.

132  {
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 }
Rpo_LCI_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
INCLUDES ///.
Definition: rpo.h:36
if
if(last==0)
Definition: sparse_int.h:34
Rpo_LCI_Edge_t* Rpo_CreateEdge ( Operator_t  op,
int  i,
int  j,
int *  vertexDegree 
)

Definition at line 121 of file rpo.c.

121  {
122  Rpo_LCI_Edge_t* edge = ABC_ALLOC(Rpo_LCI_Edge_t, 1);
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 }
Rpo_LCI_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
INCLUDES ///.
Definition: rpo.h:36
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Literal_t* Rpo_Factorize ( unsigned *  target,
int  nVars,
int  nThreshold,
int  verbose 
)

Function*************************************************************

Synopsis [Test]

Description []

SideEffects []

SeeAlso []

Definition at line 174 of file rpo.c.

174  {
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 }
Lit_Alloc
static Literal_t * Lit_Alloc(unsigned *pTruth, int nVars, int varIdx, char pol)
Definition: literal.h:131
Rpo_Recursion
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
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsConst0
static int Kit_TruthIsConst0(unsigned *pIn, int nVars)
Definition: kit.h:315
Lit_Free
static void Lit_Free(Literal_t *lit)
Definition: literal.h:283
lit
int lit
Definition: satVec.h:130
Literal_t_
Definition: literal.h:52
Kit_TruthIsConst1
static int Kit_TruthIsConst1(unsigned *pIn, int nVars)
Definition: kit.h:323
Lit_CreateLiteralConst
static Literal_t * Lit_CreateLiteralConst(unsigned *pTruth, int nVars, int constant)
Definition: literal.h:237
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Lit_PrintTT
static void Lit_PrintTT(unsigned *tt, int nVars)
Definition: literal.h:260
result
static int result
Definition: cuddGenetic.c:125
void Rpo_PrintEdge ( Rpo_LCI_Edge_t *  edge)

Definition at line 159 of file rpo.c.

159  {
160  Abc_Print(-2, "Edge (%d,%d)/%d\n", edge->idx1, edge->idx2, edge->connectionType);
161 }
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Literal_t* Rpo_Recursion ( unsigned *  target,
Literal_t **  vecLit,
int  nLit,
int  nLitCount,
int  nVars,
int *  thresholdCount,
int  thresholdMax,
int  verbose 
)

Definition at line 228 of file rpo.c.

228  {
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 }
Rpo_LCI_Edge_t
typedefABC_NAMESPACE_HEADER_START struct Rpo_LCI_Edge_t_ Rpo_LCI_Edge_t
INCLUDES ///.
Definition: rpo.h:36
LIT_OR
Definition: literal.h:45
Rpo_CheckORGroup
int Rpo_CheckORGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
Definition: rpo.c:106
Lit_Copy
static Literal_t * Lit_Copy(Literal_t *lit, int nVars)
Definition: literal.h:249
Rpo_Recursion
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
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Kit_TruthIsEqual
static int Kit_TruthIsEqual(unsigned *pIn0, unsigned *pIn1, int nVars)
Definition: kit.h:274
Lit_PrintExp
static void Lit_PrintExp(Literal_t *lit)
Definition: literal.h:267
Lit_Free
static void Lit_Free(Literal_t *lit)
Definition: literal.h:283
Literal_t_
Definition: literal.h:52
Lit_GroupLiterals
static Literal_t * Lit_GroupLiterals(Literal_t *lit1, Literal_t *lit2, Operator_t op, int nVars)
Definition: literal.h:178
Rpo_computeMinEdgeCost
int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t **edges, int edgeCount, int *vertexDegree)
Definition: rpo.c:132
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Literal_t_::function
unsigned * function
Definition: literal.h:54
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Lit_PrintTT
static void Lit_PrintTT(unsigned *tt, int nVars)
Definition: literal.h:260
result
static int result
Definition: cuddGenetic.c:125
Operator_t
Operator_t
INCLUDES ///.
Definition: literal.h:42
Rpo_CheckANDGroup
int Rpo_CheckANDGroup(Literal_t *lit1, Literal_t *lit2, int nVars)
FUNCTION DEFINITIONS ///.
Definition: rpo.c:71
Rpo_CreateEdge
Rpo_LCI_Edge_t * Rpo_CreateEdge(Operator_t op, int i, int j, int *vertexDegree)
Definition: rpo.c:121