From 12688ac9eea7daf26cb30d19b563484d7f469939 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 14 May 2016 23:14:20 -0700 Subject: Experiments with generating sat assignments. --- src/sat/bmc/bmcGen.c | 195 ++++++++++++++++++++++++++++++++++++++++++++++++ src/sat/bmc/module.make | 1 + 2 files changed, 196 insertions(+) create mode 100644 src/sat/bmc/bmcGen.c (limited to 'src/sat') diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c new file mode 100644 index 00000000..60cdd2be --- /dev/null +++ b/src/sat/bmc/bmcGen.c @@ -0,0 +1,195 @@ +/**CFile**************************************************************** + + FileName [bmcGen.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [Generating satisfying assignments.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcGen.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "sat/cnf/cnf.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline word * Gia_ManMoObj( Gia_Man_t * p, int iObj ) +{ + return Vec_WrdEntryP( p->vSims, iObj * p->iPatsPi ); +} +static inline void Gia_ManMoSetCi( Gia_Man_t * p, int iObj ) +{ + int w; + word * pSims = Gia_ManMoObj( p, iObj ); + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = Gia_ManRandomW( 0 ); +} +static inline void Gia_ManMoSimAnd( Gia_Man_t * p, int iObj ) +{ + int w; + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pSims = Gia_ManMoObj( p, iObj ); + word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) ); + word * pSims1 = Gia_ManMoObj( p, Gia_ObjFaninId1(pObj, iObj) ); + if ( Gia_ObjFaninC0(pObj) ) + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = ~(pSims0[w] | pSims1[w]); + else + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = ~pSims0[w] & pSims1[w]; + } + else + { + if ( Gia_ObjFaninC1(pObj) ) + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = pSims0[w] & ~pSims1[w]; + else + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = pSims0[w] & pSims1[w]; + } +} +static inline void Gia_ManMoSetCo( Gia_Man_t * p, int iObj ) +{ + int w; + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + word * pSims = Gia_ManMoObj( p, iObj ); + word * pSims0 = Gia_ManMoObj( p, Gia_ObjFaninId0(pObj, iObj) ); + if ( Gia_ObjFaninC0(pObj) ) + { + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = ~pSims0[w]; + } + else + { + for ( w = 0; w < p->iPatsPi; w++ ) + pSims[w] = pSims0[w]; + } +} +void Gia_ManMoFindSimulate( Gia_Man_t * p, int nWords ) +{ + int i, iObj; + Gia_ManRandomW( 1 ); + p->iPatsPi = 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 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManTestSatEnum( Gia_Man_t * p ) +{ + abctime clk = Abc_Clock(), clk2, clkTotal = 0; + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 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; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make index e1777df8..40402bf3 100644 --- a/src/sat/bmc/module.make +++ b/src/sat/bmc/module.make @@ -16,6 +16,7 @@ SRC += src/sat/bmc/bmcBCore.c \ src/sat/bmc/bmcExpand.c \ src/sat/bmc/bmcFault.c \ src/sat/bmc/bmcFx.c \ + src/sat/bmc/bmcGen.c \ src/sat/bmc/bmcICheck.c \ src/sat/bmc/bmcInse.c \ src/sat/bmc/bmcLoad.c \ -- cgit v1.2.3 From fa111ff81b56b82d1e9248f3c15d735d563e8c08 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 15 May 2016 16:43:10 -0700 Subject: Experiments with generating sat assignments. --- src/sat/bmc/bmcGen.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src/sat') diff --git a/src/sat/bmc/bmcGen.c b/src/sat/bmc/bmcGen.c index 60cdd2be..74af1b78 100644 --- a/src/sat/bmc/bmcGen.c +++ b/src/sat/bmc/bmcGen.c @@ -165,7 +165,7 @@ int Gia_ManTestSatEnum( Gia_Man_t * p ) Vec_IntPush( vVars, pCnf->pVarNums[v] ); } //sat_solver_act_var_clear( pSat ); - sat_solver_set_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); + //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 ); -- cgit v1.2.3