From 9eaa290b1f2786a292073711d4389574543932d8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 22 Jun 2013 11:54:58 -0700 Subject: Limiting runtime limit checks in 'pdr'. --- src/bool/rpo/rpo.c | 383 +++++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 383 insertions(+) create mode 100644 src/bool/rpo/rpo.c (limited to 'src/bool/rpo/rpo.c') diff --git a/src/bool/rpo/rpo.c b/src/bool/rpo/rpo.c new file mode 100644 index 00000000..5311e107 --- /dev/null +++ b/src/bool/rpo/rpo.c @@ -0,0 +1,383 @@ +/**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 $] + + ***********************************************************************/ + +#include + +#include "literal.h" +#include "rpo.h" +#include "bool/kit/kit.h" +#include "misc/util/abc_global.h" +#include "misc/vec/vec.h" + + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +typedef struct Rpo_Man_t_ Rpo_Man_t; + +struct Rpo_Man_t_ { + unsigned * target; + int nVars; + + Literal_t ** literals; + int nLits; + int nLitsMax; + + Rpo_LCI_Edge_t* lci; + int nLCIElems; + + int thresholdMax; + +}; + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Check if two literals are AND-grouped] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +int Rpo_CheckANDGroup(Literal_t* lit1, Literal_t* lit2, int nVars) { + unsigned* notLit1Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* notLit2Func = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* and1; + unsigned* and2; + int isZero; + + Kit_TruthNot(notLit1Func, lit1->function, nVars); + Kit_TruthNot(notLit2Func, lit2->function, nVars); + and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + Kit_TruthAnd(and1, lit1->transition, notLit2Func, nVars); + isZero = Kit_TruthIsConst0(and1, nVars); + if (isZero) { + Kit_TruthAnd(and2, lit2->transition, notLit1Func, nVars); + isZero = Kit_TruthIsConst0(and2, nVars); + } + ABC_FREE(notLit1Func); + ABC_FREE(notLit2Func); + ABC_FREE(and1); + ABC_FREE(and2); + return isZero; +} + +/**Function************************************************************* + + Synopsis [Check if two literals are AND-grouped] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +int Rpo_CheckORGroup(Literal_t* lit1, Literal_t* lit2, int nVars) { + unsigned* and1 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + unsigned* and2 = ABC_ALLOC(unsigned, Kit_TruthWordNum(nVars)); + int isZero; + Kit_TruthAnd(and1, lit1->transition, lit2->function, nVars); + isZero = Kit_TruthIsConst0(and1, nVars); + if (isZero) { + Kit_TruthAnd(and2, lit2->transition, lit1->function, nVars); + isZero = Kit_TruthIsConst0(and2, nVars); + } + ABC_FREE(and1); + ABC_FREE(and2); + return isZero; +} + +Rpo_LCI_Edge_t* Rpo_CreateEdge(Operator_t op, int i, int j, int* vertexDegree) { + Rpo_LCI_Edge_t* edge = ABC_ALLOC(Rpo_LCI_Edge_t, 1); + edge->connectionType = op; + edge->idx1 = i; + edge->idx2 = j; + edge->visited = 0; + vertexDegree[i]++; + vertexDegree[j]++; + return edge; +} + +int Rpo_computeMinEdgeCost(Rpo_LCI_Edge_t** edges, int edgeCount, int* vertexDegree) { + int minCostIndex = -1; + int minVertexIndex = -1; + unsigned int minCost = ~0; + Rpo_LCI_Edge_t* edge; + unsigned int edgeCost; + int minVertex; + int i; + for (i = 0; i < edgeCount; ++i) { + edge = edges[i]; + if (!edge->visited) { + edgeCost = vertexDegree[edge->idx1] + vertexDegree[edge->idx2]; + minVertex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2; + if (edgeCost < minCost) { + minCost = edgeCost; + minCostIndex = i; + minVertexIndex = minVertex; + } else if ((edgeCost == minCost) && minVertex < minVertexIndex) { + minCost = edgeCost; + minCostIndex = i; + minVertexIndex = minVertex; + } + } + } + return minCostIndex; +} + +void Rpo_PrintEdge(Rpo_LCI_Edge_t* edge) { + Abc_Print(-2, "Edge (%d,%d)/%d\n", edge->idx1, edge->idx2, edge->connectionType); +} + +/**Function************************************************************* + + Synopsis [Test] + + Description [] + + SideEffects [] + + SeeAlso [] + + ***********************************************************************/ +Literal_t* Rpo_Factorize(unsigned* target, int nVars, int nThreshold, int verbose) { + + int nLitCap = nVars * 2; + int nLit = 0; + int w; + Literal_t** vecLit; + Literal_t* lit; + Literal_t* result; + int thresholdCount = 0; + + if (Kit_TruthIsConst0(target, nVars)) { + return Lit_CreateLiteralConst(target, nVars, 0); + } else if (Kit_TruthIsConst1(target, nVars)) { + return Lit_CreateLiteralConst(target, nVars, 1); + } + + // if (nThreshold == -1) { + // nThreshold = nLitCap + nVars; + // } + if (verbose) { + Abc_Print(-2, "Target: "); + Lit_PrintTT(target, nVars); + Abc_Print(-2, "\n"); + } + vecLit = ABC_ALLOC(Literal_t*, nLitCap); + + for (w = nVars - 1; w >= 0; w--) { + lit = Lit_Alloc(target, nVars, w, '+'); + if (lit != NULL) { + vecLit[nLit] = lit; + nLit++; + } + lit = Lit_Alloc(target, nVars, w, '-'); + if (lit != NULL) { + vecLit[nLit] = lit; + nLit++; + } + } + if (verbose) { + Abc_Print(-2, "Allocated %d literal clusters\n", nLit); + } + + result = Rpo_Recursion(target, vecLit, nLit, nLit, nVars, &thresholdCount, nThreshold, verbose); + + //freeing the memory + for (w = 0; w < nLit; ++w) { + Lit_Free(vecLit[w]); + } + ABC_FREE(vecLit); + + return result; + +} + +Literal_t* Rpo_Recursion(unsigned* target, Literal_t** vecLit, int nLit, int nLitCount, int nVars, int* thresholdCount, int thresholdMax, int verbose) { + int i, j, k; + Literal_t* copyResult; + int* vertexDegree; + int v; + int edgeSize; + Rpo_LCI_Edge_t** edges; + int edgeCount = 0; + int isAnd; + int isOr; + Rpo_LCI_Edge_t* edge; + Literal_t* result = NULL; + int edgeIndex; + int minLitIndex; + int maxLitIndex; + Literal_t* oldLit1; + Literal_t* oldLit2; + Literal_t* newLit; + + *thresholdCount = *thresholdCount + 1; + if (*thresholdCount == thresholdMax) { + return NULL; + } + if (verbose) { + Abc_Print(-2, "Entering recursion %d\n", *thresholdCount); + } + // verify if solution is the target or not + if (nLitCount == 1) { + if (verbose) { + Abc_Print(-2, "Checking solution: "); + } + for (k = 0; k < nLit; ++k) { + if (vecLit[k] != NULL) { + if (Kit_TruthIsEqual(target, vecLit[k]->function, nVars)) { + copyResult = Lit_Copy(vecLit[k], nVars); + if (verbose) { + Abc_Print(-2, "FOUND!\n", thresholdCount); + } + thresholdCount = 0; //?? + return copyResult; + } + } + } + if (verbose) { + Abc_Print(-2, "FAILED!\n", thresholdCount); + } + return NULL; + } + + vertexDegree = ABC_ALLOC(int, nLit); + // if(verbose) { + // Abc_Print(-2,"Allocating vertexDegree...\n"); + // } + for (v = 0; v < nLit; v++) { + vertexDegree[v] = 0; + } + // building edges + edgeSize = (nLit * (nLit - 1)) / 2; + edges = ABC_ALLOC(Rpo_LCI_Edge_t*, edgeSize); + if (verbose) { + Abc_Print(-2, "Creating Edges: \n"); + } + + for (i = 0; i < nLit; ++i) { + if (vecLit[i] == NULL) { + continue; + } + for (j = i; j < nLit; ++j) { + if (vecLit[j] == NULL) { + continue; + } + isAnd = Rpo_CheckANDGroup(vecLit[i], vecLit[j], nVars); + isOr = Rpo_CheckORGroup(vecLit[i], vecLit[j], nVars); + if (isAnd) { + if (verbose) { + Abc_Print(-2, "Grouped: "); + Lit_PrintExp(vecLit[j]); + Abc_Print(-2, " AND "); + Lit_PrintExp(vecLit[i]); + Abc_Print(-2, "\n"); + } + // add edge + edge = Rpo_CreateEdge(LIT_AND, i, j, vertexDegree); + edges[edgeCount++] = edge; + } + if (isOr) { + if (verbose) { + Abc_Print(-2, "Grouped: "); + Lit_PrintExp(vecLit[j]); + Abc_Print(-2, " OR "); + Lit_PrintExp(vecLit[i]); + Abc_Print(-2, "\n"); + } + // add edge + edge = Rpo_CreateEdge(LIT_OR, i, j, vertexDegree); + edges[edgeCount++] = edge; + } + } + } + if (verbose) { + Abc_Print(-2, "%d edges created.\n", edgeCount); + } + + + //traverse the edges, grouping new Literal Clusters + do { + edgeIndex = Rpo_computeMinEdgeCost(edges, edgeCount, vertexDegree); + if (edgeIndex < 0) { + if (verbose) { + Abc_Print(-2, "There is no edges unvisited... Exiting recursion.\n"); + //exit(-1); + } + break; + //return NULL; // the graph does not have unvisited edges + } + edge = edges[edgeIndex]; + edge->visited = 1; + //Rpo_PrintEdge(edge); + minLitIndex = (edge->idx1 < edge->idx2) ? edge->idx1 : edge->idx2; + maxLitIndex = (edge->idx1 > edge->idx2) ? edge->idx1 : edge->idx2; + oldLit1 = vecLit[minLitIndex]; + oldLit2 = vecLit[maxLitIndex]; + newLit = Lit_GroupLiterals(oldLit1, oldLit2, edge->connectionType, nVars); + vecLit[minLitIndex] = newLit; + vecLit[maxLitIndex] = NULL; + + if (verbose) { + Abc_Print(-2, "New Literal Cluster found: "); + Lit_PrintExp(newLit); + Abc_Print(-2, " -> "); + Lit_PrintTT(newLit->function, nVars); + Abc_Print(-2, "\n"); + } + result = Rpo_Recursion(target, vecLit, nLit, (nLitCount - 1), nVars, thresholdCount, thresholdMax, verbose); + //independent of result, free the newLit and restore the vector of Literal Clusters + Lit_Free(newLit); + vecLit[minLitIndex] = oldLit1; + vecLit[maxLitIndex] = oldLit2; + if (*thresholdCount == thresholdMax) { + break; + } + } while (result == NULL); + //freeing memory + // if(verbose) { + // Abc_Print(-2,"Freeing vertexDegree...\n"); + // } + ABC_FREE(vertexDegree); + for (i = 0; i < edgeCount; ++i) { + //Abc_Print(-2, "%p ", edges[i]); + ABC_FREE(edges[i]); + } + ABC_FREE(edges); + return result; +} + +ABC_NAMESPACE_IMPL_END \ No newline at end of file -- cgit v1.2.3