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

Changes to 'pdr' to run with updated Satoko.

This commit is contained in:
Alan Mishchenko 2017-09-06 08:34:04 -07:00
parent 0fa4c86899
commit f06056d85d
5 changed files with 18 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/wlc/wlcAbs.c
View File

@ -224,8 +224,8 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int fir
sat_solver_setnvars(pSat, pCnf->nVars);
if ( RunId >= 0 )
{
pSat->RunId = RunId;
pSat->pFuncStop = Wla_CallBackToStop;
sat_solver_set_runid( pSat, RunId );
sat_solver_set_stop_func( pSat, Wla_CallBackToStop );
}
for (i = 0; i < pCnf->nClauses; i++)

8
src/proof/pdr/pdrCnf.c
View File

@ -370,8 +370,8 @@ static inline sat_solver * Pdr_ManNewSolver1( sat_solver * pSat, Pdr_Man_t * p,
}
pSat = (sat_solver *)Cnf_DataWriteIntoSolverInt( pSat, p->pCnf1, 1, fInit );
sat_solver_set_runtime_limit( pSat, p->timeToStop );
pSat->RunId = p->pPars->RunId;
pSat->pFuncStop = p->pPars->pFuncStop;
sat_solver_set_runid( pSat, p->pPars->RunId );
sat_solver_set_stop_func( pSat, p->pPars->pFuncStop );
return pSat;
}
@ -420,8 +420,8 @@ static inline sat_solver * Pdr_ManNewSolver2( sat_solver * pSat, Pdr_Man_t * p,
// pSat = sat_solver_new();
sat_solver_setnvars( pSat, 500 );
sat_solver_set_runtime_limit( pSat, p->timeToStop );
pSat->RunId = p->pPars->RunId;
pSat->pFuncStop = p->pPars->pFuncStop;
sat_solver_set_runid( pSat, p->pPars->RunId );
sat_solver_set_stop_func( pSat, p->pPars->pFuncStop );
return pSat;
}

2
src/proof/pdr/pdrCore.c
View File

@ -1296,7 +1296,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
if ( p->timeToStop && Abc_Clock() > p->timeToStop )
Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n", p->pPars->nTimeOut, iFrame );
else
Abc_Print( 1, "Reached conflict limit (%d) in frame.\n", p->pPars->nConfLimit, iFrame );
Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n", p->pPars->nConfLimit, iFrame );
}
p->pPars->iFrame = iFrame;
return -1;

4
src/proof/pdr/pdrInt.h
View File

@ -32,7 +32,7 @@
#include "misc/hash/hashInt.h"
#include "aig/gia/giaAig.h"
//#define PDR_USE_SATOKO 1
#define PDR_USE_SATOKO 1
#ifndef PDR_USE_SATOKO
#include "sat/bsat/satSolver.h"
@ -53,6 +53,8 @@
#define sat_solver_solve(s,b,e,c,x,y,z) satoko_solve_assumptions_limit(s,b,e-b,(int)c)
#define sat_solver_var_value satoko_read_cex_varvalue
#define sat_solver_set_runtime_limit satoko_set_runtime_limit
#define sat_solver_set_runid satoko_set_runid
#define sat_solver_set_stop_func satoko_set_stop_func
#define sat_solver_compress(s)
#endif

8
src/sat/bsat/satSolver.h
View File

@ -330,6 +330,14 @@ static inline int sat_solver_count_usedvars(sat_solver* s)
}
return nVars;
}
static void sat_solver_set_runid( sat_solver *s, int id )
{
s->RunId = id;
}
static void sat_solver_set_stop_func( sat_solver *s, int (*fnct)(int) )
{
s->pFuncStop = fnct;
}
static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
{