Version abc80130

1 files changed, 5 insertions, 305 deletions

diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index 7fd937d5..e5979c93 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -26,7 +26,7 @@ int timeSelect;
 int timeAssign;
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -40,89 +40,12 @@ int timeAssign;
   SeeAlso     []
 
 ***********************************************************************/
-void Prove_ParamsSetDefault( Prove_Params_t * pParams )
-{
-    // clean the parameter structure
-    memset( pParams, 0, sizeof(Prove_Params_t) );
-    // general parameters
-    pParams->fUseFraiging         = 1;       // enables fraiging
-    pParams->fUseRewriting        = 1;       // enables rewriting
-    pParams->fUseBdds             = 0;       // enables BDD construction when other methods fail
-    pParams->fVerbose             = 0;       // prints verbose stats
-    // iterations
-    pParams->nItersMax            = 6;       // the number of iterations
-    // mitering 
-    pParams->nMiteringLimitStart  = 300;    // 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
-    pParams->nRewritingLimitMulti = 1.0;     // multiplicative coefficient to increase the limit in each iteration
-    // fraiging 
-    pParams->nFraigingLimitStart  = 2;       // starting backtrack(conflict) limit
-    pParams->nFraigingLimitMulti  = 8.0;     // multiplicative coefficient to increase the limit in each iteration
-    // last-gasp BDD construction
-    pParams->nBddSizeLimit        = 1000000; // the number of BDD nodes when construction is aborted
-    pParams->fBddReorder          = 1;       // enables dynamic BDD variable reordering
-    // last-gasp mitering
-//    pParams->nMiteringLimitLast   = 1000000; // final mitering limit
-    pParams->nMiteringLimitLast   = 0;       // final mitering limit
-    // global SAT solver limits
-    pParams->nTotalBacktrackLimit = 0;       // global limit on the number of backtracks
-    pParams->nTotalInspectLimit   = 0;       // global limit on the number of clause inspects
-//    pParams->nTotalInspectLimit   = 100000000;  // global limit on the number of clause inspects
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints out the current values of CEC engine parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Prove_ParamsPrint( Prove_Params_t * pParams )
-{
-    printf( "CEC enging parameters:\n" );
-    printf( "Fraiging enabled: %s\n", pParams->fUseFraiging? "yes":"no" );
-    printf( "Rewriting enabled: %s\n", pParams->fUseRewriting? "yes":"no" );
-    printf( "BDD construction enabled: %s\n", pParams->fUseBdds? "yes":"no" );
-    printf( "Verbose output enabled: %s\n", pParams->fVerbose? "yes":"no" );
-    printf( "Solver iterations: %d\n", pParams->nItersMax );
-    printf( "Starting mitering limit: %d\n", pParams->nMiteringLimitStart );
-    printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti );
-    printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart );
-    printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti );
-    printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti );
-    printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti );
-    printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit );
-    printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" );
-    printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast );
-    printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit );
-    printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit );
-    printf( "Parameter dump complete.\n" );
-}
-
-/**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 )
 {
     memset( pParams, 0, sizeof(Fraig_Params_t) );
     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->nSeconds   = 20;                     // the max number of seconds to solve the miter
     pParams->fFuncRed   =  1;                     // performs only one level hashing
     pParams->fFeedBack  =  1;                     // enables solver feedback
     pParams->fDist1Pats =  1;                     // enables distance-1 patterns
@@ -132,39 +55,6 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
     pParams->fVerbose   =  0;                     // the verbosiness flag
     pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
     pParams->fInternal  =  0;                     // the flag indicates the internal run 
-    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
-    pParams->nInspLimit =  0;                     // the limit on the number of inspections
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the default parameters of the package.]
-
-  Description [This set of parameters is tuned for complete FRAIGing.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
-{
-    memset( pParams, 0, sizeof(Fraig_Params_t) );
-    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   = -1;                     // the max number of backtracks to perform
-    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
-    pParams->fFuncRed   =  1;                     // performs only one level hashing
-    pParams->fFeedBack  =  1;                     // enables solver feedback
-    pParams->fDist1Pats =  1;                     // enables distance-1 patterns
-    pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
-    pParams->fChoicing  =  0;                     // enables recording structural choices
-    pParams->fTryProve  =  0;                     // tries to solve the final miter
-    pParams->fVerbose   =  0;                     // the verbosiness flag
-    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
-    pParams->fInternal  =  0;                     // the flag indicates the internal run 
-    pParams->nConfLimit =  0;                     // the limit on the number of conflicts
-    pParams->nInspLimit =  0;                     // the limit on the number of inspections
 }
 
 /**Function*************************************************************
@@ -184,8 +74,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     Fraig_Man_t * p;
 
     // set the random seed for simulation
-//    srand( 0xFEEDDEAF );
-    srand( 0xDEADCAFE );
+    srand( 0xFEEDDEAF );
 
     // set parameters for equivalence checking
     if ( pParams == NULL )
@@ -211,7 +100,6 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     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->nSeconds   = pParams->nSeconds;    // the timeout for the final miter
     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)
@@ -220,7 +108,6 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams )
     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
-    p->nInspLimit = pParams->nInspLimit;  // the limit on the number of inspections
 
     // start memory managers
     p->mmNodes    = Fraig_MemFixedStart( sizeof(Fraig_Node_t) );
@@ -266,7 +153,7 @@ void Fraig_ManFree( Fraig_Man_t * p )
 //        Fraig_TablePrintStatsF( p );
 //        Fraig_TablePrintStatsF0( p );
     }
- 
+
     for ( i = 0; i < p->vNodes->nSize; i++ )
         if ( p->vNodes->pArray[i]->vFanins )
         {
@@ -307,31 +194,6 @@ void Fraig_ManFree( Fraig_Man_t * p )
     FREE( p );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Prepares the SAT solver to run on the two nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_ManCreateSolver( Fraig_Man_t * p )
-{
-    extern int timeSelect;
-    extern int timeAssign;
-    assert( p->pSat == NULL );
-    // allocate data for SAT solving
-    p->pSat       = Msat_SolverAlloc( 500, 1, 1, 1, 1, 0 );
-    p->vVarsInt   = Msat_SolverReadConeVars( p->pSat );   
-    p->vAdjacents = Msat_SolverReadAdjacents( p->pSat );
-    p->vVarsUsed  = Msat_SolverReadVarsUsed( p->pSat );
-    timeSelect = 0;
-    timeAssign = 0;
-}
-
  
 /**Function*************************************************************
 
@@ -352,8 +214,8 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
         (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. FailReal = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCounter, p->nSatFails, p->nSatFailsReal, p->nSatZeros );
+    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 );
@@ -371,168 +233,6 @@ void Fraig_ManPrintStats( Fraig_Man_t * p )
 //    PRT( "Assignment", timeAssign );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Allocates simulation information for all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fraig_NodeVec_t * Fraig_UtilInfoAlloc( int nSize, int nWords, bool fClean )
-{
-    Fraig_NodeVec_t * vInfo;
-    unsigned * pUnsigned;
-    int i;
-    assert( nSize > 0 && nWords > 0 );
-    vInfo = Fraig_NodeVecAlloc( nSize );
-    pUnsigned = ALLOC( unsigned, nSize * nWords );
-    vInfo->pArray[0] = (Fraig_Node_t *)pUnsigned;
-    if ( fClean )
-        memset( pUnsigned, 0, sizeof(unsigned) * nSize * nWords );
-    for ( i = 1; i < nSize; i++ )
-        vInfo->pArray[i] = (Fraig_Node_t *)(((unsigned *)vInfo->pArray[i-1]) + nWords);
-    vInfo->nSize = nSize;
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns simulation info of all nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p )
-{
-    Fraig_NodeVec_t * vInfo;
-    Fraig_Node_t * pNode;
-    unsigned * pUnsigned;
-    int nRandom, nDynamic;
-    int i, k, nWords;
-
-    nRandom  = Fraig_ManReadPatternNumRandom( p );
-    nDynamic = Fraig_ManReadPatternNumDynamic( p );
-    nWords = nRandom / 32 + nDynamic / 32;
-
-    vInfo = Fraig_UtilInfoAlloc( p->vNodes->nSize, nWords, 0 );
-    for ( i = 0; i < p->vNodes->nSize; i++ )
-    {
-        pNode = p->vNodes->pArray[i];
-        assert( i == pNode->Num );
-        pUnsigned = (unsigned *)vInfo->pArray[i];
-        for ( k = 0; k < nRandom / 32; k++ )
-            pUnsigned[k] = pNode->puSimR[k];
-        for ( k = 0; k < nDynamic / 32; k++ )
-            pUnsigned[nRandom / 32 + k] = pNode->puSimD[k];
-    }
-    return vInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if A v B is always true based on the siminfo.]
-
-  Description [A v B is always true iff A' * B' is always false.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 )
-{
-    int fCompl1, fCompl2, i;
-
-    fCompl1 = 1 ^ Fraig_IsComplement(pNode1) ^ Fraig_Regular(pNode1)->fInv;
-    fCompl2 = 1 ^ Fraig_IsComplement(pNode2) ^ Fraig_Regular(pNode2)->fInv;
-
-    pNode1 = Fraig_Regular(pNode1);
-    pNode2 = Fraig_Regular(pNode2);
-    assert( pNode1 != pNode2 );
-    
-    // check the simulation info
-    if ( fCompl1 && fCompl2 )
-    {
-        for ( i = 0; i < p->nWordsRand; i++ )
-            if ( ~pNode1->puSimR[i] & ~pNode2->puSimR[i] )
-                return 0;
-        for ( i = 0; i < p->iWordStart; i++ )
-            if ( ~pNode1->puSimD[i] & ~pNode2->puSimD[i] )
-                return 0;
-        return 1;
-    }
-    if ( !fCompl1 && fCompl2 )
-    {
-        for ( i = 0; i < p->nWordsRand; i++ )
-            if ( pNode1->puSimR[i] & ~pNode2->puSimR[i] )
-                return 0;
-        for ( i = 0; i < p->iWordStart; i++ )
-            if ( pNode1->puSimD[i] & ~pNode2->puSimD[i] )
-                return 0;
-        return 1;
-    }
-    if ( fCompl1 && !fCompl2 )
-    {
-        for ( i = 0; i < p->nWordsRand; i++ )
-            if ( ~pNode1->puSimR[i] & pNode2->puSimR[i] )
-                return 0;
-        for ( i = 0; i < p->iWordStart; i++ )
-            if ( ~pNode1->puSimD[i] & pNode2->puSimD[i] )
-                return 0;
-        return 1;
-    }
-//    if ( fCompl1 && fCompl2 )
-    {
-        for ( i = 0; i < p->nWordsRand; i++ )
-            if ( pNode1->puSimR[i] & pNode2->puSimR[i] )
-                return 0;
-        for ( i = 0; i < p->iWordStart; i++ )
-            if ( pNode1->puSimD[i] & pNode2->puSimD[i] )
-                return 0;
-        return 1;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds clauses to the solver.]
-
-  Description [This procedure is used to add external clauses to the solver.
-  The clauses are given by sets of nodes. Each node stands for one literal.
-  If the node is complemented, the literal is negated.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes )
-{
-    Fraig_Node_t * pNode;
-    int i, fComp, RetValue;
-    if ( p->pSat == NULL )
-        Fraig_ManCreateSolver( p );
-    // create four clauses
-    Msat_IntVecClear( p->vProj );
-    for ( i = 0; i < nNodes; i++ )
-    {
-        pNode = Fraig_Regular(ppNodes[i]);
-        fComp = Fraig_IsComplement(ppNodes[i]);
-        Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNode->Num, fComp) );
-//        printf( "%d(%d) ", pNode->Num, fComp );
-    }
-//    printf( "\n" );
-    RetValue = Msat_SolverAddClause( p->pSat, p->vProj );
-    assert( RetValue );
-}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///