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

Improvements to ternary simulation.

This commit is contained in:
Alan Mishchenko 2017-03-09 22:57:20 -08:00
parent d877074d8f
commit 5fbe218ff8
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -5403,6 +5403,10 @@ SOURCE=.\src\proof\pdr\pdrTsim2.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\pdr\pdrTsim3.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\pdr\pdrUtil.c
# End Source File
# End Group

6
src/proof/pdr/pdrTsim3.c
View File

@ -187,14 +187,14 @@ printf( "%d %d %d \n", Vec_IntSize(p->vCiObjs), Vec_IntSize(p->vFosPre), Vec_Int
***********************************************************************/
Pdr_Set_t * Txs3_ManTernarySim( Txs3_Man_t * p, int k, Pdr_Set_t * pCube )
{
int fTryNew = 1;
int fUseLit = 1;
// int fTryNew = 1;
// int fUseLit = 1;
int fVerbose = 0;
sat_solver * pSat;
Pdr_Set_t * pRes;
Gia_Obj_t * pObj;
Vec_Int_t * vVar2Ids, * vLits;
int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits, nLits;
int i, Lit, LitAux, Var, Value, RetValue, nCoreLits, * pCoreLits;//, nLits;
// if ( k == 0 )
// fVerbose = 1;
// collect CO objects