diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
commit | b1a913fb5e85ba04646632f3d771ad79bfd8a720 (patch) | |
tree | 672fd9d1e3f52bf9be192cb91355e2eee6b14302 /src/sat/bsat/satTrace.c | |
parent | 2167d6c148191f7aa65381bb0618b64050bf4de3 (diff) | |
download | abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.gz abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.bz2 abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.zip |
Version abc70123
Diffstat (limited to 'src/sat/bsat/satTrace.c')
-rw-r--r-- | src/sat/bsat/satTrace.c | 109 |
1 files changed, 109 insertions, 0 deletions
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c new file mode 100644 index 00000000..111e8dfb --- /dev/null +++ b/src/sat/bsat/satTrace.c @@ -0,0 +1,109 @@ +/**CFile**************************************************************** + + FileName [satTrace.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [SAT sat_solver.] + + Synopsis [Records the trace of SAT solving in the CNF form.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <assert.h> +#include "satSolver.h" + +/* + The trace of SAT solving contains the original clause of the problem + along with the learned clauses derived during SAT solving. + The first line of the resulting file contains 3 numbers instead of 2: + c <num_vars> <num_all_clauses> <num_root_clauses> +*/ + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Start the trace recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceStart( sat_solver * pSat, char * pName ) +{ + assert( pSat->pFile == NULL ); + pSat->pFile = fopen( pName, "w" ); + fprintf( pSat->pFile, " \n" ); + pSat->nClauses = 0; + pSat->nRoots = 0; +} + +/**Function************************************************************* + + Synopsis [Stops the trace recording.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceStop( sat_solver * pSat ) +{ + if ( pSat->pFile == NULL ) + return; + rewind( pSat->pFile ); + fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots ); + fclose( pSat->pFile ); + pSat->pFile = NULL; +} + + +/**Function************************************************************* + + Synopsis [Writes one clause into the trace file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot ) +{ + if ( pSat->pFile == NULL ) + return; + pSat->nClauses++; + pSat->nRoots += fRoot; + for ( ; pBeg < pEnd ; pBeg++ ) + fprintf( pSat->pFile, " %d", lit_print(*pBeg) ); + fprintf( pSat->pFile, " 0\n" ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |