From 1ffd9aad766b3d980b8d8a030d03e8f17371f673 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 3 Sep 2015 21:57:21 -0700 Subject: Experiments with SAT-based collapsing. --- src/sat/bmc/bmcClp.c | 227 +++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 227 insertions(+) create mode 100644 src/sat/bmc/bmcClp.c (limited to 'src/sat') diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c new file mode 100644 index 00000000..d2e4eb91 --- /dev/null +++ b/src/sat/bmc/bmcClp.c @@ -0,0 +1,227 @@ +/**CFile**************************************************************** + + FileName [bmcClp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT-based bounded model checking.] + + Synopsis [INT-FX: Interpolation-based logic sharing extraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bmcClp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "bmc.h" +#include "misc/vec/vecWec.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 [] + +***********************************************************************/ +int Bmc_CollapseExpand2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit ) +{ + int i, Index, status, nFinal, * pFinal; + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + assert( status == l_False ); + // get subset of literals + nFinal = sat_solver_final( pSat, &pFinal ); + // collect literals + Vec_IntClear( vNums ); + for ( i = 0; i < nFinal; i++ ) + { + Index = Vec_IntFind( vLits, Abc_LitNot(pFinal[i]) ); + assert( Index >= 0 ); + Vec_IntPush( vNums, Index ); + } +/* + int i; + Vec_IntClear( vNums ); + for ( i = 0; i < Vec_IntSize(vLits); i++ ) + Vec_IntPush( vNums, i ); +*/ + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit ) +{ + int k, n, iLit, status; + // try removing one literal at a time + for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- ) + { + int Save = Vec_IntEntry( vLits, k ); + Vec_IntWriteEntry( vLits, k, -1 ); + // put into new array + Vec_IntClear( vTemp ); + Vec_IntForEachEntry( vLits, iLit, n ) + if ( iLit != -1 ) + Vec_IntPush( vTemp, iLit ); + // check against offset + status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp), nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -1; + if ( status == l_True ) + Vec_IntWriteEntry( vLits, k, Save ); + } + // put into new array + Vec_IntClear( vNums ); + Vec_IntForEachEntry( vLits, iLit, n ) + if ( iLit != -1 ) + Vec_IntPush( vNums, n ); + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose ) +{ + int nVars = Gia_ManCiNum(p); + Vec_Int_t * vVars = Vec_IntAlloc( nVars ); + Vec_Int_t * vLits = Vec_IntAlloc( nVars ); + Vec_Int_t * vNums = Vec_IntAlloc( nVars ); + Vec_Int_t * vCube = Vec_IntAlloc( nVars ); + Vec_Str_t * vStr = Vec_StrAlloc( nVars+1 ); + int iOut = 0, iLit, iVar, status, n, Count; + + // create SAT solver + Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); + sat_solver * pSat[2] = { + (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), + (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) + }; + + // collect CI variables + int iCiVarBeg = pCnf->nVars - nVars;// - 1; + for ( n = 0; n < nVars; n++ ) + Vec_IntPush( vVars, iCiVarBeg + n ); + + // check that on-set/off-set is sat + for ( n = 0; n < 2; n++ ) + { + iLit = Abc_Var2Lit( iOut + 1, n ); // n=0 => F=1 n=1 => F=0 + status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 ); + if ( status == 0 ) + return -1; // const0/1 + status = sat_solver_solve( pSat[n], NULL, NULL, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -3; // timeout + if ( status == l_False ) + return -1; // const0/1 + } + + // prepare on-set for solving + sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) ); + for ( Count = 0; Count < nCubeLim; ) + { + // get the smallest assignment + status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 ); + if ( status == l_Undef ) + return -3; // timeout + if ( status == l_False ) + break; + // collect values + Vec_IntClear( vLits ); + Vec_IntForEachEntry( vVars, iVar, n ) + Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar)) ); + // print minterm +// printf( "Mint: " ); +// Vec_IntForEachEntry( vLits, iLit, n ) +// printf( "%d", !Abc_LitIsCompl(iLit) ); +// printf( "\n" ); + // expand the values + status = Bmc_CollapseExpand( pSat[1], vLits, vNums, vCube, nBTLimit ); + if ( status < 0 ) + return -3; // timeout + Count++; + // print cube + if ( fVerbose ) + { + Vec_StrFill( vStr, nVars, '-' ); + Vec_StrPush( vStr, '\0' ); + Vec_IntForEachEntry( vNums, iVar, n ) + Vec_StrWriteEntry( vStr, iVar, (char)('0' + !Abc_LitIsCompl(Vec_IntEntry(vLits, iVar))) ); + printf( "Cube: " ); + printf( "%s\n", Vec_StrArray(vStr) ); + } + // collect cube + Vec_IntClear( vCube ); + Vec_IntForEachEntry( vNums, iVar, n ) + Vec_IntPush( vCube, Abc_LitNot(Vec_IntEntry(vLits, iVar)) ); + // add cube + status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) ); + if ( status == 0 ) + break; + } + printf( "Finished enumerating %d assignments.\n", Count ); + + // cleanup + Vec_IntFree( vVars ); + Vec_IntFree( vLits ); + Vec_IntFree( vNums ); + Vec_IntFree( vCube ); + Vec_StrFree( vStr ); + sat_solver_delete( pSat[0] ); + sat_solver_delete( pSat[1] ); + Cnf_DataFree( pCnf ); + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + -- cgit v1.2.3