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

Bug fix in CNF generation for &glucose.

This commit is contained in:
Alan Mishchenko 2024-04-15 20:25:43 -07:00
parent 99e0e37da6
commit 2d6b5c9adc
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/sat/glucose/AbcGlucose.cpp
View File

@ -885,7 +885,7 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 );
s.addClause(*lits);
}
Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums,pCnf->nVars);
Vec_Int_t * vCnfIds = Vec_IntAllocArrayCopy(pCnf->pVarNums, Gia_ManObjNum(p));
printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Cnf_DataFree(pCnf);