bmcGen.c File Reference

#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"

Include dependency graph for bmcGen.c:

Go to the source code of this file.

Functions
void	Gia_ManMoFindSimulate (Gia_Man_t *p, int nWords)
int	Gia_ManTestSatEnum (Gia_Man_t *p)

Function Documentation

Gia_ManMoFindSimulate()

void Gia_ManMoFindSimulate	(	Gia_Man_t *	p,
		int	nWords )

Definition at line 101 of file bmcGen.c.

{
    int i, iObj;
    Gia_ManRandomW( 1 );
    p->nSimWords = nWords;
    if ( p->vSims )
        Vec_WrdFill( p->vSims, nWords * Gia_ManObjNum(p), 0 );
    else
        p->vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) );
    Gia_ManForEachCiId( p, iObj, i )
        Gia_ManMoSetCi( p, iObj );
    Gia_ManForEachAndId( p, iObj )
        Gia_ManMoSimAnd( p, iObj );
    Gia_ManForEachCoId( p, iObj, i )
        Gia_ManMoSetCo( p, iObj );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Gia_ManTestSatEnum()

int Gia_ManTestSatEnum

(

Gia_Man_t *

p

)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 129 of file bmcGen.c.

{
    abctime clk = Abc_Clock(), clk2, clkTotal = 0;
    Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
    sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0);
    int i, v, status, iLit, nWords = 1, iOutVar = 1, Count = 0;
    Vec_Int_t * vVars = Vec_IntAlloc( 1000 );
    word * pSimInfo;
 
    // add literals to the solver
    iLit  = Abc_Var2Lit( iOutVar, 0 ); 
    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
    assert( status );
 
    // simulate the AIG
    Gia_ManMoFindSimulate( p, nWords );
 
    // print outputs
    pSimInfo = Gia_ManMoObj( p, Gia_ObjId(p, Gia_ManCo(p, 0)) );
    for ( i = 0; i < 64*nWords; i++ )
        printf( "%d", Abc_InfoHasBit( (unsigned *)pSimInfo, i ) );
    printf( "\n" );
 
    // iterate through the assignments
    for ( i = 0; i < 64*nWords; i++ )
    {
        Vec_IntClear( vVars );
        for ( v = 0; v < Gia_ManObjNum(p); v++ )
        {
            if ( pCnf->pVarNums[v] == -1 )
                continue;
            pSimInfo = Gia_ManMoObj( p, v );
            if ( !Abc_InfoHasBit( (unsigned *)pSimInfo, i ) )
                continue;
            Vec_IntPush( vVars, pCnf->pVarNums[v] );
        }
        //sat_solver_act_var_clear( pSat );
        //sat_solver_set_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
 
        clk2 = Abc_Clock();
        status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
        clkTotal += Abc_Clock() - clk2;
        printf( "%c", status == l_True ? '+' : '-' );
        if ( status == l_True )
            Count++;
    }
    printf( "\n" );
    printf( "Finished generating %d assignments.  ", Count );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    Abc_PrintTime( 1, "SAT solver time", clkTotal );
 
    Vec_WrdFreeP( &p->vSims );
    Vec_IntFree( vVars );
    sat_solver_delete( pSat );
    Cnf_DataFree( pCnf );
    return 1;
}

Here is the call graph for this function: