sbdCnf.c File Reference

#include "sbdInt.h"

Include dependency graph for sbdCnf.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Sbd_PrintCnf (Vec_Str_t *vCnf)
	DECLARATIONS ///.
int	Sbd_TruthToCnf (word Truth, int nVars, Vec_Int_t *vCover, Vec_Str_t *vCnf)
void	Sbd_TranslateCnf (Vec_Wec_t *vRes, Vec_Str_t *vCnf, Vec_Int_t *vFaninMap, int iPivotVar)

Function Documentation

Sbd_PrintCnf()

ABC_NAMESPACE_IMPL_START void Sbd_PrintCnf

(

Vec_Str_t *

vCnf

)

DECLARATIONS ///.

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

FileName [sbdCnf.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based optimization using internal don't-cares.]

Synopsis [CNF computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

sbdCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file sbdCnf.c.

{
    signed char Entry;
    int i, Lit;
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        Lit = (int)Entry;
        if ( Lit == -1 )
            printf( "\n" );
        else
            printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
    }
}

Sbd_TranslateCnf()

void Sbd_TranslateCnf	(	Vec_Wec_t *	vRes,
		Vec_Str_t *	vCnf,
		Vec_Int_t *	vFaninMap,
		int	iPivotVar )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file sbdCnf.c.

{
    Vec_Int_t * vClause;
    signed char Entry;
    int i, Lit;
    Vec_WecClear( vRes );
    vClause = Vec_WecPushLevel( vRes );
    Vec_StrForEachEntry( vCnf, Entry, i )
    {
        if ( (int)Entry == -1 )
        {
            vClause = Vec_WecPushLevel( vRes );
            continue;
        }
        Lit = Abc_Lit2LitV( Vec_IntArray(vFaninMap), (int)Entry );
        Lit = Abc_LitNotCond( Lit, Abc_Lit2Var(Lit) == iPivotVar );
        Vec_IntPush( vClause, Lit );
    }
}

Sbd_TruthToCnf()

int Sbd_TruthToCnf	(	word	Truth,
		int	nVars,
		Vec_Int_t *	vCover,
		Vec_Str_t *	vCnf )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 70 of file sbdCnf.c.

{
    Vec_StrClear( vCnf );
    if ( Truth == 0 || ~Truth == 0 )
    {
//        assert( nVars == 0 );
        Vec_StrPush( vCnf, (char)(Truth == 0) );
        Vec_StrPush( vCnf, (char)-1 );
        return 1;
    }
    else 
    {
        int i, k, c, RetValue, Literal, Cube, nCubes = 0;
        assert( nVars > 0 );
        for ( c = 0; c < 2; c ++ )
        {
            Truth = c ? ~Truth : Truth;
            RetValue = Kit_TruthIsop( (unsigned *)&Truth, nVars, vCover, 0 );
            assert( RetValue == 0 );
            nCubes += Vec_IntSize( vCover );
            Vec_IntForEachEntry( vCover, Cube, i )
            {
                for ( k = 0; k < nVars; k++ )
                {
                    Literal = 3 & (Cube >> (k << 1));
                    if ( Literal == 1 )      // '0'  -> pos lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 0) );
                    else if ( Literal == 2 ) // '1'  -> neg lit
                        Vec_StrPush( vCnf, (char)Abc_Var2Lit(k, 1) );
                    else if ( Literal != 0 )
                        assert( 0 );
                }
                Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
                Vec_StrPush( vCnf, (char)-1 );
            }
        }
        return nCubes;
    }
}

Here is the call graph for this function: