src/sat/bsat/satTrace.c File Reference

#include <stdio.h>
#include <assert.h>
#include "satSolver.h"

Include dependency graph for satTrace.c:

Go to the source code of this file.

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

---

Function Documentation

void Sat_SolverTraceStart	(	sat_solver *	pSat,
		char *	pName
	)

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

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

Synopsis [Start the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file satTrace.c.

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

void Sat_SolverTraceStop

(

sat_solver *

pSat

)

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

Synopsis [Stops the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 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;
}

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 94 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" );
}