diff options
Diffstat (limited to 'src/sat/asat/added.c')
| -rw-r--r-- | src/sat/asat/added.c | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index 497087fb..e1b1bb2a 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -41,6 +41,7 @@ static inline int lit_sign(lit l) { return (l & 1); } static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ); +extern void Io_WriteCnfOutputPiMapping( FILE * pFile, int incrementVars ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -77,6 +78,7 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin return; } fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() ); +// Io_WriteCnfOutputPiMapping( pFile, incrementVars ); fprintf( pFile, "p cnf %d %d\n", p->size, nClauses ); // write the original clauses @@ -161,6 +163,31 @@ int * solver_get_model( solver * p, int * pVars, int nVars ) return pModel; } +/**Function************************************************************* + + Synopsis [Writes the given clause in a file in DIMACS format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Asat_SatPrintStats( FILE * pFile, solver * p ) +{ + printf( "Start = %4d. Conf = %6d. Dec = %6d. Prop = %7d. Insp = %8d.\n", + (int)p->solver_stats.starts, + (int)p->solver_stats.conflicts, + (int)p->solver_stats.decisions, + (int)p->solver_stats.propagations, + (int)p->solver_stats.inspects ); + printf( "Total runtime = %7.2f sec. Var select = %7.2f sec. Var update = %7.2f sec.\n", + (float)(p->timeTotal)/(float)(CLOCKS_PER_SEC), + (float)(p->timeSelect)/(float)(CLOCKS_PER_SEC), + (float)(p->timeUpdate)/(float)(CLOCKS_PER_SEC) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |