rpo.c

Go to the documentation of this file.

 
#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"
 
 
ABC_NAMESPACE_IMPL_START
 

 
 
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;
 
};
 


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;
}

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);
}

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, (Operator_t)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