cnf.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "aig/aig/aig.h"
#include "opt/dar/darInt.h"

Go to the source code of this file.

Data Structures
struct	Cnf_Dat_t_
struct	Cnf_Cut_t_
struct	Cnf_Man_t_

Macros
#define	Cnf_CnfForClause(p, pBeg, pEnd, i)   for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )
	MACRO DEFINITIONS ///. More...
#define	Cnf_CutForEachLeaf(p, pCut, pLeaf, i)   for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_	Cnf_Man_t
	INCLUDES ///. More...
typedef struct Cnf_Dat_t_	Cnf_Dat_t
typedef struct Cnf_Cut_t_	Cnf_Cut_t

Functions
static Dar_Cut_t *	Dar_ObjBestCut (Aig_Obj_t *pObj)
static int	Cnf_CutSopCost (Cnf_Man_t *p, Dar_Cut_t *pCut)
static int	Cnf_CutLeaveNum (Cnf_Cut_t *pCut)
static int *	Cnf_CutLeaves (Cnf_Cut_t *pCut)
static unsigned *	Cnf_CutTruth (Cnf_Cut_t *pCut)
static Cnf_Cut_t *	Cnf_ObjBestCut (Aig_Obj_t *pObj)
static void	Cnf_ObjSetBestCut (Aig_Obj_t *pObj, Cnf_Cut_t *pCut)
Vec_Int_t *	Cnf_DeriveMappingArray (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///. More...
Cnf_Dat_t *	Cnf_Derive (Aig_Man_t *pAig, int nOutputs)
Cnf_Dat_t *	Cnf_DeriveWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int nOutputs)
Cnf_Dat_t *	Cnf_DeriveOther (Aig_Man_t *pAig, int fSkipTtMin)
Cnf_Dat_t *	Cnf_DeriveOtherWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int fSkipTtMin)
void	Cnf_ManPrepare ()
	FUNCTION DEFINITIONS ///. More...
Cnf_Man_t *	Cnf_ManRead ()
void	Cnf_ManFree ()
Cnf_Cut_t *	Cnf_CutCreate (Cnf_Man_t *p, Aig_Obj_t *pObj)
void	Cnf_CutPrint (Cnf_Cut_t *pCut)
void	Cnf_CutFree (Cnf_Cut_t *pCut)
void	Cnf_CutUpdateRefs (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, Cnf_Cut_t *pCutRes)
Cnf_Cut_t *	Cnf_CutCompose (Cnf_Man_t *p, Cnf_Cut_t *pCut, Cnf_Cut_t *pCutFan, int iFan)
void	Cnf_ReadMsops (char **ppSopSizes, char ***ppSops)
	FUNCTION DEFINITIONS ///. More...
void	Cnf_CollectLeaves (Aig_Obj_t *pRoot, Vec_Ptr_t *vSuper, int fStopCompl)
void	Cnf_ComputeClauses (Aig_Man_t *p, Aig_Obj_t *pRoot, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Int_t *vMap, Vec_Int_t *vCover, Vec_Int_t *vClauses)
void	Cnf_DeriveFastMark (Aig_Man_t *p)
Cnf_Dat_t *	Cnf_DeriveFast (Aig_Man_t *p, int nOutputs)
Cnf_Man_t *	Cnf_ManStart ()
	FUNCTION DEFINITIONS ///. More...
void	Cnf_ManStop (Cnf_Man_t *p)
Vec_Int_t *	Cnf_DataCollectPiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
Cnf_Dat_t *	Cnf_DataAlloc (Aig_Man_t *pAig, int nVars, int nClauses, int nLiterals)
Cnf_Dat_t *	Cnf_DataDup (Cnf_Dat_t *p)
void	Cnf_DataFree (Cnf_Dat_t *p)
void	Cnf_DataLift (Cnf_Dat_t *p, int nVarsPlus)
void	Cnf_DataFlipLastLiteral (Cnf_Dat_t *p)
void	Cnf_DataPrint (Cnf_Dat_t *p, int fReadable)
void	Cnf_DataWriteIntoFile (Cnf_Dat_t *p, char *pFileName, int fReadable, Vec_Int_t *vForAlls, Vec_Int_t *vExists)
void *	Cnf_DataWriteIntoSolver (Cnf_Dat_t *p, int nFrames, int fInit)
void *	Cnf_DataWriteIntoSolverInt (void *pSat, Cnf_Dat_t *p, int nFrames, int fInit)
int	Cnf_DataWriteOrClause (void *pSat, Cnf_Dat_t *pCnf)
int	Cnf_DataWriteAndClauses (void *p, Cnf_Dat_t *pCnf)
void	Cnf_DataTranformPolarity (Cnf_Dat_t *pCnf, int fTransformPos)
int	Cnf_DataAddXorClause (void *pSat, int iVarA, int iVarB, int iVarC)
void	Cnf_DeriveMapping (Cnf_Man_t *p)
int	Cnf_ManMapForCnf (Cnf_Man_t *p)
void	Cnf_ManTransferCuts (Cnf_Man_t *p)
void	Cnf_ManFreeCuts (Cnf_Man_t *p)
void	Cnf_ManPostprocess (Cnf_Man_t *p)
Vec_Ptr_t *	Aig_ManScanMapping (Cnf_Man_t *p, int fCollect)
Vec_Ptr_t *	Cnf_ManScanMapping (Cnf_Man_t *p, int fCollect, int fPreorder)
Vec_Int_t *	Cnf_DataCollectCiSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
Vec_Int_t *	Cnf_DataCollectCoSatNums (Cnf_Dat_t *pCnf, Aig_Man_t *p)
unsigned char *	Cnf_DataDeriveLitPolarities (Cnf_Dat_t *p)
Cnf_Dat_t *	Cnf_DataReadFromFile (char *pFileName)
Vec_Int_t *	Cnf_ManWriteCnfMapping (Cnf_Man_t *p, Vec_Ptr_t *vMapped)
	DECLARATIONS ///. More...
void	Cnf_SopConvertToVector (char *pSop, int nCubes, Vec_Int_t *vCover)
Cnf_Dat_t *	Cnf_ManWriteCnf (Cnf_Man_t *p, Vec_Ptr_t *vMapped, int nOutputs)
Cnf_Dat_t *	Cnf_ManWriteCnfOther (Cnf_Man_t *p, Vec_Ptr_t *vMapped)
Cnf_Dat_t *	Cnf_DeriveSimple (Aig_Man_t *p, int nOutputs)
Cnf_Dat_t *	Cnf_DeriveSimpleForRetiming (Aig_Man_t *p)

Macro Definition Documentation

#define Cnf_CnfForClause	(		p,
			pBeg,
			pEnd,
			i
	)		for ( i = 0; i < p->nClauses && (pBeg = p->pClauses[i]) && (pEnd = p->pClauses[i+1]); i++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 117 of file cnf.h.

#define Cnf_CutForEachLeaf	(		p,
			pCut,
			pLeaf,
			i
	)		for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )

Definition at line 121 of file cnf.h.

Typedef Documentation

typedef struct Cnf_Cut_t_ Cnf_Cut_t

Definition at line 53 of file cnf.h.

typedef struct Cnf_Dat_t_ Cnf_Dat_t

Definition at line 52 of file cnf.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Cnf_Man_t_ Cnf_Man_t

INCLUDES ///.

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

FileName [cnf.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [DAG-aware AIG rewriting.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp

]PARAMETERS ///BASIC TYPES ///

Definition at line 51 of file cnf.h.

Function Documentation

Vec_Ptr_t* Aig_ManScanMapping	(	Cnf_Man_t *	p,
		int	fCollect
	)

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 90 of file cnfUtil.c.

{
    Vec_Ptr_t * vMapped = NULL;
    Aig_Obj_t * pObj;
    int i;
    // clean all references
    Aig_ManForEachObj( p->pManAig, pObj, i )
        pObj->nRefs = 0;
    // allocate the array
    if ( fCollect )
        vMapped = Vec_PtrAlloc( 1000 );
    // collect nodes reachable from POs in the DFS order through the best cuts
    p->aArea = 0;
    Aig_ManForEachCo( p->pManAig, pObj, i )
        p->aArea += Aig_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped );
//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
    return vMapped;
}

void Cnf_CollectLeaves	(	Aig_Obj_t *	pRoot,
		Vec_Ptr_t *	vSuper,
		int	fStopCompl
	)

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

Synopsis [Detects multi-input gate rooted at this node.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file cnfFast.c.

{
    assert( !Aig_IsComplement(pRoot) );
    Vec_PtrClear( vSuper );
    Cnf_CollectLeaves_rec( pRoot, pRoot, vSuper, fStopCompl );
}

void Cnf_ComputeClauses	(	Aig_Man_t *	p,
		Aig_Obj_t *	pRoot,
		Vec_Ptr_t *	vLeaves,
		Vec_Ptr_t *	vNodes,
		Vec_Int_t *	vMap,
		Vec_Int_t *	vCover,
		Vec_Int_t *	vClauses
	)

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

Synopsis [Collects nodes inside the cone.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file cnfFast.c.

{
    Aig_Obj_t * pLeaf;
    int c, k, Cube, OutLit, RetValue;
    word Truth;
    assert( pRoot->fMarkA );

    Vec_IntClear( vClauses );

    OutLit = Cnf_ObjGetLit( vMap, pRoot, 0 );
    // detect cone
    Cnf_CollectLeaves( pRoot, vLeaves, 0 );
    Cnf_CollectVolume( p, pRoot, vLeaves, vNodes );
    assert( pRoot == Vec_PtrEntryLast(vNodes) );
    // check if this is an AND-gate
    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pLeaf, k )
    {
        if ( Aig_ObjFaninC0(pLeaf) && !Aig_ObjFanin0(pLeaf)->fMarkA )
            break;
        if ( Aig_ObjFaninC1(pLeaf) && !Aig_ObjFanin1(pLeaf)->fMarkA )
            break;
    }
    if ( k == Vec_PtrSize(vNodes) )
    {
        Cnf_CollectLeaves( pRoot, vLeaves, 1 );
        // write big clause
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit );
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), !Aig_IsComplement(pLeaf)) );
        // write small clauses
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pLeaf, k )
        {
            Vec_IntPush( vClauses, 0 );
            Vec_IntPush( vClauses, OutLit ^ 1 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, Aig_Regular(pLeaf), Aig_IsComplement(pLeaf)) );
        }
        return;
    }
    if ( Vec_PtrSize(vLeaves) > 6 )
        printf( "FastCnfGeneration:  Internal error!!!\n" );
    assert( Vec_PtrSize(vLeaves) <= 6 );

    Truth = Cnf_CutDeriveTruth( p, vLeaves, vNodes );
    if ( Truth == 0 || Truth == ~(word)0 )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, (Truth == 0) ? (OutLit ^ 1) : OutLit );
        return;
    }

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );

    Vec_IntForEachEntry( vCover, Cube, c )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit );
        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
        {
            if ( (Cube & 3) == 0 )
                continue;
            assert( (Cube & 3) != 3 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
        }
    }

    Truth = ~Truth;

    RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 );
    assert( RetValue >= 0 );
    Vec_IntForEachEntry( vCover, Cube, c )
    {
        Vec_IntPush( vClauses, 0 );
        Vec_IntPush( vClauses, OutLit ^ 1 );
        for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 )
        {
            if ( (Cube & 3) == 0 )
                continue;
            assert( (Cube & 3) != 3 );
            Vec_IntPush( vClauses, Cnf_ObjGetLit(vMap, (Aig_Obj_t *)Vec_PtrEntry(vLeaves,k), (Cube&3)!=1) );
        }
    }
}

Cnf_Cut_t* Cnf_CutCompose	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut,
		Cnf_Cut_t *	pCutFan,
		int	iFan
	)

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

Synopsis [Merges two cuts.]

Description [Returns NULL of the cuts cannot be merged.]

SideEffects []

SeeAlso []

Definition at line 294 of file cnfCut.c.

{
    Cnf_Cut_t * pCutRes;
    static int pFanins[32];
    unsigned * pTruth, * pTruthFan, * pTruthRes;
    unsigned * pTop = p->pTruths[0], * pFan = p->pTruths[2], * pTemp = p->pTruths[3];
    unsigned uPhase, uPhaseFan;
    int i, iVar, nFanins, RetValue;

    // make sure the second cut is the fanin of the first
    for ( iVar = 0; iVar < pCut->nFanins; iVar++ )
        if ( pCut->pFanins[iVar] == iFan )
            break;
    assert( iVar < pCut->nFanins );
    // remove this variable
    Cnf_CutRemoveIthVar( pCut, iVar, iFan );
    // merge leaves of the cuts
    nFanins = Cnf_CutMergeLeaves( pCut, pCutFan, pFanins );
    if ( nFanins+1 > p->nMergeLimit )
    {
        Cnf_CutInsertIthVar( pCut, iVar, iFan );
        return NULL;
    }
    // create new cut
    pCutRes = Cnf_CutAlloc( p, nFanins );
    memcpy( pCutRes->pFanins, pFanins, sizeof(int) * nFanins );
    assert( pCutRes->nFanins <= pCut->nFanins + pCutFan->nFanins );

    // derive its truth table
    // get the truth tables in the composition space
    pTruth    = Cnf_CutTruth(pCut);
    pTruthFan = Cnf_CutTruth(pCutFan);
    pTruthRes = Cnf_CutTruth(pCutRes);
    for ( i = 0; i < 2*pCutRes->nWords; i++ )
        pTop[i] = pTruth[i % pCut->nWords];
    for ( i = 0; i < pCutRes->nWords; i++ )
        pFan[i] = pTruthFan[i % pCutFan->nWords];
    // move the variable to the end
    uPhase = Kit_BitMask( pCutRes->nFanins+1 ) & ~(1 << iVar);
    Kit_TruthShrink( pTemp, pTop, pCutRes->nFanins, pCutRes->nFanins+1, uPhase, 1 );
    // compute the phases
    uPhase    = Cnf_TruthPhase( pCutRes, pCut    ) | (1 << pCutRes->nFanins);
    uPhaseFan = Cnf_TruthPhase( pCutRes, pCutFan );
    // permute truth-tables to the common support
    Kit_TruthStretch( pTemp, pTop, pCut->nFanins+1,  pCutRes->nFanins+1, uPhase,    1 );
    Kit_TruthStretch( pTemp, pFan, pCutFan->nFanins, pCutRes->nFanins,   uPhaseFan, 1 );
    // perform Boolean operation
    Kit_TruthMux( pTruthRes, pTop, pTop+pCutRes->nWords, pFan, pCutRes->nFanins );
    // return the cut to its original condition
    Cnf_CutInsertIthVar( pCut, iVar, iFan );
    // consider the simple case
    if ( pCutRes->nFanins < 5 )
    {
        pCutRes->Cost = p->pSopSizes[0xFFFF & *pTruthRes] + p->pSopSizes[0xFFFF & ~*pTruthRes];
        return pCutRes;
    }

    // derive ISOP for positive phase
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[1] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    // derive ISOP for negative phase
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );
    RetValue = Kit_TruthIsop( pTruthRes, pCutRes->nFanins, p->vMemory, 0 );
    pCutRes->vIsop[0] = (RetValue == -1)? NULL : Vec_IntDup( p->vMemory );
    Kit_TruthNot( pTruthRes, pTruthRes, pCutRes->nFanins );

    // compute the cut cost
    if ( pCutRes->vIsop[0] == NULL || pCutRes->vIsop[1] == NULL )
        pCutRes->Cost = 127;
    else if ( Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]) > 127 )
        pCutRes->Cost = 127;
    else
        pCutRes->Cost = Vec_IntSize(pCutRes->vIsop[0]) + Vec_IntSize(pCutRes->vIsop[1]);
    return pCutRes;
}

Cnf_Cut_t* Cnf_CutCreate	(	Cnf_Man_t *	p,
		Aig_Obj_t *	pObj
	)

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

Synopsis [Creates cut for the given node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file cnfCut.c.

{
    Dar_Cut_t * pCutBest;
    Cnf_Cut_t * pCut;
    unsigned * pTruth;
    assert( Aig_ObjIsNode(pObj) );
    pCutBest = Dar_ObjBestCut( pObj );
    assert( pCutBest != NULL );
    assert( pCutBest->nLeaves <= 4 );
    pCut = Cnf_CutAlloc( p, pCutBest->nLeaves );
    memcpy( pCut->pFanins, pCutBest->pLeaves, sizeof(int) * pCutBest->nLeaves );
    pTruth = Cnf_CutTruth(pCut);
    *pTruth = (pCutBest->uTruth << 16) | pCutBest->uTruth;
    pCut->Cost = Cnf_CutSopCost( p, pCutBest );
    return pCut;
}

void Cnf_CutFree

(

Cnf_Cut_t *

pCut

)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 68 of file cnfCut.c.

{
    if ( pCut->vIsop[0] )
        Vec_IntFree( pCut->vIsop[0] );
    if ( pCut->vIsop[1] )
        Vec_IntFree( pCut->vIsop[1] );
}

static int Cnf_CutLeaveNum ( Cnf_Cut_t *  pCut )

inlinestatic

Definition at line 101 of file cnf.h.

{ return pCut->nFanins;                               }

static int* Cnf_CutLeaves ( Cnf_Cut_t *  pCut )

inlinestatic

Definition at line 102 of file cnf.h.

{ return pCut->pFanins;                               }

void Cnf_CutPrint

(

Cnf_Cut_t *

pCut

)

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

Synopsis [Deallocates cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 115 of file cnfCut.c.

{
    int i;
    printf( "{" );
    for ( i = 0; i < pCut->nFanins; i++ )
        printf( "%d ", pCut->pFanins[i] );
    printf( " } " );
}

static int Cnf_CutSopCost ( Cnf_Man_t *  p, Dar_Cut_t *  pCut  )

inlinestatic

Definition at line 99 of file cnf.h.

{ return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }

static unsigned* Cnf_CutTruth ( Cnf_Cut_t *  pCut )

inlinestatic

Definition at line 103 of file cnf.h.

{ return (unsigned *)(pCut->pFanins + pCut->nFanins); }

void Cnf_CutUpdateRefs	(	Cnf_Man_t *	p,
		Cnf_Cut_t *	pCut,
		Cnf_Cut_t *	pCutFan,
		Cnf_Cut_t *	pCutRes
	)

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

Synopsis [Allocates cut of the given size.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file cnfCut.c.

{
    Cnf_CutDeref( p, pCut );
    Cnf_CutDeref( p, pCutFan );
    Cnf_CutRef( p, pCutRes );
}

int Cnf_DataAddXorClause	(	void *	pSat,
		int	iVarA,
		int	iVarB,
		int	iVarC
	)

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

Synopsis [Adds constraints for the two-input AND-gate.]

Description []

SideEffects []

SeeAlso []

Definition at line 688 of file cnfMan.c.

{
    lit Lits[3];
    assert( iVarA > 0 && iVarB > 0 && iVarC > 0 );

    Lits[0] = toLitCond( iVarA, 1 );
    Lits[1] = toLitCond( iVarB, 1 );
    Lits[2] = toLitCond( iVarC, 1 );
    if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
        return 0;

    Lits[0] = toLitCond( iVarA, 1 );
    Lits[1] = toLitCond( iVarB, 0 );
    Lits[2] = toLitCond( iVarC, 0 );
    if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
        return 0;

    Lits[0] = toLitCond( iVarA, 0 );
    Lits[1] = toLitCond( iVarB, 1 );
    Lits[2] = toLitCond( iVarC, 0 );
    if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
        return 0;

    Lits[0] = toLitCond( iVarA, 0 );
    Lits[1] = toLitCond( iVarB, 0 );
    Lits[2] = toLitCond( iVarC, 1 );
    if ( !sat_solver_addclause( (sat_solver *)pSat, Lits, Lits + 3 ) )
        return 0;

    return 1;
}

Cnf_Dat_t* Cnf_DataAlloc	(	Aig_Man_t *	pAig,
		int	nVars,
		int	nClauses,
		int	nLiterals
	)

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

Synopsis [Allocates the new CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 126 of file cnfMan.c.

{
    Cnf_Dat_t * pCnf;
    int i;
    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
    pCnf->pMan = pAig;
    pCnf->nVars = nVars;
    pCnf->nClauses = nClauses;
    pCnf->nLiterals = nLiterals;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
        pCnf->pVarNums[i] = -1;
    return pCnf;
}

Vec_Int_t* Cnf_DataCollectCiSatNums	(	Cnf_Dat_t *	pCnf,
		Aig_Man_t *	p
	)

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file cnfUtil.c.

{
    Vec_Int_t * vCiIds;
    Aig_Obj_t * pObj;
    int i;
    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
    Aig_ManForEachCi( p, pObj, i )
        Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
    return vCiIds;
}

Vec_Int_t* Cnf_DataCollectCoSatNums	(	Cnf_Dat_t *	pCnf,
		Aig_Man_t *	p
	)

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 222 of file cnfUtil.c.

{
    Vec_Int_t * vCoIds;
    Aig_Obj_t * pObj;
    int i;
    vCoIds = Vec_IntAlloc( Aig_ManCoNum(p) );
    Aig_ManForEachCo( p, pObj, i )
        Vec_IntPush( vCoIds, pCnf->pVarNums[pObj->Id] );
    return vCoIds;
}

Vec_Int_t* Cnf_DataCollectPiSatNums	(	Cnf_Dat_t *	pCnf,
		Aig_Man_t *	p
	)

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

Synopsis [Returns the array of CI IDs.]

Description []

SideEffects []

SeeAlso []

Definition at line 104 of file cnfMan.c.

{
    Vec_Int_t * vCiIds;
    Aig_Obj_t * pObj;
    int i;
    vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
    Aig_ManForEachCi( p, pObj, i )
        Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
    return vCiIds;
}

unsigned char* Cnf_DataDeriveLitPolarities

(

Cnf_Dat_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 244 of file cnfUtil.c.

{
    int i, c, iClaBeg, iClaEnd, * pLit;
    unsigned * pPols0 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
    unsigned * pPols1 = ABC_CALLOC( unsigned, Aig_ManObjNumMax(p->pMan) );
    unsigned char * pPres = ABC_CALLOC( unsigned char, p->nClauses );
    for ( i = 0; i < Aig_ManObjNumMax(p->pMan); i++ )
    {
        if ( p->pObj2Count[i] == 0 )
            continue;
        iClaBeg = p->pObj2Clause[i];
        iClaEnd = p->pObj2Clause[i] + p->pObj2Count[i];
        // go through the negative polarity clauses
        for ( c = iClaBeg; c < iClaEnd; c++ )
            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
                    pPols0[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
                else
                    pPols1[Abc_Lit2Var(*pLit)] |= (unsigned)(2 - Abc_LitIsCompl(*pLit));  // taking the opposite (!) -- not the case
        // record these clauses
        for ( c = iClaBeg; c < iClaEnd; c++ )
            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
                if ( Abc_LitIsCompl(p->pClauses[c][0]) )
                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols0[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
                else
                    pPres[c] = (unsigned char)( (unsigned)pPres[c] | (pPols1[Abc_Lit2Var(*pLit)] << (2*(pLit-p->pClauses[c]-1))) );
        // clean negative polarity
        for ( c = iClaBeg; c < iClaEnd; c++ )
            for ( pLit = p->pClauses[c]+1; pLit < p->pClauses[c+1]; pLit++ )
                pPols0[Abc_Lit2Var(*pLit)] = pPols1[Abc_Lit2Var(*pLit)] = 0;
    }
    ABC_FREE( pPols0 );
    ABC_FREE( pPols1 );
/*
//    for ( c = 0; c < p->nClauses; c++ )
    for ( c = 0; c < 100; c++ )
    {
        printf( "Clause %6d : ", c );
        for ( i = 0; i < 4; i++ )
            printf( "%d ", ((unsigned)pPres[c] >> (2*i)) & 3 );
        printf( "  " );
        for ( pLit = p->pClauses[c]; pLit < p->pClauses[c+1]; pLit++ )
            printf( "%6d ", *pLit );
        printf( "\n" );
    }
*/
    return pPres;
}

Cnf_Dat_t* Cnf_DataDup

(

Cnf_Dat_t *

p

)

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

Synopsis [Allocates the new CNF.]

Description []

SideEffects []

SeeAlso []

Definition at line 157 of file cnfMan.c.

{
    Cnf_Dat_t * pCnf;
    int i;
    pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
    memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
    memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
    for ( i = 1; i < p->nClauses; i++ )
        pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
    return pCnf;
}

void Cnf_DataFlipLastLiteral

(

Cnf_Dat_t *

p

)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 230 of file cnfMan.c.

{
    p->pClauses[0][p->nLiterals-1] = lit_neg( p->pClauses[0][p->nLiterals-1] );
}

void Cnf_DataFree

(

Cnf_Dat_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file cnfMan.c.

{
    if ( p == NULL )
        return;
    Vec_IntFreeP( &p->vMapping );
    ABC_FREE( p->pClaPols );
    ABC_FREE( p->pObj2Clause );
    ABC_FREE( p->pObj2Count );
    ABC_FREE( p->pClauses[0] );
    ABC_FREE( p->pClauses );
    ABC_FREE( p->pVarNums );
    ABC_FREE( p );
}

void Cnf_DataLift	(	Cnf_Dat_t *	p,
		int	nVarsPlus
	)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file cnfMan.c.

{
    Aig_Obj_t * pObj;
    int v;
    if ( p->pMan )
    {
        Aig_ManForEachObj( p->pMan, pObj, v )
            if ( p->pVarNums[pObj->Id] >= 0 )
                p->pVarNums[pObj->Id] += nVarsPlus;
    }
    for ( v = 0; v < p->nLiterals; v++ )
        p->pClauses[0][v] += 2*nVarsPlus;
}

void Cnf_DataPrint	(	Cnf_Dat_t *	p,
		int	fReadable
	)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file cnfMan.c.

{
    FILE * pFile = stdout;
    int * pLit, * pStop, i;
    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
    for ( i = 0; i < p->nClauses; i++ )
    {
        for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
            fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
        fprintf( pFile, "\n" );
    }
    fprintf( pFile, "\n" );
}

Cnf_Dat_t* Cnf_DataReadFromFile

(

char *

pFileName

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file cnfUtil.c.

{
    int MaxLine = 1000000;
    int Var, Lit, nVars = -1, nClas = -1, i, Entry, iLine = 0;
    Cnf_Dat_t * pCnf = NULL;
    Vec_Int_t * vClas = NULL;
    Vec_Int_t * vLits = NULL;
    char * pBuffer, * pToken;
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open file \"%s\" for writing.\n", pFileName );
        return NULL;
    }
    pBuffer = ABC_ALLOC( char, MaxLine );
    while ( fgets(pBuffer, MaxLine, pFile) != NULL )
    {
        iLine++;
        if ( pBuffer[0] == 'c' )
            continue;
        if ( pBuffer[0] == 'p' )
        {
            pToken = strtok( pBuffer+1, " \t" );
            if ( strcmp(pToken, "cnf") )
            {
                printf( "Incorrect input file.\n" );
                goto finish;
            }
            pToken = strtok( NULL, " \t" );
            nVars = atoi( pToken );
            pToken = strtok( NULL, " \t" );
            nClas = atoi( pToken );
            if ( nVars <= 0 || nClas <= 0 )
            {
                printf( "Incorrect parameters.\n" );
                goto finish;
            }
            // temp storage
            vClas = Vec_IntAlloc( nClas+1 );
            vLits = Vec_IntAlloc( nClas*8 );
            continue;
        }
        pToken = strtok( pBuffer, " \t\r\n" );
        if ( pToken == NULL )
            continue;
        Vec_IntPush( vClas, Vec_IntSize(vLits) );
        while ( pToken )
        {
            Var = atoi( pToken );
            if ( Var == 0 )
                break;
            Lit = (Var > 0) ? Abc_Var2Lit(Var-1, 0) : Abc_Var2Lit(-Var-1, 1);
            if ( Lit >= 2*nVars )
            {
                printf( "Literal %d is out-of-bound for %d variables.\n", Lit, nVars );
                goto finish;
            }
            Vec_IntPush( vLits, Lit );
            pToken = strtok( NULL, " \t\r\n" );
        }
        if ( Var != 0 )
        {
            printf( "There is no zero-terminator in line %d.\n", iLine );
            goto finish;
        }
    }
    // finalize
    if ( Vec_IntSize(vClas) != nClas )
        printf( "Warning! The number of clauses (%d) is different from declaration (%d).\n", Vec_IntSize(vClas), nClas );
    Vec_IntPush( vClas, Vec_IntSize(vLits) );
    // create
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->nVars     = nVars;
    pCnf->nClauses  = nClas;
    pCnf->nLiterals = Vec_IntSize(vLits);
    pCnf->pClauses  = ABC_ALLOC( int *, Vec_IntSize(vClas) );
    pCnf->pClauses[0] = Vec_IntReleaseArray(vLits);
    Vec_IntForEachEntry( vClas, Entry, i )
        pCnf->pClauses[i] = pCnf->pClauses[0] + Entry;
finish:
    fclose( pFile );
    Vec_IntFreeP( &vClas );
    Vec_IntFreeP( &vLits );
    ABC_FREE( pBuffer );
    return pCnf;
}

void Cnf_DataTranformPolarity	(	Cnf_Dat_t *	pCnf,
		int	fTransformPos
	)

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

Synopsis [Transforms polarity of the internal veriables.]

Description []

SideEffects []

SeeAlso []

Definition at line 652 of file cnfMan.c.

{
    Aig_Obj_t * pObj;
    int * pVarToPol;
    int i, iVar;
    // create map from the variable number to its polarity
    pVarToPol = ABC_CALLOC( int, pCnf->nVars );
    Aig_ManForEachObj( pCnf->pMan, pObj, i )
    {
        if ( !fTransformPos && Aig_ObjIsCo(pObj) )
            continue;
        if ( pCnf->pVarNums[pObj->Id] >= 0 )
            pVarToPol[ pCnf->pVarNums[pObj->Id] ] = pObj->fPhase;
    }
    // transform literals
    for ( i = 0; i < pCnf->nLiterals; i++ )
    {
        iVar = lit_var(pCnf->pClauses[0][i]);
        assert( iVar < pCnf->nVars );
        if ( pVarToPol[iVar] )
            pCnf->pClauses[0][i] = lit_neg( pCnf->pClauses[0][i] );
    }
    ABC_FREE( pVarToPol );
}

int Cnf_DataWriteAndClauses	(	void *	p,
		Cnf_Dat_t *	pCnf
	)

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

Synopsis [Adds the OR-clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 627 of file cnfMan.c.

{
    sat_solver * pSat = (sat_solver *)p;
    Aig_Obj_t * pObj;
    int i, Lit;
    Aig_ManForEachCo( pCnf->pMan, pObj, i )
    {
        Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
            return 0;
    }
    return 1;
}

void Cnf_DataWriteIntoFile	(	Cnf_Dat_t *	p,
		char *	pFileName,
		int	fReadable,
		Vec_Int_t *	vForAlls,
		Vec_Int_t *	vExists
	)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file cnfMan.c.

{
    FILE * pFile;
    int * pLit, * pStop, i, VarId;
    if ( !strncmp(pFileName+strlen(pFileName)-3,".gz",3) ) 
    {
        Cnf_DataWriteIntoFileGz( p, pFileName, fReadable, vForAlls, vExists );
        return;
    }
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Cnf_WriteIntoFile(): Output file cannot be opened.\n" );
        return;
    }
    fprintf( pFile, "c Result of efficient AIG-to-CNF conversion using package CNF\n" );
    fprintf( pFile, "p cnf %d %d\n", p->nVars, p->nClauses );
    if ( vForAlls )
    {
        fprintf( pFile, "a " );
        Vec_IntForEachEntry( vForAlls, VarId, i )
            fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
        fprintf( pFile, "0\n" );
    }
    if ( vExists )
    {
        fprintf( pFile, "e " );
        Vec_IntForEachEntry( vExists, VarId, i )
            fprintf( pFile, "%d ", fReadable? VarId : VarId+1 );
        fprintf( pFile, "0\n" );
    }
    for ( i = 0; i < p->nClauses; i++ )
    {
        for ( pLit = p->pClauses[i], pStop = p->pClauses[i+1]; pLit < pStop; pLit++ )
            fprintf( pFile, "%d ", fReadable? Cnf_Lit2Var2(*pLit) : Cnf_Lit2Var(*pLit) );
        fprintf( pFile, "0\n" );
    }
    fprintf( pFile, "\n" );
    fclose( pFile );
}

void* Cnf_DataWriteIntoSolver	(	Cnf_Dat_t *	p,
		int	nFrames,
		int	fInit
	)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 463 of file cnfMan.c.

{
    return Cnf_DataWriteIntoSolverInt( sat_solver_new(), p, nFrames, fInit );
}

void* Cnf_DataWriteIntoSolverInt	(	void *	pSolver,
		Cnf_Dat_t *	p,
		int	nFrames,
		int	fInit
	)

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 370 of file cnfMan.c.

{
    sat_solver * pSat = (sat_solver *)pSolver;
    int i, f, status;
    assert( nFrames > 0 );
    assert( pSat );
//    pSat = sat_solver_new();
    sat_solver_setnvars( pSat, p->nVars * nFrames );
    for ( i = 0; i < p->nClauses; i++ )
    {
        if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
        {
            sat_solver_delete( pSat );
            return NULL;
        }
    }
    if ( nFrames > 1 )
    {
        Aig_Obj_t * pObjLo, * pObjLi;
        int nLitsAll, * pLits, Lits[2];
        nLitsAll = 2 * p->nVars;
        pLits = p->pClauses[0];
        for ( f = 1; f < nFrames; f++ )
        {
            // add equality of register inputs/outputs for different timeframes
            Aig_ManForEachLiLoSeq( p->pMan, pObjLi, pObjLo, i )
            {
                Lits[0] = (f-1)*nLitsAll + toLitCond( p->pVarNums[pObjLi->Id], 0 );
                Lits[1] =  f   *nLitsAll + toLitCond( p->pVarNums[pObjLo->Id], 1 );
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return NULL;
                }
                Lits[0]++;
                Lits[1]--;
                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
                {
                    sat_solver_delete( pSat );
                    return NULL;
                }
            }
            // add clauses for the next timeframe
            for ( i = 0; i < p->nLiterals; i++ )
                pLits[i] += nLitsAll;
            for ( i = 0; i < p->nClauses; i++ )
            {
                if ( !sat_solver_addclause( pSat, p->pClauses[i], p->pClauses[i+1] ) )
                {
                    sat_solver_delete( pSat );
                    return NULL;
                }
            }
        }
        // return literals to their original state
        nLitsAll = (f-1) * nLitsAll;
        for ( i = 0; i < p->nLiterals; i++ )
            pLits[i] -= nLitsAll;
    }
    if ( fInit )
    {
        Aig_Obj_t * pObjLo;
        int Lits[1];
        Aig_ManForEachLoSeq( p->pMan, pObjLo, i )
        {
            Lits[0] = toLitCond( p->pVarNums[pObjLo->Id], 1 );
            if ( !sat_solver_addclause( pSat, Lits, Lits + 1 ) )
            {
                sat_solver_delete( pSat );
                return NULL;
            }
        }
    }
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        sat_solver_delete( pSat );
        return NULL;
    }
    return pSat;
}

int Cnf_DataWriteOrClause	(	void *	p,
		Cnf_Dat_t *	pCnf
	)

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

Synopsis [Adds the OR-clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 571 of file cnfMan.c.

{
    sat_solver * pSat = (sat_solver *)p;
    Aig_Obj_t * pObj;
    int i, * pLits;
    pLits = ABC_ALLOC( int, Aig_ManCoNum(pCnf->pMan) );
    Aig_ManForEachCo( pCnf->pMan, pObj, i )
        pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
    if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManCoNum(pCnf->pMan) ) )
    {
        ABC_FREE( pLits );
        return 0;
    }
    ABC_FREE( pLits );
    return 1;
}

Cnf_Dat_t* Cnf_Derive	(	Aig_Man_t *	pAig,
		int	nOutputs
	)

Definition at line 165 of file cnfCore.c.

{
    Cnf_ManPrepare();
    return Cnf_DeriveWithMan( s_pManCnf, pAig, nOutputs );
}

Cnf_Dat_t* Cnf_DeriveFast	(	Aig_Man_t *	p,
		int	nOutputs
	)

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

Synopsis [Fast CNF computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 666 of file cnfFast.c.

{
    Cnf_Dat_t * pCnf = NULL;
    abctime clk;//, clkTotal = Abc_Clock();
//    printf( "\n" );
    Aig_ManCleanMarkAB( p );
    // create initial marking
    clk = Abc_Clock();
    Cnf_DeriveFastMark( p );
//    Abc_PrintTime( 1, "Marking", Abc_Clock() - clk );
    // compute CNF size
    clk = Abc_Clock();
    pCnf = Cnf_DeriveFastClauses( p, nOutputs );
//    Abc_PrintTime( 1, "Clauses", Abc_Clock() - clk );
    // derive the resulting CNF
    Aig_ManCleanMarkA( p );
//    Abc_PrintTime( 1, "TOTAL  ", Abc_Clock() - clkTotal );

//    printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d.   \n", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );

//    Cnf_DataFree( pCnf );
//    pCnf = NULL;
    return pCnf;
}

void Cnf_DeriveFastMark

(

Aig_Man_t *

p

)

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

Synopsis [Marks AIG for CNF computation.]

Description []

SideEffects []

SeeAlso []

Definition at line 297 of file cnfFast.c.

{
    Vec_Int_t * vSupps;
    Vec_Ptr_t * vLeaves, * vNodes;
    Aig_Obj_t * pObj, * pTemp, * pObjC, * pObj0, * pObj1;
    int i, k, nFans, Counter;

    vLeaves = Vec_PtrAlloc( 100 );
    vNodes  = Vec_PtrAlloc( 100 );
    vSupps  = Vec_IntStart( Aig_ManObjNumMax(p) );

    // mark CIs
    Aig_ManForEachCi( p, pObj, i )
        pObj->fMarkA = 1;

    // mark CO drivers
    Aig_ManForEachCo( p, pObj, i )
        Aig_ObjFanin0(pObj)->fMarkA = 1;

    // mark MUX/XOR nodes
    Aig_ManForEachNode( p, pObj, i )
    {
        assert( !pObj->fMarkB );
        if ( !Aig_ObjIsMuxType(pObj) )
            continue;
        pObj0 = Aig_ObjFanin0(pObj);
        if ( pObj0->fMarkB || Aig_ObjRefs(pObj0) > 1 )
            continue;
        pObj1 = Aig_ObjFanin1(pObj);
        if ( pObj1->fMarkB || Aig_ObjRefs(pObj1) > 1 )
            continue;
        // mark nodes
        pObj->fMarkB = 1;
        pObj0->fMarkB = 1;
        pObj1->fMarkB = 1;
        // mark inputs and outputs
        pObj->fMarkA = 1;
        Aig_ObjFanin0(pObj0)->fMarkA = 1;
        Aig_ObjFanin1(pObj0)->fMarkA = 1;
        Aig_ObjFanin0(pObj1)->fMarkA = 1;
        Aig_ObjFanin1(pObj1)->fMarkA = 1;
    }

    // mark nodes with multiple fanouts and pointed to by complemented edges
    Aig_ManForEachNode( p, pObj, i )
    {
        // mark nodes with many fanouts
        if ( Aig_ObjRefs(pObj) > 1 )
            pObj->fMarkA = 1;
        // mark nodes pointed to by a complemented edge
        if ( Aig_ObjFaninC0(pObj) && !Aig_ObjFanin0(pObj)->fMarkB )
            Aig_ObjFanin0(pObj)->fMarkA = 1;
        if ( Aig_ObjFaninC1(pObj) && !Aig_ObjFanin1(pObj)->fMarkB )
            Aig_ObjFanin1(pObj)->fMarkA = 1;
    }

    // compute supergate size for internal marked nodes
    Aig_ManForEachNode( p, pObj, i )
    {
        if ( !pObj->fMarkA )
            continue;
        if ( pObj->fMarkB )
        {
            if ( !Aig_ObjIsMuxType(pObj) )
                continue;
            pObjC = Aig_ObjRecognizeMux( pObj, &pObj1, &pObj0 );
            pObj0 = Aig_Regular(pObj0);
            pObj1 = Aig_Regular(pObj1);
            assert( pObj0->fMarkA );
            assert( pObj1->fMarkA );
//            if ( pObj0 == pObj1 )
//                continue;
            nFans = 1 + (pObj0 == pObj1);
            if ( !pObj0->fMarkB && !Aig_ObjIsCi(pObj0) && Aig_ObjRefs(pObj0) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj0)) < 3 )
            {
                pObj0->fMarkA = 0;
                continue;
            }
            if ( !pObj1->fMarkB && !Aig_ObjIsCi(pObj1) && Aig_ObjRefs(pObj1) == nFans && Vec_IntEntry(vSupps, Aig_ObjId(pObj1)) < 3 )
            {
                pObj1->fMarkA = 0;
                continue;
            }
            continue;
        }

        Cnf_CollectLeaves( pObj, vLeaves, 1 );
        Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), Vec_PtrSize(vLeaves) );
        if ( Vec_PtrSize(vLeaves) >= 6 )
            continue;
        Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pTemp, k )
        {
            pTemp = Aig_Regular(pTemp);
            assert( pTemp->fMarkA );
            if ( pTemp->fMarkB || Aig_ObjIsCi(pTemp) || Aig_ObjRefs(pTemp) > 1 )
                continue;
            assert( Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 0 );
            if ( Vec_PtrSize(vLeaves) - 1 + Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) > 6 )
                continue;
            pTemp->fMarkA = 0;
            Vec_IntWriteEntry( vSupps, Aig_ObjId(pObj), 6 );
//printf( "%d %d   ", Vec_PtrSize(vLeaves), Vec_IntEntry(vSupps, Aig_ObjId(pTemp)) );
            break;
        }
    }
    Aig_ManCleanMarkB( p );

    // check CO drivers
    Counter = 0;
    Aig_ManForEachCo( p, pObj, i )
        Counter += !Aig_ObjFanin0(pObj)->fMarkA;
    if ( Counter )
    printf( "PO-driver rule is violated %d times.\n", Counter );

    // check that the AND-gates are fine
    Counter = 0;
    Aig_ManForEachNode( p, pObj, i )
    {
        assert( pObj->fMarkB == 0 );
        if ( !pObj->fMarkA )
            continue;
        Cnf_CollectLeaves( pObj, vLeaves, 0 );
        if ( Vec_PtrSize(vLeaves) <= 6 )
            continue;
        Cnf_CollectVolume( p, pObj, vLeaves, vNodes );
        Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, k )
        {
            if ( Aig_ObjFaninC0(pTemp) && !Aig_ObjFanin0(pTemp)->fMarkA )
                Counter++;
            if ( Aig_ObjFaninC1(pTemp) && !Aig_ObjFanin1(pTemp)->fMarkA )
                Counter++;
        }
    }
    if ( Counter )
    printf( "AND-gate rule is violated %d times.\n", Counter );

    Vec_PtrFree( vLeaves );
    Vec_PtrFree( vNodes );
    Vec_IntFree( vSupps );
}

