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 ***********************************************************************/
Sat_SolverTraceStart(sat_solver * pSat,char * pName)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 ***********************************************************************/
Sat_SolverTraceStop(sat_solver * pSat)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 ***********************************************************************/
Sat_SolverTraceWrite(sat_solver * pSat,int * pBeg,int * pEnd,int fRoot)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
113