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

Updating "lutexact -c" to fix the change in Cadical after upgrade.

This commit is contained in:
Alan Mishchenko 2025-12-24 13:20:26 -08:00
parent b822d47fcf
commit 3d32b8b2ad
1 changed files with 3 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/sat/bmc/bmcMaj7.c
View File

@ -291,7 +291,8 @@ static Exa7_Man_t * Exa7_ManAlloc( Bmc_EsPar_t * pPars, word * pTruth )
p->pSat = cadical_solver_new();
p->nVarAlloc = Exa7_ManVarReserve( p );
assert( p->nVarAlloc >= p->iVar );
cadical_solver_setnvars( p->pSat, p->nVarAlloc );
//cadical_solver_setnvars( p->pSat, p->nVarAlloc );
cadical_solver_setnvars( p->pSat, p->nVarAlloc+(p->nLutSize+1)*p->nNodes*(1 << p->nVars) );
if ( pPars->RuntimeLim )
Exa7_CadicalSetRuntimeLimit( p->pSat, pPars->RuntimeLim );
return p;
@ -585,7 +586,7 @@ static int Exa7_ManAddCnf( Exa7_Man_t * p, int iMint )
for ( i = 0; i < p->nVars; i++ )
p->VarVals[i] = (iMint >> i) & 1;
// sat_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
cadical_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
//cadical_solver_setnvars( p->pSat, p->iVar + (p->nLutSize+1)*p->nNodes );
//printf( "Adding clauses for minterm %d with value %d.\n", iMint, Value );
for ( i = p->nVars; i < p->nObjs; i++ )
{