bmcMaj3.c File Reference

#include "bmc.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
#include "sat/glucose/AbcGlucose.h"
#include "opt/dau/dau.h"

Include dependency graph for bmcMaj3.c:

Go to the source code of this file.

Classes
struct	Maj3_Man_t_
struct	Zyx_Man_t_

Macros
#define	MAJ3_OBJS   32
	DECLARATIONS ///.

Typedefs
typedef struct Maj3_Man_t_	Maj3_Man_t
typedef struct Zyx_Man_t_	Zyx_Man_t

Functions
Vec_Wrd_t *	Maj3_ManTruthTables (Maj3_Man_t *p)
void	Maj3_ManFirstAndLevel (Vec_Int_t *vLevels, int Firsts[MAJ3_OBJS], int Levels[MAJ3_OBJS], int nVars, int nObjs)
int	Maj3_ManMarkup (Maj3_Man_t *p)
void	Maj3_ManVarMapPrint (Maj3_Man_t *p)
void	Maj3_PrintClause (int *pLits, int nLits)
int	Maj3_ManAddCnfStart (Maj3_Man_t *p)
int	Maj3_ManAddCnf (Maj3_Man_t *p, int iMint)
int	Maj3_ManAddConstraintsLazy (Maj3_Man_t *p)
Maj3_Man_t *	Maj3_ManAlloc (int nVars, int nNodes, Vec_Int_t *vLevels)
void	Maj3_ManFree (Maj3_Man_t *p)
int	Maj3_ManExactSynthesis (int nVars, int nNodes, int fVerbose, Vec_Int_t *vLevels)
int	Maj3_ManTest ()
void	Zyx_SetConstVar (Zyx_Man_t *p, int Var, int Value)
void	Zyx_ManSetupVars (Zyx_Man_t *p)
int	Zyx_ManAddCnfStart (Zyx_Man_t *p)
void	Zyx_ManPrintVarMap (Zyx_Man_t *p, int fSat)
void	Zyx_PrintClause (int *pLits, int nLits)
Vec_Wrd_t *	Zyx_ManTruthTables (Zyx_Man_t *p, word *pTruth)
Vec_Int_t *	Zyx_ManCreateSymVarPairs (word *pTruth, int nVars)
Zyx_Man_t *	Zyx_ManAlloc (Bmc_EsPar_t *pPars, word *pTruth)
void	Zyx_ManFree (Zyx_Man_t *p)
int	Zyx_ManCollectFanins (Zyx_Man_t *p, int i)
int	Zyx_ManAddCnfLazyTopo (Zyx_Man_t *p)
int	Zyx_ManAddCnfBlockSolution (Zyx_Man_t *p)
int	Zyx_ManAddCnfLazyFunc2 (Zyx_Man_t *p, int iMint)
int	Zyx_ManAddCnfLazyFunc (Zyx_Man_t *p, int iMint)
void	Zyx_ManExactSynthesis (Bmc_EsPar_t *pPars)
int	Zyx_TestGetTruthTablePars (char *pFileName, word *pTruth, int *nVars, int *nLutSize, int *nNodes)
Vec_Wrd_t *	Zyx_TestCreateTruthTables (int nVars, int nNodes)
int	Zyx_TestReadNode (char *pLine, Vec_Wrd_t *vTruths, int nVars, int nLutSize, int iObj)
void	Zyx_TestExact (char *pFileName)

Macro Definition Documentation

MAJ3_OBJS

#define MAJ3_OBJS   32

DECLARATIONS ///.

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

FileName [bmcMaj3.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Majority gate synthesis.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

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

]

Definition at line 34 of file bmcMaj3.c.

Typedef Documentation

Maj3_Man_t

typedef struct Maj3_Man_t_ Maj3_Man_t

Definition at line 36 of file bmcMaj3.c.

Zyx_Man_t

typedef struct Zyx_Man_t_ Zyx_Man_t

Definition at line 551 of file bmcMaj3.c.

Function Documentation

Maj3_ManAddCnf()

int Maj3_ManAddCnf	(	Maj3_Man_t *	p,
		int	iMint )

Definition at line 323 of file bmcMaj3.c.

{
    // input values
    int i, k, j, n, * pVals = p->ObjVals;
    for ( i = 0; i < p->nVars; i++ )
        pVals[i] = (iMint >> i) & 1;
    // first node value
    pVals[p->nVars] = (pVals[0] && pVals[1]) || (pVals[0] && pVals[2]) || (pVals[1] && pVals[2]);
    // last node value
    pVals[p->nObjs-1] = Maj3_ManValue(iMint, p->nVars);
    // intermediate node values
    for ( i = p->nVars + 1; i < p->nObjs - 1; i++ )
        pVals[i] = p->iVar++;
    //printf( "Adding clauses for minterm %d.\n", iMint );
    bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
    for ( n = 0; n < 2; n++ )
    for ( i = p->nVars + 1; i < p->nObjs; i++ )
    {
        //printf( "\nNode %d. Phase %d.\n", i, n );
        for ( k = 0; k < p->nObjs; k++ ) if ( p->VarMarks[i][k] >= 1 )
        {
            // add first input
            int pLits[5], nLits = 0;
            if ( pVals[k] == !n )
                continue;
            if ( pVals[k] > 1 )
                pLits[nLits++] = Abc_Var2Lit( pVals[k], n );
            if ( p->VarMarks[i][k] > 1 )
                pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 1 );
            for ( j = k+1; j < p->nObjs; j++ ) if ( p->VarMarks[i][j] >= 1 )
            {
                // add second input
                int nLits2 = nLits;
                if ( pVals[j] == !n )
                    continue;
                if ( pVals[j] > 1 )
                    pLits[nLits2++] = Abc_Var2Lit( pVals[j], n );
                if ( p->VarMarks[i][j] > 1 )
                    pLits[nLits2++] = Abc_Var2Lit( p->VarMarks[i][j], 1 );
                // add output
                if ( pVals[i] == n )
                    continue;
                if ( pVals[i] > 1 )
                    pLits[nLits2++] = Abc_Var2Lit( pVals[i], !n );
                assert( nLits2 > 0 && nLits2 <= 5 );
                //Maj3_PrintClause( pLits, nLits2 );
                if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits2 ) )
                    return 0;
            }
        }
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManAddCnfStart()

int Maj3_ManAddCnfStart

(

Maj3_Man_t *

p

)

Definition at line 273 of file bmcMaj3.c.

{
    int i, k, status, nLits, pLits[MAJ3_OBJS];
    // nodes have at least one fanin
    //printf( "Fanin clauses:\n" );
    for ( i = p->nVars; i < p->nObjs; i++ )
    {
        // check if it is already connected
        int Count = 0;
        for ( k = 0; k < p->nObjs; k++ ) 
            Count += p->VarMarks[i][k] == 1;
        assert( Count <= 3 );
        if ( Count == 3 )
            continue;
        // collect connections
        nLits = 0;
        for ( k = 0; k < p->nObjs; k++ ) 
            if ( p->VarMarks[i][k] > 1 )
                pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
        //Maj3_PrintClause( pLits, nLits );
        assert( nLits > 0 );
        if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
            assert(0);
    }
    // nodes have at least one fanout
    //printf( "Fanout clauses:\n" );
    for ( k = 0; k < p->nObjs-1; k++ )
    {
        // check if it is already connected
        int Count = 0;
        for ( i = 0; i < p->nObjs; i++ ) 
            Count += p->VarMarks[i][k] == 1;
        assert( Count <= 3 );
        if ( Count > 0 )
            continue;
        // collect connections
        nLits = 0;
        for ( i = 0; i < p->nObjs; i++ ) 
            if ( p->VarMarks[i][k] > 1 )
                pLits[nLits++] = Abc_Var2Lit( p->VarMarks[i][k], 0 );
        //Maj3_PrintClause( pLits, nLits );
        //assert( nLits > 0 );
        if ( nLits > 0 && !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
            assert(0);
    }
    status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
    assert( status == GLUCOSE_SAT );
    Maj3_ManVarMapPrint( p );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManAddConstraintsLazy()

int Maj3_ManAddConstraintsLazy

(

Maj3_Man_t *

p

)

Definition at line 376 of file bmcMaj3.c.

{
    int i, pFanins[MAJ3_OBJS], nConstr = 0;
    //Maj3_ManVarMapPrint( p );
    for ( i = p->nVars+1; i < p->nObjs; i++ )
    {
        int nFanins = Maj3_ManFindFanin( p, i, pFanins );
        if ( nFanins == 3 )
            continue;
        //printf( "Node %d has %d fanins.\n", i, nFanins );
        nConstr++;
        if ( nFanins < 3 )
        {
            assert( p->nLits[0] > 0 );
            //Maj3_PrintClause( p->pLits[0], p->nLits[0] );
            if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                return -1;
        }
        else if ( nFanins > 3 )
        {
            int nLits = Abc_MinInt(4 - p->nLits[2], p->nLits[1]);
            assert( nLits > 0 );
            //Maj3_PrintClause( p->pLits[1], nLits );
            if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], nLits ) )
                return -1;
        }
    }
    return nConstr;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManAlloc()

Maj3_Man_t * Maj3_ManAlloc	(	int	nVars,
		int	nNodes,
		Vec_Int_t *	vLevels )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 417 of file bmcMaj3.c.

