/**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 <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


////////////////////////////////////////////////////////////////////////
///                        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, (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