utilIsop.c File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "misc/util/utilTruth.h"

Go to the source code of this file.

Macros
#define	ABC_ISOP_MAX_VAR   16
	DECLARATIONS ///. More...
#define	ABC_ISOP_MAX_WORD   (ABC_ISOP_MAX_VAR > 6 ? (1 << (ABC_ISOP_MAX_VAR-6)) : 1)
#define	ABC_ISOP_MAX_CUBE   0xFFFF

Typedefs
typedef word	FUNC_ISOP (word *, word *, word *, word, int *)

Functions
word	Abc_IsopCheck (word *pOn, word *pOnDc, word *pRes, int nVars, word CostLim, int *pCover)
word	Abc_EsopCheck (word *pOn, int nVars, word CostLim, int *pCover)
static word	Abc_Cube2Cost (int nCubes)
static int	Abc_CostCubes (word Cost)
static int	Abc_CostLits (word Cost)
static void	Abc_IsopAddLits (int *pCover, word Cost0, word Cost1, int Var)
	FUNCTION DEFINITIONS ///. More...
word	Abc_Isop6Cover (word uOn, word uOnDc, word *pRes, int nVars, word CostLim, int *pCover)
word	Abc_Isop7Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop8Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop9Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop10Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop11Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop12Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop13Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop14Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop15Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
word	Abc_Isop16Cover (word *pOn, word *pOnDc, word *pRes, word CostLim, int *pCover)
static word **	Abc_IsopTtElems ()
void	Abc_IsopBuildTruth (Vec_Int_t *vCover, int nVars, word *pRes, int fXor, int fCompl)
static void	Abc_IsopVerify (word *pFunc, int nVars, word *pRes, Vec_Int_t *vCover, int fXor, int fCompl)
int	Abc_Isop (word *pFunc, int nVars, int nCubeLim, Vec_Int_t *vCover, int fTryBoth)
int	Abc_IsopCnf (word *pFunc, int nVars, int nCubeLim, int *pCover)
int	Abc_IsopCountLits (Vec_Int_t *vCover, int nVars)
void	Abc_IsopPrintCover (Vec_Int_t *vCover, int nVars, int fCompl)
void	Abc_IsopPrint (word *t, int nVars, Vec_Int_t *vCover, int fTryBoth)
static int	Abc_EsopAddLits (int *pCover, word r0, word r1, word r2, word Max, int Var)
word	Abc_Esop6Cover (word t, int nVars, word CostLim, int *pCover)
word	Abc_EsopCover (word *pOn, int nVars, word CostLim, int *pCover)
static int	Abc_TtIntersect (word *pIn1, word *pIn2, int nWords)
static int	Abc_TtCheckWithCubePos2Neg (word *t, word *c, int nWords, int iVar)
static int	Abc_TtCheckWithCubeNeg2Pos (word *t, word *c, int nWords, int iVar)
static void	Abc_TtExpandCubePos2Neg (word *t, int nWords, int iVar)
static void	Abc_TtExpandCubeNeg2Pos (word *t, int nWords, int iVar)
word	Abc_IsopNew (word *pOn, word *pOnDc, word *pRes, int nVars, word CostLim, int *pCover)
void	Abc_IsopTestNew ()
int	Abc_IsopTest (word *pFunc, int nVars, Vec_Int_t *vCover)

Variables
static FUNC_ISOP	Abc_Isop7Cover
static FUNC_ISOP	Abc_Isop8Cover
static FUNC_ISOP	Abc_Isop9Cover
static FUNC_ISOP	Abc_Isop10Cover
static FUNC_ISOP	Abc_Isop11Cover
static FUNC_ISOP	Abc_Isop12Cover
static FUNC_ISOP	Abc_Isop13Cover
static FUNC_ISOP	Abc_Isop14Cover
static FUNC_ISOP	Abc_Isop15Cover
static FUNC_ISOP	Abc_Isop16Cover
static FUNC_ISOP *	s_pFuncIsopCover [17]

Macro Definition Documentation

#define ABC_ISOP_MAX_CUBE   0xFFFF

Definition at line 37 of file utilIsop.c.

#define ABC_ISOP_MAX_VAR   16

DECLARATIONS ///.

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

FileName [utilIsop.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [ISOP computation.]

Synopsis [ISOP computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - October 4, 2014.]

Revision [

Id:

utilIsop.c,v 1.00 2014/10/04 00:00:00 alanmi Exp

]

Definition at line 35 of file utilIsop.c.

#define ABC_ISOP_MAX_WORD   (ABC_ISOP_MAX_VAR > 6 ? (1 << (ABC_ISOP_MAX_VAR-6)) : 1)

Definition at line 36 of file utilIsop.c.

Typedef Documentation

typedef word FUNC_ISOP(word *, word *, word *, word, int *)

Definition at line 39 of file utilIsop.c.

Function Documentation

static int Abc_CostCubes ( word  Cost )

inlinestatic

Definition at line 77 of file utilIsop.c.

{ return (int)(Cost >> 32);        }

static int Abc_CostLits ( word  Cost )

inlinestatic

Definition at line 78 of file utilIsop.c.

{ return (int)(Cost & 0xFFFFFFFF); }

static word Abc_Cube2Cost ( int  nCubes )

inlinestatic

Definition at line 76 of file utilIsop.c.

{ return (word)nCubes << 32;       }

word Abc_Esop6Cover	(	word	t,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 713 of file utilIsop.c.

{
    word c0, c1;
    word r0, r1, r2, Max;
    int Var;
    assert( nVars <= 6 );
    if ( t == 0 )
        return 0;
    if ( t == ~(word)0 )
    {
        if ( pCover ) *pCover = 0;
        return Abc_Cube2Cost(1);
    }
    assert( nVars > 0 );
    // find the topmost var
    for ( Var = nVars-1; Var >= 0; Var-- )
        if ( Abc_Tt6HasVar( t, Var ) )
             break;
    assert( Var >= 0 );
    // cofactor
    c0 = Abc_Tt6Cofactor0( t, Var );
    c1 = Abc_Tt6Cofactor1( t, Var );
    // call recursively
    r0 = Abc_Esop6Cover( c0,      Var, CostLim, pCover ? pCover : NULL );
    if ( r0 >= CostLim ) return CostLim;
    r1 = Abc_Esop6Cover( c1,      Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
    if ( r1 >= CostLim ) return CostLim;
    r2 = Abc_Esop6Cover( c0 ^ c1, Var, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
    if ( r2 >= CostLim ) return CostLim;
    Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
    if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
    return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, Var );
}

static int Abc_EsopAddLits ( int *  pCover, word  r0, word  r1, word  r2, word  Max, int  Var  )

inlinestatic

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

Synopsis [These procedures assume that function has exact support.]

Description []

SideEffects []

SeeAlso []

Definition at line 669 of file utilIsop.c.

{
    int i, c0, c1, c2;
    if ( Max == r0 )
    {
        c2 = Abc_CostCubes(r2);
        if ( pCover )
        {
            c0 = Abc_CostCubes(r0);
            c1 = Abc_CostCubes(r1);
            for ( i = 0; i < c1; i++ )
                pCover[i] = pCover[c0+i];
            for ( i = 0; i < c2; i++ )
                pCover[c1+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,0));
        }
        return c2;
    }
    else if ( Max == r1 )
    {
        c2 = Abc_CostCubes(r2);
        if ( pCover )
        {
            c0 = Abc_CostCubes(r0);
            c1 = Abc_CostCubes(r1);
            for ( i = 0; i < c2; i++ )
                pCover[c0+i] = pCover[c0+c1+i] | (1 << Abc_Var2Lit(Var,1));
        }
        return c2;
    }
    else
    {
        c0 = Abc_CostCubes(r0);
        c1 = Abc_CostCubes(r1);
        if ( pCover )
        {
            c2 = Abc_CostCubes(r2);
            for ( i = 0; i < c0; i++ )
                pCover[i] |= (1 << Abc_Var2Lit(Var,0));
            for ( i = 0; i < c1; i++ )
                pCover[c0+i] |= (1 << Abc_Var2Lit(Var,1));
        }
        return c0 + c1;
    }
}

word Abc_EsopCheck	(	word *	pOn,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 766 of file utilIsop.c.

{
    int nVarsNew; word Cost;
    if ( nVars <= 6 )
        return Abc_Esop6Cover( *pOn, nVars, CostLim, pCover );
    for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
        if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) )
            break;
    if ( nVarsNew == 6 )
        Cost = Abc_Esop6Cover( *pOn, nVarsNew, CostLim, pCover );
    else
        Cost = Abc_EsopCover( pOn, nVarsNew, CostLim, pCover );
    return Cost;
}

word Abc_EsopCover	(	word *	pOn,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 746 of file utilIsop.c.

{
    word r0, r1, r2, Max;
    int c, nWords = (1 << (nVars - 7));
    assert( nVars > 6 );
    assert( Abc_TtHasVar( pOn, nVars, nVars - 1 ) );
    r0 = Abc_EsopCheck( pOn,        nVars-1, CostLim, pCover );
    if ( r0 >= CostLim ) return CostLim;
    r1 = Abc_EsopCheck( pOn+nWords, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) : NULL );
    if ( r1 >= CostLim ) return CostLim;
    for ( c = 0; c < nWords; c++ )
        pOn[c] ^= pOn[nWords+c];
    r2 = Abc_EsopCheck( pOn, nVars-1, CostLim, pCover ? pCover + Abc_CostCubes(r0) + Abc_CostCubes(r1) : NULL );
    for ( c = 0; c < nWords; c++ )
        pOn[c] ^= pOn[nWords+c];
    if ( r2 >= CostLim ) return CostLim;
    Max = Abc_MaxWord( r0, Abc_MaxWord(r1, r2) );
    if ( r0 + r1 + r2 - Max >= CostLim ) return CostLim;
    return r0 + r1 + r2 - Max + Abc_EsopAddLits( pCover, r0, r1, r2, Max, nVars-1 );
}

int Abc_Isop	(	word *	pFunc,
		int	nVars,
		int	nCubeLim,
		Vec_Int_t *	vCover,
		int	fTryBoth
	)

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

Synopsis [This procedure assumes that function has exact support.]

Description []

SideEffects []

SeeAlso []

Definition at line 511 of file utilIsop.c.

{
    word pRes[ABC_ISOP_MAX_WORD];
    word Cost0, Cost1, Cost, CostInit = Abc_Cube2Cost(nCubeLim);
    assert( nVars <= ABC_ISOP_MAX_VAR );
    Vec_IntGrow( vCover, 1 << (nVars-1) );
    if ( fTryBoth )
    {
        Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, NULL );
        Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
        Cost1 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Cost0, NULL );
        Cost = Abc_MinWord( Cost0, Cost1 );
        if ( Cost == CostInit )
        {
            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
            return -1;
        }
        if ( Cost == Cost0 )
        {
            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
            Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
        }
        else // if ( Cost == Cost1 )
        {
            Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
            Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
        }
    }
    else
    {
        Cost = Cost0 = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, CostInit, Vec_IntArray(vCover) );
        if ( Cost == CostInit )
            return -1;
    }
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, Cost != Cost0 );
    return Cost != Cost0;
}

