summaryrefslogtreecommitdiffstats
path: root/src/sat/fraig
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/fraig')
-rw-r--r--src/sat/fraig/fraig.h16
-rw-r--r--src/sat/fraig/fraigApi.c5
-rw-r--r--src/sat/fraig/fraigCanon.c5
-rw-r--r--src/sat/fraig/fraigChoice.c5
-rw-r--r--src/sat/fraig/fraigFanout.c5
-rw-r--r--src/sat/fraig/fraigFeed.c7
-rw-r--r--src/sat/fraig/fraigInt.h12
-rw-r--r--src/sat/fraig/fraigMan.c11
-rw-r--r--src/sat/fraig/fraigMem.c15
-rw-r--r--src/sat/fraig/fraigNode.c5
-rw-r--r--src/sat/fraig/fraigPrime.c5
-rw-r--r--src/sat/fraig/fraigSat.c14
-rw-r--r--src/sat/fraig/fraigTable.c5
-rw-r--r--src/sat/fraig/fraigUtil.c7
-rw-r--r--src/sat/fraig/fraigVec.c5
15 files changed, 99 insertions, 23 deletions
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index ce686cef..2b499967 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -19,6 +19,7 @@
#ifndef __FRAIG_H__
#define __FRAIG_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -27,9 +28,10 @@
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-extern "C" {
-#endif
+
+
+ABC_NAMESPACE_HEADER_START
+
////////////////////////////////////////////////////////////////////////
/// STRUCTURE DEFINITIONS ///
@@ -249,8 +251,10 @@ extern Fraig_NodeVec_t * Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
-#ifdef __cplusplus
-}
-#endif
+
+
+ABC_NAMESPACE_HEADER_END
+
+
#endif
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index 79a7c224..6e0ab959 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -295,3 +298,5 @@ void Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t * pNodeOld, Fraig_Nod
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index 89bc924f..47539db2 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -19,6 +19,9 @@
#include <limits.h>
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -216,3 +219,5 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigChoice.c b/src/sat/fraig/fraigChoice.c
index 896e5d2d..21d4fe10 100644
--- a/src/sat/fraig/fraigChoice.c
+++ b/src/sat/fraig/fraigChoice.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -239,3 +242,5 @@ Fraig_ManCheckConsistency( pMan );
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigFanout.c b/src/sat/fraig/fraigFanout.c
index 789bffca..0e6c86f8 100644
--- a/src/sat/fraig/fraigFanout.c
+++ b/src/sat/fraig/fraigFanout.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
#ifdef FRAIG_ENABLE_FANOUTS
////////////////////////////////////////////////////////////////////////
@@ -173,3 +176,5 @@ int Fraig_NodeGetFanoutNum( Fraig_Node_t * pNode )
#endif
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c
index 7977824d..47f946e1 100644
--- a/src/sat/fraig/fraigFeed.c
+++ b/src/sat/fraig/fraigFeed.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -736,7 +739,7 @@ void Fraig_ReallocateSimulationInfo( Fraig_Man_t * p )
// signatures remain without changes
}
- // replace the manager to ABC_FREE up some memory
+ // replace the manager to free up some memory
Fraig_MemFixedStop( p->mmSims, 0 );
p->mmSims = mmSimsNew;
@@ -906,3 +909,5 @@ printf( "\n" );
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index ac6ea873..7cc2194a 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -19,6 +19,7 @@
#ifndef __FRAIG_INT_H__
#define __FRAIG_INT_H__
+
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
@@ -33,6 +34,9 @@
#include "fraig.h"
#include "msat.h"
+ABC_NAMESPACE_HEADER_START
+
+
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
@@ -57,9 +61,9 @@
#define FRAIG_MAX_PRIMES 1024 // the maximum number of primes used for hashing
// this parameter determines when simulation info is extended
-// it will be extended when the ABC_FREE storage in the dynamic simulation
+// it will be extended when the free storage in the dynamic simulation
// info is less or equal to this number of words (FRAIG_WORDS_STORE)
-// this is done because if the ABC_FREE storage for dynamic simulation info
+// this is done because if the free storage for dynamic simulation info
// is not sufficient, computation becomes inefficient
#define FRAIG_WORDS_STORE 5
@@ -419,6 +423,10 @@ extern int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig
/*=== fraigVec.c ===============================================================*/
extern void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
+
+
+ABC_NAMESPACE_HEADER_END
+
#endif
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index b71262d8..ba08d793 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -42,7 +45,7 @@ int timeAssign;
***********************************************************************/
void Prove_ParamsSetDefault( Prove_Params_t * pParams )
{
- // clean the parameter structure
+ // clean the parameter structure
memset( pParams, 0, sizeof(Prove_Params_t) );
// general parameters
pParams->fUseFraiging = 1; // enables fraiging
@@ -52,7 +55,7 @@ void Prove_ParamsSetDefault( Prove_Params_t * pParams )
// iterations
pParams->nItersMax = 6; // the number of iterations
// mitering
- pParams->nMiteringLimitStart = 300; // starting mitering limit
+ pParams->nMiteringLimitStart = 5000; // starting mitering limit
pParams->nMiteringLimitMulti = 2.0; // multiplicative coefficient to increase the limit in each iteration
// rewriting (currently not used)
pParams->nRewritingLimitStart = 3; // the number of rewriting iterations
@@ -382,7 +385,7 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
SeeAlso []
***********************************************************************/
-Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
+Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, int fClean )
{
Fraig_NodeVec_t * vInfo;
unsigned * pUnsigned;
@@ -538,3 +541,5 @@ void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigMem.c b/src/sat/fraig/fraigMem.c
index 1cc99790..ef52765e 100644
--- a/src/sat/fraig/fraigMem.c
+++ b/src/sat/fraig/fraigMem.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -29,7 +32,7 @@ struct Fraig_MemFixed_t_
int nEntriesAlloc; // the total number of entries allocated
int nEntriesUsed; // the number of entries in use
int nEntriesMax; // the max number of entries in use
- char * pEntriesFree; // the linked list of ABC_FREE entries
+ char * pEntriesFree; // the linked list of free entries
// this is where the memory is stored
int nChunkSize; // the size of one chunk
@@ -130,7 +133,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p )
char * pTemp;
int i;
- // check if there are still ABC_FREE entries
+ // check if there are still free entries
if ( p->nEntriesUsed == p->nEntriesAlloc )
{ // need to allocate more entries
assert( p->pEntriesFree == NULL );
@@ -159,7 +162,7 @@ char * Fraig_MemFixedEntryFetch( Fraig_MemFixed_t * p )
p->nEntriesUsed++;
if ( p->nEntriesMax < p->nEntriesUsed )
p->nEntriesMax = p->nEntriesUsed;
- // return the first entry in the ABC_FREE entry list
+ // return the first entry in the free entry list
pTemp = p->pEntriesFree;
p->pEntriesFree = *((char **)pTemp);
return pTemp;
@@ -180,7 +183,7 @@ void Fraig_MemFixedEntryRecycle( Fraig_MemFixed_t * p, char * pEntry )
{
// decrement the counter of used entries
p->nEntriesUsed--;
- // add the entry to the linked list of ABC_FREE entries
+ // add the entry to the linked list of free entries
*((char **)pEntry) = p->pEntriesFree;
p->pEntriesFree = pEntry;
}
@@ -214,7 +217,7 @@ void Fraig_MemFixedRestart( Fraig_MemFixed_t * p )
}
// set the last link
*((char **)pTemp) = NULL;
- // set the ABC_FREE entry list
+ // set the free entry list
p->pEntriesFree = p->pChunks[0];
// set the correct statistics
p->nMemoryAlloc = p->nEntrySize * p->nChunkSize;
@@ -244,3 +247,5 @@ int Fraig_MemFixedReadMemUsage( Fraig_MemFixed_t * p )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 4cfe035d..9f95cd46 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -311,3 +314,5 @@ void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, in
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigPrime.c b/src/sat/fraig/fraigPrime.c
index 127ad478..42a079fd 100644
--- a/src/sat/fraig/fraigPrime.c
+++ b/src/sat/fraig/fraigPrime.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -142,3 +145,5 @@ unsigned int Cudd_PrimeFraig( unsigned int p)
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c
index 084d1538..b96bc5a1 100644
--- a/src/sat/fraig/fraigSat.c
+++ b/src/sat/fraig/fraigSat.c
@@ -16,8 +16,12 @@
***********************************************************************/
+#include <math.h>
#include "fraigInt.h"
-#include "math.h"
+#include "msatInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -36,8 +40,6 @@ static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNo
static void Fraig_DetectFanoutFreeConeMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
static void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew );
-extern void * Msat_ClauseVecReadEntry( void * p, int i );
-
// The lesson learned seems to be that variable should be in reverse topological order
// from the output of the miter. The ordering of adjacency lists is very important.
// The best way seems to be fanins followed by fanouts. Slight changes to this order
@@ -318,7 +320,7 @@ int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t *
// nBTLimit /= 10;
if ( nBTLimit <= 10 )
return 0;
- nBTLimit = (int)sqrt(nBTLimit);
+ nBTLimit = (int)sqrt((double)nBTLimit);
// fSwitch = 1;
}
@@ -907,7 +909,7 @@ void Fraig_OrderVariables( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t
{
// create the fanins of the supergate
assert( pNode->fClauses == 0 );
- // detecting a fanout-ABC_FREE cone (experiment only)
+ // detecting a fanout-free cone (experiment only)
// Fraig_DetectFanoutFreeCone( pMan, pNode );
if ( fUseMuxes && Fraig_NodeIsMuxType(pNode) )
@@ -1453,3 +1455,5 @@ void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t *
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 55d92b4a..79ab7ffc 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -655,3 +658,5 @@ int Fraig_TableRehashF0( Fraig_Man_t * pMan, int fLinkEquiv )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigUtil.c b/src/sat/fraig/fraigUtil.c
index 0930edbd..0d4cdfaf 100644
--- a/src/sat/fraig/fraigUtil.c
+++ b/src/sat/fraig/fraigUtil.c
@@ -19,6 +19,9 @@
#include "fraigInt.h"
#include <limits.h>
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -237,7 +240,7 @@ int Fraig_CheckTfi2( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNe
Description [This procedure collects the nodes reachable from
the POs of the AIG and sets the type of fanout counter (none, one,
or many) for each node. This procedure is useful to determine
- fanout-ABC_FREE cones of AND-nodes, which is helpful for rebalancing
+ fanout-free cones of AND-nodes, which is helpful for rebalancing
the AIG (see procedure Fraig_ManRebalance, or something like that).]
SideEffects []
@@ -1032,3 +1035,5 @@ int Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig_Node_t * pNode )
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/fraig/fraigVec.c b/src/sat/fraig/fraigVec.c
index b47c6a2f..25d50bf3 100644
--- a/src/sat/fraig/fraigVec.c
+++ b/src/sat/fraig/fraigVec.c
@@ -18,6 +18,9 @@
#include "fraigInt.h"
+ABC_NAMESPACE_IMPL_START
+
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -543,3 +546,5 @@ void Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p )
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-15 08:25:52 +0000