/**CFile****************************************************************
Copyright (c) The Regents of the University of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or
royalty fees, to use, copy, modify, and distribute this software and its
documentation for any purpose, provided that the above copyright notice and
the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF
THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING,
BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS,
AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE,
SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.


  FileName    [kitIsop.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Computation kit.]

  Synopsis    [ISOP computation based on Morreale's algorithm.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - Dec 6, 2006.]

  Revision    [$Id: kitIsop.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $]

***********************************************************************/

#include "kit.h"

////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

// ISOP computation fails if intermediate memory usage exceed this limit
#define KIT_ISOP_MEM_LIMIT  (1<<16)

// static procedures to compute ISOP
static unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );
static unsigned   Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Computes ISOP from TT.]

  Description [Returns the cover in vMemory. Uses the rest of array in vMemory
  as an intermediate memory storage. Returns the cover with -1 cubes, if the
  the computation exceeded the memory limit (KIT_ISOP_MEM_LIMIT words of
  intermediate data).]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth )
{
    Kit_Sop_t cRes, * pcRes = &cRes;
    Kit_Sop_t cRes2, * pcRes2 = &cRes2;
    unsigned * pResult;
    int RetValue = 0;
    assert( nVars >= 0 && nVars < 16 );
    // if nVars < 5, make sure it does not depend on those vars
//    for ( i = nVars; i < 5; i++ )
//        assert( !Kit_TruthVarInSupport(puTruth, 5, i) );
    // prepare memory manager
    Vec_IntClear( vMemory );
    Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT );
    // compute ISOP for the direct polarity
    pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes, vMemory );
    if ( pcRes->nCubes == -1 )
    {
        vMemory->nSize = -1;
        return -1;
    }
    assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
    if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) )
    {
        vMemory->pArray[0] = 0;
        Vec_IntShrink( vMemory, pcRes->nCubes );
        return 0;
    }
    if ( fTryBoth )
    {
        // compute ISOP for the complemented polarity
        Kit_TruthNot( puTruth, puTruth, nVars );
        pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory );
        if ( pcRes2->nCubes >= 0 )
        {
            assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) );
            if ( pcRes->nCubes > pcRes2->nCubes )
            {
                RetValue = 1;
                pcRes = pcRes2;
            }
        }
        Kit_TruthNot( puTruth, puTruth, nVars );
    }
//    printf( "%d ", vMemory->nSize );
    // move the cover representation to the beginning of the memory buffer
    memmove( vMemory->pArray, pcRes->pCubes, pcRes->nCubes * sizeof(unsigned) );
    Vec_IntShrink( vMemory, pcRes->nCubes );
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Computes ISOP 6 variables or more.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
{
    Kit_Sop_t cRes0, cRes1, cRes2;
    Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
    unsigned * puRes0, * puRes1, * puRes2;
    unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1;
    int i, k, Var, nWords, nWordsAll;
//    assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) );
    // allocate room for the resulting truth table
    nWordsAll = Kit_TruthWordNum( nVars );
    pTemp = Vec_IntFetch( vStore, nWordsAll );
    if ( pTemp == NULL )
    {
        pcRes->nCubes = -1;
        return NULL;
    }
    // check for constants
    if ( Kit_TruthIsConst0( puOn, nVars ) )
    {
        pcRes->nCubes = 0;
        pcRes->pCubes = NULL;
        Kit_TruthClear( pTemp, nVars );
        return pTemp;
    }
    if ( Kit_TruthIsConst1( puOnDc, nVars ) )
    {
        pcRes->nCubes = 1;
        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
        if ( pcRes->pCubes == NULL )
        {
            pcRes->nCubes = -1;
            return NULL;
        }
        pcRes->pCubes[0] = 0;
        Kit_TruthFill( pTemp, nVars );
        return pTemp;
    }
    assert( nVars > 0 );
    // find the topmost var
    for ( Var = nVars-1; Var >= 0; Var-- )
        if ( Kit_TruthVarInSupport( puOn, nVars, Var ) || 
             Kit_TruthVarInSupport( puOnDc, nVars, Var ) )
             break;
    assert( Var >= 0 );
    // consider a simple case when one-word computation can be used
    if ( Var < 5 )
    {
        unsigned uRes = Kit_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes, vStore );
        for ( i = 0; i < nWordsAll; i++ )
            pTemp[i] = uRes;
        return pTemp;
    }
    assert( Var >= 5 );
    nWords = Kit_TruthWordNum( Var );
    // cofactor
    puOn0   = puOn;    puOn1   = puOn + nWords;
    puOnDc0 = puOnDc;  puOnDc1 = puOnDc + nWords;
    pTemp0  = pTemp;   pTemp1  = pTemp + nWords;
    // solve for cofactors
    Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var );
    puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore );
    if ( pcRes0->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return NULL;
    }
    Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var );
    puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore );
    if ( pcRes1->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return NULL;
    }
    Kit_TruthSharp( pTemp0, puOn0, puRes0, Var );
    Kit_TruthSharp( pTemp1, puOn1, puRes1, Var );
    Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var );
    Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var );
    puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore );
    if ( pcRes2->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return NULL;
    }
    // create the resulting cover
    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
    if ( pcRes->pCubes == NULL )
    {
        pcRes->nCubes = -1;
        return NULL;
    }
    k = 0;
    for ( i = 0; i < pcRes0->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
    for ( i = 0; i < pcRes1->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
    for ( i = 0; i < pcRes2->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes2->pCubes[i];
    assert( k == pcRes->nCubes );
    // create the resulting truth table
    Kit_TruthOr( pTemp0, puRes0, puRes2, Var );
    Kit_TruthOr( pTemp1, puRes1, puRes2, Var );
    // copy the table if needed
    nWords <<= 1;
    for ( i = 1; i < nWordsAll/nWords; i++ )
        for ( k = 0; k < nWords; k++ )
            pTemp[i*nWords + k] = pTemp[k];
    // verify in the end
//    assert( Kit_TruthIsImply( puOn, pTemp, nVars ) );
//    assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) );
    return pTemp;
}

/**Function*************************************************************

  Synopsis    [Computes ISOP for 5 variables or less.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t * pcRes, Vec_Int_t * vStore )
{
    unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 };
    Kit_Sop_t cRes0, cRes1, cRes2;
    Kit_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2;
    unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
    int i, k, Var;
    assert( nVars <= 5 );
    assert( (uOn & ~uOnDc) == 0 );
    if ( uOn == 0 )
    {
        pcRes->nCubes = 0;
        pcRes->pCubes = NULL;
        return 0;
    }
    if ( uOnDc == 0xFFFFFFFF )
    {
        pcRes->nCubes = 1;
        pcRes->pCubes = Vec_IntFetch( vStore, 1 );
        if ( pcRes->pCubes == NULL )
        {
            pcRes->nCubes = -1;
            return 0;
        }
        pcRes->pCubes[0] = 0;
        return 0xFFFFFFFF;
    }
    assert( nVars > 0 );
    // find the topmost var
    for ( Var = nVars-1; Var >= 0; Var-- )
        if ( Kit_TruthVarInSupport( &uOn, 5, Var ) || 
             Kit_TruthVarInSupport( &uOnDc, 5, Var ) )
             break;
    assert( Var >= 0 );
    // cofactor
    uOn0   = uOn1   = uOn;
    uOnDc0 = uOnDc1 = uOnDc;
    Kit_TruthCofactor0( &uOn0, Var + 1, Var );
    Kit_TruthCofactor1( &uOn1, Var + 1, Var );
    Kit_TruthCofactor0( &uOnDc0, Var + 1, Var );
    Kit_TruthCofactor1( &uOnDc1, Var + 1, Var );
    // solve for cofactors
    uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore );
    if ( pcRes0->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return 0;
    }
    uRes1 = Kit_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1, vStore );
    if ( pcRes1->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return 0;
    }
    uRes2 = Kit_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2, vStore );
    if ( pcRes2->nCubes == -1 )
    {
        pcRes->nCubes = -1;
        return 0;
    }
    // create the resulting cover
    pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes;
    pcRes->pCubes = Vec_IntFetch( vStore, pcRes->nCubes );
    if ( pcRes->pCubes == NULL )
    {
        pcRes->nCubes = -1;
        return 0;
    }
    k = 0;
    for ( i = 0; i < pcRes0->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+0));
    for ( i = 0; i < pcRes1->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+1));
    for ( i = 0; i < pcRes2->nCubes; i++ )
        pcRes->pCubes[k++] = pcRes2->pCubes[i];
    assert( k == pcRes->nCubes );
    // derive the final truth table
    uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]);
//    assert( (uOn & ~uRes2) == 0 );
//    assert( (uRes2 & ~uOnDc) == 0 );
    return uRes2;
}


////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////