Skip to content

A
abc
Commit 7753e097 by Alan Mishchenko
Options

Adding command to dump UNSAT core of BMC instance.

parent 42927d5e
Showing with 2 additions and 2 deletions
src/sat/bmc/bmcBCore.c
...@@ -240,7 +240,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) ...@@ -240,7 +240,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
} }
assert( RetValue == l_False ); assert( RetValue == l_False );
pSatCnf = sat_solver_store_release( pSat ); pSatCnf = sat_solver_store_release( pSat );
Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" ); // Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" );
// derive the UNSAT core // derive the UNSAT core
clk = clock(); clk = clock();
pManProof = Intp_ManAlloc(); pManProof = Intp_ManAlloc();
...@@ -248,7 +248,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) ...@@ -248,7 +248,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
Intp_ManFree( pManProof ); Intp_ManFree( pManProof );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
printf( "UNSAT core contains %8d (out of %8d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) ); printf( "UNSAT core contains %d (out of %d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) );
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
// write the problem // write the problem
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment