luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Trying &bmcs with external solvers.

This commit is contained in:
Alan Mishchenko 2017-08-15 18:13:31 +07:00
parent 2a0289f97b
commit 2280c2e8fe
2 changed files with 34 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/base/abci/abc.c
View File

@ -40082,7 +40082,12 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9SBmc(): There is no AIG.\n" );
Abc_Print( -1, "Abc_CommandAbc9Bmcs(): There is no AIG.\n" );
return 0;
}
if ( pPars->nProcs > 3 )
{
Abc_Print( -1, "Abc_CommandAbc9Bmcs(): Currently this command can run at most 3 concurrent solvers.\n" );
return 0;
}
pAbc->Status = Bmcs_ManPerform( pAbc->pGia, pPars );

48
src/sat/bmc/bmcBmcS.c
View File

@ -23,18 +23,20 @@
#include "sat/satoko/satoko.h"
#include "sat/satoko/solver.h"
//#define ABC_USE_EXT_SOLVERS 1
#ifdef ABC_USE_EXT_SOLVERS
#include "extsat/bmc/bmcApi.h"
#include "extsat/bmc/bmcApi.h"
#else
#define bmc_sat_solver satoko_t
#define bmc_sat_solver_start(type) satoko_create()
#define bmc_sat_solver_stop satoko_destroy
#define bmc_sat_solver_addclause satoko_add_clause
#define bmc_sat_solver_solve satoko_solve_with_assumptions
#define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue
#define bmc_sat_solver_setstop solver_set_stop
#define bmc_sat_solver satoko_t
#define bmc_sat_solver_start(type) satoko_create()
#define bmc_sat_solver_stop satoko_destroy
#define bmc_sat_solver_addclause satoko_add_clause
#define bmc_sat_solver_addvar(s) satoko_add_variable(s, 0)
#define bmc_sat_solver_solve satoko_solve_with_assumptions
#define bmc_sat_solver_read_cex_varvalue solver_read_cex_varvalue
#define bmc_sat_solver_setstop solver_set_stop
#endif
@ -62,16 +64,17 @@ ABC_NAMESPACE_IMPL_START
typedef struct Bmcs_Man_t_ Bmcs_Man_t;
struct Bmcs_Man_t_
{
Bmc_AndPar_t * pPars; // parameters
Gia_Man_t * pGia; // user's AIG
Gia_Man_t * pFrames; // unfolded AIG (pFrames->vCopies point to pClean)
Gia_Man_t * pClean; // incremental AIG (pClean->Value point to pFrames)
Vec_Ptr_t vGia2Fr; // copies of GIA in each timeframe
Vec_Int_t vFr2Sat; // mapping of objects in pFrames into SAT variables
Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA
Bmc_AndPar_t * pPars; // parameters
Gia_Man_t * pGia; // user's AIG
Gia_Man_t * pFrames; // unfolded AIG (pFrames->vCopies point to pClean)
Gia_Man_t * pClean; // incremental AIG (pClean->Value point to pFrames)
Vec_Ptr_t vGia2Fr; // copies of GIA in each timeframe
Vec_Int_t vFr2Sat; // mapping of objects in pFrames into SAT variables
Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA
bmc_sat_solver * pSats[PAR_THR_MAX]; // concurrent SAT solvers
int nSatVars; // number of SAT variables used
int fStopNow; // signal when it is time to stop
int nSatVars; // number of SAT variables used
int nSatVarsOld; // number of SAT variables used
int fStopNow; // signal when it is time to stop
};
//static inline int * Bmcs_ManCopies( Bmcs_Man_t * p, int f ) { return (int*)Vec_PtrEntry(&p->vGia2Fr, f % Vec_PtrSize(&p->vGia2Fr)); }
@ -377,6 +380,7 @@ Bmcs_Man_t * Bmcs_ManStart( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
opts.garbage_max_ratio = (float) 0.3 + i * 0.05;
// create SAT solvers
p->pSats[i] = bmc_sat_solver_start( i );
bmc_sat_solver_addvar( p->pSats[i] );
bmc_sat_solver_addclause( p->pSats[i], &Lit, 1 );
bmc_sat_solver_setstop( p->pSats[i], &p->fStopNow );
#ifndef ABC_USE_EXT_SOLVERS
@ -527,6 +531,7 @@ Cnf_Dat_t * Bmcs_ManAddNewCnf( Bmcs_Man_t * p, int f, int nFramesAdd )
int i, iVar, * pMap;
if ( pNew == NULL )
return NULL;
p->nSatVarsOld = p->nSatVars;
pCnf = Mf_ManGenerateCnf( pNew, 8, 1, 0, 0, 0 );
pMap = ABC_FALLOC( int, Gia_ManObjNum(pNew) );
pMap[0] = 0;
@ -589,9 +594,12 @@ Abc_Cex_t * Bmcs_ManGenerateCex( Bmcs_Man_t * p, int i, int f, int s )
}
return pCex;
}
void Bmcs_ManAddCnf( bmc_sat_solver * pSat, Cnf_Dat_t * pCnf )
void Bmcs_ManAddCnf( Bmcs_Man_t * p, bmc_sat_solver * pSat, Cnf_Dat_t * pCnf )
{
int i;
for ( i = p->nSatVarsOld; i < p->nSatVars; i++ )
bmc_sat_solver_addvar( pSat );
p->nSatVarsOld = p->nSatVars;
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !bmc_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 );
@ -615,7 +623,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
continue;
}
nClauses += pCnf->nClauses;
Bmcs_ManAddCnf( p->pSats[0], pCnf );
Bmcs_ManAddCnf( p, p->pSats[0], pCnf );
Cnf_DataFree( pCnf );
assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) );
for ( k = 0; k < pPars->nFramesAdd; k++ )
@ -799,7 +807,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
// load CNF into solvers
nClauses += pCnf->nClauses;
for ( i = 0; i < pPars->nProcs; i++ )
Bmcs_ManAddCnf( p->pSats[i], pCnf );
Bmcs_ManAddCnf( p, p->pSats[i], pCnf );
Cnf_DataFree( pCnf );
// solve outputs
assert( Gia_ManPoNum(p->pFrames) == (f + pPars->nFramesAdd) * Gia_ManPoNum(pGia) );