Major restructuring of the code.

1 files changed, 0 insertions, 123 deletions

diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
deleted file mode 100644
index 6b18a3a6..00000000
--- a/src/aig/ssw/sswSimSat.c
+++ /dev/null
@@ -1,123 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [sswSimSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Inductive prover with constraints.]
-
-  Synopsis    [Performs resimulation using counter-examples.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - September 1, 2008.]
-
-  Revision    [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "sswInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Handle the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr )
-{
-    Aig_Obj_t * pObj;
-    int i, RetValue1, RetValue2, clk = clock();
-    // set the PI simulation information
-    Aig_ManConst1(p->pAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pAig, pObj, i )
-        pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
-    // simulate internal nodes
-    Aig_ManForEachNode( p->pAig, pObj, i )
-        pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
-                     & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
-    // if repr is given, perform refinement
-    if ( pRepr )
-    {
-        // check equivalence classes
-        RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
-        RetValue2 = Ssw_ClassesRefine( p->ppClasses, 0 );
-        // make sure refinement happened
-        if ( Aig_ObjIsConst1(pRepr) ) 
-        {
-            assert( RetValue1 );
-            if ( RetValue1 == 0 )
-                printf( "\nSsw_ManResimulateBit() Error: RetValue1 does not hold.\n" );
-        }
-        else
-        {
-            assert( RetValue2 );
-            if ( RetValue2 == 0 )
-                printf( "\nSsw_ManResimulateBit() Error: RetValue2 does not hold.\n" );
-        }
-    }
-p->timeSimSat += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Handle the counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
-{
-    int RetValue1, RetValue2, clk = clock();
-    // set the PI simulation information
-    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
-    // simulate internal nodes
-    Ssw_SmlSimulateOne( p->pSml );
-    // check equivalence classes
-    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
-    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
-    // make sure refinement happened
-    if ( Aig_ObjIsConst1(pRepr) )
-    {
-        assert( RetValue1 );
-        if ( RetValue1 == 0 )
-            printf( "\nSsw_ManResimulateWord() Error: RetValue1 does not hold.\n" );
-    }
-    else
-    {
-        assert( RetValue2 );
-        if ( RetValue2 == 0 )
-            printf( "\nSsw_ManResimulateWord() Error: RetValue2 does not hold.\n" );
-    }
-p->timeSimSat += clock() - clk;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-