msatSolverIo.c File Reference

#include "msatInt.h"

Include dependency graph for msatSolverIo.c:

Go to the source code of this file.

Functions
void	Msat_SolverPrintAssignment (Msat_Solver_t *p)
	FUNCTION DEFINITIONS ///.
void	Msat_SolverPrintClauses (Msat_Solver_t *p)
void	Msat_SolverWriteDimacs (Msat_Solver_t *p, char *pFileName)

Function Documentation

Msat_SolverPrintAssignment()

void Msat_SolverPrintAssignment

(

Msat_Solver_t *

p

)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file msatSolverIo.c.

{
    int i;
    printf( "Current assignments are: \n" );
    for ( i = 0; i < p->nVars; i++ )
        printf( "%d", i % 10 );
    printf( "\n" );
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pAssigns[i] == MSAT_VAR_UNASSIGNED )
            printf( "." );
        else
        {
            assert( i == MSAT_LIT2VAR(p->pAssigns[i]) );
            if ( MSAT_LITSIGN(p->pAssigns[i]) )
                printf( "0" );
            else 
                printf( "1" );
        }
    printf( "\n" );
}

Msat_SolverPrintClauses()

void Msat_SolverPrintClauses

(

Msat_Solver_t *

p

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file msatSolverIo.c.

{
    Msat_Clause_t ** pClauses;
    int nClauses, i;
 
    printf( "Original clauses: \n" );
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
    {
        printf( "%3d: ", i );
        Msat_ClausePrint( pClauses[i] );
    }
 
    printf( "Learned clauses: \n" );
    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
    {
        printf( "%3d: ", i );
        Msat_ClausePrint( pClauses[i] );
    }
 
    printf( "Variable activity: \n" );
    for ( i = 0; i < p->nVars; i++ )
        printf( "%3d : %.4f\n", i, p->pdActivity[i] );
}

Here is the call graph for this function:

Msat_SolverWriteDimacs()

void Msat_SolverWriteDimacs	(	Msat_Solver_t *	p,
		char *	pFileName )

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 118 of file msatSolverIo.c.

{
    FILE * pFile;
    Msat_Clause_t ** pClauses;
    int nClauses, i;
 
    nClauses = Msat_ClauseVecReadSize(p->vClauses) + Msat_ClauseVecReadSize(p->vLearned);
    for ( i = 0; i < p->nVars; i++ )
        nClauses += ( p->pLevel[i] == 0 );
 
    pFile = fopen( pFileName, "wb" );
    fprintf( pFile, "c Produced by Msat_SolverWriteDimacs() on %s\n", Msat_TimeStamp() );
    fprintf( pFile, "p cnf %d %d\n", p->nVars, nClauses );
 
    nClauses = Msat_ClauseVecReadSize( p->vClauses );
    pClauses = Msat_ClauseVecReadArray( p->vClauses );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
 
    nClauses = Msat_ClauseVecReadSize( p->vLearned );
    pClauses = Msat_ClauseVecReadArray( p->vLearned );
    for ( i = 0; i < nClauses; i++ )
        Msat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
 
    // write zero-level assertions
    for ( i = 0; i < p->nVars; i++ )
        if ( p->pLevel[i] == 0 )
            fprintf( pFile, "%s%d 0\n", ((p->pAssigns[i]&1)? "-": ""), i + 1 );
 
    fprintf( pFile, "\n" );
    fclose( pFile );
}

Here is the call graph for this function: