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 (three more places).

This commit is contained in:
Alan Mishchenko 2024-04-15 20:29:38 -07:00
parent 2d6b5c9adc
commit bc725b85de
2 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -899,7 +899,7 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S )
for ( int i = 0; i < pCnf->nClauses; i++ ) for ( int i = 0; i < pCnf->nClauses; i++ )
if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 ); assert( 0 );
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 ); //printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
//Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Cnf_DataFree(pCnf); Cnf_DataFree(pCnf);

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

@ -903,7 +903,7 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 ); lits->push( toLit(*pLit) ), s.addVar( *pLit >> 1 );
s.addClause(*lits); 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 ); printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Cnf_DataFree(pCnf); Cnf_DataFree(pCnf);
@ -917,7 +917,7 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S )
for ( int i = 0; i < pCnf->nClauses; i++ ) for ( int i = 0; i < pCnf->nClauses; i++ )
if ( !glucose2_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) if ( !glucose2_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 ); assert( 0 );
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 ); //printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
//Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); //Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Cnf_DataFree(pCnf); Cnf_DataFree(pCnf);