Version abc50905

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;