From bc725b85deb2d2df135833daa590b2ac1417d3c4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 15 Apr 2024 20:29:38 -0700 Subject: [PATCH] Bug fix in CNF generation for &glucose (three more places). --- src/sat/glucose/AbcGlucose.cpp | 2 +- src/sat/glucose2/AbcGlucose2.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index bc22ff5d2..d6f4c454d 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -899,7 +899,7 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) for ( int i = 0; i < pCnf->nClauses; i++ ) if ( !glucose_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) 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 ); //Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Cnf_DataFree(pCnf); diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 0e4871187..6201779cb 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -903,7 +903,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); @@ -917,7 +917,7 @@ Vec_Int_t * Glucose_SolverFromAig2( Gia_Man_t * p, SimpSolver& S ) for ( int i = 0; i < pCnf->nClauses; i++ ) if ( !glucose2_solver_addclause( &S, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) 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 ); //Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); Cnf_DataFree(pCnf);