cnfCore.c File Reference

#include "cnf.h"

Go to the source code of this file.

Functions
void	Cnf_ManPrepare ()
	FUNCTION DEFINITIONS ///. More...
Cnf_Man_t *	Cnf_ManRead ()
void	Cnf_ManFree ()
Vec_Int_t *	Cnf_DeriveMappingArray (Aig_Man_t *pAig)
	FUNCTION DECLARATIONS ///. More...
Cnf_Dat_t *	Cnf_DeriveWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int nOutputs)
Cnf_Dat_t *	Cnf_Derive (Aig_Man_t *pAig, int nOutputs)
Cnf_Dat_t *	Cnf_DeriveOtherWithMan (Cnf_Man_t *p, Aig_Man_t *pAig, int fSkipTtMin)
Cnf_Dat_t *	Cnf_DeriveOther (Aig_Man_t *pAig, int fSkipTtMin)

Variables
static ABC_NAMESPACE_IMPL_START Cnf_Man_t *	s_pManCnf = NULL
	DECLARATIONS ///. More...

Function Documentation

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

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

Variable Documentation

ABC_NAMESPACE_IMPL_START Cnf_Man_t* s_pManCnf = NULL

static

DECLARATIONS ///.

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

FileName [cnfCore.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:

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

]

Definition at line 30 of file cnfCore.c.