void Cnf_DeriveMapping

(

Cnf_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file cnfMap.c.

{
    Vec_Ptr_t * vSuper;
    Aig_Obj_t * pObj;
    Dar_Cut_t * pCut, * pCutBest;
    int i, k, AreaFlow, * pAreaFlows;
    // allocate area flows
    pAreaFlows = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
    memset( pAreaFlows, 0, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
    // visit the nodes in the topological order and update their best cuts
    vSuper = Vec_PtrAlloc( 100 );
    Aig_ManForEachNode( p->pManAig, pObj, i )
    {
        // go through the cuts
        pCutBest = NULL;
        Dar_ObjForEachCut( pObj, pCut, k )
        {
            pCut->fBest = 0;
            if ( k == 0 )
                continue;
            Cnf_CutAssignAreaFlow( p, pCut, pAreaFlows );
            if ( pCutBest == NULL || pCutBest->uSign > pCut->uSign || 
                (pCutBest->uSign == pCut->uSign && pCutBest->Value < pCut->Value) )
                 pCutBest = pCut;
        }
        // check the big cut
//        Aig_ObjCollectSuper( pObj, vSuper );
        // get the area flow of this cut
//        AreaFlow = Cnf_CutSuperAreaFlow( vSuper, pAreaFlows );
        AreaFlow = ABC_INFINITY;
        if ( AreaFlow >= (int)pCutBest->uSign )
        {
            pAreaFlows[pObj->Id] = pCutBest->uSign;
            pCutBest->fBest = 1;
        }
        else
        {
            pAreaFlows[pObj->Id] = AreaFlow;
            pObj->fMarkB = 1; // mark the special node
        }
    }
    Vec_PtrFree( vSuper );
    ABC_FREE( pAreaFlows );

/*
    // compute the area of mapping
    AreaFlow = 0;
    Aig_ManForEachCo( p->pManAig, pObj, i )
        AreaFlow += Dar_ObjBestCut(Aig_ObjFanin0(pObj))->uSign / 100 / Aig_ObjFanin0(pObj)->nRefs;
    printf( "Area of the network = %d.\n", AreaFlow );
*/
}

Vec_Int_t* Cnf_DeriveMappingArray

(

Aig_Man_t *

pAig

)

FUNCTION DECLARATIONS ///.

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file cnfCore.c.

{
    Vec_Int_t * vResult;
    Cnf_Man_t * p;
    Vec_Ptr_t * vMapped;
    Aig_MmFixed_t * pMemCuts;
    abctime clk;
    // allocate the CNF manager
    p = Cnf_ManStart();
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
clk = Abc_Clock();
    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = Abc_Clock() - clk;

    // find the mapping
clk = Abc_Clock();
    Cnf_DeriveMapping( p );
p->timeMap = Abc_Clock() - clk;
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
clk = Abc_Clock();
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 0 );
    vResult = Cnf_ManWriteCnfMapping( p, vMapped );
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = Abc_Clock() - clk;

   // reset reference counters
    Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
    Cnf_ManStop( p );
    return vResult;
}

Cnf_Dat_t* Cnf_DeriveOther	(	Aig_Man_t *	pAig,
		int	fSkipTtMin
	)

Definition at line 219 of file cnfCore.c.

{
    Cnf_ManPrepare();
    return Cnf_DeriveOtherWithMan( s_pManCnf, pAig, fSkipTtMin );
}

Cnf_Dat_t* Cnf_DeriveOtherWithMan	(	Cnf_Man_t *	p,
		Aig_Man_t *	pAig,
		int	fSkipTtMin
	)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file cnfCore.c.

{
    Cnf_Dat_t * pCnf;
    Vec_Ptr_t * vMapped;
    Aig_MmFixed_t * pMemCuts;
    abctime clk;
    // connect the managers
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
clk = Abc_Clock();
    pMemCuts = Dar_ManComputeCuts( pAig, 10, fSkipTtMin, 0 );
p->timeCuts = Abc_Clock() - clk;

    // find the mapping
clk = Abc_Clock();
    Cnf_DeriveMapping( p );
p->timeMap = Abc_Clock() - clk;
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
clk = Abc_Clock();
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 1 );
    pCnf = Cnf_ManWriteCnfOther( p, vMapped );
    pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = Abc_Clock() - clk;

   // reset reference counters
    Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
    return pCnf;
}

