50 printf(
"Current assignments are: \n" );
51 for ( i = 0; i < p->nVars; i++ )
52 printf(
"%d", i % 10 );
54 for ( i = 0; i < p->nVars; i++ )
84 printf(
"Original clauses: \n" );
87 for ( i = 0; i < nClauses; i++ )
93 printf(
"Learned clauses: \n" );
96 for ( i = 0; i < nClauses; i++ )
102 printf(
"Variable activity: \n" );
103 for ( i = 0; i < p->nVars; i++ )
104 printf(
"%3d : %.4f\n", i, p->pdActivity[i] );
125 for ( i = 0; i < p->nVars; i++ )
126 nClauses += ( p->pLevel[i] == 0 );
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 );
134 for ( i = 0; i < nClauses; i++ )
139 for ( i = 0; i < nClauses; i++ )
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 );
147 fprintf( pFile,
"\n" );
165 static char Buffer[100];
170 TimeStamp = asctime( localtime( <ime ) );
171 TimeStamp[
strlen(TimeStamp) - 1 ] = 0;
172 strcpy( Buffer, TimeStamp );
#define MSAT_VAR_UNASSIGNED
static ABC_NAMESPACE_IMPL_START char * Msat_TimeStamp()
DECLARATIONS ///.
void Msat_SolverPrintClauses(Msat_Solver_t *p)
typedefABC_NAMESPACE_HEADER_START struct Msat_Clause_t_ Msat_Clause_t
INCLUDES ///.
int Msat_ClauseVecReadSize(Msat_ClauseVec_t *p)
void Msat_ClausePrint(Msat_Clause_t *pC)
Msat_Clause_t ** Msat_ClauseVecReadArray(Msat_ClauseVec_t *p)
#define ABC_NAMESPACE_IMPL_END
void Msat_SolverWriteDimacs(Msat_Solver_t *p, char *pFileName)
#define ABC_NAMESPACE_IMPL_START
void Msat_SolverPrintAssignment(Msat_Solver_t *p)
FUNCTION DEFINITIONS ///.
typedefABC_NAMESPACE_HEADER_START struct Msat_Solver_t_ Msat_Solver_t
INCLUDES ///.
void Msat_ClauseWriteDimacs(FILE *pFile, Msat_Clause_t *pC, int fIncrement)