relationGeneration.cpp File Reference

#include <cassert>
#include "misc/vec/vec.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "relationGeneration.hpp"

Include dependency graph for relationGeneration.cpp:

Go to the source code of this file.

Namespaces
namespace	eSLIM

Functions
ABC_NAMESPACE_HEADER_START void *	Mf_ManGenerateCnf (Gia_Man_t *pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose)
void *	Cnf_DataWriteIntoSolver (Cnf_Dat_t *p, int nFrames, int fInit)
Vec_Int_t *	Gia_ManCollectNodeTfos (Gia_Man_t *p, int *pNodes, int nNodes)
Vec_Int_t *	Gia_ManCollectNodeTfis (Gia_Man_t *p, Vec_Int_t *vNodes)

Function Documentation

Cnf_DataWriteIntoSolver()

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

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

Synopsis [Writes CNF into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file cnfMan.c.

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

Here is the call graph for this function:

Gia_ManCollectNodeTfis()

Vec_Int_t * Gia_ManCollectNodeTfis	(	Gia_Man_t *	p,
		Vec_Int_t *	vNodes )

Definition at line 1093 of file giaQbf.c.

{
    Vec_Int_t * vTfi = Vec_IntAlloc( 100 );
    Gia_Obj_t * pObj; int i, Id;
    Gia_ManIncrementTravId( p );
    Gia_ManForEachObjVec( vNodes, p, pObj, i )
        if ( Gia_ObjIsCo(pObj) )
            Gia_ObjSetTravIdCurrentId( p, Gia_ObjFaninId0p(p, pObj) );
    Gia_ManForEachAndReverse( p, pObj, i ) {
        if ( !Gia_ObjIsTravIdCurrentId(p, i) )
            continue;        
        Gia_ObjSetTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i));
        Gia_ObjSetTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i));
    }
    Gia_ManForEachCiId( p, Id, i )
        if ( Gia_ObjIsTravIdCurrentId(p, Id) )
            Vec_IntPush( vTfi, Id );
    Gia_ManForEachAnd( p, pObj, i )
        if ( Gia_ObjIsTravIdCurrentId(p, i) )
            Vec_IntPush( vTfi, i );
    return vTfi;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManCollectNodeTfos()

Vec_Int_t * Gia_ManCollectNodeTfos	(	Gia_Man_t *	p,
		int *	pNodes,
		int	nNodes )

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

Synopsis [Derive the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 1075 of file giaQbf.c.

{
    Vec_Int_t * vTfo = Vec_IntAlloc( 100 );
    Gia_Obj_t * pObj; int i;
    Gia_ManIncrementTravId( p );
    for ( i = 0; i < nNodes; i++ )
        Gia_ObjSetTravIdCurrentId( p, pNodes[i] );
    Gia_ManForEachAnd( p, pObj, i ) {
        if ( Gia_ObjIsTravIdCurrentId(p, i) )
            continue;
        if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0(pObj, i)) || Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId1(pObj, i)) )
            Gia_ObjSetTravIdCurrentId( p, i ), Vec_IntPush( vTfo, i );
    }
    Gia_ManForEachCo( p, pObj, i )
        if ( Gia_ObjIsTravIdCurrentId(p, Gia_ObjFaninId0p(p, pObj)) )
            Vec_IntPush( vTfo, Gia_ObjId(p, pObj) );
    return vTfo;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Mf_ManGenerateCnf()

ABC_NAMESPACE_HEADER_START void * Mf_ManGenerateCnf	(	Gia_Man_t *	pGia,
		int	nLutSize,
		int	fCnfObjIds,
		int	fAddOrCla,
		int	fMapping,
		int	fVerbose )

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

FileName [relationGeneration.cpp]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Using Exact Synthesis with the SAT-based Local Improvement Method (eSLIM).]

Synopsis [Procedures for computing Boolean relations.]

Author [Franz-Xaver Reichl]

Affiliation [University of Freiburg]

Date [Ver. 1.0. Started - March 2025.]

Revision [

Id

relationGeneration.cpp,v 1.00 2025/03/17 00:00:00 Exp

]

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

Synopsis [CNF generation]

Description []

SideEffects []

SeeAlso []

Definition at line 1877 of file giaMf.c.

{
    Gia_Man_t * pNew;
    Jf_Par_t Pars, * pPars = &Pars;
    assert( nLutSize >= 3 && nLutSize <= 8 );
    Mf_ManSetDefaultPars( pPars );
    pPars->fGenCnf     = 1;
    pPars->fCoarsen    = !fCnfObjIds;
    pPars->nLutSize    = nLutSize;
    pPars->fCnfObjIds  = fCnfObjIds;
    pPars->fAddOrCla   = fAddOrCla;
    pPars->fCnfMapping = fMapping;
    pPars->fVerbose    = fVerbose;
    pNew = Mf_ManPerformMapping( pGia, pPars );
    Gia_ManStopP( &pNew );
//    Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );
    return pGia->pData;
}

Here is the caller graph for this function: