diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-23 21:45:23 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-12-23 21:45:23 -0800 |
| commit | c59e2e9c962590540c2e78ec26f991c0251a47d5 (patch) | |
| tree | 346b13c434583336faa62b1da7d730b4ebb0eb2a /src/sat/bsat/satSolver2.c | |
| parent | 7facbc3cc932bf72581d164a0d2d5ea60ab9aa2d (diff) | |
| download | abc-c59e2e9c962590540c2e78ec26f991c0251a47d5.tar.gz abc-c59e2e9c962590540c2e78ec26f991c0251a47d5.tar.bz2 abc-c59e2e9c962590540c2e78ec26f991c0251a47d5.zip | |
Transforming the solver to use different clause representation.
Diffstat (limited to 'src/sat/bsat/satSolver2.c')
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index cb0d7b60..a4166fef 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1308,15 +1308,16 @@ void sat_solver2_setnvars(sat_solver2* s,int n) void sat_solver2_delete(sat_solver2* s) { -// veci * pCore; + veci * pCore; + // report statistics printf( "Used %6.2f Mb for proof-logging. Unit clauses = %d.\n", 2.0 * veci_size(&s->proofs) / (1<<20), s->nUnits ); -/* + pCore = Sat_ProofCore( s ); printf( "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) ); veci_delete( pCore ); ABC_FREE( pCore ); -*/ + if ( s->fProofLogging ) Sat_ProofCheck( s ); |