abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
satTrace.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [satTrace.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT sat_solver.]
8 
9  Synopsis [Records the trace of SAT solving in the CNF form.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
18 
19 ***********************************************************************/
20 
21 #include "satSolver.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 /*
27  The trace of SAT solving contains the original clause of the problem
28  along with the learned clauses derived during SAT solving.
29  The first line of the resulting file contains 3 numbers instead of 2:
30  c <num_vars> <num_all_clauses> <num_root_clauses>
31 */
32 
33 ////////////////////////////////////////////////////////////////////////
34 /// DECLARATIONS ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis [Start the trace recording.]
45 
46  Description []
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 void Sat_SolverTraceStart( sat_solver * pSat, char * pName )
54 {
55  assert( pSat->pFile == NULL );
56  pSat->pFile = fopen( pName, "w" );
57  fprintf( pSat->pFile, " \n" );
58  pSat->nClauses = 0;
59  pSat->nRoots = 0;
60 }
61 
62 /**Function*************************************************************
63 
64  Synopsis [Stops the trace recording.]
65 
66  Description []
67 
68  SideEffects []
69 
70  SeeAlso []
71 
72 ***********************************************************************/
73 void Sat_SolverTraceStop( sat_solver * pSat )
74 {
75  if ( pSat->pFile == NULL )
76  return;
77  rewind( pSat->pFile );
78  fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
79  fclose( pSat->pFile );
80  pSat->pFile = NULL;
81 }
82 
83 
84 /**Function*************************************************************
85 
86  Synopsis [Writes one clause into the trace file.]
87 
88  Description []
89 
90  SideEffects []
91 
92  SeeAlso []
93 
94 ***********************************************************************/
95 void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )
96 {
97  if ( pSat->pFile == NULL )
98  return;
99  pSat->nClauses++;
100  pSat->nRoots += fRoot;
101  for ( ; pBeg < pEnd ; pBeg++ )
102  fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
103  fprintf( pSat->pFile, " 0\n" );
104 }
105 
106 ////////////////////////////////////////////////////////////////////////
107 /// END OF FILE ///
108 ////////////////////////////////////////////////////////////////////////
109 
110 
111 ABC_NAMESPACE_IMPL_END
112 
sat_solver_t::pFile
FILE * pFile
Definition: satSolver.h:184
Sat_SolverTraceWrite
void Sat_SolverTraceWrite(sat_solver *pSat, int *pBeg, int *pEnd, int fRoot)
Definition: satTrace.c:95
sat_solver_t::nRoots
int nRoots
Definition: satSolver.h:186
Sat_SolverTraceStart
ABC_NAMESPACE_IMPL_START void Sat_SolverTraceStart(sat_solver *pSat, char *pName)
DECLARATIONS ///.
Definition: satTrace.c:53
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
sat_solver_t
Definition: satSolver.h:91
assert
#define assert(ex)
Definition: util_old.h:213
sat_solver_t::nClauses
int nClauses
Definition: satSolver.h:185
Sat_SolverTraceStop
void Sat_SolverTraceStop(sat_solver *pSat)
Definition: satTrace.c:73
rewind
VOID_HACK rewind()
lit_print
static int lit_print(lit l)
Definition: satVec.h:147