summaryrefslogtreecommitdiffstats
path: root/abc70930/src/opt/sim/simSymSat.c
diff options
context:
space:
mode:
Diffstat (limited to 'abc70930/src/opt/sim/simSymSat.c')
-rw-r--r--abc70930/src/opt/sim/simSymSat.c199
1 files changed, 0 insertions, 199 deletions
diff --git a/abc70930/src/opt/sim/simSymSat.c b/abc70930/src/opt/sim/simSymSat.c
deleted file mode 100644
index 7690a891..00000000
--- a/abc70930/src/opt/sim/simSymSat.c
+++ /dev/null
@@ -1,199 +0,0 @@
-/**CFile****************************************************************
-
- FileName [simSymSat.c]
-
- SystemName [ABC: Logic synthesis and verification system.]
-
- PackageName [Network and node package.]
-
- Synopsis [Satisfiability to determine two variable symmetries.]
-
- Author [Alan Mishchenko]
-
- Affiliation [UC Berkeley]
-
- Date [Ver. 1.0. Started - June 20, 2005.]
-
- Revision [$Id: simSymSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "abc.h"
-#include "sim.h"
-#include "fraig.h"
-
-////////////////////////////////////////////////////////////////////////
-/// DECLARATIONS ///
-////////////////////////////////////////////////////////////////////////
-
-static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern );
-
-////////////////////////////////////////////////////////////////////////
-/// FUNCTION DEFINITIONS ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
- Synopsis [Tries to prove the remaining pairs using SAT.]
-
- Description [Continues to prove as long as it encounters symmetric pairs.
- Returns 1 if a non-symmetric pair is found (which gives a counter-example).
- Returns 0 if it finishes considering all pairs for all outputs.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sim_SymmsGetPatternUsingSat( Sym_Man_t * p, unsigned * pPattern )
-{
- Vec_Int_t * vSupport;
- Extra_BitMat_t * pMatSym, * pMatNonSym;
- int Index1, Index2, Index3, IndexU, IndexV;
- int v, u, i, k, b, out;
-
- // iterate through outputs
- for ( out = p->iOutput; out < p->nOutputs; out++ )
- {
- pMatSym = Vec_PtrEntry( p->vMatrSymms, out );
- pMatNonSym = Vec_PtrEntry( p->vMatrNonSymms, out );
-
- // go through the remaining variable pairs
- vSupport = Vec_VecEntry( p->vSupports, out );
- Vec_IntForEachEntry( vSupport, v, Index1 )
- Vec_IntForEachEntryStart( vSupport, u, Index2, Index1+1 )
- {
- if ( Extra_BitMatrixLookup1( pMatSym, v, u ) || Extra_BitMatrixLookup1( pMatNonSym, v, u ) )
- continue;
- p->nSatRuns++;
-
- // collect the support variables that are symmetric with u and v
- Vec_IntClear( p->vVarsU );
- Vec_IntClear( p->vVarsV );
- Vec_IntForEachEntry( vSupport, b, Index3 )
- {
- if ( Extra_BitMatrixLookup1( pMatSym, u, b ) )
- Vec_IntPush( p->vVarsU, b );
- if ( Extra_BitMatrixLookup1( pMatSym, v, b ) )
- Vec_IntPush( p->vVarsV, b );
- }
-
- if ( Sim_SymmsSatProveOne( p, out, v, u, pPattern ) )
- { // update the symmetric variable info
- p->nSatRunsUnsat++;
- Vec_IntForEachEntry( p->vVarsU, i, IndexU )
- Vec_IntForEachEntry( p->vVarsV, k, IndexV )
- {
- Extra_BitMatrixInsert1( pMatSym, i, k ); // Theorem 1
- Extra_BitMatrixInsert2( pMatSym, i, k ); // Theorem 1
- Extra_BitMatrixOrTwo( pMatNonSym, i, k ); // Theorem 2
- }
- }
- else
- { // update the assymmetric variable info
- p->nSatRunsSat++;
- Vec_IntForEachEntry( p->vVarsU, i, IndexU )
- Vec_IntForEachEntry( p->vVarsV, k, IndexV )
- {
- Extra_BitMatrixInsert1( pMatNonSym, i, k ); // Theorem 3
- Extra_BitMatrixInsert2( pMatNonSym, i, k ); // Theorem 3
- }
-
- // remember the out
- p->iOutput = out;
- p->iVar1Old = p->iVar1;
- p->iVar2Old = p->iVar2;
- p->iVar1 = v;
- p->iVar2 = u;
- return 1;
-
- }
- }
- // make sure that the symmetry matrix contains only cliques
- assert( Extra_BitMatrixIsClique( pMatSym ) );
- }
-
- // mark that we finished all outputs
- p->iOutput = p->nOutputs;
- return 0;
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if the variables are symmetric; 0 otherwise.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern )
-{
- Fraig_Params_t Params;
- Fraig_Man_t * pMan;
- Abc_Ntk_t * pMiter;
- int RetValue, i, clk;
- int * pModel;
-
- // get the miter for this problem
- pMiter = Abc_NtkMiterForCofactors( p->pNtk, Out, Var1, Var2 );
- // transform the miter into a fraig
- Fraig_ParamsSetDefault( &Params );
- Params.fInternal = 1;
- Params.nPatsRand = 512;
- Params.nPatsDyna = 512;
- Params.nSeconds = ABC_INFINITY;
-
-clk = clock();
- pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 );
-p->timeFraig += clock() - clk;
-clk = clock();
- Fraig_ManProveMiter( pMan );
-p->timeSat += clock() - clk;
-
- // analyze the result
- RetValue = Fraig_ManCheckMiter( pMan );
-// assert( RetValue >= 0 );
- // save the pattern
- if ( RetValue == 0 )
- {
- // get the pattern
- pModel = Fraig_ManReadModel( pMan );
- assert( pModel != NULL );
-//printf( "Disproved by SAT: out = %d pair = (%d, %d)\n", Out, Var1, Var2 );
- // transfer the model into the pattern
- for ( i = 0; i < p->nSimWords; i++ )
- pPattern[i] = 0;
- for ( i = 0; i < p->nInputs; i++ )
- if ( pModel[i] )
- Sim_SetBit( pPattern, i );
- // make sure these variables have the same value (1)
- Sim_SetBit( pPattern, Var1 );
- Sim_SetBit( pPattern, Var2 );
- }
- else if ( RetValue == -1 )
- {
- // this should never happen; if it happens, such is life
- // we are conservative and assume that there is no symmetry
-//printf( "STRANGE THING: out = %d %s pair = (%d %s, %d %s)\n",
-// Out, Abc_ObjName(Abc_NtkCo(p->pNtk,Out)),
-// Var1, Abc_ObjName(Abc_NtkCi(p->pNtk,Var1)),
-// Var2, Abc_ObjName(Abc_NtkCi(p->pNtk,Var2)) );
- memset( pPattern, 0, sizeof(unsigned) * p->nSimWords );
- RetValue = 0;
- }
- // delete the fraig manager
- Fraig_ManFree( pMan );
- // delete the miter
- Abc_NtkDelete( pMiter );
- return RetValue;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-/// END OF FILE ///
-////////////////////////////////////////////////////////////////////////
-
-
generated by cgit v1.2.3 (git 2.25.1) at 2025-09-13 11:50:57 +0000