summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig/fraigMan.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/fraig/fraigMan.c')
-rw-r--r--src/sat/fraig/fraigMan.c237
1 files changed, 237 insertions, 0 deletions
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
new file mode 100644
index 00000000..d41f5d0b
--- /dev/null
+++ b/src/sat/fraig/fraigMan.c
@@ -0,0 +1,237 @@
+/**CFile****************************************************************
+
+ FileName [fraigMan.c]
+
+ PackageName [FRAIG: Functionally reduced AND-INV graphs.]
+
+ Synopsis [Implementation of the FRAIG manager.]
+
+ Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 2.0. Started - October 1, 2004]
+
+ Revision [$Id: fraigMan.c,v 1.11 2005/07/08 01:01:31 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fraigInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+int timeSelect;
+int timeAssign;
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Sets the default parameters of the package.]
+
+ Description [This set of parameters is tuned for equivalence checking.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
+{
+ pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info
+ pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
+ pParams->nBTLimit = 99; // the max number of backtracks to perform
+ pParams->fFuncRed = 1; // performs only one level hashing
+ pParams->fFeedBack = 1; // enables solver feedback
+ pParams->fDist1Pats = 1; // enables distance-1 patterns
+ pParams->fDoSparse = 0; // performs equiv tests for sparse functions
+ pParams->fChoicing = 0; // enables recording structural choices
+ pParams->fTryProve = 1; // tries to solve the final miter
+ pParams->fVerbose = 0; // the verbosiness flag
+ pParams->fVerboseP = 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates the new FRAIG manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
+{
+ Fraig_Params_t Params;
+ Fraig_Man_t * p;
+
+ // set the random seed for simulation
+ srand( 0xFEEDDEAF );
+
+ // set parameters for equivalence checking
+ if ( pParams == NULL )
+ Fraig_ParamsSetDefault( pParams = &Params );
+ // adjust the amount of simulation info
+ if ( pParams->nPatsRand < 128 )
+ pParams->nPatsRand = 128;
+ if ( pParams->nPatsRand > 32768 )
+ pParams->nPatsRand = 32768;
+ if ( pParams->nPatsDyna < 128 )
+ pParams->nPatsDyna = 128;
+ if ( pParams->nPatsDyna > 32768 )
+ pParams->nPatsDyna = 32768;
+ // if reduction is not performed, allocate minimum simulation info
+ if ( !pParams->fFuncRed )
+ pParams->nPatsRand = pParams->nPatsDyna = 128;
+
+ // start the manager
+ p = ALLOC( Fraig_Man_t, 1 );
+ memset( p, 0, sizeof(Fraig_Man_t) );
+
+ // set the default parameters
+ p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info
+ p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info
+ p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit
+ p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed)
+ p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation)
+ p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation)
+ p->fDoSparse = pParams->fDoSparse; // performs equivalence checking for sparse functions (whose sim-info is 0)
+ p->fChoicing = pParams->fChoicing; // disable accumulation of structural choices (keeps only the first choice)
+ p->fTryProve = pParams->fTryProve; // disable accumulation of structural choices (keeps only the first choice)
+ p->fVerbose = pParams->fVerbose; // disable verbose output
+ p->fVerboseP = pParams->fVerboseP; // disable verbose output
+
+ // start memory managers
+ p->mmNodes = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
+ p->mmSims = Fraig_MemFixedStart( sizeof(unsigned) * (p->nWordsRand + p->nWordsDyna) );
+ // allocate node arrays
+ p->vInputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary inputs
+ p->vOutputs = Fraig_NodeVecAlloc( 1000 ); // the array of primary outputs
+ p->vNodes = Fraig_NodeVecAlloc( 1000 ); // the array of internal nodes
+ // start the tables
+ p->pTableS = Fraig_HashTableCreate( 1000 ); // hashing by structure
+ p->pTableF = Fraig_HashTableCreate( 1000 ); // hashing by function
+ p->pTableF0 = Fraig_HashTableCreate( 1000 ); // hashing by function (for sparse functions)
+ // create the constant node
+ p->pConst1 = Fraig_NodeCreateConst( p );
+ // initialize SAT solver feedback data structures
+ Fraig_FeedBackInit( p );
+ // initialize other variables
+ p->vProj = Msat_IntVecAlloc( 10 );
+ p->nTravIds = 1;
+ p->nTravIds2 = 1;
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fraig_ManFree( Fraig_Man_t * p )
+{
+ int i;
+ if ( p->fVerbose )
+ {
+ if ( p->fChoicing ) Fraig_ManReportChoices( p );
+ Fraig_ManPrintStats( p );
+// Fraig_TablePrintStatsS( p );
+// Fraig_TablePrintStatsF( p );
+// Fraig_TablePrintStatsF0( p );
+ }
+
+ for ( i = 0; i < p->vNodes->nSize; i++ )
+ if ( p->vNodes->pArray[i]->vFanins )
+ {
+ Fraig_NodeVecFree( p->vNodes->pArray[i]->vFanins );
+ p->vNodes->pArray[i]->vFanins = NULL;
+ }
+
+ if ( p->vInputs ) Fraig_NodeVecFree( p->vInputs );
+ if ( p->vNodes ) Fraig_NodeVecFree( p->vNodes );
+ if ( p->vOutputs ) Fraig_NodeVecFree( p->vOutputs );
+
+ if ( p->pTableS ) Fraig_HashTableFree( p->pTableS );
+ if ( p->pTableF ) Fraig_HashTableFree( p->pTableF );
+ if ( p->pTableF0 ) Fraig_HashTableFree( p->pTableF0 );
+
+ if ( p->pSat ) Msat_SolverFree( p->pSat );
+ if ( p->vProj ) Msat_IntVecFree( p->vProj );
+ if ( p->vCones ) Fraig_NodeVecFree( p->vCones );
+ if ( p->vPatsReal ) Msat_IntVecFree( p->vPatsReal );
+
+ Fraig_MemFixedStop( p->mmNodes, 0 );
+ Fraig_MemFixedStop( p->mmSims, 0 );
+
+ if ( p->pSuppS )
+ {
+ FREE( p->pSuppS[0] );
+ FREE( p->pSuppS );
+ }
+ if ( p->pSuppF )
+ {
+ FREE( p->pSuppF[0] );
+ FREE( p->pSuppF );
+ }
+
+ FREE( p->ppOutputNames );
+ FREE( p->ppInputNames );
+ FREE( p );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Deallocates the mapping manager.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Fraig_ManPrintStats( Fraig_Man_t * p )
+{
+ double nMemory;
+ int clk = clock();
+ nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) *
+ (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20);
+ printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n",
+ p->nWordsRand, p->nWordsDyna, p->iWordPerm, nMemory );
+ printf( "Proof = %d. Counter-example = %d. Fail = %d. Zero = %d.\n",
+ p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatZeros );
+ printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) ClaVars = %d.\n",
+ Fraig_CountNodes(p,0), p->vNodes->nSize, Fraig_ManCountMuxes(p), Fraig_ManCountExors(p), p->nVarsClauses );
+ if ( p->pSat ) Msat_SolverPrintStats( p->pSat );
+ Fraig_PrintTime( "AIG simulation ", p->timeSims );
+ Fraig_PrintTime( "AIG traversal ", p->timeTrav );
+ Fraig_PrintTime( "Solver feedback ", p->timeFeed );
+ Fraig_PrintTime( "SAT solving ", p->timeSat );
+ Fraig_PrintTime( "Network update ", p->timeToNet );
+ Fraig_PrintTime( "TOTAL RUNTIME ", p->timeTotal );
+ if ( p->time1 > 0 ) { Fraig_PrintTime( "time1", p->time1 ); }
+ if ( p->time2 > 0 ) { Fraig_PrintTime( "time2", p->time2 ); }
+ if ( p->time3 > 0 ) { Fraig_PrintTime( "time3", p->time3 ); }
+ if ( p->time4 > 0 ) { Fraig_PrintTime( "time4", p->time4 ); }
+// PRT( "Selection ", timeSelect );
+// PRT( "Assignment", timeAssign );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:36:53 +0000