1 files changed, 0 insertions, 109 deletions
diff --git a/src/sat/bsat/satTrace.c b/src/sat/bsat/satTrace.c
deleted file mode 100644
index 111e8dfb..00000000
--- a/src/sat/bsat/satTrace.c
+++ /dev/null
@@ -1,109 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <assert.h>
-#include "satSolver.h"
-
-/*
-    The trace of SAT solving contains the original clause of the problem
-    along with the learned clauses derived during SAT solving.
-    The first line of the resulting file contains 3 numbers instead of 2:
-    c <num_vars> <num_all_clauses> <num_root_clauses>
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Start the trace recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_SolverTraceStart( sat_solver * pSat, char * pName )
-{
-    assert( pSat->pFile == NULL );
-    pSat->pFile = fopen( pName, "w" );
-    fprintf( pSat->pFile, "                                        \n" );
-    pSat->nClauses = 0;
-    pSat->nRoots = 0;
-}   
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the trace recording.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_SolverTraceStop( sat_solver * pSat )
-{
-    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;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Writes one clause into the trace file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Sat_SolverTraceWrite( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )
-{
-    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" );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-