satTrace.c File Reference

#include "satSolver.h"

Include dependency graph for satTrace.c:

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START void	Sat_SolverTraceStart (sat_solver *pSat, char *pName)
	DECLARATIONS ///.
void	Sat_SolverTraceStop (sat_solver *pSat)
void	Sat_SolverTraceWrite (sat_solver *pSat, int *pBeg, int *pEnd, int fRoot)

Function Documentation

Sat_SolverTraceStart()

ABC_NAMESPACE_IMPL_START void Sat_SolverTraceStart	(	sat_solver *	pSat,
		char *	pName )

DECLARATIONS ///.

CFile****************************************************************

FileName [satTrace.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sat_solver.]

Synopsis [Records the trace of SAT solving in the CNF form.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Start the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file satTrace.c.

{
    assert( pSat->pFile == NULL );
    pSat->pFile = fopen( pName, "w" );
    fprintf( pSat->pFile, "                                        \n" );
    pSat->nClauses = 0;
    pSat->nRoots = 0;
}   

Sat_SolverTraceStop()

void Sat_SolverTraceStop

(

sat_solver *

pSat

)

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

Synopsis [Stops the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file satTrace.c.

{
    if ( pSat->pFile == NULL )
        return;
    rewind( pSat->pFile );
    fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
    fclose( pSat->pFile );
    pSat->pFile = NULL;
}

Here is the call graph for this function:

Sat_SolverTraceWrite()

void Sat_SolverTraceWrite	(	sat_solver *	pSat,
		int *	pBeg,
		int *	pEnd,
		int	fRoot )

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

Synopsis [Writes one clause into the trace file.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file satTrace.c.

{
    if ( pSat->pFile == NULL )
        return;
    pSat->nClauses++;
    pSat->nRoots += fRoot;
    for ( ; pBeg < pEnd ; pBeg++ )
        fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
    fprintf( pSat->pFile, " 0\n" );
}