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

Experiments with SAT sweeping.

This commit is contained in:
Alan Mishchenko 2022-04-24 10:25:46 -07:00
parent cb30ea0516
commit 1abd0457ab
4 changed files with 22 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -36999,7 +36999,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle );
Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0;
int fUseAlgoG3 = 0, fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF )

3
src/proof/cec/cecSatG3.c
View File

@ -1564,9 +1564,8 @@ void Cec5_ManLoadInstance( Cec5_Man_t * p, int iObj0, int iObj1, int * piVar0, i
int iVar1 = Cec5_ObjGetCnfVar( p, iObj1 );
if( p->pPars->jType > 0 )
{
extern void glucose2_markapprox( void * pSat, int v0, int v1, int nlim );
int nlim = p->approxLim;
glucose2_markapprox( p->pSat, iVar0, iVar1, nlim );
bmcg2_sat_solver_markapprox( p->pSat, iVar0, iVar1, nlim );
}
* piVar0 = iVar0;

25
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -132,6 +132,10 @@ void glucose2_solver_setstop(Gluco2::SimpSolver* S, int * pstop)
S->pstop = pstop;
}
void glucose2_markapprox( Gluco2::SimpSolver* S, int v0, int v1, int nlim )
{
S->markApprox(v0, v1, nlim);
}
/**Function*************************************************************
@ -228,6 +232,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
glucose2_solver_setstop((Gluco2::SimpSolver*)s, pstop);
}
void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim)
{
glucose2_markapprox((Gluco2::SimpSolver*)s, v0, v1, nlim);
}
abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco2::SimpSolver*)s)->nRuntimeLimit;
@ -474,6 +483,11 @@ void glucose2_solver_setstop(Gluco2::Solver* S, int * pstop)
S->pstop = pstop;
}
void glucose2_markapprox( Gluco2::Solver* S, int v0, int v1, int nlim )
{
S->markApprox(v0, v1, nlim);
}
/**Function*************************************************************
@ -570,6 +584,11 @@ void bmcg2_sat_solver_set_stop(bmcg2_sat_solver* s, int * pstop)
glucose2_solver_setstop((Gluco2::Solver*)s, pstop);
}
void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim)
{
glucose2_markapprox((Gluco2::Solver*)s, v0, v1, nlim);
}
abctime bmcg2_sat_solver_set_runtime_limit(bmcg2_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco2::Solver*)s)->nRuntimeLimit;
@ -1536,12 +1555,6 @@ int Glucose2_SolveAig(Gia_Man_t * p, Glucose2_Pars * pPars)
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
}
extern "C" {
void glucose2_markapprox( void * pSat, int v0, int v1, int nlim ){
((Gluco2::Solver*) pSat)->markApprox(v0, v1, nlim);
}
};
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

1
src/sat/glucose2/AbcGlucose2.h
View File

@ -86,6 +86,7 @@ extern int bmcg2_sat_solver_elim_varnum(bmcg2_sat_solver* s);
extern int * bmcg2_sat_solver_read_cex( bmcg2_sat_solver* s );
extern int bmcg2_sat_solver_read_cex_varvalue( bmcg2_sat_solver* s, int );
extern void bmcg2_sat_solver_set_stop( bmcg2_sat_solver* s, int * pstop );
extern void bmcg2_sat_solver_markapprox(bmcg2_sat_solver* s, int v0, int v1, int nlim);
extern abctime bmcg2_sat_solver_set_runtime_limit( bmcg2_sat_solver* s, abctime Limit );
extern void bmcg2_sat_solver_set_conflict_budget( bmcg2_sat_solver* s, int Limit );
extern int bmcg2_sat_solver_varnum( bmcg2_sat_solver* s );