diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 11:58:55 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-04-12 11:58:55 -0700 |
| commit | 3a553e15ac2f6c035bab1bec32c76ca8830ac4d7 (patch) | |
| tree | efec3db04fe9b191572c275573477a287f7da755 /src/sat/bsat/satUtil.c | |
| parent | 90cf0b579f2c6e710e82aae2c032301f7cfbcb35 (diff) | |
| download | abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.tar.gz abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.tar.bz2 abc-3a553e15ac2f6c035bab1bec32c76ca8830ac4d7.zip | |
Removing unused feature of the SAT solver (native support for cardinality constraint).
Diffstat (limited to 'src/sat/bsat/satUtil.c')
| -rw-r--r-- | src/sat/bsat/satUtil.c | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 188c308b..f1f03ce2 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -195,8 +195,6 @@ 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 ); |