abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
msatSolverIo.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [msatSolverIo.c]
4 
5  PackageName [A C version of SAT solver MINISAT, originally developed
6  in C++ by Niklas Een and Niklas Sorensson, Chalmers University of
7  Technology, Sweden: http://www.cs.chalmers.se/~een/Satzoo.]
8 
9  Synopsis [Input/output of CNFs.]
10 
11  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - January 1, 2004.]
16 
17  Revision [$Id: msatSolverIo.c,v 1.0 2004/01/01 1:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "msatInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 static char * Msat_TimeStamp();
31 
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35 
36 /**Function*************************************************************
37 
38  Synopsis []
39 
40  Description []
41 
42  SideEffects []
43 
44  SeeAlso []
45 
46 ***********************************************************************/
48 {
49  int i;
50  printf( "Current assignments are: \n" );
51  for ( i = 0; i < p->nVars; i++ )
52  printf( "%d", i % 10 );
53  printf( "\n" );
54  for ( i = 0; i < p->nVars; i++ )
55  if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
56  printf( "." );
57  else
58  {
59  assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
60  if ( MSAT_LITSIGN(p->pAssigns[i]) )
61  printf( "0" );
62  else
63  printf( "1" );
64  }
65  printf( "\n" );
66 }
67 
68 /**Function*************************************************************
69 
70  Synopsis []
71 
72  Description []
73 
74  SideEffects []
75 
76  SeeAlso []
77 
78 ***********************************************************************/
80 {
81  Msat_Clause_t ** pClauses;
82  int nClauses, i;
83 
84  printf( "Original clauses: \n" );
85  nClauses = Msat_ClauseVecReadSize( p->vClauses );
86  pClauses = Msat_ClauseVecReadArray( p->vClauses );
87  for ( i = 0; i < nClauses; i++ )
88  {
89  printf( "%3d: ", i );
90  Msat_ClausePrint( pClauses[i] );
91  }
92 
93  printf( "Learned clauses: \n" );
94  nClauses = Msat_ClauseVecReadSize( p->vLearned );
95  pClauses = Msat_ClauseVecReadArray( p->vLearned );
96  for ( i = 0; i < nClauses; i++ )
97  {
98  printf( "%3d: ", i );
99  Msat_ClausePrint( pClauses[i] );
100  }
101 
102  printf( "Variable activity: \n" );
103  for ( i = 0; i < p->nVars; i++ )
104  printf( "%3d : %.4f\n", i, p->pdActivity[i] );
105 }
106 
107 /**Function*************************************************************
108 
109  Synopsis []
110 
111  Description []
112 
113  SideEffects []
114 
115  SeeAlso []
116 
117 ***********************************************************************/
118 void Msat_SolverWriteDimacs( Msat_Solver_t * p, char * pFileName )
119 {
120  FILE * pFile;
121  Msat_Clause_t ** pClauses;
122  int nClauses, i;
123 
124  nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
125  for ( i = 0; i < p->nVars; i++ )
126  nClauses += ( p->pLevel[i] == 0 );
127 
128  pFile = fopen( pFileName, "wb" );
129  fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
130  fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );
131 
132  nClauses = Msat_ClauseVecReadSize( p->vClauses );
133  pClauses = Msat_ClauseVecReadArray( p->vClauses );
134  for ( i = 0; i < nClauses; i++ )
135  Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
136 
137  nClauses = Msat_ClauseVecReadSize( p->vLearned );
138  pClauses = Msat_ClauseVecReadArray( p->vLearned );
139  for ( i = 0; i < nClauses; i++ )
140  Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
141 
142  // write zero-level assertions
143  for ( i = 0; i < p->nVars; i++ )
144  if ( p->pLevel[i] == 0 )
145  fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );
146 
147  fprintf( pFile, "\n" );
148  fclose( pFile );
149 }
150 
151 
152 /**Function*************************************************************
153 
154  Synopsis [Returns the time stamp.]
155 
156  Description []
157 
158  SideEffects []
159 
160  SeeAlso []
161 
162 ***********************************************************************/
164 {
165  static char Buffer[100];
166  time_t ltime;
167  char * TimeStamp;
168  // get the current time
169  time( &ltime );
170  TimeStamp = asctime( localtime( &ltime ) );
171  TimeStamp[ strlen(TimeStamp) - 1 ] = 0;
172  strcpy( Buffer, TimeStamp );
173  return Buffer;
174 }
175 
176 ////////////////////////////////////////////////////////////////////////
177 /// END OF FILE ///
178 ////////////////////////////////////////////////////////////////////////
179 
180 
182 
#define MSAT_VAR_UNASSIGNED
Definition: msatInt.h:68
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static ABC_NAMESPACE_IMPL_START char * Msat_TimeStamp()
DECLARATIONS ///.
Definition: msatSolverIo.c:163
#define MSAT_LIT2VAR(l)
Definition: msat.h:59
void Msat_SolverPrintClauses(Msat_Solver_t *p)
Definition: msatSolverIo.c:79
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
Definition: msatInt.h:57
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClausePrint(Msat_Clause_t *pC)
Definition: msatClause.c:468
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
Definition: msatClauseVec.c:85
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
void Msat_SolverWriteDimacs(Msat_Solver_t *p, char *pFileName)
Definition: msatSolverIo.c:118
char * strcpy()
#define MSAT_LITSIGN(l)
Definition: msat.h:58
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
void Msat_SolverPrintAssignment(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
Definition: msatSolverIo.c:47
#define assert(ex)
Definition: util_old.h:213
int strlen()
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
Definition: msat.h:42
void Msat_ClauseWriteDimacs(FILE *pFile, Msat_Clause_t *pC, int fIncrement)
Definition: msatClause.c:494