Cnf_Dat_t* Cnf_DeriveSimple	(	Aig_Man_t *	p,
		int	nOutputs
	)

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

Synopsis [Derives a simple CNF for the AIG.]

Description [The last argument lists the number of last outputs of the manager, which will not be converted into clauses. New variables will be introduced for these outputs.]

SideEffects []

SeeAlso []

Definition at line 587 of file cnfWrite.c.

{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    int i, nLiterals, nClauses, Number;

    // count the number of literals and clauses
    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + 3 * nOutputs;
    nClauses = 1 + 3 * Aig_ManNodeNum(p) + Aig_ManCoNum( p ) + nOutputs;

    // allocate CNF
    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
    pCnf->pMan = p;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;

    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
        pCnf->pVarNums[i] = -1;
    // assign variables to the last (nOutputs) POs
    Number = 1;
    if ( nOutputs )
    {
//        assert( nOutputs == Aig_ManRegNum(p) );
//        Aig_ManForEachLiSeq( p, pObj, i )
//            pCnf->pVarNums[pObj->Id] = Number++;
        Aig_ManForEachCo( p, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
    }
    // assign variables to the internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the PIs and constant node
    Aig_ManForEachCi( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
    pCnf->nVars = Number;
/*
    // print CNF numbers
    printf( "SAT numbers of each node:\n" );
    Aig_ManForEachObj( p, pObj, i )
        printf( "%d=%d ", pObj->Id, pCnf->pVarNums[pObj->Id] );
    printf( "\n" );
*/
    // assign the clauses
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Aig_ManForEachNode( p, pObj, i )
    {
        OutVar   = pCnf->pVarNums[ pObj->Id ];
        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];

        // positive phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar; 
        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
        // negative phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
    }
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar;  

    // write the output literals
    Aig_ManForEachCo( p, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        if ( i < Aig_ManCoNum(p) - nOutputs )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
        else
        {
            PoVar  = pCnf->pVarNums[ pObj->Id ];
            // first clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar; 
            *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
            // second clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar + 1; 
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
    return pCnf;
}

Cnf_Dat_t* Cnf_DeriveSimpleForRetiming

(

Aig_Man_t *

p

)

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

Synopsis [Derives a simple CNF for backward retiming computation.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses. New variables will be introduced for these outputs.]

SideEffects []

SeeAlso []

Definition at line 709 of file cnfWrite.c.

{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    int i, nLiterals, nClauses, Number;

    // count the number of literals and clauses
    nLiterals = 1 + 7 * Aig_ManNodeNum(p) + 5 * Aig_ManCoNum(p);
    nClauses = 1 + 3 * Aig_ManNodeNum(p) + 3 * Aig_ManCoNum(p);

    // allocate CNF
    pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
    memset( pCnf, 0, sizeof(Cnf_Dat_t) );
    pCnf->pMan = p;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;

    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
        pCnf->pVarNums[i] = -1;
    // assign variables to the last (nOutputs) POs
    Number = 1;
    Aig_ManForEachCo( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    // assign variables to the PIs and constant node
    Aig_ManForEachCi( p, pObj, i )
        pCnf->pVarNums[pObj->Id] = Number++;
    pCnf->pVarNums[Aig_ManConst1(p)->Id] = Number++;
    pCnf->nVars = Number;
    // assign the clauses
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Aig_ManForEachNode( p, pObj, i )
    {
        OutVar   = pCnf->pVarNums[ pObj->Id ];
        pVars[0] = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        pVars[1] = pCnf->pVarNums[ Aig_ObjFanin1(pObj)->Id ];

        // positive phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar; 
        *pLits++ = 2 * pVars[0] + !Aig_ObjFaninC0(pObj); 
        *pLits++ = 2 * pVars[1] + !Aig_ObjFaninC1(pObj); 
        // negative phase
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[0] + Aig_ObjFaninC0(pObj); 
        *pClas++ = pLits;
        *pLits++ = 2 * OutVar + 1; 
        *pLits++ = 2 * pVars[1] + Aig_ObjFaninC1(pObj); 
    }
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // write the output literals
    Aig_ManForEachCo( p, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        PoVar  = pCnf->pVarNums[ pObj->Id ];
        // first clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar; 
        *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
        // second clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        // final clause (init-state is always 0 -> set the output to 0)
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
    return pCnf;
}

Cnf_Dat_t* Cnf_DeriveWithMan	(	Cnf_Man_t *	p,
		Aig_Man_t *	pAig,
		int	nOutputs
	)

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

Synopsis [Converts AIG into the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file cnfCore.c.

{
    Cnf_Dat_t * pCnf;
    Vec_Ptr_t * vMapped;
    Aig_MmFixed_t * pMemCuts;
    abctime clk;
    // connect the managers
    p->pManAig = pAig;

    // generate cuts for all nodes, assign cost, and find best cuts
clk = Abc_Clock();
    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0, 0 );
p->timeCuts = Abc_Clock() - clk;

    // find the mapping
clk = Abc_Clock();
    Cnf_DeriveMapping( p );
p->timeMap = Abc_Clock() - clk;
//    Aig_ManScanMapping( p, 1 );

    // convert it into CNF
clk = Abc_Clock();
    Cnf_ManTransferCuts( p );
    vMapped = Cnf_ManScanMapping( p, 1, 1 );
    pCnf = Cnf_ManWriteCnf( p, vMapped, nOutputs );
    Vec_PtrFree( vMapped );
    Aig_MmFixedStop( pMemCuts, 0 );
p->timeSave = Abc_Clock() - clk;

   // reset reference counters
    Aig_ManResetRefs( pAig );
//ABC_PRT( "Cuts   ", p->timeCuts );
//ABC_PRT( "Map    ", p->timeMap  );
//ABC_PRT( "Saving ", p->timeSave );
    return pCnf;
}

void Cnf_ManFree

(

)

Definition at line 58 of file cnfCore.c.

{
    if ( s_pManCnf == NULL )
        return;
    Cnf_ManStop( s_pManCnf );
    s_pManCnf = NULL;
}

void Cnf_ManFreeCuts

(

Cnf_Man_t *

p

)

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 142 of file cnfPost.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_ManForEachObj( p->pManAig, pObj, i )
        if ( pObj->pData )
        {
            Cnf_CutFree( (Cnf_Cut_t *)pObj->pData );
            pObj->pData = NULL;
        }
}

int Cnf_ManMapForCnf

(

Cnf_Man_t *

p

)

void Cnf_ManPostprocess

(

Cnf_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file cnfPost.c.

{
    Cnf_Cut_t * pCut, * pCutFan, * pCutRes;
    Aig_Obj_t * pObj, * pFan;
    int Order[16], Costs[16];
    int i, k, fChanges;
    Aig_ManForEachNode( p->pManAig, pObj, i )
    {
        if ( pObj->nRefs == 0 )
            continue;
        pCut = Cnf_ObjBestCut(pObj);

        // sort fanins according to their size
        Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
        {
            Order[k] = k;
            Costs[k] = Aig_ObjIsNode(pFan)? Cnf_ObjBestCut(pFan)->Cost : 0;
        }
        // sort the cuts by Weight
        do {
            int Temp;
            fChanges = 0;
            for ( k = 0; k < pCut->nFanins - 1; k++ )
            {
                if ( Costs[Order[k]] <= Costs[Order[k+1]] )
                    continue;
                Temp = Order[k];
                Order[k] = Order[k+1];
                Order[k+1] = Temp;
                fChanges = 1;
            }
        } while ( fChanges );


//        Cnf_CutForEachLeaf( p->pManAig, pCut, pFan, k )
        for ( k = 0; (k < (int)(pCut)->nFanins) && ((pFan) = Aig_ManObj(p->pManAig, (pCut)->pFanins[Order[k]])); k++ )
        {
            if ( !Aig_ObjIsNode(pFan) )
                continue;
            assert( pFan->nRefs != 0 );
            if ( pFan->nRefs != 1 )
                continue;
            pCutFan = Cnf_ObjBestCut(pFan);
            // try composing these two cuts
//            Cnf_CutPrint( pCut );
            pCutRes = Cnf_CutCompose( p, pCut, pCutFan, pFan->Id );
//            Cnf_CutPrint( pCut );
//            printf( "\n" );
            // check if the cost if reduced
            if ( pCutRes == NULL || pCutRes->Cost == 127 || pCutRes->Cost > pCut->Cost + pCutFan->Cost )
            {
                if ( pCutRes )
                    Cnf_CutFree( pCutRes );
                continue;
            }
            // update the cut
            Cnf_ObjSetBestCut( pObj, pCutRes );
            Cnf_ObjSetBestCut( pFan, NULL );
            Cnf_CutUpdateRefs( p, pCut, pCutFan, pCutRes );
            assert( pFan->nRefs == 0 );
            Cnf_CutFree( pCut );
            Cnf_CutFree( pCutFan );
            break;
        }
    }
}

void Cnf_ManPrepare

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file cnfCore.c.

{
    if ( s_pManCnf == NULL )
    {
//        printf( "\n\nCreating CNF manager!!!!!\n\n" );
        s_pManCnf = Cnf_ManStart();
    }
}

Cnf_Man_t* Cnf_ManRead

(

)

Definition at line 54 of file cnfCore.c.

{
    return s_pManCnf;
}

Vec_Ptr_t* Cnf_ManScanMapping	(	Cnf_Man_t *	p,
		int	fCollect,
		int	fPreorder
	)

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

Synopsis [Computes area, references, and nodes used in the mapping.]

Description [Collects the nodes in reverse topological order.]

SideEffects []

SeeAlso []

Definition at line 170 of file cnfUtil.c.

{
    Vec_Ptr_t * vMapped = NULL;
    Aig_Obj_t * pObj;
    int i;
    // clean all references
    Aig_ManForEachObj( p->pManAig, pObj, i )
        pObj->nRefs = 0;
    // allocate the array
    if ( fCollect )
        vMapped = Vec_PtrAlloc( 1000 );
    // collect nodes reachable from POs in the DFS order through the best cuts
    p->aArea = 0;
    Aig_ManForEachCo( p->pManAig, pObj, i )
        p->aArea += Cnf_ManScanMapping_rec( p, Aig_ObjFanin0(pObj), vMapped, fPreorder );
//    printf( "Variables = %6d. Clauses = %8d.\n", vMapped? Vec_PtrSize(vMapped) + Aig_ManCiNum(p->pManAig) + 1 : 0, p->aArea + 2 );
    return vMapped;
}

Cnf_Man_t* Cnf_ManStart

(

)

FUNCTION DEFINITIONS ///.

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

Synopsis [Starts the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file cnfMan.c.

{
    Cnf_Man_t * p;
    int i;
    // allocate the manager
    p = ABC_ALLOC( Cnf_Man_t, 1 );
    memset( p, 0, sizeof(Cnf_Man_t) );
    // derive internal data structures
    Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
    // allocate memory manager for cuts
    p->pMemCuts = Aig_MmFlexStart();
    p->nMergeLimit = 10;
    // allocate temporary truth tables
    p->pTruths[0] = ABC_ALLOC( unsigned, 4 * Abc_TruthWordNum(p->nMergeLimit) );
    for ( i = 1; i < 4; i++ )
        p->pTruths[i] = p->pTruths[i-1] + Abc_TruthWordNum(p->nMergeLimit);
    p->vMemory = Vec_IntAlloc( 1 << 18 );
    return p;
}

void Cnf_ManStop

(

Cnf_Man_t *

p

)

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

Synopsis [Stops the fraiging manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file cnfMan.c.

{
    Vec_IntFree( p->vMemory );
    ABC_FREE( p->pTruths[0] );
    Aig_MmFlexStop( p->pMemCuts, 0 );
    ABC_FREE( p->pSopSizes );
    ABC_FREE( p->pSops[1] );
    ABC_FREE( p->pSops );
    ABC_FREE( p );
}

void Cnf_ManTransferCuts

(

Cnf_Man_t *

p

)

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

Synopsis [Transfers cuts of the mapped nodes into internal representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 117 of file cnfPost.c.

{
    Aig_Obj_t * pObj;
    int i;
    Aig_MmFlexRestart( p->pMemCuts );
    Aig_ManForEachObj( p->pManAig, pObj, i )
    {
        if ( Aig_ObjIsNode(pObj) && pObj->nRefs > 0 )
            pObj->pData = Cnf_CutCreate( p, pObj );
        else
            pObj->pData = NULL;
    }
}

Cnf_Dat_t* Cnf_ManWriteCnf	(	Cnf_Man_t *	p,
		Vec_Ptr_t *	vMapped,
		int	nOutputs
	)

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

Synopsis [Derives CNF for the mapping.]

Description [The last argument shows the number of last outputs of the manager, which will not be converted into clauses but the new variables for which will be introduced.]

SideEffects []

SeeAlso []

Definition at line 199 of file cnfWrite.c.

{
    int fChangeVariableOrder = 0; // should be set to 0 to improve performance
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Cnf_Cut_t * pCut;
    Vec_Int_t * vCover, * vSopTemp;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    unsigned uTruth;
    int i, k, nLiterals, nClauses, Cube, Number;

    // count the number of literals and clauses
    nLiterals = 1 + Aig_ManCoNum( p->pManAig ) + 3 * nOutputs;
    nClauses = 1 + Aig_ManCoNum( p->pManAig ) + nOutputs;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
            nClauses += Vec_IntSize(pCut->vIsop[1]);
        }
        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
            nClauses += Vec_IntSize(pCut->vIsop[0]);
        }
//printf( "%d ", nClauses-(1 + Aig_ManCoNum( p->pManAig )) );
    }
//printf( "\n" );

    // allocate CNF
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->pMan = p->pManAig;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses = nClauses;
    pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
    // create room for variable numbers
    pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
    for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
        pCnf->pVarNums[i] = -1;

    if ( !fChangeVariableOrder )
    {
        // assign variables to the last (nOutputs) POs
        Number = 1;
        if ( nOutputs )
        {
            if ( Aig_ManRegNum(p->pManAig) == 0 )
            {
                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                Aig_ManForEachCo( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number++;
            }
            else
            {
                assert( nOutputs == Aig_ManRegNum(p->pManAig) );
                Aig_ManForEachLiSeq( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number++;
            }
        }
        // assign variables to the internal nodes
        Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
        // assign variables to the PIs and constant node
        Aig_ManForEachCi( p->pManAig, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number++;
        pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number++;
        pCnf->nVars = Number;
    }
    else
    {
        // assign variables to the last (nOutputs) POs
        Number = Aig_ManObjNumMax(p->pManAig) + 1;
        pCnf->nVars = Number + 1;
        if ( nOutputs )
        {
            if ( Aig_ManRegNum(p->pManAig) == 0 )
            {
                assert( nOutputs == Aig_ManCoNum(p->pManAig) );
                Aig_ManForEachCo( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number--;
            }
            else
            {
                assert( nOutputs == Aig_ManRegNum(p->pManAig) );
                Aig_ManForEachLiSeq( p->pManAig, pObj, i )
                    pCnf->pVarNums[pObj->Id] = Number--;
            }
        }
        // assign variables to the internal nodes
        Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number--;
        // assign variables to the PIs and constant node
        Aig_ManForEachCi( p->pManAig, pObj, i )
            pCnf->pVarNums[pObj->Id] = Number--;
        pCnf->pVarNums[Aig_ManConst1(p->pManAig)->Id] = Number--;
        assert( Number >= 0 );
    }

    // assign the clauses
    vSopTemp = Vec_IntAlloc( 1 << 16 );
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        pCut = Cnf_ObjBestCut( pObj );

        // save variables of this cut
        OutVar = pCnf->pVarNums[ pObj->Id ];
        for ( k = 0; k < (int)pCut->nFanins; k++ )
        {
            pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ];
            assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
        }

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[1];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }

        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[0];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + 1; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
    }
    Vec_IntFree( vSopTemp );
 
    // write the constant literal
    OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ];
    assert( OutVar <= Aig_ManObjNumMax(p->pManAig) );
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // write the output literals
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        OutVar = pCnf->pVarNums[ Aig_ObjFanin0(pObj)->Id ];
        if ( i < Aig_ManCoNum(p->pManAig) - nOutputs )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
        else
        {
            PoVar = pCnf->pVarNums[ pObj->Id ];
            // first clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar; 
            *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
            // second clause
            *pClas++ = pLits;
            *pLits++ = 2 * PoVar + 1; 
            *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
        }
    }

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
    return pCnf;
}

Vec_Int_t* Cnf_ManWriteCnfMapping	(	Cnf_Man_t *	p,
		Vec_Ptr_t *	vMapped
	)

DECLARATIONS ///.

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

FileName [cnfWrite.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [AIG-to-CNF conversion.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - April 28, 2007.]

Revision [

Id:

cnfWrite.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Derives CNF mapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file cnfWrite.c.

{
    Vec_Int_t * vResult;
    Aig_Obj_t * pObj;
    Cnf_Cut_t * pCut;
    int i, k, nOffset;
    nOffset = Aig_ManObjNumMax(p->pManAig);
    vResult = Vec_IntStart( nOffset );
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );
        assert( pCut->nFanins < 5 );
        Vec_IntWriteEntry( vResult, Aig_ObjId(pObj), nOffset );
        Vec_IntPush( vResult, *Cnf_CutTruth(pCut) );
        for ( k = 0; k < pCut->nFanins; k++ )
            Vec_IntPush( vResult, pCut->pFanins[k] );
        for (      ; k < 4; k++ )
            Vec_IntPush( vResult, -1 );
        nOffset += 5;
    }
    return vResult;
}

Cnf_Dat_t* Cnf_ManWriteCnfOther	(	Cnf_Man_t *	p,
		Vec_Ptr_t *	vMapped
	)

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

Synopsis [Derives CNF for the mapping.]

Description [Derives CNF with obj IDs as SAT vars and mapping of objects into clauses (pObj2Clause and pObj2Count).]

SideEffects []

SeeAlso []

Definition at line 419 of file cnfWrite.c.

{
    Aig_Obj_t * pObj;
    Cnf_Dat_t * pCnf;
    Cnf_Cut_t * pCut;
    Vec_Int_t * vCover, * vSopTemp;
    int OutVar, PoVar, pVars[32], * pLits, ** pClas;
    unsigned uTruth;
    int i, k, nLiterals, nClauses, Cube;

    // count the number of literals and clauses
    nLiterals = 1 + 4 * Aig_ManCoNum( p->pManAig );
    nClauses  = 1 + 2 * Aig_ManCoNum( p->pManAig );
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        assert( Aig_ObjIsNode(pObj) );
        pCut = Cnf_ObjBestCut( pObj );
        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[1], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[1]);
            nClauses += Vec_IntSize(pCut->vIsop[1]);
        }
        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            nLiterals += Cnf_SopCountLiterals( p->pSops[uTruth], p->pSopSizes[uTruth] ) + p->pSopSizes[uTruth];
            assert( p->pSopSizes[uTruth] >= 0 );
            nClauses += p->pSopSizes[uTruth];
        }
        else
        {
            nLiterals += Cnf_IsopCountLiterals( pCut->vIsop[0], pCut->nFanins ) + Vec_IntSize(pCut->vIsop[0]);
            nClauses += Vec_IntSize(pCut->vIsop[0]);
        }
    }

    // allocate CNF
    pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
    pCnf->pMan = p->pManAig;
    pCnf->nLiterals = nLiterals;
    pCnf->nClauses  = nClauses;
    pCnf->pClauses  = ABC_ALLOC( int *, nClauses + 1 );
    pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
    pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
    // create room for variable numbers
    pCnf->pObj2Clause = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
    pCnf->pObj2Count  = ABC_ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
    for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
        pCnf->pObj2Clause[i] = pCnf->pObj2Count[i] = -1;
    pCnf->nVars = Aig_ManObjNumMax(p->pManAig);

    // clear the PI counters
    Aig_ManForEachCi( p->pManAig, pObj, i )
        pCnf->pObj2Count[pObj->Id] = 0;

    // assign the clauses
    vSopTemp = Vec_IntAlloc( 1 << 16 );
    pLits = pCnf->pClauses[0];
    pClas = pCnf->pClauses;
    Vec_PtrForEachEntry( Aig_Obj_t *, vMapped, pObj, i )
    {
        // remember the starting clause
        pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
        pCnf->pObj2Count[pObj->Id] = 0;

        // get the best cut
        pCut = Cnf_ObjBestCut( pObj );
        // save variables of this cut
        OutVar = pObj->Id;
        for ( k = 0; k < (int)pCut->nFanins; k++ )
        {
            pVars[k] = pCut->pFanins[k];
            assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) );
        }

        // positive polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & *Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[1];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
        pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);

        // negative polarity of the cut
        if ( pCut->nFanins < 5 )
        {
            uTruth = 0xFFFF & ~*Cnf_CutTruth(pCut);
            Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vSopTemp );
            vCover = vSopTemp;
        }
        else
            vCover = pCut->vIsop[0];
        Vec_IntForEachEntry( vCover, Cube, k )
        {
            *pClas++ = pLits;
            *pLits++ = 2 * OutVar + 1; 
            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
        }
        pCnf->pObj2Count[pObj->Id] += Vec_IntSize(vCover);
    }
    Vec_IntFree( vSopTemp );

    // write the output literals
    Aig_ManForEachCo( p->pManAig, pObj, i )
    {
        // remember the starting clause
        pCnf->pObj2Clause[pObj->Id] = pClas - pCnf->pClauses;
        pCnf->pObj2Count[pObj->Id] = 2;
        // get variables
        OutVar = Aig_ObjFanin0(pObj)->Id;
        PoVar = pObj->Id;
        // first clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar; 
        *pLits++ = 2 * OutVar + !Aig_ObjFaninC0(pObj); 
        // second clause
        *pClas++ = pLits;
        *pLits++ = 2 * PoVar + 1; 
        *pLits++ = 2 * OutVar + Aig_ObjFaninC0(pObj); 
    }
 
    // remember the starting clause
    pCnf->pObj2Clause[Aig_ManConst1(p->pManAig)->Id] = pClas - pCnf->pClauses;
    pCnf->pObj2Count[Aig_ManConst1(p->pManAig)->Id] = 1;
    // write the constant literal
    OutVar = Aig_ManConst1(p->pManAig)->Id;
    *pClas++ = pLits;
    *pLits++ = 2 * OutVar; 

    // verify that the correct number of literals and clauses was written
    assert( pLits - pCnf->pClauses[0] == nLiterals );
    assert( pClas - pCnf->pClauses == nClauses );
//Cnf_DataPrint( pCnf, 1 );
    return pCnf;
}

static Cnf_Cut_t* Cnf_ObjBestCut ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 105 of file cnf.h.

{ return (Cnf_Cut_t *)pObj->pData;  }

static void Cnf_ObjSetBestCut ( Aig_Obj_t *  pObj, Cnf_Cut_t *  pCut  )

inlinestatic

Definition at line 106 of file cnf.h.

{ pObj->pData = pCut;  }

void Cnf_ReadMsops	(	char **	ppSopSizes,
		char ***	ppSops
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Prepares the data for MSOPs of 4-variable functions.]

Description []

SideEffects []

SeeAlso []

Definition at line 4537 of file cnfData.c.

{
    unsigned uMasks[4][2] = {
        { 0x5555, 0xAAAA },
        { 0x3333, 0xCCCC },
        { 0x0F0F, 0xF0F0 },
        { 0x00FF, 0xFF00 }
    };
    char Map[256], * pPrev, * pMemory;
    char * pSopSizes, ** pSops;
    int i, k, b, Size;

    // map chars into their numbers
    for ( i = 0; i < 256; i++ )
        Map[i] = (char)(-1);
    for ( i = 0; i < 81; i++ )
        Map[(int)s_Data3[i]] = (char)i;

    // count the number of strings
    for ( Size = 0; s_Data4[Size] && Size < 100000; Size++ );
    assert( Size < 100000 );

    // allocate memory
    pMemory = ABC_ALLOC( char, Size * 75 );
    // copy the array into memory
    for ( i = 0; i < Size; i++ )
        for ( k = 0; k < 75; k++ )
            if ( s_Data4[i][k] == ' ' )
                pMemory[i*75+k] = (char)(-1);
            else
                pMemory[i*75+k] = Map[(int)s_Data4[i][k]];

    // set pointers and compute SOP sizes
    pSopSizes = ABC_ALLOC( char, 65536 );
    pSops = ABC_ALLOC( char *, 65536 );
    pSopSizes[0] = 0;
    pSops[0] = NULL;
    pPrev = pMemory;
    for ( k = 0, i = 1; i < 65536; k++ )
        if ( pMemory[k] == (char)(-1) )
        {
            pSopSizes[i] = pMemory + k - pPrev; 
            pSops[i++] = pPrev;
            pPrev = pMemory + k + 1;
        }
    *ppSopSizes = pSopSizes;
    *ppSops = pSops;

    // verify the results - derive truth table from SOP
    for ( i = 1; i < 65536; i++ )
    {
        int uTruth = 0, uCube, Lit;
        for ( k = 0; k < pSopSizes[i]; k++ )
        {
            uCube = 0xFFFF;
            Lit = pSops[i][k];
            for ( b = 3; b >= 0; b-- )
            {
                if ( Lit % 3 == 0 )
                    uCube &= uMasks[b][0];
                else if ( Lit % 3 == 1 )
                    uCube &= uMasks[b][1];
                Lit = Lit / 3;
            }
            uTruth |= uCube;
        }
        assert( uTruth == i );
    }
}

void Cnf_SopConvertToVector	(	char *	pSop,
		int	nCubes,
		Vec_Int_t *	vCover
	)

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

Synopsis [Writes the cover into the array.]

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file cnfWrite.c.

{
    int Lits[4], Cube, iCube, i, b;
    Vec_IntClear( vCover );
    for ( i = 0; i < nCubes; i++ )
    {
        Cube = pSop[i];
        for ( b = 0; b < 4; b++ )
        {
            if ( Cube % 3 == 0 )
                Lits[b] = 1;
            else if ( Cube % 3 == 1 )
                Lits[b] = 2;
            else
                Lits[b] = 0;
            Cube = Cube / 3;
        }
        iCube = 0;
        for ( b = 0; b < 4; b++ )
            iCube = (iCube << 2) | Lits[b];
        Vec_IntPush( vCover, iCube );
    }
}

static Dar_Cut_t* Dar_ObjBestCut ( Aig_Obj_t *  pObj )

inlinestatic

Definition at line 97 of file cnf.h.

{ Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }