summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/csat/csat_apis.c43
-rw-r--r--src/sat/fraig/fraig.h6
-rw-r--r--src/sat/fraig/fraigApi.c14
-rw-r--r--src/sat/fraig/fraigCanon.c2
-rw-r--r--src/sat/fraig/fraigInt.h2
-rw-r--r--src/sat/fraig/fraigMan.c3
-rw-r--r--src/sat/fraig/fraigNode.c4
-rw-r--r--src/sat/fraig/fraigTable.c4
8 files changed, 62 insertions, 16 deletions
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 242de8e2..b030caef 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -28,8 +28,9 @@ struct CSAT_ManagerStruct_t
{
// information about the problem
stmm_table * tName2Node; // the hash table mapping names to nodes
+ stmm_table * tNode2Name; // the hash table mapping nodes to names
Abc_Ntk_t * pNtk; // the starting ABC network
- Abc_Ntk_t * pTarget; // the AIG of the target
+ Abc_Ntk_t * pTarget; // the AIG representing the target
char * pDumpFileName; // the name of the file to dump the target network
// solving parameters
int mode; // 0 = baseline; 1 = resource-aware fraiging
@@ -44,6 +45,7 @@ struct CSAT_ManagerStruct_t
static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars );
static void CSAT_TargetResFree( CSAT_Target_ResultT * p );
+static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode );
// some external procedures
extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes );
@@ -72,8 +74,9 @@ CSAT_Manager CSAT_InitManager()
mng->pNtk = Abc_NtkAlloc( ABC_TYPE_LOGIC, ABC_FUNC_SOP );
mng->pNtk->pName = util_strsav("csat_network");
mng->tName2Node = stmm_init_table(strcmp, stmm_strhash);
- mng->vNodes = Vec_PtrAlloc( 100 );
- mng->vValues = Vec_IntAlloc( 100 );
+ mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+ mng->vNodes = Vec_PtrAlloc( 100 );
+ mng->vValues = Vec_IntAlloc( 100 );
return mng;
}
@@ -90,6 +93,7 @@ CSAT_Manager CSAT_InitManager()
***********************************************************************/
void CSAT_QuitManager( CSAT_Manager mng )
{
+ if ( mng->tNode2Name ) stmm_free_table( mng->tNode2Name );
if ( mng->tName2Node ) stmm_free_table( mng->tName2Node );
if ( mng->pNtk ) Abc_NtkDelete( mng->pNtk );
if ( mng->pTarget ) Abc_NtkDelete( mng->pTarget );
@@ -151,7 +155,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
{ printf( "CSAT_AddGate: The PI/PPI gate \"%s\" has fanins.\n", name ); return 0; }
// create the PI
pObj = Abc_NtkCreatePi( mng->pNtk );
- pObj->pNext = (Abc_Obj_t *)name;
+ stmm_insert( mng->tNode2Name, (char *)pObj, name );
break;
case CSAT_CONST:
case CSAT_BAND:
@@ -234,7 +238,7 @@ int CSAT_AddGate( CSAT_Manager mng, enum GateType type, char * name, int nofi, c
{ printf( "CSAT_AddGate: The PO/PPO gate \"%s\" does not have exactly one fanin.\n", name ); return 0; }
// create the PO
pObj = Abc_NtkCreatePo( mng->pNtk );
- pObj->pNext = (Abc_Obj_t *)name;
+ stmm_insert( mng->tNode2Name, (char *)pObj, name );
// connect to the PO fanin
if ( !stmm_lookup( mng->tName2Node, fanins[0], (char **)&pFanin ) )
{ printf( "CSAT_AddGate: The fanin gate \"%s\" is not in the network.\n", fanins[0] ); return 0; }
@@ -270,13 +274,13 @@ int CSAT_Check_Integrity( CSAT_Manager mng )
// this procedure also finalizes construction of the ABC network
Abc_NtkFixNonDrivenNets( pNtk );
Abc_NtkForEachPi( pNtk, pObj, i )
- Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+ Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
Abc_NtkForEachPo( pNtk, pObj, i )
- Abc_NtkLogicStoreName( pObj, (char *)pObj->pNext );
+ Abc_NtkLogicStoreName( pObj, CSAT_GetNodeName(mng, pObj) );
assert( Abc_NtkLatchNum(pNtk) == 0 );
// make sure everything is okay with the network structure
- if ( !Abc_NtkCheck( pNtk ) )
+ if ( !Abc_NtkCheckRead( pNtk ) )
{
printf( "CSAT_Check_Integrity: The internal network check has failed.\n" );
return 0;
@@ -520,7 +524,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
// create the array of PI names and values
for ( i = 0; i < mng->pResult->no_sig; i++ )
{
- mng->pResult->names[i] = (char *)Abc_NtkCi(mng->pNtk, i)->pNext; // returns the same string that was given
+ mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given
mng->pResult->values[i] = pModel[i];
}
}
@@ -623,6 +627,27 @@ void CSAT_TargetResFree( CSAT_Target_ResultT * p )
free( p );
}
+/**Function*************************************************************
+
+ Synopsis [Dumps the target AIG into the BENCH file.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode )
+{
+ char * pName = NULL;
+ if ( !stmm_lookup( mng->tNode2Name, (char *)pNode, (char **)&pName ) )
+ {
+ assert( 0 );
+ }
+ return pName;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 39c6fae8..901bbac9 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -36,6 +36,7 @@ typedef struct Fraig_NodeStruct_t_ Fraig_Node_t;
typedef struct Fraig_NodeVecStruct_t_ Fraig_NodeVec_t;
typedef struct Fraig_HashTableStruct_t_ Fraig_HashTable_t;
typedef struct Fraig_ParamsStruct_t_ Fraig_Params_t;
+typedef struct Fraig_PatternsStruct_t_ Fraig_Patterns_t;
struct Fraig_ParamsStruct_t_
{
@@ -99,6 +100,9 @@ extern int Fraig_ManReadDoSparse( Fraig_Man_t * p );
extern int Fraig_ManReadChoicing( Fraig_Man_t * p );
extern int Fraig_ManReadVerbose( Fraig_Man_t * p );
extern int * Fraig_ManReadModel( Fraig_Man_t * p );
+extern int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
+extern int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
+extern int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
extern void Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );
extern void Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );
@@ -124,6 +128,8 @@ extern int Fraig_NodeReadNumRefs( Fraig_Node_t * p );
extern int Fraig_NodeReadNumFanouts( Fraig_Node_t * p );
extern int Fraig_NodeReadSimInv( Fraig_Node_t * p );
extern int Fraig_NodeReadNumOnes( Fraig_Node_t * p );
+extern unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p );
+extern unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p );
extern void Fraig_NodeSetData0( Fraig_Node_t * p, Fraig_Node_t * pData );
extern void Fraig_NodeSetData1( Fraig_Node_t * p, Fraig_Node_t * pData );
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index c9e6960c..b92f6afd 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [fraigAccess.c]
+ FileName [fraigApi.c]
PackageName [FRAIG: Functionally reduced AND-INV graphs.]
@@ -58,6 +58,12 @@ int Fraig_ManReadDoSparse( Fraig_Man_t * p ) {
int Fraig_ManReadChoicing( Fraig_Man_t * p ) { return p->fChoicing; }
int Fraig_ManReadVerbose( Fraig_Man_t * p ) { return p->fVerbose; }
int * Fraig_ManReadModel( Fraig_Man_t * p ) { return p->pModel; }
+// returns the number of patterns used for random simulation (this number is fixed for the FRAIG run)
+int Fraig_ManReadPatternNumRandom( Fraig_Man_t * p ) { return p->nWordsRand * 32; }
+// returns the number of dynamic patterns accumulated at runtime (include SAT solver counter-examples and distance-1 patterns derived from them)
+int Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p ) { return p->iWordStart * 32; }
+// returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
+int Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p ) { return p->iPatsPerm; }
/**Function*************************************************************
@@ -104,6 +110,12 @@ int Fraig_NodeReadNumRefs( Fraig_Node_t * p ) { retu
int Fraig_NodeReadNumFanouts( Fraig_Node_t * p ) { return p->nFanouts; }
int Fraig_NodeReadSimInv( Fraig_Node_t * p ) { return p->fInv; }
int Fraig_NodeReadNumOnes( Fraig_Node_t * p ) { return p->nOnes; }
+// returns the pointer to the random simulation patterns (their number is returned by Fraig_ManReadPatternNumRandom)
+// memory pointed to by this and the following procedure is maintained by the FRAIG package and exists as long as the package runs
+unsigned * Fraig_NodeReadPatternsRandom( Fraig_Node_t * p ) { return p->puSimR; }
+// returns the pointer to the dynamic simulation patterns (their number is returned by Fraig_ManReadPatternNumDynamic or Fraig_ManReadPatternNumDynamicFiltered)
+// if the number of patterns is not evenly divisible by 32, the patterns beyond the given number contain garbage
+unsigned * Fraig_NodeReadPatternsDynamic( Fraig_Node_t * p ) { return p->puSimD; }
/**Function*************************************************************
diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c
index ae20531d..5a7d0563 100644
--- a/src/sat/fraig/fraigCanon.c
+++ b/src/sat/fraig/fraigCanon.c
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [fraigAnd.c]
+ FileName [fraigCanon.c]
PackageName [FRAIG: Functionally reduced AND-INV graphs.]
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index 1c765c12..131b750c 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -259,8 +259,6 @@ struct Fraig_NodeStruct_t_
Fraig_Node_t * pRepr; // the canonical functional representative of the node
// simulation data
-// Fraig_Sims_t * pSimsR; // the random simulation info
-// Fraig_Sims_t * pSimsD; // the systematic simulation info
unsigned uHashR; // the hash value for random information
unsigned uHashD; // the hash value for dynamic information
unsigned * puSimR; // the simulation information (random)
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index cfdba619..e5979c93 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -53,7 +53,8 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
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;
+ pParams->fVerboseP = 0; // the verbose flag for reporting the proof
+ pParams->fInternal = 0; // the flag indicates the internal run
}
/**Function*************************************************************
diff --git a/src/sat/fraig/fraigNode.c b/src/sat/fraig/fraigNode.c
index 9da9b88c..a6c1d5a6 100644
--- a/src/sat/fraig/fraigNode.c
+++ b/src/sat/fraig/fraigNode.c
@@ -113,6 +113,10 @@ clk = clock();
{
// generate the simulation info
pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
+ // for reasons that take very long to explain, it makes sense to have (0000000...)
+ // pattern in the set (this helps if we need to return the counter-examples)
+ if ( i == 0 )
+ pNode->puSimR[i] <<= 1;
// compute the hash key
pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
}
diff --git a/src/sat/fraig/fraigTable.c b/src/sat/fraig/fraigTable.c
index 7a8af749..d0f22acd 100644
--- a/src/sat/fraig/fraigTable.c
+++ b/src/sat/fraig/fraigTable.c
@@ -355,7 +355,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
return 0;
// check the simulation info
for ( i = 0; i < iWordLast; i++ )
- if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
+ if ( pNode1->puSimR[i] != pNode2->puSimR[i] )
return 0;
}
else
@@ -365,7 +365,7 @@ int Fraig_CompareSimInfo( Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int iWor
return 0;
// check the simulation info
for ( i = 0; i < iWordLast; i++ )
- if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
+ if ( pNode1->puSimD[i] != pNode2->puSimD[i] )
return 0;
}
return 1;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-07 19:16:32 +0000