{
    Maj3_Man_t * p = ABC_CALLOC( Maj3_Man_t, 1 );
    p->vLevels    = vLevels;
    p->nVars      = nVars;
    p->nNodes     = nNodes;
    p->nObjs      = nVars + nNodes;
    p->nWords     = Abc_TtWordNum(nVars);
    p->iVar       = Maj3_ManMarkup( p );
    p->vInfo      = Maj3_ManTruthTables( p );
    p->pSat       = bmcg_sat_solver_start();
    bmcg_sat_solver_set_nvars( p->pSat, p->iVar );
    Maj3_ManAddCnfStart( p );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManExactSynthesis()

int Maj3_ManExactSynthesis	(	int	nVars,
		int	nNodes,
		int	fVerbose,
		Vec_Int_t *	vLevels )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file bmcMaj3.c.

{
    Maj3_Man_t * p;  abctime clkTotal = Abc_Clock();
    int i, status, nLazy, nLazyAll = 0, iMint = 0;
    printf( "Running exact synthesis for %d-input majority with %d MAJ3 gates...\n", nVars, nNodes );
    p = Maj3_ManAlloc( nVars, nNodes, vLevels );
    for ( i = 0; iMint != -1; i++ )
    {
        abctime clk = Abc_Clock();
        if ( !Maj3_ManAddCnf( p, iMint ) )
            break;
        while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
        {
            nLazy = Maj3_ManAddConstraintsLazy( p );
            if ( nLazy == -1 )
            {
                printf( "Became UNSAT after adding lazy constraints.\n" );
                status = GLUCOSE_UNSAT;
                break;
            }
            //printf( "Added %d lazy constraints.\n\n", nLazy );
            if ( nLazy == 0 )
                break;
            nLazyAll += nLazy;
        }
        if ( fVerbose )
        {
            printf( "Iter %3d : ", i );
            Extra_PrintBinary( stdout, (unsigned *)&iMint, p->nVars );
            printf( "  Var =%5d  ", p->iVar );
            printf( "Cla =%6d  ", bmcg_sat_solver_clausenum(p->pSat) );
            printf( "Conf =%9d  ", bmcg_sat_solver_conflictnum(p->pSat) );
            printf( "Lazy =%9d  ", nLazyAll );
            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
        }
        if ( status == GLUCOSE_UNSAT )
        {
            printf( "The problem has no solution.\n" );
            break;
        }
        iMint = Maj3_ManEval( p );
    }
    if ( iMint == -1 )
        Maj3_ManPrintSolution( p );
    Maj3_ManFree( p );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
    return iMint == -1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManFirstAndLevel()

void Maj3_ManFirstAndLevel	(	Vec_Int_t *	vLevels,
		int	Firsts[MAJ3_OBJS],
		int	Levels[MAJ3_OBJS],
		int	nVars,
		int	nObjs )

Definition at line 89 of file bmcMaj3.c.

{
    int i, k, Entry, Obj = 0;
    Firsts[0] = Obj;
    for ( k = 0; k < nVars; k++ )
        Levels[Obj++] = 0;
    Vec_IntReverseOrder( vLevels );
    Vec_IntForEachEntry( vLevels, Entry, i )
    {
        Firsts[i+1] = Obj;
        for ( k = 0; k < Entry; k++ )
            Levels[Obj++] = i+1;
    }
    Vec_IntReverseOrder( vLevels );
    assert( Obj == nObjs );
}

Here is the caller graph for this function:

Maj3_ManFree()

void Maj3_ManFree

(

Maj3_Man_t *

p

)

Definition at line 432 of file bmcMaj3.c.

{
    bmcg_sat_solver_stop( p->pSat );
    Vec_WrdFree( p->vInfo );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManMarkup()

int Maj3_ManMarkup

(

Maj3_Man_t *

p

)

Definition at line 105 of file bmcMaj3.c.

{
    int nSatVars = 2; // SAT variable counter
    int nLevels = Vec_IntSize(p->vLevels);
    int nSecond = Vec_IntEntry(p->vLevels, 1);
    int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
    assert( Vec_IntEntry(p->vLevels, 0) == 1 );
    assert( p->nObjs <= MAJ3_OBJS );
    assert( p->nNodes == Vec_IntSum(p->vLevels) );
    Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
    // create map 
    for ( i = 0; i < p->nObjs; i++ )
    for ( k = 0; k < p->nObjs; k++ )
        p->VarMarks[i][k] = -1;
    for ( k = 0; k < 3; k++ ) // first node
        p->VarMarks[p->nVars][k] = 1;
    for ( k = 0; k < nSecond; k++ ) // top node
        p->VarMarks[p->nObjs-1][p->nObjs-2-k] = 1;
    for ( k = 2; k < nLevels; k++ ) // cascade
        p->VarMarks[Firsts[k]][Firsts[k-1]] = 1;
    for ( i = p->nVars+1; i < (nSecond == 3 ? p->nObjs-1 : p->nObjs); i++ )
        for ( k = 0; k < Firsts[Levels[i]]; k++ )
            if ( p->VarMarks[i][k] == -1 )
                p->VarMarks[i][k] = nSatVars++;
    //printf( "The number of variables is %d.\n", nSatVars );
    return nSatVars;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_ManTest()

int Maj3_ManTest

(

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 510 of file bmcMaj3.c.

{
/*
    int nVars    =  5;
    int nNodes   =  4;
    int fVerbose =  1;
    int Levels[MAJ3_OBJS] = { 1, 2, 1 };
    Vec_Int_t vLevels = { 3, 3, Levels };
*/
 
    int nVars    =  7;
    int nNodes   =  7;
    int fVerbose =  1;
    int Levels[MAJ3_OBJS] = { 1, 2, 2, 2 };
    Vec_Int_t vLevels = { 4, 4, Levels };
 
/*
    int nVars    =  9;
    int nNodes   = 10;
    int fVerbose =  1;
    int Levels[MAJ3_OBJS] = { 1, 2, 3, 2, 2 };
    Vec_Int_t vLevels = { 5, 5, Levels };
*/
/*
    int nVars    =  9;
    int nNodes   = 10;
    int fVerbose =  1;
    int Levels[MAJ3_OBJS] = { 1, 1, 1, 1, 1, 1, 1, 1, 1, 1 };
    Vec_Int_t vLevels = { 10, 10, Levels };
*/
 
//    Maj3_Man_t * p = Maj3_ManAlloc( nVars, nNodes, &vLevels );
//    Maj3_ManFree( p );
    Maj3_ManExactSynthesis( nVars, nNodes, fVerbose, &vLevels );
    return 0;
}

Here is the call graph for this function:

Maj3_ManTruthTables()

Vec_Wrd_t * Maj3_ManTruthTables

(

Maj3_Man_t *

p

)

Definition at line 77 of file bmcMaj3.c.

{
    Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) ); 
    int i, nMints = Abc_MaxInt( 64, 1 << p->nVars );
    for ( i = 0; i < p->nVars; i++ )
        Abc_TtIthVar( Maj3_ManTruth(p, i), i, p->nVars );
    for ( i = 0; i < nMints; i++ )
        if ( Maj3_ManValue(i, p->nVars) )
            Abc_TtSetBit( Maj3_ManTruth(p, p->nObjs), i );
    //Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
    return vInfo;
}

Here is the caller graph for this function:

Maj3_ManVarMapPrint()

void Maj3_ManVarMapPrint

(

Maj3_Man_t *

p

)

Definition at line 132 of file bmcMaj3.c.

{
    int i, k, Firsts[MAJ3_OBJS], Levels[MAJ3_OBJS];
    Maj3_ManFirstAndLevel( p->vLevels, Firsts, Levels, p->nVars, p->nObjs );
    // print
    printf( "Variable map for problem with %d inputs, %d nodes and %d levels: ", p->nVars, p->nNodes, Vec_IntSize(p->vLevels) );
    Vec_IntPrint( p->vLevels );
    printf( "    " );
    printf( "      " );
    for ( i = 0; i < p->nObjs; i++ )
        printf( "%3d  ", i );
    printf( "\n" );
    for ( i = p->nObjs-1; i >= p->nVars; i-- )
    {
        printf( " %2d ", i );
        printf( " %2d   ", Levels[i] );
        for ( k = 0; k < p->nObjs; k++ )
            if ( p->VarMarks[i][k] == -1 )
                printf( "  .  " );
            else if ( p->VarMarks[i][k] == 1 )
                printf( "  +  " );
            else 
                printf( "%3d%c ", p->VarMarks[i][k], bmcg_sat_solver_read_cex_varvalue(p->pSat, p->VarMarks[i][k]) ? '+' : ' ' );
        printf( "\n" );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Maj3_PrintClause()

void Maj3_PrintClause	(	int *	pLits,
		int	nLits )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 266 of file bmcMaj3.c.

{
    int i;
    for ( i = 0; i < nLits; i++ )
        printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
    printf( "\n" );
}

Zyx_ManAddCnfBlockSolution()

int Zyx_ManAddCnfBlockSolution

(

Zyx_Man_t *

p

)

Definition at line 986 of file bmcMaj3.c.

{
    Vec_Int_t * vLits = Vec_IntAlloc( 100 ); int i, k;
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
    {
        int nFanins = Zyx_ManCollectFanins( p, i );
        assert( nFanins == p->pPars->nLutSize );
        for ( k = 0; k < p->pPars->nLutSize; k++ )
            Vec_IntPush( vLits, Abc_Var2Lit(Zyx_TopoVar(p, i, p->pFanins[i][k]), 1) );
    }
    //Zyx_ManPrintVarMap( p, 1 );
    //Zyx_PrintClause( Vec_IntArray(vLits), Vec_IntSize(vLits) );
    if ( !bmcg_sat_solver_addclause( p->pSat, Vec_IntArray(vLits), Vec_IntSize(vLits) ) )
        return 0;
    Vec_IntFree( vLits );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManAddCnfLazyFunc()

int Zyx_ManAddCnfLazyFunc	(	Zyx_Man_t *	p,
		int	iMint )

Definition at line 1059 of file bmcMaj3.c.

{
    int i, k, n, j, s, t, u;
    //printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
    assert( !p->pPars->fMajority && p->pPars->nLutSize < 4 );
    p->Counts[iMint]++;
    if ( p->pPars->nLutSize == 2 )
    {
        for ( i = p->pPars->nVars; i < p->nObjs; i++ )
        for ( s = 0;               s < i;        s++ )
        for ( t = s+1;             t < i;        t++ )
        {
            p->pFanins[i][0] = s;
            p->pFanins[i][1] = t;
            for ( k = 0; k <= p->LutMask; k++ )
            for ( n = 0; n < 2; n++ )
            {
                p->nLits[0] = 0;
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
                for ( j = 0; j < p->pPars->nLutSize; j++ )
                {
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
                }
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
                if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                    return 0;
            }
        }
    }
    else if ( p->pPars->nLutSize == 3 )
    {
        for ( i = p->pPars->nVars; i < p->nObjs; i++ )
        for ( s = 0;               s < i;        s++ )
        for ( t = s+1;             t < i;        t++ )
        for ( u = t+1;             u < i;        u++ )
        {
            p->pFanins[i][0] = s;
            p->pFanins[i][1] = t;
            p->pFanins[i][2] = u;
            for ( k = 0; k <= p->LutMask; k++ )
            for ( n = 0; n < 2; n++ )
            {
                p->nLits[0] = 0;
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
                for ( j = 0; j < p->pPars->nLutSize; j++ )
                {
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
                }
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
                if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                    return 0;
            }
        }
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManAddCnfLazyFunc2()

int Zyx_ManAddCnfLazyFunc2	(	Zyx_Man_t *	p,
		int	iMint )

Definition at line 1003 of file bmcMaj3.c.

{
    int i, k, n, j, s;
    assert( !p->pPars->fMajority || p->pPars->nLutSize == 3 );
    //printf( "Adding functionality clauses for minterm %d.\n", iMint );
    p->Counts[iMint]++;
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
    {
        int nFanins = Zyx_ManCollectFanins( p, i );
        assert( nFanins == p->pPars->nLutSize );
        if ( p->pPars->fMajority )
        {
            int Sets[3][2] = {{0, 1}, {0, 2}, {1, 2}};
            for ( k = 0; k < 3; k++ )
            {
                if ( Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][Sets[k][0]], p->pFanins[i][Sets[k][1]]) )
                    continue;
                for ( n = 0; n < 2; n++ )
                {
                    p->nLits[0] = 0;
                    for ( s = 0; s < 2; s++ )
                    {
                        p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][Sets[k][s]]), 1 );
                        p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][Sets[k][s]]), n );
                    }
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
                    if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                        return 0;
                }
            }
        }
        else
        {
            if ( p->pPars->nLutSize == 2 && Zyx_ManIsUsed2(p, iMint, i, p->pFanins[i][0], p->pFanins[i][1]) )
                continue;
            if ( p->pPars->nLutSize == 3 && Zyx_ManIsUsed3(p, iMint, i, p->pFanins[i][0], p->pFanins[i][1], p->pFanins[i][2]) )
                continue;
            for ( k = 0; k <= p->LutMask; k++ )
            for ( n = 0; n < 2; n++ )
            {
                p->nLits[0] = 0;
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_FuncVar(p, i, k), n );
                for ( j = 0; j < p->pPars->nLutSize; j++ )
                {
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_TopoVar(p, i, p->pFanins[i][j]), 1 );
                    p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, p->pFanins[i][j]), (k >> j) & 1 );
                }
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit( Zyx_MintVar(p, iMint, i), !n );
                if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                    return 0;
            }
        }
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManAddCnfLazyTopo()

int Zyx_ManAddCnfLazyTopo

(

Zyx_Man_t *

p

)

Definition at line 857 of file bmcMaj3.c.

{
    int i, k, j, Entry[2], Node[2], nLazy = 0;
    // fanin count
    //printf( "Adding topology clauses.\n" );
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
    {
        int nFanins = Zyx_ManCollectFanins( p, i );
        if ( nFanins == p->pPars->nLutSize )
            continue;
        nLazy++;
        assert( nFanins == p->nLits[1] );
        if ( p->nLits[1] > p->pPars->nLutSize )
        {
            p->nLits[1] = p->pPars->nLutSize + 1;
            //Zyx_PrintClause( p->pLits[1], p->nLits[1] );
            if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[1], p->nLits[1] ) )
                return -1;
        }
        else // if ( p->nLits[1] < p->pPars->nLutSize )
        {
            //Zyx_PrintClause( p->pLits[0], p->nLits[0] );
            if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                return -1;
        }
    }
    if ( nLazy || !p->pPars->fOrderNodes )
        return nLazy;
    // ordering
    for ( i = p->pPars->nVars + 1; i < p->nObjs; i++ )
    {
        for ( k = p->pPars->nLutSize - 1; k >= 0; k-- )
            if ( p->pFanins[i-1][k] != p->pFanins[i][k] )
                break;
        if ( k == -1 ) // fanins are equal
        {
            if ( p->pPars->fMajority )
                continue;
            // compare by LUT functions
            for ( k = p->LutMask; k >= 0; k-- )
                if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) != 
                     bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i  , k)) )
                    break;
            if ( k == -1 ) // truth tables cannot be equal
                continue;
            // rule out these truth tables
            if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 0 && 
                 bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i  , k)) == 1 )
            {
                continue;
            }
            nLazy++;
            assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, k)) == 1 );
            assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i  , k)) == 0 );
            // rule out this order
            p->nLits[0] = 0;
            for ( j = p->LutMask; j >= k; j-- )
            {
                int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i-1, j));
                int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_FuncVar(p, i,   j));
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i-1, j), ValA );
                p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_FuncVar(p, i,   j), ValB );
            }
            if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
                return -1;
            continue;
        }
        if ( p->pFanins[i-1][k] < p->pFanins[i][k] )
        {
            assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i][k])) == 0 );
            assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i  , p->pFanins[i][k])) == 1 );
            continue;
        }
        nLazy++;
        assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, p->pFanins[i-1][k])) == 1 );
        assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i  , p->pFanins[i-1][k])) == 0 );
        // rule out this order
        p->nLits[0] = 0;
        for ( j = p->pFanins[i-1][k]; j < p->nObjs-1; j++ )
        {
            int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i-1, j));
            int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i,   j));
            p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i-1, j), ValA );
            p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, i,   j), ValB );
        }
        //printf( "\n" );
        //Zyx_ManPrintVarMap( p, 1 );
        //Zyx_PrintClause( p->pLits[0], p->nLits[0] );
        if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
            return -1;
        //break;
    }
    // check symmetric variables
    Vec_IntForEachEntryDouble( p->vPairs, Entry[0], Entry[1], k )
    {
        assert( Entry[0] < Entry[1] );
        for ( j = 0; j < 2; j++ )
        {
            Node[j] = -1;
            for ( i = p->pPars->nVars; i < p->nObjs; i++ )
                if ( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, Entry[j])) )
                {
                    Node[j] = i;
                    break;
                }
            assert( Node[j] >= p->pPars->nVars );
        }
        // compare the nodes
        if ( Node[0] <= Node[1] )
            continue;
        assert( Node[0] > Node[1] );
        // create blocking clause
        nLazy++;
        assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[0])) == 0 );
        assert( bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, Node[1], Entry[1])) == 1 );
        // rule out this order
        p->nLits[0] = 0;
        for ( j = p->pPars->nVars; j <= Node[1]; j++ )
        {
            int ValA = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[0]));
            int ValB = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, j, Entry[1]));
            p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[0]), ValA );
            p->pLits[0][p->nLits[0]++] = Abc_Var2Lit(Zyx_TopoVar(p, j, Entry[1]), ValB );
        }
        if ( !bmcg_sat_solver_addclause( p->pSat, p->pLits[0], p->nLits[0] ) )
            return -1;
    }
    return nLazy;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManAddCnfStart()