word Abc_Isop10Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 232 of file utilIsop.c.

{
    word uOn2[8], uOnDc2[8], uRes0[8], uRes1[8], uRes2[8];
    word Cost0, Cost1, Cost2; int c, nVars = 9, nWords = 8;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop11Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 260 of file utilIsop.c.

{
    word uOn2[16], uOnDc2[16], uRes0[16], uRes1[16], uRes2[16];
    word Cost0, Cost1, Cost2; int c, nVars = 10, nWords = 16;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop12Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 288 of file utilIsop.c.

{
    word uOn2[32], uOnDc2[32], uRes0[32], uRes1[32], uRes2[32];
    word Cost0, Cost1, Cost2; int c, nVars = 11, nWords = 32;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop13Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 316 of file utilIsop.c.

{
    word uOn2[64], uOnDc2[64], uRes0[64], uRes1[64], uRes2[64];
    word Cost0, Cost1, Cost2; int c, nVars = 12, nWords = 64;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop14Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 344 of file utilIsop.c.

{
    word uOn2[128], uOnDc2[128], uRes0[128], uRes1[128], uRes2[128];
    word Cost0, Cost1, Cost2; int c, nVars = 13, nWords = 128;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop15Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 372 of file utilIsop.c.

{
    word uOn2[256], uOnDc2[256], uRes0[256], uRes1[256], uRes2[256];
    word Cost0, Cost1, Cost2; int c, nVars = 14, nWords = 256;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop16Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 400 of file utilIsop.c.

{
    word uOn2[512], uOnDc2[512], uRes0[512], uRes1[512], uRes2[512];
    word Cost0, Cost1, Cost2; int c, nVars = 15, nWords = 512;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop6Cover	(	word	uOn,
		word	uOnDc,
		word *	pRes,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 108 of file utilIsop.c.

{
    word uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2;
    word Cost0, Cost1, Cost2;  int Var; 
    assert( nVars <= 6 );
    assert( (uOn & ~uOnDc) == 0 );
    if ( uOn == 0 )
    {
        pRes[0] = 0;
        return 0;
    }
    if ( uOnDc == ~(word)0 )
    {
        pRes[0] = ~(word)0;
        if ( pCover ) pCover[0] = 0;
        return Abc_Cube2Cost(1);
    }
    assert( nVars > 0 );
    // find the topmost var
    for ( Var = nVars-1; Var >= 0; Var-- )
        if ( Abc_Tt6HasVar( uOn, Var ) || Abc_Tt6HasVar( uOnDc, Var ) )
             break;
    assert( Var >= 0 );
    // cofactor
    uOn0   = Abc_Tt6Cofactor0( uOn,   Var );
    uOn1   = Abc_Tt6Cofactor1( uOn  , Var );
    uOnDc0 = Abc_Tt6Cofactor0( uOnDc, Var );
    uOnDc1 = Abc_Tt6Cofactor1( uOnDc, Var );
    // solve for cofactors
    Cost0 = Abc_Isop6Cover( uOn0 & ~uOnDc1, uOnDc0, &uRes0, Var, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    Cost1 = Abc_Isop6Cover( uOn1 & ~uOnDc0, uOnDc1, &uRes1, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    Cost2 = Abc_Isop6Cover( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, &uRes2, Var, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    *pRes = uRes2 | (uRes0 & s_Truths6Neg[Var]) | (uRes1 & s_Truths6[Var]);
    assert( (uOn & ~*pRes) == 0 && (*pRes & ~uOnDc) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, Var );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop7Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 149 of file utilIsop.c.

{
    word uOn0, uOn1, uOn2, uOnDc2, uRes0, uRes1, uRes2;
    word Cost0, Cost1, Cost2;  int nVars = 6; 
    assert( (pOn[0] & ~pOnDc[0]) == 0 );
    assert( (pOn[1] & ~pOnDc[1]) == 0 );
    // cofactor
    uOn0 = pOn[0] & ~pOnDc[1];
    uOn1 = pOn[1] & ~pOnDc[0];
    // solve for cofactors
    Cost0 = Abc_IsopCheck( &uOn0, pOnDc,   &uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    Cost1 = Abc_IsopCheck( &uOn1, pOnDc+1, &uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    uOn2 = (pOn[0] & ~uRes0) | (pOn[1] & ~uRes1);
    uOnDc2 = pOnDc[0] & pOnDc[1];
    Cost2 = Abc_IsopCheck( &uOn2, &uOnDc2,  &uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    pRes[0] = uRes2 | uRes0;
    pRes[1] = uRes2 | uRes1;
    assert( (pOn[0] & ~pRes[0]) == 0 && (pRes[0] & ~pOnDc[0]) == 0 );
    assert( (pOn[1] & ~pRes[1]) == 0 && (pRes[1] & ~pOnDc[1]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop8Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 175 of file utilIsop.c.

{
    word uOn2[2], uOnDc2[2], uRes0[2], uRes1[2], uRes2[2];
    word Cost0, Cost1, Cost2;  int nVars = 7;
    // negative cofactor
    uOn2[0] = pOn[0] & ~pOnDc[2];
    uOn2[1] = pOn[1] & ~pOnDc[3];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,   uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    uOn2[0] = pOn[2] & ~pOnDc[0];
    uOn2[1] = pOn[3] & ~pOnDc[1];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+2, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    uOn2[0] = (pOn[0] & ~uRes0[0]) | (pOn[2] & ~uRes1[0]); uOnDc2[0] = pOnDc[0] & pOnDc[2];
    uOn2[1] = (pOn[1] & ~uRes0[1]) | (pOn[3] & ~uRes1[1]); uOnDc2[1] = pOnDc[1] & pOnDc[3];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,  uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    pRes[0] = uRes2[0] | uRes0[0];
    pRes[1] = uRes2[1] | uRes0[1];
    pRes[2] = uRes2[0] | uRes1[0];
    pRes[3] = uRes2[1] | uRes1[1];
    assert( (pOn[0] & ~pRes[0]) == 0 && (pOn[1] & ~pRes[1]) == 0 && (pOn[2] & ~pRes[2]) == 0 && (pOn[3] & ~pRes[3]) == 0 );
    assert( (pRes[0] & ~pOnDc[0])==0 && (pRes[1] & ~pOnDc[1])==0 && (pRes[2] & ~pOnDc[2])==0 && (pRes[3] & ~pOnDc[3])==0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

word Abc_Isop9Cover	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		word	CostLim,
		int *	pCover
	)

Definition at line 204 of file utilIsop.c.

{
    word uOn2[4], uOnDc2[4], uRes0[4], uRes1[4], uRes2[4];
    word Cost0, Cost1, Cost2; int c, nVars = 8, nWords = 4;
    // negative cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c] & ~pOnDc[c+nWords];
    Cost0 = Abc_IsopCheck( uOn2, pOnDc,        uRes0, nVars, CostLim, pCover );
    if ( Cost0 >= CostLim ) return CostLim;
    // positive cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = pOn[c+nWords] & ~pOnDc[c];
    Cost1 = Abc_IsopCheck( uOn2, pOnDc+nWords, uRes1, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    if ( Cost0 + Cost1 >= CostLim ) return CostLim;
    // middle cofactor
    for ( c = 0; c < nWords; c++ )
        uOn2[c] = (pOn[c] & ~uRes0[c]) | (pOn[c+nWords] & ~uRes1[c]), uOnDc2[c] = pOnDc[c] & pOnDc[c+nWords];
    Cost2 = Abc_IsopCheck( uOn2, uOnDc2,       uRes2, nVars, CostLim, pCover ? pCover + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1) : NULL );
    if ( Cost0 + Cost1 + Cost2 >= CostLim ) return CostLim;
    // derive the final truth table
    for ( c = 0; c < nWords; c++ )
        pRes[c] = uRes2[c] | uRes0[c], pRes[c+nWords] = uRes2[c] | uRes1[c];
    // verify
    for ( c = 0; c < (nWords<<1); c++ )
        assert( (pOn[c]  & ~pRes[c] ) == 0 && (pRes[c] & ~pOnDc[c]) == 0 );
    Abc_IsopAddLits( pCover, Cost0, Cost1, nVars );
    return Cost0 + Cost1 + Cost2 + Abc_CostCubes(Cost0) + Abc_CostCubes(Cost1);
}

static void Abc_IsopAddLits ( int *  pCover, word  Cost0, word  Cost1, int  Var  )

inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [These procedures assume that function has exact support.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file utilIsop.c.

{
    if ( pCover ) 
    {
        int c, nCubes0, nCubes1;
        nCubes0 = Abc_CostCubes( Cost0 );
        nCubes1 = Abc_CostCubes( Cost1 );
        for ( c = 0; c < nCubes0; c++ )
            pCover[c] |= (1 << Abc_Var2Lit(Var,0));
        for ( c = 0; c < nCubes1; c++ )
            pCover[nCubes0+c] |= (1 << Abc_Var2Lit(Var,1));
    }
}

void Abc_IsopBuildTruth	(	Vec_Int_t *	vCover,
		int	nVars,
		word *	pRes,
		int	fXor,
		int	fCompl
	)

Definition at line 467 of file utilIsop.c.

{
    word ** pTtElems = Abc_IsopTtElems();
    word pCube[ABC_ISOP_MAX_WORD];
    int nWords = Abc_TtWordNum( nVars );
    int c, v, Cube;
    assert( nVars <= ABC_ISOP_MAX_VAR );
    Abc_TtClear( pRes, nWords );
    Vec_IntForEachEntry( vCover, Cube, c )
    {
        Abc_TtFill( pCube, nWords );
        for ( v = 0; v < nVars; v++ )
            if ( ((Cube >> (v << 1)) & 3) == 1 )
                Abc_TtSharp( pCube, pCube, pTtElems[v], nWords );
            else if ( ((Cube >> (v << 1)) & 3) == 2 )
                Abc_TtAnd( pCube, pCube, pTtElems[v], nWords, 0 );
        if ( fXor )
            Abc_TtXor( pRes, pRes, pCube, nWords, 0 );
        else
            Abc_TtOr( pRes, pRes, pCube, nWords );
    }
    if ( fCompl )
        Abc_TtNot( pRes, nWords );
}

word Abc_IsopCheck	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 428 of file utilIsop.c.

{
    int nVarsNew; word Cost;
    if ( nVars <= 6 )
        return Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVars, CostLim, pCover );
    for ( nVarsNew = nVars; nVarsNew > 6; nVarsNew-- )
        if ( Abc_TtHasVar( pOn, nVars, nVarsNew-1 ) || Abc_TtHasVar( pOnDc, nVars, nVarsNew-1 ) )
            break;
    if ( nVarsNew == 6 )
        Cost = Abc_Isop6Cover( *pOn, *pOnDc, pRes, nVarsNew, CostLim, pCover );
    else
        Cost = s_pFuncIsopCover[nVarsNew]( pOn, pOnDc, pRes, CostLim, pCover );
    Abc_TtStretch6( pRes, nVarsNew, nVars );
    return Cost;
}

int Abc_IsopCnf	(	word *	pFunc,
		int	nVars,
		int	nCubeLim,
		int *	pCover
	)

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

Synopsis [Compute CNF assuming it does not exceed the limit.]

Description [Please note that pCover should have at least 32 extra entries!]

SideEffects []

SeeAlso []

Definition at line 562 of file utilIsop.c.

{
    word pRes[ABC_ISOP_MAX_WORD];
    word Cost0, Cost1, CostInit = Abc_Cube2Cost(nCubeLim);
    int c, nCubes0, nCubes1;
    assert( nVars <= ABC_ISOP_MAX_VAR );
    assert( Abc_TtHasVar( pFunc, nVars, nVars - 1 ) );
    if ( nVars > 6 )
        Cost0 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover );
    else
        Cost0 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover );
    if ( Cost0 >= CostInit )
        return CostInit;
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    if ( nVars > 6 )
        Cost1 = s_pFuncIsopCover[nVars]( pFunc, pFunc, pRes, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    else
        Cost1 = Abc_Isop6Cover( *pFunc, *pFunc, pRes, nVars, CostInit, pCover ? pCover + Abc_CostCubes(Cost0) : NULL );
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    if ( Cost0 + Cost1 >= CostInit )
        return CostInit;
    nCubes0 = Abc_CostCubes(Cost0);
    nCubes1 = Abc_CostCubes(Cost1);
    if ( pCover )
    {
        for ( c = 0; c < nCubes0; c++ )
            pCover[c] |= (1 << Abc_Var2Lit(nVars, 0));
        for ( c = 0; c < nCubes1; c++ )
            pCover[c+nCubes0] |= (1 << Abc_Var2Lit(nVars, 1));
    }
    return nCubes0 + nCubes1;
}

int Abc_IsopCountLits	(	Vec_Int_t *	vCover,
		int	nVars
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 607 of file utilIsop.c.

{
    int i, k, Entry, Literal, nLits = 0;
    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
        return 0;
    Vec_IntForEachEntry( vCover, Entry, i )
    { 
        for ( k = 0; k < nVars; k++ )
        {
            Literal = 3 & (Entry >> (k << 1));
            if ( Literal == 1 ) // neg literal
                nLits++;
            else if ( Literal == 2 ) // pos literal
                nLits++;
            else if ( Literal != 0 ) 
                assert( 0 );
        }
    }
    return nLits;
}

word Abc_IsopNew	(	word *	pOn,
		word *	pOnDc,
		word *	pRes,
		int	nVars,
		word	CostLim,
		int *	pCover
	)

Definition at line 877 of file utilIsop.c.

{
    word pCube[ABC_ISOP_MAX_WORD];
    word pOnset[ABC_ISOP_MAX_WORD];
    word pOffset[ABC_ISOP_MAX_WORD];
    int pBlocks[16], nBlocks, vTwo, uTwo;
    int nWords = Abc_TtWordNum(nVars);
    int c, v, u, iMint, Cube, nLits = 0;
    assert( nVars <= ABC_ISOP_MAX_VAR );
    Abc_TtClear( pRes, nWords );
    Abc_TtCopy( pOnset, pOn, nWords, 0 ); 
    Abc_TtCopy( pOffset, pOnDc, nWords, 1 ); 
    if ( nVars < 6 )
        pOnset[0] >>= (64 - (1 << nVars));
    for ( c = 0; !Abc_TtIsConst0(pOnset, nWords); c++ )
    {
        // pick one minterm
        iMint = Abc_TtFindFirstBit(pOnset, nVars);
        for ( Cube = v = 0; v < nVars; v++ )
            Cube |= (1 << Abc_Var2Lit(v, (iMint >> v) & 1));
        // check expansion for the minterm
        nBlocks = 0;
        for ( v = 0; v < nVars; v++ )
            if ( (pBlocks[v] = Abc_TtGetBit(pOffset, iMint ^ (1 << v))) )
                nBlocks++;
        // check second step
        if ( nBlocks == nVars ) // cannot expand
        {
            Abc_TtSetBit( pRes, iMint );
            Abc_TtXorBit( pOnset, iMint );
            pCover[c] = Cube;
            nLits += nVars;
            continue;
        }
        // check dual expansion
        vTwo = uTwo = -1;
        if ( nBlocks < nVars - 1 )
        {
            for ( v = 0; v < nVars && vTwo == -1; v++ )
            if ( !pBlocks[v] )
            for ( u = v + 1; u < nVars; u++ )
            if ( !pBlocks[u] )
            {
                if ( Abc_TtGetBit( pOffset, iMint ^ (1 << v) ^ (1 << u) ) )
                    continue;
                // can expand both directions
                vTwo = v;
                uTwo = u;
                break;
            }
        }
        if ( vTwo == -1 ) // can expand only one
        {
            for ( v = 0; v < nVars; v++ )
                if ( !pBlocks[v] )
                    break;
            Abc_TtSetBit( pRes, iMint );
            Abc_TtSetBit( pRes, iMint ^ (1 << v) );
            Abc_TtXorBit( pOnset, iMint );
            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << v)) )
                Abc_TtXorBit( pOnset, iMint ^ (1 << v) );
            pCover[c] = Cube & ~(3 << Abc_Var2Lit(v, 0));
            nLits += nVars - 1;
            continue;
        }
        if ( nBlocks == nVars - 2 && vTwo >= 0 ) // can expand only these two
        {
            Abc_TtSetBit( pRes, iMint );
            Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) );
            Abc_TtSetBit( pRes, iMint ^ (1 << uTwo) );
            Abc_TtSetBit( pRes, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
            Abc_TtXorBit( pOnset, iMint );
            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo)) )
                Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) );
            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << uTwo)) )
                Abc_TtXorBit( pOnset, iMint ^ (1 << uTwo) );
            if ( Abc_TtGetBit(pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo)) )
                Abc_TtXorBit( pOnset, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
            pCover[c] = Cube & ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
            nLits += nVars - 2;
            continue;
        }
        // can expand others as well
        Abc_TtClear( pCube, nWords );
        Abc_TtSetBit( pCube, iMint );
        Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) );
        Abc_TtSetBit( pCube, iMint ^ (1 << uTwo) );
        Abc_TtSetBit( pCube, iMint ^ (1 << vTwo) ^ (1 << uTwo) );
        Cube &= ~(3 << Abc_Var2Lit(vTwo, 0)) & ~(3 << Abc_Var2Lit(uTwo, 0));
        assert( !Abc_TtIntersect(pCube, pOffset, nWords) );        
        // expand against offset
        for ( v = 0; v < nVars; v++ )
        if ( v != vTwo && v != uTwo )
        {
            int Shift = Abc_Var2Lit( v, 0 );
            if ( (Cube >> Shift) == 2 && Abc_TtCheckWithCubePos2Neg(pOffset, pCube, nWords, v) ) // pos literal
            {
                Abc_TtExpandCubePos2Neg( pCube, nWords, v );
                Cube &= ~(3 << Shift);
            }
            else if ( (Cube >> Shift) == 1 && Abc_TtCheckWithCubeNeg2Pos(pOffset, pCube, nWords, v) ) // neg literal
            {
                Abc_TtExpandCubeNeg2Pos( pCube, nWords, v );
                Cube &= ~(3 << Shift);
            }
            else 
                nLits++;
        }
        // add cube to solution
        Abc_TtOr( pRes, pRes, pCube, nWords );
        Abc_TtSharp( pOnset, pOnset, pCube, nWords );
        pCover[c] = Cube;
    }
    pRes[0] = Abc_Tt6Stretch( pRes[0], nVars );
    return Abc_Cube2Cost(c) | nLits;
}

void Abc_IsopPrint	(	word *	t,
		int	nVars,
		Vec_Int_t *	vCover,
		int	fTryBoth
	)

Definition at line 651 of file utilIsop.c.

{
    int fCompl = Abc_Isop( t, nVars, ABC_ISOP_MAX_CUBE, vCover, fTryBoth );
    Abc_IsopPrintCover( vCover, nVars, fCompl );
}

void Abc_IsopPrintCover	(	Vec_Int_t *	vCover,
		int	nVars,
		int	fCompl
	)

Definition at line 627 of file utilIsop.c.

{
    int i, k, Entry, Literal;
    if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover, 0) == 0) )
    {
        printf( "Constant %d\n", Vec_IntSize(vCover) );
        return;
    }
    Vec_IntForEachEntry( vCover, Entry, i )
    { 
        for ( k = 0; k < nVars; k++ )
        {
            Literal = 3 & (Entry >> (k << 1));
            if ( Literal == 1 ) // neg literal
                printf( "0" );
            else if ( Literal == 2 ) // pos literal
                printf( "1" );
            else if ( Literal == 0 ) 
                printf( "-" );
            else assert( 0 );
        }
        printf( " %d\n", !fCompl );
    }
}

int Abc_IsopTest	(	word *	pFunc,
		int	nVars,
		Vec_Int_t *	vCover
	)

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

Synopsis [Compute CNF assuming it does not exceed the limit.]

Description [Please note that pCover should have at least 32 extra entries!]

SideEffects []

SeeAlso []

Definition at line 1022 of file utilIsop.c.

{
    int fVerbose = 0;    
    static word TotalCost[6] = {0};
    static abctime TotalTime[6] = {0};
    static int Counter;
    word pRes[ABC_ISOP_MAX_WORD];
    word Cost;
    abctime clk;
    Counter++;
    if ( Counter == 9999 )
    {
        Abc_PrintTime( 1, "0", TotalTime[0] );
        Abc_PrintTime( 1, "1", TotalTime[1] );
        Abc_PrintTime( 1, "2", TotalTime[2] );
        Abc_PrintTime( 1, "3", TotalTime[3] );
        Abc_PrintTime( 1, "4", TotalTime[4] );
        Abc_PrintTime( 1, "5", TotalTime[5] );
    }
    assert( nVars <= ABC_ISOP_MAX_VAR );
//    if ( fVerbose )
//    Dau_DsdPrintFromTruth( pFunc, nVars ), printf( "         " );

    clk = Abc_Clock();
    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d  ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
    TotalCost[0] += Abc_CostCubes(Cost);
    TotalTime[0] += Abc_Clock() - clk;


    clk = Abc_Clock();
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    Cost = Abc_IsopCheck( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d  ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 1 );
    TotalCost[1] += Abc_CostCubes(Cost);
    TotalTime[1] += Abc_Clock() - clk;

/*
    clk = Abc_Clock();
    Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 0 );
    TotalCost[2] += Abc_CostCubes(Cost);
    TotalTime[2] += Abc_Clock() - clk;


    clk = Abc_Clock();
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    Cost = Abc_EsopCheck( pFunc, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    Abc_TtNot( pFunc, Abc_TtWordNum(nVars) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
//    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 1, 1 );
    TotalCost[3] += Abc_CostCubes(Cost);
    TotalTime[3] += Abc_Clock() - clk;
*/

/*
    // try new computation
    clk = Abc_Clock();
    Cost = Abc_IsopNew( pFunc, pFunc, pRes, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d   ", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
    Abc_IsopVerify( pFunc, nVars, pRes, vCover, 0, 0 );
    TotalCost[4] += Abc_CostCubes(Cost);
    TotalTime[4] += Abc_Clock() - clk;
*/
/*
    // try old computation
    clk = Abc_Clock();
    Cost = Kit_TruthIsop( (unsigned *)pFunc, nVars, vCover, 1 );
    vCover->nSize = Vec_IntSize(vCover);
    assert( vCover->nSize <= vCover->nCap );
    if ( fVerbose )
    printf( "%5d %7d   ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
    TotalCost[4] += Vec_IntSize(vCover);
    TotalTime[4] += Abc_Clock() - clk;
*/

    clk = Abc_Clock();
    Cost = Abc_Isop( pFunc, nVars, ABC_ISOP_MAX_CUBE, vCover, 1 );
    if ( fVerbose )
    printf( "%5d %7d   ", Vec_IntSize(vCover), Abc_IsopCountLits(vCover, nVars) );
    TotalCost[5] += Vec_IntSize(vCover);
    TotalTime[5] += Abc_Clock() - clk;

    if ( fVerbose )
    printf( "  | %8d %8d %8d %8d %8d %8d", (int)TotalCost[0], (int)TotalCost[1], (int)TotalCost[2], (int)TotalCost[3], (int)TotalCost[4], (int)TotalCost[5] );
    if ( fVerbose )
    printf( "\n" );
//Abc_IsopPrintCover( vCover, nVars, 0 );
    return 1; 
}

void Abc_IsopTestNew

(

)

Definition at line 993 of file utilIsop.c.

{
    int nVars = 4;
    Vec_Int_t * vCover = Vec_IntAlloc( 1000 );
    word r, t = (s_Truths6[0] & s_Truths6[1]) ^ (s_Truths6[2] & s_Truths6[3]), copy = t;
//    word r, t = ~s_Truths6[0] | (s_Truths6[1] & s_Truths6[2] & s_Truths6[3]), copy = t;
//    word r, t = 0xABCDABCDABCDABCD, copy = t;
//    word r, t = 0x6996000000006996, copy = t;
//    word Cost = Abc_IsopNew( &t, &t, &r, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    word Cost = Abc_EsopCheck( &t, nVars, Abc_Cube2Cost(ABC_ISOP_MAX_CUBE), Vec_IntArray(vCover) );
    vCover->nSize = Abc_CostCubes(Cost);
    assert( vCover->nSize <= vCover->nCap );
    printf( "Cubes = %d.  Lits = %d.\n", Abc_CostCubes(Cost), Abc_CostLits(Cost) );
    Abc_IsopPrintCover( vCover, nVars, 0 );
    Abc_IsopVerify( &copy, nVars, &r, vCover, 1, 0 );
    Vec_IntFree( vCover );
}

static word** Abc_IsopTtElems ( )

inlinestatic

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

Synopsis [Create truth table for the given cover.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file utilIsop.c.

{
    static word TtElems[ABC_ISOP_MAX_VAR+1][ABC_ISOP_MAX_WORD], * pTtElems[ABC_ISOP_MAX_VAR+1] = {NULL};
    if ( pTtElems[0] == NULL )
    {
        int v;
        for ( v = 0; v <= ABC_ISOP_MAX_VAR; v++ )
            pTtElems[v] = TtElems[v];
        Abc_TtElemInit( pTtElems, ABC_ISOP_MAX_VAR );
    }
    return pTtElems;
}

static void Abc_IsopVerify ( word *  pFunc, int  nVars, word *  pRes, Vec_Int_t *  vCover, int  fXor, int  fCompl  )

inlinestatic

Definition at line 491 of file utilIsop.c.

{
    Abc_IsopBuildTruth( vCover, nVars, pRes, fXor, fCompl );
    if ( !Abc_TtEqual( pFunc, pRes, Abc_TtWordNum(nVars) ) )
        printf( "Verification failed.\n" );
//    else
//        printf( "Verification succeeded.\n" );
}

static int Abc_TtCheckWithCubeNeg2Pos ( word *  t, word *  c, int  nWords, int  iVar  )

inlinestatic

Definition at line 822 of file utilIsop.c.

{
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            if ( t[i] & (c[i] << Shift) )
                return 0;
        return 1;
    }
    else
    {
        int i, Step = (1 << (iVar - 6));
        word * tLimit = t + nWords;
        for ( ; t < tLimit; t += 2*Step )
            for ( i = 0; i < Step; i++ )
                if ( t[i] & c[Step+i] )
                    return 0;
        return 1;
    }
}

static int Abc_TtCheckWithCubePos2Neg ( word *  t, word *  c, int  nWords, int  iVar  )

inlinestatic

Definition at line 801 of file utilIsop.c.

{
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            if ( t[i] & (c[i] >> Shift) )
                return 0;
        return 1;
    }
    else
    {
        int i, Step = (1 << (iVar - 6));
        word * tLimit = t + nWords;
        for ( ; t < tLimit; t += 2*Step )
            for ( i = 0; i < Step; i++ )
                if ( t[Step+i] & c[i] )
                    return 0;
        return 1;
    }
}

static void Abc_TtExpandCubeNeg2Pos ( word *  t, int  nWords, int  iVar  )

inlinestatic

Definition at line 860 of file utilIsop.c.

{
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            t[i] |= (t[i] << Shift);
    }
    else
    {
        int i, Step = (1 << (iVar - 6));
        word * tLimit = t + nWords;
        for ( ; t < tLimit; t += 2*Step )
            for ( i = 0; i < Step; i++ )
                t[Step+i] = t[i];
    }
}

static void Abc_TtExpandCubePos2Neg ( word *  t, int  nWords, int  iVar  )

inlinestatic

Definition at line 843 of file utilIsop.c.

{
    if ( iVar < 6 )
    {
        int i, Shift = (1 << iVar);
        for ( i = 0; i < nWords; i++ )
            t[i] |= (t[i] >> Shift);
    }
    else
    {
        int i, Step = (1 << (iVar - 6));
        word * tLimit = t + nWords;
        for ( ; t < tLimit; t += 2*Step )
            for ( i = 0; i < Step; i++ )
                t[i] = t[Step+i];
    }
}

static int Abc_TtIntersect ( word *  pIn1, word *  pIn2, int  nWords  )

inlinestatic

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

Synopsis [Perform ISOP computation by subtracting cubes.]

Description []

SideEffects []

SeeAlso []

Definition at line 793 of file utilIsop.c.

{
    int w;
    for ( w = 0; w < nWords; w++ )
        if ( pIn1[w] & pIn2[w] )
            return 1;
    return 0;
}

Variable Documentation

FUNC_ISOP Abc_Isop10Cover

static

Definition at line 44 of file utilIsop.c.

FUNC_ISOP Abc_Isop11Cover

static

Definition at line 45 of file utilIsop.c.

FUNC_ISOP Abc_Isop12Cover

static

Definition at line 46 of file utilIsop.c.

FUNC_ISOP Abc_Isop13Cover

static

Definition at line 47 of file utilIsop.c.

FUNC_ISOP Abc_Isop14Cover

static

Definition at line 48 of file utilIsop.c.

FUNC_ISOP Abc_Isop15Cover

static

Definition at line 49 of file utilIsop.c.

FUNC_ISOP Abc_Isop16Cover

static

Definition at line 50 of file utilIsop.c.

FUNC_ISOP Abc_Isop7Cover

static

Definition at line 41 of file utilIsop.c.

FUNC_ISOP Abc_Isop8Cover

static

Definition at line 42 of file utilIsop.c.

FUNC_ISOP Abc_Isop9Cover

static

Definition at line 43 of file utilIsop.c.

FUNC_ISOP* s_pFuncIsopCover[17]

static

Initial value:

=
{
    NULL, 
    NULL, 
    NULL, 
    NULL, 
    NULL, 
    NULL, 
    NULL, 
    Abc_Isop7Cover,  
    Abc_Isop8Cover,  
    Abc_Isop9Cover,  
    Abc_Isop10Cover, 
    Abc_Isop11Cover, 
    Abc_Isop12Cover, 
    Abc_Isop13Cover, 
    Abc_Isop14Cover, 
    Abc_Isop15Cover, 
    Abc_Isop16Cover  
}

Definition at line 52 of file utilIsop.c.