diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-01-10 10:19:26 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-01-10 10:19:26 -0800 |
| commit | d6178631be82089dc65263cd10293211abad5924 (patch) | |
| tree | e5b663cd124026a7694a75b46b4b71811fb1b7a8 /src/sat/bsat/satUtil.c | |
| parent | a4f977638849d8ba679cbdfd66e3a74c9bf91fe3 (diff) | |
| download | abc-d6178631be82089dc65263cd10293211abad5924.tar.gz abc-d6178631be82089dc65263cd10293211abad5924.tar.bz2 abc-d6178631be82089dc65263cd10293211abad5924.zip | |
Adding support of candinality clause to the SAT solver.
Diffstat (limited to 'src/sat/bsat/satUtil.c')
| -rw-r--r-- | src/sat/bsat/satUtil.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index f1f03ce2..188c308b 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -195,6 +195,8 @@ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) // printf( "calls : %10d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); printf( "starts : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) ); printf( "conflicts : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) ); + if ( p->nCardClauses ) + printf( "conflictsCard : %16.0f\n", Sat_Wrd2Dbl((word)p->nCardClauses) ); printf( "decisions : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) ); printf( "propagations : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) ); // printf( "inspects : %10d\n", (int)p->stats.inspects ); |