int Zyx_ManAddCnfStart

(

Zyx_Man_t *

p

)

Definition at line 653 of file bmcMaj3.c.

{
    // nodes have fanins
    int i, k, pLits[MAJ3_OBJS];
    //printf( "Adding initial clauses:\n" );
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
    {
        int nLits = 0;
        for ( k = 0; k < i; k++ )
            pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
        assert( nLits > 0 );
        if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
            return 0;
    }
 
    // nodes have fanouts
    for ( k = 0; k < p->nObjs-1; k++ )
    {
        int nLits = 0;
        for ( i = p->pPars->nVars; i < p->nObjs; i++ )
            pLits[nLits++] = Abc_Var2Lit( Zyx_TopoVar(p, i, k), 0 );
        assert( nLits > 0 );
        if ( !bmcg_sat_solver_addclause( p->pSat, pLits, nLits ) )
            return 0;
    }
 
    // two input functions
    if ( p->pPars->nLutSize != 2 )
        return 1;
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
    {
        for ( k = 0; k < 3; k++ )
        {
            pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), k==1 );
            pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), k==2 );
            pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), k!=0 );
            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
                return 0;
        }
        if ( p->pPars->fOnlyAnd )
        {
            pLits[0] = Abc_Var2Lit( Zyx_FuncVar(p, i, 1), 1 );
            pLits[1] = Abc_Var2Lit( Zyx_FuncVar(p, i, 2), 1 );
            pLits[2] = Abc_Var2Lit( Zyx_FuncVar(p, i, 3), 0 );
            if ( !bmcg_sat_solver_addclause( p->pSat, pLits, 3 ) )
                return 0;
        }
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManAlloc()

Zyx_Man_t * Zyx_ManAlloc	(	Bmc_EsPar_t *	pPars,
		word *	pTruth )

Definition at line 793 of file bmcMaj3.c.

{
    Zyx_Man_t * p = ABC_CALLOC( Zyx_Man_t, 1 );
    p->pPars      = pPars;
    p->pTruth     = pTruth;
    p->nObjs      = p->pPars->nVars + p->pPars->nNodes;
    p->nWords     = Abc_TtWordNum(p->pPars->nVars);
    p->LutMask    = (1 << p->pPars->nLutSize) - 1;
    p->TopoBase   = (1 << p->pPars->nLutSize) * p->pPars->nNodes;
    p->MintBase   = p->TopoBase + p->pPars->nNodes * p->nObjs;
    p->vVarValues = Vec_IntStartFull( p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
    p->vMidMints  = Vec_IntAlloc( 1 << p->pPars->nVars );
    p->vInfo      = Zyx_ManTruthTables( p, pTruth );
    p->vPairs     = Zyx_ManCreateSymVarPairs( p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : pTruth, p->pPars->nVars );
    p->pSat       = bmcg_sat_solver_start();
    if ( pPars->fUseIncr )
    {
        if ( p->pPars->nLutSize == 2 || p->pPars->fMajority )
            p->vUsed2     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs );
        else if ( p->pPars->nLutSize == 3 )
            p->vUsed3     = Vec_BitStart( (1 << p->pPars->nVars) * p->pPars->nNodes * p->nObjs * p->nObjs * p->nObjs );
    }
    bmcg_sat_solver_set_nvars( p->pSat, p->MintBase + (1 << p->pPars->nVars) * p->nObjs );
    Zyx_ManSetupVars( p );
    Zyx_ManAddCnfStart( p );
    Zyx_ManPrintVarMap( p, 0 );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManCollectFanins()

int Zyx_ManCollectFanins	(	Zyx_Man_t *	p,
		int	i )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 844 of file bmcMaj3.c.

{
    int k, Val;
    assert( i >= p->pPars->nVars && i < p->nObjs );
    p->nLits[0] = p->nLits[1] = 0;
    for ( k = 0; k < i; k++ )
    {
        Val = bmcg_sat_solver_read_cex_varvalue(p->pSat, Zyx_TopoVar(p, i, k));
        p->pFanins[i][p->nLits[1]] = k;
        p->pLits[Val][p->nLits[Val]++] = Abc_Var2Lit(Zyx_TopoVar(p, i, k), Val);
    }
    return p->nLits[1];
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManCreateSymVarPairs()

Vec_Int_t * Zyx_ManCreateSymVarPairs	(	word *	pTruth,
		int	nVars )

Definition at line 772 of file bmcMaj3.c.

{
    Vec_Int_t * vPairs = Vec_IntAlloc( 100 ); 
    int i, k, nWords = Abc_TtWordNum(nVars);
    word Cof0[64], Cof1[64]; 
    word Cof01[64], Cof10[64];
    assert( nVars <= 12 );
    for ( i = 0; i < nVars; i++ )
    {
        Abc_TtCofactor0p( Cof0, pTruth, nWords, i );
        Abc_TtCofactor1p( Cof1, pTruth, nWords, i );
        for ( k = i+1; k < nVars; k++ )
        {
            Abc_TtCofactor1p( Cof01, Cof0, nWords, k );
            Abc_TtCofactor0p( Cof10, Cof1, nWords, k );
            if ( Abc_TtEqual( Cof01, Cof10, nWords ) )
                 Vec_IntPushTwo( vPairs, i, k );
        }
    }
    return vPairs;
}

Here is the caller graph for this function:

Zyx_ManExactSynthesis()

void Zyx_ManExactSynthesis

(

Bmc_EsPar_t *

pPars

)

Definition at line 1262 of file bmcMaj3.c.

{
    int status, Iter, iMint = 0, fCompl = 0, nLazyAll = 0, nSols = 0;
    abctime clkTotal = Abc_Clock(), clk = Abc_Clock();  Zyx_Man_t * p; 
    word pTruth[16]; 
    if ( !pPars->fMajority )
    {
        Abc_TtReadHex( pTruth, pPars->pTtStr );
        if ( pTruth[0] & 1 ) { fCompl = 1; Abc_TtNot( pTruth, Abc_TtWordNum(pPars->nVars) ); }
    }
    assert( pPars->nVars <= 10 );
    assert( pPars->nLutSize <= 6 );
    p = Zyx_ManAlloc( pPars, pPars->fMajority ? NULL : pTruth );
    printf( "Running exact synthesis for %d-input function with %d %d-input %s...\n", 
        p->pPars->nVars, p->pPars->nNodes, p->pPars->nLutSize, p->pPars->fMajority ? "MAJ-gates" : "LUTs" );
    for ( Iter = 0 ; ; Iter++ )
    {
        while ( (status = bmcg_sat_solver_solve(p->pSat, NULL, 0)) == GLUCOSE_SAT )
        {
            int nLazy = Zyx_ManAddCnfLazyTopo( p );
            if ( nLazy == -1 )
            {
                printf( "Became UNSAT after adding lazy constraints.\n" );
                status = GLUCOSE_UNSAT;
                break;
            }
            //printf( "Added %d lazy constraints.\n\n", nLazy );
            if ( nLazy == 0 )
                break;
            nLazyAll += nLazy;
        }
        if ( status == GLUCOSE_UNSAT )
            break;
        // find mismatch
        iMint = Zyx_ManEval( p );
        if ( iMint == -1 )
        {
            if ( pPars->fEnumSols )
            {
                nSols++;
                if ( pPars->fVerbose )
                {
                    Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
                    clk = Abc_Clock();
                }
                Zyx_ManPrintSolution( p, fCompl, nSols==1 );
                if ( !Zyx_ManAddCnfBlockSolution( p ) )
                {
                    status = GLUCOSE_UNSAT;
                    break;
                }
                continue;
            }
            else
                break;
        }
        if ( pPars->fUseIncr ? !Zyx_ManAddCnfLazyFunc2(p, iMint) : !Zyx_ManAddCnfLazyFunc(p, iMint) )
        {
            printf( "Became UNSAT after adding constraints for minterm %d\n", iMint );
            status = GLUCOSE_UNSAT;
            break;
        }
        status = bmcg_sat_solver_solve( p->pSat, NULL, 0 );
        if ( pPars->fVerbose && (!pPars->fUseIncr || Iter % 100 == 0) )
        {
            Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clk );
            clk = Abc_Clock();
        }
        if ( status == GLUCOSE_UNSAT )
            break;
    }
    if ( pPars->fVerbose )
        Zyx_ManPrint( p, Iter, iMint, nLazyAll, Abc_Clock() - clkTotal );
    if ( pPars->fEnumSols )
        printf( "Finished enumerating %d solutions.\n", nSols );
    else if ( iMint == -1 )
        Zyx_ManPrintSolution( p, fCompl, 1 );
    else
        printf( "The problem has no solution.\n" );
    //Zyx_ManEvalStats( p );
    printf( "Added = %d.  Tried = %d.  ", p->nUsed[1], p->nUsed[0] );
    Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
    Zyx_ManFree( p );
}

Here is the call graph for this function:

Zyx_ManFree()

void Zyx_ManFree

(

Zyx_Man_t *

p

)

Definition at line 821 of file bmcMaj3.c.

{
    bmcg_sat_solver_stop( p->pSat );
    Vec_WrdFree( p->vInfo );
    Vec_BitFreeP( &p->vUsed2 );
    Vec_BitFreeP( &p->vUsed3 );
    Vec_IntFree( p->vPairs );
    Vec_IntFree( p->vMidMints );
    Vec_IntFree( p->vVarValues );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManPrintVarMap()

void Zyx_ManPrintVarMap	(	Zyx_Man_t *	p,
		int	fSat )

Definition at line 703 of file bmcMaj3.c.

{
    int i, k, nTopoVars = 0;
    printf( "      " );
    for ( k = 0; k < p->nObjs-1; k++ )
        printf( "%3d  ", k );
    printf( "\n" );
    for ( i = p->nObjs-1; i >= p->pPars->nVars; i-- )
    {
        printf( "%3d   ", i );
        for ( k = 0; k < p->nObjs-1; k++ )
        {
            int iVar = Zyx_TopoVar(p, i, k);
            if ( Vec_IntEntry(p->vVarValues, iVar) == -1 )
                printf( "%3d%c ", iVar, (fSat && bmcg_sat_solver_read_cex_varvalue(p->pSat, iVar)) ? '*' : ' ' ), nTopoVars++;
            else
                printf( "%3d  ", Vec_IntEntry(p->vVarValues, iVar) );
        }
        printf( "\n" );
    }
    if ( fSat ) return;
    printf( "Using %d active functionality vars and %d active topology vars (out of %d SAT vars).\n", 
        p->pPars->fMajority ? 0 : p->pPars->nNodes * p->LutMask, nTopoVars, bmcg_sat_solver_varnum(p->pSat) );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManSetupVars()

void Zyx_ManSetupVars

(

Zyx_Man_t *

p

)

Definition at line 628 of file bmcMaj3.c.

{
    int i, k, m;
    word * pSpec = p->pPars->fMajority ? Zyx_ManTruth(p, p->nObjs) : p->pTruth;
    // set unused functionality vars to 0
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
        Zyx_SetConstVar( p, Zyx_FuncVar(p, i, 0), 0 );
    // set unused topology vars
    for ( i = p->pPars->nVars; i < p->nObjs; i++ )
        for ( k = i; k < p->nObjs; k++ )
            Zyx_SetConstVar( p, Zyx_TopoVar(p, i, k), 0 );
    // connect topmost node
    Zyx_SetConstVar( p, Zyx_TopoVar(p, p->nObjs-1, p->nObjs-2), 1 );
    // connect first node
    if ( p->pPars->fMajority )
        for ( k = 0; k < p->pPars->nVars; k++ )
            Zyx_SetConstVar( p, Zyx_TopoVar(p, p->pPars->nVars, k), k < 3 );
    // set minterm vars
    for ( m = 0; m < (1 << p->pPars->nVars); m++ )
    {
        for ( i = 0; i < p->pPars->nVars; i++ )
            Zyx_SetConstVar( p, Zyx_MintVar(p, m, i), (m >> i) & 1 );
        Zyx_SetConstVar( p, Zyx_MintVar(p, m, p->nObjs-1), Abc_TtGetBit(pSpec, m) );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_ManTruthTables()

Vec_Wrd_t * Zyx_ManTruthTables	(	Zyx_Man_t *	p,
		word *	pTruth )

Definition at line 753 of file bmcMaj3.c.

{
    Vec_Wrd_t * vInfo = p->vInfo = Vec_WrdStart( p->nWords * (p->nObjs + 1) ); 
    int i, nMints = Abc_MaxInt( 64, 1 << p->pPars->nVars );
    assert( p->pPars->fMajority == (pTruth == NULL) );
    for ( i = 0; i < p->pPars->nVars; i++ )
        Abc_TtIthVar( Zyx_ManTruth(p, i), i, p->pPars->nVars );
    if ( p->pPars->fMajority )
    {
        for ( i = 0; i < nMints; i++ )
            if ( Zyx_ManValue(i, p->pPars->nVars) )
                Abc_TtSetBit( Zyx_ManTruth(p, p->nObjs), i );
        for ( i = 0; i < nMints; i++ )
            if ( Abc_TtBitCount16(i) == p->pPars->nVars/2 || Abc_TtBitCount16(i) == p->pPars->nVars/2+1 )
                Vec_IntPush( p->vMidMints, i );
    }
    //Dau_DsdPrintFromTruth( Zyx_ManTruth(p, p->nObjs), p->pPars->nVars );
    return vInfo;
}

Here is the caller graph for this function:

Zyx_PrintClause()

void Zyx_PrintClause	(	int *	pLits,
		int	nLits )

Definition at line 727 of file bmcMaj3.c.

{
    int i;
    for ( i = 0; i < nLits; i++ )
        printf( "%c%d ", Abc_LitIsCompl(pLits[i]) ? '-' : '+', Abc_Lit2Var(pLits[i]) );
    printf( "\n" );
}

Zyx_SetConstVar()

void Zyx_SetConstVar	(	Zyx_Man_t *	p,
		int	Var,
		int	Value )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 619 of file bmcMaj3.c.

{
    int iLit = Abc_Var2Lit( Var, !Value );
    int status = bmcg_sat_solver_addclause( p->pSat, &iLit, 1 );
    assert( status );
    assert( Vec_IntEntry(p->vVarValues, Var) == -1 );
    Vec_IntWriteEntry( p->vVarValues, Var, Value );
    //printf( "Setting var %d to value %d.\n", Var, Value );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_TestCreateTruthTables()

Vec_Wrd_t * Zyx_TestCreateTruthTables	(	int	nVars,
		int	nNodes )

Definition at line 1415 of file bmcMaj3.c.

{
    int i, nWords = Abc_TtWordNum(nVars);
    Vec_Wrd_t * vInfo = Vec_WrdStart( nWords * (nVars + nNodes + 1) ); 
    for ( i = 0; i < nVars; i++ )
        Abc_TtIthVar( Zyx_TestTruth(vInfo, i, nWords), i, nVars );
    //Dau_DsdPrintFromTruth( Maj3_ManTruth(p, p->nObjs), p->nVars );
    return vInfo;
}

Here is the caller graph for this function:

Zyx_TestExact()

void Zyx_TestExact

(

char *

pFileName

)

Definition at line 1461 of file bmcMaj3.c.

{
    int iObj, nStrs = 0, nVars = -1, nLutSize = -1, nNodes = -1;
    word * pImpl, pSpec[4]; Vec_Wrd_t * vInfo; char Line[1000];
    FILE * pFile = fopen( pFileName, "rb" );
    if ( pFile == NULL )
    {
        printf( "Cannot open input file \"%s\".\n", pFileName );
        return;
    }
    if ( !Zyx_TestGetTruthTablePars( pFileName, pSpec, &nVars, &nLutSize, &nNodes ) )
        return;
    if ( nVars > 8 )
    {
        printf( "This tester does not support functions with more than 8 inputs.\n" );
        return;
    }
    if ( nLutSize > 6 )
    {
        printf( "This tester does not support nodes with more than 6 inputs.\n" );
        return;
    }
    if ( nNodes > 16 )
    {
        printf( "This tester does not support structures with more than 16 inputs.\n" );
        return;
    }
    vInfo = Zyx_TestCreateTruthTables( nVars, nNodes );
    for ( iObj = nVars; fgets(Line, 1000, pFile) != NULL; iObj++ )
    {
        if ( Zyx_TestReadNode( Line, vInfo, nVars, nLutSize, iObj ) )
            continue;
        if ( iObj != nVars + nNodes )
        {
            printf( "The number of nodes in the structure is not correct.\n" );
            break;
        }
        nStrs++;
        pImpl = Zyx_TestTruth( vInfo, iObj-1, Abc_TtWordNum(nVars) );
        if ( Abc_TtEqual( pImpl, pSpec, Abc_TtWordNum(nVars) ) )
            printf( "Structure %3d : Verification successful.\n", nStrs );
        else
        {
            printf( "Structure %3d : Verification FAILED.\n", nStrs );
            printf( "Implementation: " ); Dau_DsdPrintFromTruth( pImpl, nVars );
            printf( "Specification:  " ); Dau_DsdPrintFromTruth( pSpec, nVars );
        }
        iObj = nVars - 1;
    }
    Vec_WrdFree( vInfo );
    fclose( pFile );
}

Here is the call graph for this function:

Zyx_TestGetTruthTablePars()

int Zyx_TestGetTruthTablePars	(	char *	pFileName,
		word *	pTruth,
		int *	nVars,
		int *	nLutSize,
		int *	nNodes )

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

Synopsis [Tests solution to the exact synthesis problem.]

Description []

SideEffects []

SeeAlso []

Definition at line 1360 of file bmcMaj3.c.

{
    char Symb, * pCur, * pBuffer = Abc_UtilStrsav( pFileName );
    int nLength;
    for ( pCur = pBuffer; *pCur; pCur++ )
        if ( !Abc_TtIsHexDigit(*pCur) )
            break;
    Symb = *pCur; *pCur = 0;
    nLength = (int)strlen(pBuffer);
    if ( nLength == 1 )
        *nVars = 2;
    else if ( nLength == 2 )
        *nVars = 3;
    else if ( nLength == 4 )
        *nVars = 4;
    else if ( nLength == 8 )
        *nVars = 5;
    else if ( nLength == 16 )
        *nVars = 6;
    else if ( nLength == 32 )
        *nVars = 7;
    else if ( nLength == 64 )
        *nVars = 8;
    else
    {
        ABC_FREE( pBuffer );
        printf( "Invalid truth table size.\n" );
        return 0;
    }
    Abc_TtReadHex( pTruth, pBuffer );
    *pCur = Symb;
    // read LUT size
    while ( *pCur && *pCur++ != '-' );
    if ( *pCur == 0 )
    {
        ABC_FREE( pBuffer );
        printf( "Expecting \'-\' after truth table before LUT size.\n" );
        return 0;
    }
    // read node count
    *nLutSize = atoi(pCur);
    while ( *pCur && *pCur++ != '-' );
    if ( *pCur == 0 )
    {
        ABC_FREE( pBuffer );
        printf( "Expecting \'-\' after LUT size before node count.\n" );
        return 0;
    }
    *nNodes = atoi(pCur);
    ABC_FREE( pBuffer );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Zyx_TestReadNode()

int Zyx_TestReadNode	(	char *	pLine,
		Vec_Wrd_t *	vTruths,
		int	nVars,
		int	nLutSize,
		int	iObj )

Definition at line 1424 of file bmcMaj3.c.

{
    int k, j, nWords = Abc_TtWordNum(nVars);
    word * pFaninsW[6]; char * pTruth, * pFanins;
    word * pThis, * pLast = Zyx_TestTruth( vTruths, Vec_WrdSize(vTruths)/nWords - 1, nWords );
    if ( pLine[strlen(pLine)-1] == '\n' ) pLine[strlen(pLine)-1] = 0;
    if ( pLine[strlen(pLine)-1] == '\r' ) pLine[strlen(pLine)-1] = 0;
    if ( pLine[0] == 0 )
        return 0;
    if ( (int)strlen(pLine) != 1 + nLutSize + (1 << nLutSize) )
    {
        printf( "Node representation has %d chars (expecting %d chars).\n", (int)strlen(pLine), 1 + nLutSize + (1 << nLutSize) );
        return 0;
    }
    if ( pLine[0] != 'A' + iObj )
    {
        printf( "The output node in line %s is not correct.\n", pLine );
        return 0;
    }
    pTruth  = pLine + 1;
    pFanins = pTruth + (1 << nLutSize);
    for ( k = nLutSize - 1; k >= 0; k-- )
        pFaninsW[k] = Zyx_TestTruth( vTruths, pFanins[k] >= 'a' ? pFanins[k] - 'a' : pFanins[k] - 'A', nWords );
    pThis = Zyx_TestTruth(vTruths, iObj, nWords);
    Abc_TtConst0( pThis, nWords );
    for ( k = 0; k < (1 << nLutSize); k++ )
    {
        if ( pTruth[(1 << nLutSize) - 1 - k] == '0' )
            continue;
        Abc_TtConst1( pLast, nWords );
        for ( j = 0; j < nLutSize; j++ )
            Abc_TtAndCompl( pLast, pLast, 0, pFaninsW[j], !((k >> j) & 1), nWords );
        Abc_TtOr( pThis, pThis, pLast, nWords );
    }
    //Dau_DsdPrintFromTruth( pThis, nVars );
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function: