Version abc60916

abc.dsp

@@ -1006,7 +1006,7 @@ SOURCE=.\src\sat\msat\msatMem.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\sat\msat\msatOrderJ.c
+SOURCE=.\src\sat\msat\msatOrderH.c
 # End Source File
 # Begin Source File
 
@@ -1762,6 +1762,10 @@ SOURCE=.\src\misc\vec\vec.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\vec\vecFlt.h
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\vec\vecInt.h
 # End Source File
 # Begin Source File
@@ -2054,6 +2058,10 @@ SOURCE=.\src\temp\ivy\ivyFastMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\temp\ivy\ivyFraig.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\temp\ivy\ivyHaig.c
 # End Source File
 # Begin Source File
@@ -2104,6 +2112,22 @@ SOURCE=.\src\temp\ivy\ivyTable.c
 
 SOURCE=.\src\temp\ivy\ivyUtil.c
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\satSolver.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\satSolver.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\satUtil.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\temp\ivy\satVec.h
+# End Source File
 # End Group
 # Begin Group "player"
 

abc.rc

@@ -2,8 +2,8 @@
 #set check         # checks intermediate networks
 #set checkfio      # prints warnings when fanins/fanouts are duplicated
 #set checkread     # checks new networks after reading from file
-set backup        # saves backup networks retrived by "undo" and "recall"
-set savesteps 1   # sets the maximum number of backup networks to save 
+#set backup        # saves backup networks retrived by "undo" and "recall"
+#set savesteps 1   # sets the maximum number of backup networks to save 
 set progressbar   # display the progress bar
 
 # program names for internal calls
@@ -99,6 +99,8 @@ alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l;
 alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 
 # temporaries
-alias test        "rvl th/lib.v; rvv th/t2.v"
+#alias test        "rvl th/lib.v; rvv th/t2.v"
+alias test         "so c/pure_sat/test.c"
+
 
 

src/base/abc/abc.h

@@ -516,7 +516,7 @@ extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckRead( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
-extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
+extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
 /*=== abcCut.c ==========================================================*/
@@ -589,7 +589,6 @@ extern Abc_Ntk_t *        Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fE
 extern Abc_Ntk_t *        Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter );
 extern void               Abc_NtkMiterReport( Abc_Ntk_t * pMiter );
-extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial );
 /*=== abcObj.c ==========================================================*/
 extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
@@ -743,7 +742,7 @@ extern char *             Abc_SopFromTruthHex( char * pTruth );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
 extern Abc_Obj_t *        Abc_NodeStrash( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode );
-extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
+extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos );
 extern Abc_Ntk_t *        Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels );
 /*=== abcSweep.c ==========================================================*/
 extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );

src/base/abc/abcCheck.c

@@ -709,16 +709,19 @@ bool Abc_NtkCompareBoxes( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
+bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fOnlyPis, int fComb )
 {
     Abc_NtkOrderObjsByName( pNtk1, fComb );
     Abc_NtkOrderObjsByName( pNtk2, fComb );
-    if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) )
-        return 0;
     if ( !Abc_NtkComparePis( pNtk1, pNtk2, fComb ) )
         return 0;
+    if ( !fOnlyPis )
+    {
+        if ( !Abc_NtkCompareBoxes( pNtk1, pNtk2, fComb ) )
+            return 0;
         if ( !Abc_NtkComparePos( pNtk1, pNtk2, fComb ) )
             return 0;
+    }
     return 1;
 }
 

src/base/abci/abc.c

@@ -71,6 +71,7 @@ static int Abc_CommandLogic          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandMiter          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDemiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOrPos          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAppend         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFrames         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSop            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBdd            ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -96,6 +97,7 @@ static int Abc_CommandICut           ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIRewrite       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIRewriteSeq    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -196,6 +198,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "demiter",       Abc_CommandDemiter,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "orpos",         Abc_CommandOrPos,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "append",        Abc_CommandAppend,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
     Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
@@ -221,6 +224,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "irw",           Abc_CommandIRewrite,         1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "irws",          Abc_CommandIRewriteSeq,      1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iresyn",        Abc_CommandIResyn,           1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
 
@@ -3276,6 +3280,105 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAppend( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk, * pNtk2;
+    char * FileName;
+    int fComb;
+    int c;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'c':
+            fComb ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+
+    // get the second network
+    if ( argc != globalUtilOptind + 1 )
+    {
+        fprintf( pErr, "The network to append is not given.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "The base network should be strashed for the appending to work.\n" );
+        return 1;
+    }
+
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+ 
+    // read the second network
+    pNtk2 = Io_Read( FileName, 1 );
+    if ( pNtk2 == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+        return 1;
+    }
+
+    // check if the second network is combinational
+    if ( Abc_NtkLatchNum(pNtk2) )
+    {
+        fprintf( pErr, "The second network has latches. Appending does not work for such networks.\n" );
+        return 1;
+    }
+
+    // get the new network
+    if ( !Abc_NtkAppend( pNtk, pNtk2, 1 ) )
+    {
+        Abc_NtkDelete( pNtk2 );
+        fprintf( pErr, "Appending the networks failed.\n" );
+        return 1;
+    }
+    Abc_NtkDelete( pNtk2 );
+
+    // replace the current network
+//    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: append [-h] <file>\n" );
+    fprintf( pErr, "\t         appends a combinational network on top of the current network\n" );
+//    fprintf( pErr, "\t-c     : computes combinational miter (latches as POs) [default = %s]\n", fComb? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : file name with the second network\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4810,13 +4913,13 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Only works for strashed networks.\n" );
         return 1;
     }
-
+/*
     if ( nLutMax < 2 || nLutMax > 12 || nPlaMax < 8 || nPlaMax > 128  )
     {
         fprintf( pErr, "Incorrect LUT/PLA parameters.\n" );
         return 1;
     }
-
+*/
     // run the command
 //    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fInvs, fVerbose );
     pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, RankCost, fFastMode, fRewriting, fSynthesis, fVerbose );
@@ -5338,6 +5441,79 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, fUpdateLevel, fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUpdateLevel = 1;
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "lzvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'l':
+            fUpdateLevel ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Only works for non-sequential networks.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkIvyFraig( pNtk );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: ifraig [-h]\n" );
+    fprintf( pErr, "\t         performs fraiging using a new method\n" );
+//    fprintf( pErr, "\t-l     : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" );
+//    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandHaig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;

src/base/abci/abcFpga.c

@@ -209,6 +209,7 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     Abc_NtkForEachCi( pNtk, pNode, i )
         Fpga_NodeSetData0( Fpga_ManReadInputs(pMan)[i], (char *)pNode->pCopy );
     // set the constant node
+//    if ( Fpga_NodeReadRefs(Fpga_ManReadConst1(pMan)) > 0 )
         Fpga_NodeSetData0( Fpga_ManReadConst1(pMan), (char *)Abc_NodeCreateConst1(pNtkNew) );
     // process the nodes in topological order
     pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
@@ -222,6 +223,10 @@ Abc_Ntk_t * Abc_NtkFromFpga( Fpga_Man_t * pMan, Abc_Ntk_t * pNtk )
     Extra_ProgressBarStop( pProgress );
     // finalize the new network
     Abc_NtkFinalize( pNtk, pNtkNew );
+    // remove the constant node if not used
+    pNodeNew = (Abc_Obj_t *)Fpga_NodeReadData0(Fpga_ManReadConst1(pMan));
+    if ( Abc_ObjFanoutNum(pNodeNew) == 0 )
+        Abc_NtkDeleteObj( pNodeNew );
     // decouple the PO driver nodes to reduce the number of levels
     nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
 //    if ( nDupGates && Fpga_ManReadVerbose(pMan) )

src/base/abci/abcFraig.c

@@ -679,7 +679,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     {
         // add the new network to storage
         nAndsOld = Abc_NtkNodeNum( pStore );
-        if ( !Abc_NtkAppend( pStore, pNtk ) )
+        if ( !Abc_NtkAppend( pStore, pNtk, 0 ) )
         {
             printf( "The current network cannot be appended to the stored network.\n" );
             return 0;

src/base/abci/abcIvy.c

@@ -288,6 +288,31 @@ Abc_Ntk_t * Abc_NtkIvyRewriteSeq( Abc_Ntk_t * pNtk, int fUseZeroCost, int fVerbo
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyResyn0( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Ivy_ManResyn0( pTemp = pMan, fUpdateLevel, fVerbose );
+    Ivy_ManStop( pTemp );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
@@ -313,6 +338,33 @@ Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk )
+{
+    Ivy_FraigParams_t Params, * pParams = &Params; 
+    Abc_Ntk_t * pNtkAig;
+    Ivy_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkIvyBefore( pNtk, 0, 0 );
+    if ( pMan == NULL )
+        return NULL;
+    Ivy_FraigParamsDefault( pParams );
+    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
+    Ivy_ManStop( pTemp );
+    pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 );
+    Ivy_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
 {
 //    Abc_Ntk_t * pNtkAig;
@@ -538,12 +590,12 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig
         if ( fHaig && pNode->pEquiv && Ivy_ObjRefs(pNode) > 0 )
         {
             pFaninNew = Abc_EdgeToNode( pNtk, pNode->TravId );
-            pFaninNew->fPhase = 0;
+//            pFaninNew->fPhase = 0;
             assert( !Ivy_IsComplement(pNode->pEquiv) );
             for ( pTemp = pNode->pEquiv; pTemp != pNode; pTemp = Ivy_Regular(pTemp->pEquiv) )
             {
                 pFaninNew1 = Abc_EdgeToNode( pNtk, pTemp->TravId );
-                pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
+//                pFaninNew1->fPhase = Ivy_IsComplement( pTemp->pEquiv );
                 pFaninNew->pData = pFaninNew1;
                 pFaninNew = pFaninNew1;
             }

src/base/abci/abcMiter.c

@@ -57,7 +57,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) );
     assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) );
     // check that the networks have the same PIs/POs/latches
-    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) )
+    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 0, fComb ) )
         return NULL;
     // make sure the circuits are strashed 
     fRemove1 = (!Abc_NtkIsStrash(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0, 0));

src/base/abci/abcProve.c

@@ -122,8 +122,24 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
         {
             clk = clock();
             Counter = (int)(pParams->nRewritingLimitStart * pow(pParams->nRewritingLimitMulti,nIter));
+//            Counter = 1;
             while ( 1 )
             {
+/*
+                extern Abc_Ntk_t * Abc_NtkIvyResyn( Abc_Ntk_t * pNtk, int fUpdateLevel, int fVerbose );
+                pNtk = Abc_NtkIvyResyn( pNtkTemp = pNtk, 0, 0 );  Abc_NtkDelete( pNtkTemp );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+*/
+/*
+                Abc_NtkRewrite( pNtk, 0, 0, 0 );
+                if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
+                    break;
+                if ( --Counter == 0 )
+                    break;
+*/
                 Abc_NtkRewrite( pNtk, 0, 0, 0 );
                 if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 )
                     break;

src/base/abci/abcSat.c

@@ -429,7 +429,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 {
     Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE;
     Vec_Ptr_t * vNodes, * vSuper;
-//    Vec_Int_t * vLevels;
+    Vec_Flt_t * vFactors;
     Vec_Int_t * vVars, * vFanio;
     Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
@@ -588,6 +588,23 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
 //        Asat_JManStop( pSat );
 //    PRT( "Total", clock() - clk1 );
     }
+
+    Abc_NtkStartReverseLevels( pNtk );
+    vFactors = Vec_FltStart( solver_nvars(pSat) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->fMarkA )
+            Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, Abc_NodeReadReverseLevel(pNode)) );
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( pNode->fMarkA )
+            Vec_FltWriteEntry( vFactors, (int)pNode->pCopy, (float)pow(0.97, nLevelsMax+1) );
+    // set the PI levels
+//    Abc_NtkForEachObj( pNtk, pNode, i )
+//        if ( pNode->fMarkA )
+//            printf( "(%d) %.3f   ", Abc_NodeReadReverseLevel(pNode), Vec_FltEntry(vFactors, (int)pNode->pCopy) );
+//    printf( "\n" );
+    Asat_SolverSetFactors( pSat, Vec_FltReleaseArray(vFactors) );
+    Vec_FltFree( vFactors );
+
 /*
     // create factors
     vLevels = Vec_IntStart( Vec_PtrSize(vNodes) );   // the reverse levels of the nodes

src/base/abci/abcStrash.c

@@ -144,7 +144,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
+int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fAddPos )
 {
     Abc_Obj_t * pObj;
     int i;
@@ -158,7 +158,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     }
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
-    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
+    if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1, 1 ) )
         return 0;
     // perform strashing
     Abc_NtkCleanCopy( pNtk2 );
@@ -170,6 +170,16 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     else
         Abc_NtkForEachNode( pNtk2, pObj, i )
             pObj->pCopy = Abc_AigAnd( pNtk1->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // add the COs of the second network
+    if ( fAddPos )
+    {
+        Abc_NtkForEachPo( pNtk2, pObj, i )
+        {
+            Abc_NtkDupObj( pNtk1, pObj, 0 );
+            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjChild0Copy(pObj) );
+            Abc_ObjAssignName( pObj->pCopy, Abc_ObjName(pObj->pCopy), NULL );
+        }
+    }
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtk1 ) )
     {

src/map/fpga/fpga.h

@@ -105,6 +105,7 @@ extern int             Fpga_LibReadLutMax( Fpga_LutLib_t * pLib );
 
 extern char *          Fpga_NodeReadData0( Fpga_Node_t * p );
 extern Fpga_Node_t *   Fpga_NodeReadData1( Fpga_Node_t * p );
+extern int             Fpga_NodeReadRefs( Fpga_Node_t * p );
 extern int             Fpga_NodeReadNum( Fpga_Node_t * p );
 extern int             Fpga_NodeReadLevel( Fpga_Node_t * p );
 extern Fpga_Cut_t *    Fpga_NodeReadCuts( Fpga_Node_t * p );

src/map/fpga/fpgaCreate.c

@@ -97,6 +97,7 @@ int             Fpga_LibReadLutMax( Fpga_LutLib_t * pLib )  { return pLib->LutMa
 ***********************************************************************/
 char *          Fpga_NodeReadData0( Fpga_Node_t * p )                   { return p->pData0;    }
 Fpga_Node_t *   Fpga_NodeReadData1( Fpga_Node_t * p )                   { return p->pLevel;    }
+int             Fpga_NodeReadRefs( Fpga_Node_t * p )                    { return p->nRefs;     }
 int             Fpga_NodeReadNum( Fpga_Node_t * p )                     { return p->Num;       }
 int             Fpga_NodeReadLevel( Fpga_Node_t * p )                   { return Fpga_Regular(p)->Level;  }
 Fpga_Cut_t *    Fpga_NodeReadCuts( Fpga_Node_t * p )                    { return p->pCuts;     }

src/sat/asat/added.c

@@ -220,7 +220,7 @@ void Asat_SolverSetPrefVars(solver * s, int * pPrefVars, int nPrefVars)
   SeeAlso     []
 
 ***********************************************************************/
-void Asat_SolverSetFactors(solver * s, int * pFactors)
+void Asat_SolverSetFactors(solver * s, float * pFactors)
 {
     assert( s->factors == NULL );
     s->factors = pFactors;

src/sat/asat/solver.c

@@ -253,12 +253,11 @@ static inline void act_var_rescale(solver* s) {
 
 static inline void act_var_bump(solver* s, int v) {
     double* activity = s->activity;
-    if ((activity[v] += s->var_inc) > 1e100)
-//    if ((activity[v] += s->var_inc*s->factors[v]/100000000) > 1e100)
+    activity[v] += s->var_inc;
+//    activity[v] += s->var_inc * s->factors[v];
+    if (activity[v] > 1e100)
         act_var_rescale(s);
-
     //printf("bump %d %f\n", v-1, activity[v]);
-
     if ( s->pJMan == NULL && s->orderpos[v] != -1 )
         order_update(s,v);
 
@@ -842,6 +841,7 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
 
     int     conflictC       = 0;
     veci    learnt_clause;
+    int     i;
 
     assert(s->root_level == solver_dlevel(s));
 
@@ -851,6 +851,12 @@ static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
     veci_resize(&s->model,0);
     veci_new(&learnt_clause);
 
+    // reset the activities
+    if ( s->factors )
+        for ( i = 0; i < s->size; i++ )
+            s->activity[i] = (double)s->factors[i];
+//            s->activity[i] = 1.0;
+
     for (;;){
         clause* confl = solver_propagate(s);
         if (confl != 0){

src/sat/asat/solver.h

@@ -89,7 +89,7 @@ extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
                                        int incrementVars);
 extern void    Asat_SatPrintStats( FILE * pFile, solver * p );
 extern void    Asat_SolverSetPrefVars( solver * s, int * pPrefVars, int nPrefVars );
-extern void    Asat_SolverSetFactors( solver * s, int * pFactors );
+extern void    Asat_SolverSetFactors( solver * s, float * pFactors );
 
 // J-frontier support
 extern Asat_JMan_t * Asat_JManStart( solver * pSat, void * vCircuit );
@@ -128,7 +128,7 @@ struct solver_t
 
     vec*     wlists;        // 
     double*  activity;      // A heuristic measurement of the activity of a variable.
-    int *    factors;       // the factor of variable activity
+    float *  factors;       // the factor of variable activity
     lbool*   assigns;       // Current values of variables.
     int*     orderpos;      // Index in variable order.
     clause** reasons;       //

src/sat/asat_fixed/satSolver.c

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <math.h>
+
+#include "solver.h"
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    solver_dlevel(s)*3+3,solver_dlevel(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+void sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int   clause_size       (clause* c)          { return c->size_learnt >> 1; }
+static inline lit*  clause_begin      (clause* c)          { return c->lits; }
+static inline int   clause_learnt     (clause* c)          { return c->size_learnt & 1; }
+static inline float clause_activity   (clause* c)          { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
+bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     solver_dlevel(solver* s)    { return veci_size(&s->trail_lim); }
+static inline vecp*   solver_read_wlist     (solver* s, lit l){ return &s->wlists[l]; }
+static inline void    vecp_remove(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+    vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(solver* s, int v) // updateorder
+{
+    int*    orderpos = s->orderpos;
+    double* activity = s->activity;
+    int*    heap     = veci_begin(&s->order);
+    int     i        = orderpos[v];
+    int     x        = heap[i];
+    int     parent   = (i - 1) / 2;
+
+    assert(s->orderpos[v] != -1);
+
+    while (i != 0 && activity[x] > activity[heap[parent]]){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+    heap[i]     = x;
+    orderpos[x] = i;
+}
+
+static inline void order_assigned(solver* s, int v) 
+{
+}
+
+static inline void order_unassigned(solver* s, int v) // undoorder
+{
+    int* orderpos = s->orderpos;
+    if (orderpos[v] == -1){
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
+        order_update(s,v);
+    }
+}
+
+static int  order_select(solver* s, float random_var_freq) // selectvar
+{
+    int*    heap;
+    double* activity;
+    int*    orderpos;
+
+    lbool* values = s->assigns;
+
+    // Random decision:
+    if (drand(&s->random_seed) < random_var_freq){
+        int next = irand(&s->random_seed,s->size);
+        assert(next >= 0 && next < s->size);
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    // Activity based decision:
+
+    heap     = veci_begin(&s->order);
+    activity = s->activity;
+    orderpos = s->orderpos;
+
+
+    while (veci_size(&s->order) > 0){
+        int    next  = heap[0];
+        int    size  = veci_size(&s->order)-1;
+        int    x     = heap[size];
+
+        veci_resize(&s->order,size);
+
+        orderpos[next] = -1;
+
+        if (size > 0){
+            double act   = activity[x];
+
+            int    i     = 0;
+            int    child = 1;
+
+
+            while (child < size){
+                if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
+                    child++;
+
+                assert(child < size);
+
+                if (act >= activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(solver* s) {
+    double* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
+}
+
+static inline void act_var_bump(solver* s, int v) {
+    double* activity = s->activity;
+    if ((activity[v] += s->var_inc) > 1e100)
+        act_var_rescale(s);
+
+    //printf("bump %d %f\n", v-1, activity[v]);
+
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+
+}
+
+static inline void act_var_decay(solver* s) { s->var_inc *= s->var_decay; }
+
+static inline void act_clause_rescale(solver* s) {
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i;
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        float a = clause_activity(cs[i]);
+        clause_setactivity(cs[i], a * (float)1e-20);
+    }
+    s->cla_inc *= (float)1e-20;
+}
+
+
+static inline void act_clause_bump(solver* s, clause *c) {
+    float a = clause_activity(c) + s->cla_inc;
+    clause_setactivity(c,a);
+    if (a > 1e20) act_clause_rescale(s);
+}
+
+static inline void act_clause_decay(solver* s) { s->cla_inc *= s->cla_decay; }
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(solver* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+    c->size_learnt = (size << 1) | learnt;
+    assert(((unsigned int)c & 1) == 0);
+
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    if (learnt)
+        *((float*)&c->lits[size]) = 0.0;
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    //vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    //vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+    vecp_push(solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+    vecp_push(solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+    return c;
+}
+
+
+static void clause_remove(solver* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    //vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    assert(lits[0] < s->size*2);
+    vecp_remove(solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+    vecp_remove(solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+    free(c);
+}
+
+
+static lbool clause_simplify(solver* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(solver_dlevel(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void solver_setnvars(solver* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
+        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
+        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
+        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
+        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
+        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
+        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
+        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        vecp_new(&s->wlists[2*var]);
+        vecp_new(&s->wlists[2*var+1]);
+        s->activity [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        
+        /* does not hold because variables enqueued at top level will not be reinserted in the heap
+           assert(veci_size(&s->order) == var); 
+         */
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+
+    s->size = n > s->size ? n : s->size;
+}
+
+
+static inline bool enqueue(solver* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    lbool sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+
+        values [v] = sig;
+        levels [v] = solver_dlevel(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline void assume(solver* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    enqueue(s,l,(clause*)0);
+}
+
+
+static inline void solver_canceluntil(solver* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      c;
+    
+    if (solver_dlevel(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void solver_record(solver* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    enqueue(s,*begin,c);
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double solver_progress(solver* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static bool solver_lit_removable(solver* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(reasons[v] != 0);
+        c    = reasons[v];
+
+        if (clause_is_lit(c)){
+            int v = lit_var(clause_read_lit(c));
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+                    veci_push(&s->stack,v);
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    int j;
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }else{
+            lit*    lits = clause_begin(c);
+            int     i, j;
+
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (tags[v] == l_Undef && levels[v] != 0){
+                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        tags[v] = l_True;
+                        veci_push(&s->tagged,v);
+                    }else{
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
+                            tags[tagged[j]] = l_Undef;
+                        veci_resize(&s->tagged,top);
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+static void solver_analyze(solver* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+
+        if (clause_is_lit(c)){
+            lit q = clause_read_lit(c);
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == solver_dlevel(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }else{
+
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
+
+            lits = clause_begin(c);
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+                lit q = lits[j];
+                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                    tags[lit_var(q)] = l_True;
+                    veci_push(&s->tagged,lit_var(q));
+                    act_var_bump(s,lit_var(q));
+                    if (levels[lit_var(q)] == solver_dlevel(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,q);
+                }
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !solver_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    s->stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* solver_propagate(solver* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+
+    //printf("solver_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = solver_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+            if (clause_is_lit(*i)){
+                *j++ = *i;
+                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }else{
+                lit false_lit;
+                lbool sig;
+
+                lits = clause_begin(*i);
+
+                // Make sure the false literal is data[1]:
+                false_lit = lit_neg(p);
+                if (lits[0] == false_lit){
+                    lits[0] = lits[1];
+                    lits[1] = false_lit;
+                }
+                assert(lits[1] == false_lit);
+                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+                // If 0th watch is true, then clause is already satisfied.
+                sig = !lit_sign(lits[0]); sig += sig - 1;
+                if (values[lit_var(lits[0])] == sig){
+                    *j++ = *i;
+                }else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(*i);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        lbool sig = lit_sign(*k); sig += sig - 1;
+                        if (values[lit_var(*k)] != sig){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            vecp_push(solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if (!enqueue(s,lits[0], *i)){
+                        confl = *i++;
+                        // Copy the remaining watches:
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+static inline int clause_cmp (const void* x, const void* y) {
+    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void solver_reducedb(solver* s)
+{
+    int      i, j;
+    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+static lbool solver_search(solver* s, int nof_conflicts, int nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = 0.02;
+
+    int     conflictC       = 0;
+    veci    learnt_clause;
+
+    assert(s->root_level == solver_dlevel(s));
+
+    s->stats.starts++;
+    s->var_decay = (float)(1 / var_decay   );
+    s->cla_decay = (float)(1 / clause_decay);
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    for (;;){
+        clause* confl = solver_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (solver_dlevel(s) == s->root_level){
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            solver_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            solver_canceluntil(s,blevel);
+            solver_record(s,&learnt_clause);
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                s->progress_estimate = solver_progress(s);
+                solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            if (solver_dlevel(s) == 0)
+                // Simplify the set of problem clauses:
+                solver_simplify(s);
+
+            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                solver_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
+                solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+solver* solver_new(void)
+{
+    solver* s = (solver*)malloc(sizeof(solver));
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+    s->cla_inc                = 1;
+    s->cla_decay              = 1;
+    s->var_inc                = 1;
+    s->var_decay              = 1;
+    s->root_level             = 0;
+    s->simpdb_assigns         = 0;
+    s->simpdb_props           = 0;
+    s->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->binary                 = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.max_literals     = 0;
+    s->stats.tot_literals     = 0;
+
+    return s;
+}
+
+
+void solver_delete(solver* s)
+{
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        free(vecp_begin(&s->clauses)[i]);
+
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        free(vecp_begin(&s->learnts)[i]);
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+    free(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->size*2; i++)
+            vecp_delete(&s->wlists[i]);
+
+        // if one is different from null, all are
+        free(s->wlists);
+        free(s->activity );
+        free(s->assigns  );
+        free(s->orderpos );
+        free(s->reasons  );
+        free(s->levels   );
+        free(s->trail    );
+        free(s->tags     );
+    }
+
+    free(s);
+}
+
+
+bool solver_addclause(solver* s, lit* begin, lit* end)
+{
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    if (begin == end) return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    solver_setnvars(s,maxvar+1);
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+
+    //printf("final: "); printlits(begin,j); printf("\n");
+
+    if (j == begin)          // empty clause
+        return false;
+    else if (j - begin == 1) // unit clause
+        return enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    vecp_push(&s->clauses,clause_new(s,begin,j,0));
+
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+bool   solver_simplify(solver* s)
+{
+    clause** reasons;
+    int type;
+
+    assert(solver_dlevel(s) == 0);
+
+    if (solver_propagate(s) != 0)
+        return false;
+
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+
+    reasons = s->reasons;
+    for (type = 0; type < 2; type++){
+        vecp*    cs  = type ? &s->learnts : &s->clauses;
+        clause** cls = (clause**)vecp_begin(cs);
+
+        int i, j;
+        for (j = i = 0; i < vecp_size(cs); i++){
+            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+                clause_simplify(s,cls[i]) == l_True)
+                clause_remove(s,cls[i]);
+            else
+                cls[j++] = cls[i];
+        }
+        vecp_resize(cs,j);
+    }
+
+    s->simpdb_assigns = s->qhead;
+    // (shouldn't depend on 'stats' really, but it will do for now)
+    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+    return true;
+}
+
+
+bool   solver_solve(solver* s, lit* begin, lit* end)
+{
+    double  nof_conflicts = 100;
+    double  nof_learnts   = solver_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+    
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: /* l_True: */
+            break;
+        case 0: /* l_Undef */
+            assume(s, *i);
+            if (solver_propagate(s) == NULL)
+                break;
+            // falltrough
+        case -1: /* l_False */
+            solver_canceluntil(s, 0);
+            return false;
+        }
+    }
+
+    s->root_level = solver_dlevel(s);
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+
+        if (s->verbosity >= 1){
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        status = solver_search(s,(int)nof_conflicts, (int)nof_learnts);
+        nof_conflicts *= 1.5;
+        nof_learnts   *= 1.1;
+    }
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    solver_canceluntil(s,0);
+    return status != l_False;
+}
+
+
+int solver_nvars(solver* s)
+{
+    return s->size;
+}
+
+
+int solver_nclauses(solver* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int solver_nconflicts(solver* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+}

src/sat/asat_fixed/satSolver.h

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef solver_h
+#define solver_h
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "vec.h"
+
+//=================================================================================================
+// Simple types:
+
+// does not work for c++
+typedef int  bool;
+static const bool  true      = 1;
+static const bool  false     = 0;
+
+typedef int                lit;
+typedef char               lbool;
+
+#ifdef _WIN32
+typedef signed __int64     uint64;   // compatible with MS VS 6.0
+#else
+typedef unsigned long long uint64;
+#endif
+
+static const int   var_Undef = -1;
+static const lit   lit_Undef = -2;
+
+static const lbool l_Undef   =  0;
+static const lbool l_True    =  1;
+static const lbool l_False   = -1;
+
+static inline lit  toLit   (int v) { return v + v; }
+static inline lit  lit_neg (lit l) { return l ^ 1; }
+static inline int  lit_var (lit l) { return l >> 1; }
+static inline int  lit_sign(lit l) { return (l & 1); }
+
+
+//=================================================================================================
+// Public interface:
+
+struct solver_t;
+typedef struct solver_t solver;
+
+extern solver* solver_new(void);
+extern void    solver_delete(solver* s);
+
+extern bool    solver_addclause(solver* s, lit* begin, lit* end);
+extern bool    solver_simplify(solver* s);
+extern bool    solver_solve(solver* s, lit* begin, lit* end);
+
+extern int     solver_nvars(solver* s);
+extern int     solver_nclauses(solver* s);
+extern int     solver_nconflicts(solver* s);
+
+extern void    solver_setnvars(solver* s,int n);
+
+struct stats_t
+{
+    uint64   starts, decisions, propagations, inspects, conflicts;
+    uint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats;
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct solver_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+    double   var_inc;       // Amount to bump next variable with.
+    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    float    cla_inc;       // Amount to bump next clause with.
+    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vecp*    wlists;        // 
+    double*  activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats    stats;
+};
+
+#endif

src/sat/fraig/fraigFeed.c

@@ -463,6 +463,10 @@ Fraig_NodeVec_t * Fraig_FeedBackCoveringStart( Fraig_Man_t * p )
             Fraig_NodeVecPush( p->vCones, pEntD );
         if ( p->vCones->nSize == 1 )
             continue;
+        //////////////////////////////// bug fix by alanmi, September 14, 2006
+        if ( p->vCones->nSize > 20 ) 
+            continue;
+        ////////////////////////////////
 
         for ( k = 0; k < p->vCones->nSize; k++ )
             for ( m = k+1; m < p->vCones->nSize; m++ )

src/sat/fraig/fraigSat.c

@@ -34,6 +34,7 @@ static void Fraig_SupergateAddClausesExor( Fraig_Man_t * pMan, Fraig_Node_t * pN
 static void Fraig_SupergateAddClausesMux( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 //static void Fraig_DetectFanoutFreeCone( Fraig_Man_t * pMan, Fraig_Node_t * pNode );
 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 );
 
@@ -355,6 +356,9 @@ if ( fVerbose )
     printf( "%d(%d) - ", Fraig_CountPis(p,p->vVarsInt), Msat_IntVecReadSize(p->vVarsInt) );
 
 
+    // prepare variable activity
+    Fraig_SetActivity( p, pOld, pNew );
+
     // get the complemented attribute
     fComp = Fraig_NodeComparePhase( pOld, pNew );
 //Msat_SolverPrintClauses( p->pSat );
@@ -1396,6 +1400,40 @@ printf( "%d(%d)", vFanins->nSize, nCubes );
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Collect variables using their proximity from the nodes.]
+
+  Description [This procedure creates a variable order based on collecting
+  first the nodes that are the closest to the given two target nodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_SetActivity( Fraig_Man_t * pMan, Fraig_Node_t * pOld, Fraig_Node_t * pNew )
+{
+    Fraig_Node_t * pNode;
+    int i, Number, MaxLevel;
+    float * pFactors = Msat_SolverReadFactors(pMan->pSat);
+    if ( pFactors == NULL )
+        return;
+    MaxLevel = FRAIG_MAX( pOld->Level, pNew->Level );
+    // create the variable order
+    for ( i = 0; i < Msat_IntVecReadSize(pMan->vVarsInt); i++ )
+    {
+        // get the new node on the frontier
+        Number = Msat_IntVecReadEntry(pMan->vVarsInt, i);
+        pNode = pMan->vNodes->pArray[Number];
+        pFactors[pNode->Num] = (float)pow( 0.97, MaxLevel - pNode->Level );
+//        if ( pNode->Num % 50 == 0 )
+//        printf( "(%d) %.2f  ", MaxLevel - pNode->Level, pFactors[pNode->Num] );
+    }
+//    printf( "\n" );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/msat/msat.h

@@ -104,6 +104,7 @@ extern void             Msat_SolverSetVarTypeA( Msat_Solver_t * p, int Var );
 extern void             Msat_SolverSetVarMap( Msat_Solver_t * p, Msat_IntVec_t * vVarMap );
 extern void             Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p );
 extern void             Msat_SolverMarkClausesStart( Msat_Solver_t * p );
+extern float *          Msat_SolverReadFactors( Msat_Solver_t * p );
 // returns the solution after incremental solving
 extern int              Msat_SolverReadSolutions( Msat_Solver_t * p );
 extern int *            Msat_SolverReadSolutionsArray( Msat_Solver_t * p );

src/sat/msat/msatActivity.c

@@ -45,8 +45,9 @@ void Msat_SolverVarBumpActivity( Msat_Solver_t * p, Msat_Lit_t Lit )
     if ( p->dVarDecay < 0 ) // (negative decay means static variable order -- don't bump)
         return;
     Var = MSAT_LIT2VAR(Lit);
-    if ( (p->pdActivity[Var] += p->dVarInc) > 1e100 )
-//    if ( (p->pdActivity[Var] += p->dVarInc * (1.0 + 0.005*p->pActLevels[Var])) > 1e100 )
+    p->pdActivity[Var] += p->dVarInc;
+//    p->pdActivity[Var] += p->dVarInc * p->pFactors[Var];
+    if ( p->pdActivity[Var] > 1e100 )
         Msat_SolverVarRescaleActivity( p );
     Msat_OrderUpdate( p->pOrder, Var );
 }

src/sat/msat/msatInt.h

@@ -119,7 +119,7 @@ struct Msat_Solver_t_
     double              dClaDecay;   // INVERSE decay factor for clause activity: stores 1/decay.
 
     double *            pdActivity;  // A heuristic measurement of the activity of a variable.
-    int *               pActLevels;  // the levels of the variables
+    float *             pFactors;    // the multiplicative factors of variable activity
     double              dVarInc;     // Amount to bump next variable with.
     double              dVarDecay;   // INVERSE decay factor for variable activity: stores 1/decay. Use negative value for static variable order.
     Msat_Order_t *      pOrder;      // Keeps track of the decision variable order.

src/sat/msat/msatSolverApi.c

@@ -64,6 +64,7 @@ void               Msat_SolverClausesIncrementL( Msat_Solver_t * p )           {
 void               Msat_SolverClausesDecrementL( Msat_Solver_t * p )           { p->nClausesAllocL--;  }
 void               Msat_SolverMarkLastClauseTypeA( Msat_Solver_t * p )         { Msat_ClauseSetTypeA( Msat_ClauseVecReadEntry( p->vClauses, Msat_ClauseVecReadSize(p->vClauses)-1 ), 1 ); }
 void               Msat_SolverMarkClausesStart( Msat_Solver_t * p )            { p->nClausesStart = Msat_ClauseVecReadSize(p->vClauses); }
+float *            Msat_SolverReadFactors( Msat_Solver_t * p )                 { return p->pFactors;   }
 
 /**Function*************************************************************
 
@@ -174,11 +175,11 @@ Msat_Solver_t * Msat_SolverAlloc( int nVarsAlloc,
     p->dVarDecay = dVarDecay;
 
     p->pdActivity = ALLOC( double, p->nVarsAlloc );
-    p->pActLevels = ALLOC( int, p->nVarsAlloc );
+    p->pFactors   = ALLOC( float, p->nVarsAlloc );
     for ( i = 0; i < p->nVarsAlloc; i++ )
     {
-        p->pdActivity[i] = 0;
-        p->pActLevels[i] = 0;
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
     }
 
     p->pAssigns  = ALLOC( int, p->nVarsAlloc ); 
@@ -243,9 +244,12 @@ void Msat_SolverResize( Msat_Solver_t * p, int nVarsAlloc )
     p->nVarsAlloc = nVarsAlloc;
 
     p->pdActivity = REALLOC( double, p->pdActivity, p->nVarsAlloc );
-    p->pActLevels = REALLOC( int, p->pActLevels, p->nVarsAlloc );
+    p->pFactors   = REALLOC( float, p->pFactors, p->nVarsAlloc );
     for ( i = nVarsAllocOld; i < p->nVarsAlloc; i++ )
-        p->pdActivity[i] = 0;
+    {
+        p->pdActivity[i] = 0.0;
+        p->pFactors[i]   = 1.0;
+    }
 
     p->pAssigns  = REALLOC( int, p->pAssigns, p->nVarsAlloc );
     p->pModel    = REALLOC( int, p->pModel, p->nVarsAlloc );
@@ -399,7 +403,7 @@ void Msat_SolverFree( Msat_Solver_t * p )
     Msat_ClauseVecFree( p->vLearned );
 
     FREE( p->pdActivity );
-    FREE( p->pActLevels );
+    FREE( p->pFactors );
     Msat_OrderFree( p->pOrder );
 
     for ( i = 0; i < 2 * p->nVarsAlloc; i++ )

src/sat/msat/msatSolverSearch.c

@@ -534,12 +534,18 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
     Msat_Clause_t * pConf;
     Msat_Var_t Var;
     int nLevelBack, nConfs, nAssigns, Value;
+    int i;
 
     assert( Msat_SolverReadDecisionLevel(p) == p->nLevelRoot );
     p->Stats.nStarts++;
     p->dVarDecay = 1 / pPars->dVarDecay;
     p->dClaDecay = 1 / pPars->dClaDecay;
 
+    // reset the activities
+    for ( i = 0; i < p->nVars; i++ )
+       p->pdActivity[i] = (double)p->pFactors[i];
+//       p->pdActivity[i] = 0.0;
+
     nConfs = 0;
     while ( 1 )
     {

src/temp/ivy/ivy.h

@@ -43,6 +43,7 @@ extern "C" {
 typedef struct Ivy_Man_t_            Ivy_Man_t;
 typedef struct Ivy_Obj_t_            Ivy_Obj_t;
 typedef int                          Ivy_Edge_t;
+typedef struct Ivy_FraigParams_t_    Ivy_FraigParams_t;
 
 // object types
 typedef enum { 
@@ -71,12 +72,13 @@ struct Ivy_Obj_t_  // 24 bytes (32-bit) or 32 bytes (64-bit)   // 10 words - 16
     int              Id;             // integer ID
     int              TravId;         // traversal ID
     unsigned         Type     :  4;  // object type
-    unsigned         fPhase  :  1;   // value under 000...0 pattern
     unsigned         fMarkA   :  1;  // multipurpose mask
     unsigned         fMarkB   :  1;  // multipurpose mask
     unsigned         fExFan   :  1;  // set to 1 if last fanout added is EXOR
+    unsigned         fPhase   :  1;  // value under 000...0 pattern
+    unsigned         fFailTfo :  1;  // the TFO of the failed node
     unsigned         Init     :  2;  // latch initial value
-    unsigned         Level   : 22;   // logic level
+    unsigned         Level    : 21;  // logic level
     int              nRefs;          // reference counter
     Ivy_Obj_t *      pFanin0;        // fanin
     Ivy_Obj_t *      pFanin1;        // fanin
@@ -124,6 +126,12 @@ struct Ivy_Man_t_
     int              time2;
 };
 
+struct Ivy_FraigParams_t_
+{
+    int              nSimWords;      // the number of words in the simulation info
+    double           SimSatur;       // the ratio of refined classes when saturation is reached
+};
+
 
 #define IVY_CUT_LIMIT     256
 #define IVY_CUT_INPUT       6
@@ -249,6 +257,8 @@ static inline Ivy_Obj_t *  Ivy_ObjChild0Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy
 static inline Ivy_Obj_t *  Ivy_ObjChild1Equiv( Ivy_Obj_t * pObj ) { assert( !Ivy_IsComplement(pObj) ); return Ivy_ObjFanin1(pObj)? Ivy_NotCond(Ivy_ObjFanin1(pObj)->pEquiv, Ivy_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Ivy_ObjLevel( Ivy_Obj_t * pObj )       { return pObj->Level;                            }
 static inline int          Ivy_ObjLevelNew( Ivy_Obj_t * pObj )    { return 1 + Ivy_ObjIsExor(pObj) + IVY_MAX(Ivy_ObjFanin0(pObj)->Level, Ivy_ObjFanin1(pObj)->Level);       }
+static inline int          Ivy_ObjFaninPhase( Ivy_Obj_t * pObj )  { return Ivy_IsComplement(pObj)? !Ivy_Regular(pObj)->fPhase : pObj->fPhase; }
+
 static inline void         Ivy_ObjClean( Ivy_Obj_t * pObj )       
 { 
     int IdSaved = pObj->Id; 
@@ -430,6 +440,9 @@ extern void            Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit );
 extern void            Ivy_FastMapStop( Ivy_Man_t * pAig );
 extern void            Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeaves );
 extern void            Ivy_FastMapReverseLevel( Ivy_Man_t * pAig );
+/*=== ivyFraig.c ==========================================================*/
+extern Ivy_Man_t *     Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+extern void            Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams );
 /*=== ivyHaig.c ==========================================================*/
 extern void            Ivy_ManHaigStart( Ivy_Man_t * p, int fVerbose );
 extern void            Ivy_ManHaigTrasfer( Ivy_Man_t * p, Ivy_Man_t * pNew );
@@ -442,6 +455,7 @@ extern void            Ivy_ManHaigSimulate( Ivy_Man_t * p );
 extern int             Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover, int fTryBoth );
 /*=== ivyMan.c ==========================================================*/
 extern Ivy_Man_t *     Ivy_ManStart();
+extern Ivy_Man_t *     Ivy_ManStartFrom( Ivy_Man_t * p );
 extern Ivy_Man_t *     Ivy_ManDup( Ivy_Man_t * p );
 extern void            Ivy_ManStop( Ivy_Man_t * p );
 extern int             Ivy_ManCleanup( Ivy_Man_t * p );
@@ -487,7 +501,7 @@ extern int             Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int f
 /*=== ivySeq.c =========================================================*/
 extern int             Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose );
 /*=== ivyShow.c =========================================================*/
-extern void            Ivy_ManShow( Ivy_Man_t * pMan, int fHaig );
+extern void            Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold );
 /*=== ivyTable.c ========================================================*/
 extern Ivy_Obj_t *     Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj );
 extern void            Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj );

src/temp/ivy/ivyBalance.c

@@ -73,7 +73,9 @@ Ivy_Man_t * Ivy_ManBalance( Ivy_Man_t * p, int fUpdateLevel )
     }
     Vec_VecFree( vStore );
     if ( i = Ivy_ManCleanup( pNew ) )
-        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    {
+//        printf( "Cleanup after balancing removed %d dangling nodes.\n", i );
+    }
     // check the resulting AIG
     if ( !Ivy_ManCheck(pNew) )
         printf( "Ivy_ManBalance(): The check has failed.\n" );

src/temp/ivy/ivyFastMap.c

@@ -68,13 +68,16 @@ static int  Ivy_FastMapPrint( Ivy_Man_t * pAig, int Time );
 static int  Ivy_FastMapDelay( Ivy_Man_t * pAig );
 static int  Ivy_FastMapArea( Ivy_Man_t * pAig );
 static void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
+static void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit );
 static int  Ivy_FastMapMerge( Ivy_Supp_t * pSupp0, Ivy_Supp_t * pSupp1, Ivy_Supp_t * pSupp, int nLimit );
-static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay );
+static void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter );
 static void Ivy_FastMapRecover( Ivy_Man_t * pAig, int nLimit );
 static int  Ivy_FastMapNodeDelay( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 static int  Ivy_FastMapNodeAreaRefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 static int  Ivy_FastMapNodeAreaDerefed( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 static void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld );
+static int  Ivy_FastMapNodeRef( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
+static int  Ivy_FastMapNodeDeref( Ivy_Man_t * pAig, Ivy_Obj_t * pObj );
 
 
 extern int s_MappingTime;
@@ -108,6 +111,7 @@ void Ivy_FastMapPerform( Ivy_Man_t * pAig, int nLimit )
     pMan->nObjs  = Ivy_ManObjIdMax(pAig) + 1;
     pMan->nSize  = sizeof(Ivy_Supp_t) + nLimit * sizeof(int);
     pMan->pMem   = (char *)malloc( pMan->nObjs * pMan->nSize );
+    memset( pMan->pMem, 0, pMan->nObjs * pMan->nSize );
     pMan->vLuts  = Vec_VecAlloc( 100 );
     pAig->pData  = pMan;
 clk = clock();
@@ -122,28 +126,43 @@ clk = clock();
     printf( "Delay oriented mapping: " );
     Delay = Ivy_FastMapPrint( pAig, clock() - clk );
 
-    // perform area recovery
-clk = clock();
-    Ivy_FastMapRequired( pAig, Delay );
-//    PRT( "Required time computation", clock() - clk );
+// 2-1-2 (doing 2-1-2-1-2 improves 0.5%)
 
+clk = clock();
+    Ivy_FastMapRequired( pAig, Delay, 0 );
     // remap the nodes
     Ivy_FastMapRecover( pAig, nLimit );
-    printf( "Area recovery         : " );
+    printf( "Area recovery 2       : " );
     Delay = Ivy_FastMapPrint( pAig, clock() - clk );
 
-    // perform area recovery
 clk = clock();
-    Ivy_FastMapRequired( pAig, Delay );
-//    PRT( "Required time computation", clock() - clk );
+    Ivy_FastMapRequired( pAig, Delay, 0 );
+    // iterate through all nodes in the topological order
+    Ivy_ManForEachNode( pAig, pObj, i )
+        Ivy_FastMapNodeArea( pAig, pObj, nLimit );
+    printf( "Area recovery 1       : " );
+    Delay = Ivy_FastMapPrint( pAig, clock() - clk );
 
+clk = clock();
+    Ivy_FastMapRequired( pAig, Delay, 0 );
     // remap the nodes
     Ivy_FastMapRecover( pAig, nLimit );
-    printf( "Area recovery         : " );
+    printf( "Area recovery 2       : " );
     Delay = Ivy_FastMapPrint( pAig, clock() - clk );
 
+
     s_MappingTime = clock() - clkTotal;
     s_MappingMem = pMan->nObjs * pMan->nSize;
+/*
+    {
+        Vec_Ptr_t * vNodes;
+        vNodes = Vec_PtrAlloc( 100 );
+        Vec_VecForEachEntry( pMan->vLuts, pObj, i, k )
+            Vec_PtrPush( vNodes, pObj );
+        Ivy_ManShow( pAig, 0, vNodes );
+        Vec_PtrFree( vNodes );
+    }
+*/
 }
 
 /**Function*************************************************************
@@ -283,9 +302,261 @@ int Ivy_FastMapArea( Ivy_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
+static inline Ivy_ObjIsNodeInt1( Ivy_Obj_t * pObj )
+{
+    return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) == 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Ivy_ObjIsNodeInt2( Ivy_Obj_t * pObj )
+{
+    return Ivy_ObjIsNode(pObj) && Ivy_ObjRefs(pObj) <= 2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_IntSelectSort( int * pArray, int nSize )
+{
+    int temp, i, j, best_i;
+    for ( i = 0; i < nSize-1; i++ )
+    {
+        best_i = i;
+        for ( j = i+1; j < nSize; j++ )
+            if ( pArray[j] < pArray[best_i] )
+                best_i = j;
+        temp = pArray[i]; 
+        pArray[i] = pArray[best_i]; 
+        pArray[best_i] = temp;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Vec_IntRemoveDup( int * pArray, int nSize )
+{
+    int i, k;
+    if ( nSize < 2 )
+        return nSize;
+    for ( i = k = 1; i < nSize; i++ )
+        if ( pArray[i] != pArray[i-1] )
+            pArray[k++] = pArray[i];
+    return k;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FastMapNodeArea2( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
+{
+    static int Store[32], StoreSize;
+    static char Supp0[16], Supp1[16];
+    static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0;
+    static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1;
+    Ivy_Obj_t * pFanin0, * pFanin1;
+    Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+    int RetValue, DelayOld;
+    assert( nLimit <= 32 );
+    assert( Ivy_ObjIsNode(pObj) );
+    // get the fanins
+    pFanin0 = Ivy_ObjFanin0(pObj);
+    pFanin1 = Ivy_ObjFanin1(pObj);
+    // get the supports
+    pSupp0 = Ivy_ObjSupp( pAig, pFanin0 );
+    pSupp1 = Ivy_ObjSupp( pAig, pFanin1 );
+    pSupp  = Ivy_ObjSupp( pAig, pObj );
+    assert( pSupp->fMark == 0 );
+    // get the old delay of the node
+    DelayOld = Ivy_FastMapNodeDelay(pAig, pObj);
+    assert( DelayOld <= pSupp->DelayR );
+    // copy the current cut
+    memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize );
+    StoreSize = pSupp->nSize;
+    // get the fanin support
+    if ( Ivy_ObjRefs(pFanin0) > 1 && pSupp0->Delay < pSupp->DelayR )
+    {
+        pSupp0 = pTemp0;
+        pSupp0->nSize = 1;
+        pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj);
+    }
+    // get the fanin support
+    if ( Ivy_ObjRefs(pFanin1) > 1 && pSupp1->Delay < pSupp->DelayR )
+    {
+        pSupp1 = pTemp1;
+        pSupp1->nSize = 1;
+        pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj);
+    }
+    // merge the cuts
+    if ( pSupp0->nSize < pSupp1->nSize )
+        RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+    else
+        RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+    if ( !RetValue )
+    {
+        pSupp->nSize = 2;
+        pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+        pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+    }
+    // check the resulting delay
+    pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj);
+    if ( pSupp->Delay > pSupp->DelayR )
+    {
+        pSupp->nSize = StoreSize;
+        memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize );
+        pSupp->Delay = DelayOld;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FastMapNodeArea( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
+{
+    static int Store[32], StoreSize;
+    static char Supp0[16], Supp1[16];
+    static Ivy_Supp_t * pTemp0 = (Ivy_Supp_t *)Supp0;
+    static Ivy_Supp_t * pTemp1 = (Ivy_Supp_t *)Supp1;
+    Ivy_Obj_t * pFanin0, * pFanin1;
+    Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+    int RetValue, DelayOld, RefsOld;
+    int AreaBef, AreaAft;
+    assert( nLimit <= 32 );
+    assert( Ivy_ObjIsNode(pObj) );
+    // get the fanins
+    pFanin0 = Ivy_ObjFanin0(pObj);
+    pFanin1 = Ivy_ObjFanin1(pObj);
+    // get the supports
+    pSupp0 = Ivy_ObjSupp( pAig, pFanin0 );
+    pSupp1 = Ivy_ObjSupp( pAig, pFanin1 );
+    pSupp  = Ivy_ObjSupp( pAig, pObj );
+    assert( pSupp->fMark == 0 );
+
+    // get the area
+    if ( pSupp->nRefs == 0 )
+        AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+    else
+        AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+//    if ( AreaBef == 1 )
+//        return;
+
+    // deref the cut if the node is refed
+    if ( pSupp->nRefs != 0 )
+        Ivy_FastMapNodeDeref( pAig, pObj );
+
+    // get the old delay of the node
+    DelayOld = Ivy_FastMapNodeDelay(pAig, pObj);
+    assert( DelayOld <= pSupp->DelayR );
+    // copy the current cut
+    memcpy( Store, pSupp->pArray, sizeof(int) * pSupp->nSize );
+    StoreSize = pSupp->nSize;
+    // get the fanin support
+    if ( Ivy_ObjRefs(pFanin0) > 2 && pSupp0->Delay < pSupp->DelayR )
+//    if ( pSupp0->nRefs > 0 && pSupp0->Delay < pSupp->DelayR ) // this leads to 2% worse results
+    {
+        pSupp0 = pTemp0;
+        pSupp0->nSize = 1;
+        pSupp0->pArray[0] = Ivy_ObjFaninId0(pObj);
+    }
+    // get the fanin support
+    if ( Ivy_ObjRefs(pFanin1) > 2 && pSupp1->Delay < pSupp->DelayR )
+//    if ( pSupp1->nRefs > 0 && pSupp1->Delay < pSupp->DelayR )
+    {
+        pSupp1 = pTemp1;
+        pSupp1->nSize = 1;
+        pSupp1->pArray[0] = Ivy_ObjFaninId1(pObj);
+    }
+    // merge the cuts
+    if ( pSupp0->nSize < pSupp1->nSize )
+        RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+    else
+        RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+    if ( !RetValue )
+    {
+        pSupp->nSize = 2;
+        pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
+        pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
+    }
+
+    // check the resulting delay
+    pSupp->Delay = Ivy_FastMapNodeDelay(pAig, pObj);
+
+    RefsOld = pSupp->nRefs; pSupp->nRefs = 0;
+    AreaAft = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+    pSupp->nRefs = RefsOld;
+
+    if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
+//    if ( pSupp->Delay > pSupp->DelayR )
+    {
+        pSupp->nSize = StoreSize;
+        memcpy( pSupp->pArray, Store, sizeof(int) * pSupp->nSize );
+        pSupp->Delay = DelayOld;
+//        printf( "-" );
+    }
+//    else
+//        printf( "+" );
+
+    if ( pSupp->nRefs != 0 )
+        Ivy_FastMapNodeRef( pAig, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fast mapping for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
 {
     Ivy_Supp_t * pSupp0, * pSupp1, * pSupp;
+    int fFaninParam = 2;
     int RetValue;
     assert( Ivy_ObjIsNode(pObj) );
     // get the supports
@@ -316,10 +587,124 @@ void Ivy_FastMapNode( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit )
     if ( !RetValue )
     {
         pSupp->Delay++;
+        if ( fFaninParam == 2 )
+        {
             pSupp->nSize = 2;
             pSupp->pArray[0] = Ivy_ObjFaninId0(pObj);
             pSupp->pArray[1] = Ivy_ObjFaninId1(pObj);
         }
+        else if ( fFaninParam == 3 )
+        {
+            Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB;
+            pFanin0 = Ivy_ObjFanin0(pObj);
+            pFanin1 = Ivy_ObjFanin1(pObj);
+            pSupp->nSize = 0;
+            // process the first fanin
+            if ( Ivy_ObjIsNodeInt1(pFanin0) )
+            {
+                pFaninA = Ivy_ObjFanin0(pFanin0);
+                pFaninB = Ivy_ObjFanin1(pFanin0);
+                if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+                else
+                {
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+                }
+            }
+            else
+                pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+            // process the second fanin
+            if ( Ivy_ObjIsNodeInt1(pFanin1) )
+            {
+                pFaninA = Ivy_ObjFanin0(pFanin1);
+                pFaninB = Ivy_ObjFanin1(pFanin1);
+                if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+                else
+                {
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+                }
+            }
+            else
+                pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+            // sort the fanins
+            Vec_IntSelectSort( pSupp->pArray, pSupp->nSize );
+            pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize );
+            assert( pSupp->pArray[0] < pSupp->pArray[1] );
+        }
+        else if ( fFaninParam == 4 )
+        {
+            Ivy_Obj_t * pFanin0, * pFanin1, * pFaninA, * pFaninB;
+            pFanin0 = Ivy_ObjFanin0(pObj);
+            pFanin1 = Ivy_ObjFanin1(pObj);
+            pSupp->nSize = 0;
+            // consider the case when exactly one of them is internal
+            if ( Ivy_ObjIsNodeInt1(pFanin0) ^ Ivy_ObjIsNodeInt1(pFanin1) )
+            {
+                pSupp0 = Ivy_ObjSupp( pAig, Ivy_ObjFanin0(pObj) );
+                pSupp1 = Ivy_ObjSupp( pAig, Ivy_ObjFanin1(pObj) );
+                if ( Ivy_ObjIsNodeInt1(pFanin0) && pSupp0->nSize < nLimit )
+                {
+                    pSupp->Delay = IVY_MAX( pSupp0->Delay, pSupp1->Delay + 1 );
+                    pSupp1 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+                    pSupp1->pArray[0] = Ivy_ObjId(pFanin1);
+                    // merge the cuts
+                    RetValue = Ivy_FastMapMerge( pSupp0, pSupp1, pSupp, nLimit );
+                    assert( RetValue );
+                    assert( pSupp->nSize > 1 );
+                    return;
+                }
+                if ( Ivy_ObjIsNodeInt1(pFanin1) && pSupp1->nSize < nLimit )
+                {
+                    pSupp->Delay = IVY_MAX( pSupp1->Delay, pSupp0->Delay + 1 );
+                    pSupp0 = Ivy_ObjSupp( pAig, Ivy_ManConst1(pAig) );
+                    pSupp0->pArray[0] = Ivy_ObjId(pFanin0);
+                    // merge the cuts
+                    RetValue = Ivy_FastMapMerge( pSupp1, pSupp0, pSupp, nLimit );
+                    assert( RetValue );
+                    assert( pSupp->nSize > 1 );
+                    return;
+                }
+            }
+            // process the first fanin
+            if ( Ivy_ObjIsNodeInt1(pFanin0) )
+            {
+                pFaninA = Ivy_ObjFanin0(pFanin0);
+                pFaninB = Ivy_ObjFanin1(pFanin0);
+                if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+                else
+                {
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+                }
+            }
+            else
+                pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin0);
+            // process the second fanin
+            if ( Ivy_ObjIsNodeInt1(pFanin1) )
+            {
+                pFaninA = Ivy_ObjFanin0(pFanin1);
+                pFaninB = Ivy_ObjFanin1(pFanin1);
+                if ( Ivy_ObjIsNodeInt1(pFaninA) && Ivy_ObjIsNodeInt1(pFaninB) )
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+                else
+                {
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninA);
+                    pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFaninB);
+                }
+            }
+            else
+                pSupp->pArray[pSupp->nSize++] = Ivy_ObjId(pFanin1);
+            // sort the fanins
+            Vec_IntSelectSort( pSupp->pArray, pSupp->nSize );
+            pSupp->nSize = Vec_IntRemoveDup( pSupp->pArray, pSupp->nSize );
+            assert( pSupp->pArray[0] < pSupp->pArray[1] );
+            assert( pSupp->nSize > 1 );
+        }
+    }
     assert( pSupp->Delay > 0 );
 }
 
@@ -431,6 +816,29 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave
 
 /**Function*************************************************************
 
+  Synopsis    [Sets the required times of the intermediate nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FastMapRequired_rec( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Ivy_Obj_t * pRoot, int DelayR )
+{
+    Ivy_Supp_t * pSupp;
+    pSupp = Ivy_ObjSupp( pAig, pObj );
+    if ( pObj != pRoot && (pSupp->nRefs > 0 || Ivy_ObjIsCi(pObj)) )
+        return;
+    Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin0(pObj), pRoot, DelayR );
+    Ivy_FastMapRequired_rec( pAig, Ivy_ObjFanin1(pObj), pRoot, DelayR );
+//    assert( pObj == pRoot || pSupp->DelayR == IVY_INFINITY );
+    pSupp->DelayR = DelayR;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the required times for each node.]
 
   Description [Sets reference counters for each node.]
@@ -440,7 +848,7 @@ void Ivy_FastMapReadSupp( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, Vec_Int_t * vLeave
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay )
+void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay, int fSetInter )
 {
     Vec_Vec_t * vLuts;
     Vec_Ptr_t * vNodes;
@@ -491,6 +899,23 @@ void Ivy_FastMapRequired( Ivy_Man_t * pAig, int Delay )
     }
     printf( "\n" );    
 */
+
+    if ( fSetInter )
+    {
+        // set the required times of the intermediate nodes
+        Vec_VecForEachLevelReverse( vLuts, vNodes, i )
+        Vec_PtrForEachEntry( vNodes, pObj, k )
+        {
+            pSupp = Ivy_ObjSupp( pAig, pObj );
+            Ivy_FastMapRequired_rec( pAig, pObj, pObj, pSupp->DelayR ); 
+        }
+        // make sure that all required times are assigned
+        Ivy_ManForEachNode( pAig, pObj, i )
+        {
+            pSupp = Ivy_ObjSupp( pAig, pObj );
+            assert( pSupp->DelayR < IVY_INFINITY );
+        }
+    }
 }
 
 /**Function*************************************************************
@@ -688,7 +1113,7 @@ int Ivy_FastMapCutCost( Ivy_Man_t * pAig, Vec_Ptr_t * vFront )
     Vec_PtrForEachEntry( vFront, pFanin, i )
     {
         pSuppF = Ivy_ObjSupp( pAig, pFanin );
-        if ( pSuppF->nRefs == 1 )
+        if ( pSuppF->nRefs == 0 )
             Counter++;
     }
     return Counter;
@@ -754,17 +1179,17 @@ int Ivy_FastMapNodeFaninCost( Ivy_Man_t * pAig, Ivy_Obj_t * pObj )
     assert( Ivy_ObjIsNode(pObj) );
     // check if the node has external refs
     pSuppF = Ivy_ObjSupp( pAig, pObj );
-    if ( pSuppF->nRefs == 1 )
+    if ( pSuppF->nRefs == 0 )
         Counter--;
     // increment the number of fanins without external refs
     pFanin = Ivy_ObjFanin0(pObj);
     pSuppF = Ivy_ObjSupp( pAig, pFanin );
-    if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 )
+    if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 )
         Counter++;
     // increment the number of fanins without external refs
     pFanin = Ivy_ObjFanin1(pObj);
     pSuppF = Ivy_ObjSupp( pAig, pFanin );
-    if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 1 )
+    if ( !Ivy_ObjIsTravIdCurrent(pAig, pFanin) && pSuppF->nRefs == 0 )
         Counter++;
     return Counter;
 }
@@ -1055,13 +1480,79 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec
     Ivy_Supp_t * pSupp;
     int CostBef, CostAft;
     int AreaBef, AreaAft;
+    int DelayOld;
     pSupp = Ivy_ObjSupp( pAig, pObj );
+    DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+    assert( pSupp->Delay <= pSupp->DelayR );
     if ( pSupp->nRefs == 0 )
         return;
     // get the area
     AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+//    if ( AreaBef == 1 )
+//        return;
+    if ( pObj->Id == 102 )
+    {
+        int x = 0;
+    }
+    // the cut is non-trivial
+    Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld );
+    // iteratively modify the cut
+    Ivy_FastMapNodeDeref( pAig, pObj );
+    CostBef = Ivy_FastMapCutCost( pAig, vFront );
+    Ivy_FastMapNodeFaninCompact( pAig, pObj, nLimit, vFront );
+    CostAft = Ivy_FastMapCutCost( pAig, vFront );
+    Ivy_FastMapNodeRef( pAig, pObj );
+    assert( CostBef >= CostAft );
+    // update the node
+    Ivy_FastMapNodeUpdate( pAig, pObj, vFront );
+    pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+    // get the new area
+    AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+    if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
+    {
+        Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld );
+        AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+        assert( AreaAft == AreaBef );
+        pSupp->Delay = DelayOld;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs area recovery for each node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FastMapNodeRecover4( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec_Ptr_t * vFront, Vec_Ptr_t * vFrontOld )
+{
+    Ivy_Supp_t * pSupp;
+    int CostBef, CostAft;
+    int AreaBef, AreaAft;
+    int DelayOld;
+    pSupp = Ivy_ObjSupp( pAig, pObj );
+    DelayOld = pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
+    assert( pSupp->Delay <= pSupp->DelayR );
+//    if ( pSupp->nRefs == 0 )
+//        return;
+//    AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
+    // get the area
+    if ( pSupp->nRefs == 0 )
+        AreaBef = Ivy_FastMapNodeAreaDerefed( pAig, pObj );
+    else
+        AreaBef = Ivy_FastMapNodeAreaRefed( pAig, pObj );
     if ( AreaBef == 1 )
         return;
+
+    if ( pSupp->nRefs == 0 )
+    {
+        pSupp->nRefs = 1000000;
+        Ivy_FastMapNodeRef( pAig, pObj );
+    }
     // the cut is non-trivial
     Ivy_FastMapNodePrepare( pAig, pObj, nLimit, vFront, vFrontOld );
     // iteratively modify the cut
@@ -1071,13 +1562,20 @@ void Ivy_FastMapNodeRecover( Ivy_Man_t * pAig, Ivy_Obj_t * pObj, int nLimit, Vec
     assert( CostBef >= CostAft );
     // update the node
     Ivy_FastMapNodeUpdate( pAig, pObj, vFront );
+    pSupp->Delay = Ivy_FastMapNodeDelay( pAig, pObj );
     // get the new area
     AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
-    if ( AreaAft > AreaBef )
+    if ( AreaAft > AreaBef || pSupp->Delay > pSupp->DelayR )
     {
         Ivy_FastMapNodeUpdate( pAig, pObj, vFrontOld );
         AreaAft = Ivy_FastMapNodeAreaRefed( pAig, pObj );
         assert( AreaAft == AreaBef );
+        pSupp->Delay = DelayOld;
+    }
+    if ( pSupp->nRefs == 1000000 )
+    {
+        pSupp->nRefs = 0;
+        Ivy_FastMapNodeDeref( pAig, pObj );
     }
 }
 

src/temp/ivy/ivyFraig.c

+/**CFile****************************************************************
+
+  FileName    [ivyFraig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [And-Inverter Graph package.]
+
+  Synopsis    [Functional reduction of AIGs]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - May 11, 2006.]
+
+  Revision    [$Id: ivyFraig.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "ivy.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Ivy_Fraig_t_        Ivy_Fraig_t;
+struct Ivy_Fraig_t_
+{
+    // general info 
+    Ivy_FraigParams_t * pParams;        // various parameters
+    // AIG manager
+    Ivy_Man_t *         pManAig;        // the starting AIG manager
+    Ivy_Man_t *         pManFraig;      // the final AIG manager
+    // simulation information
+    int                 nWords;         // the number of words
+    unsigned *          pWords;         // the simulation info
+    // counter example storage
+    int                 nPatWords;      // the number of words in the counter example
+    unsigned *          pPatWords;      // the counter example
+    // equivalence classes 
+    int                 nClasses;       // the number of equivalence classes
+    Ivy_Obj_t *         pClassesHead;   // the linked list of classes
+    Ivy_Obj_t *         pClassesTail;   // the linked list of classes
+    // equivalence checking
+    sat_solver *        pSat;           // SAT solver
+    int                 nSatVars;       // the number of variables currently used
+    // statistics
+    int                 nSimRounds;
+    int                 nClassesZero;
+    int                 nClassesBeg;
+    int                 nClassesEnd;
+    int                 nSatCalls;
+    int                 nSatCallsSat;
+    int                 nSatCallsUnsat;
+    int                 nSatProof;
+    int                 nSatFails;
+    int                 nSatFailsReal;
+    // runtime
+    int                 timeSim;
+    int                 timeTrav;
+    int                 timeSat;
+    int                 timeRef;
+    int                 timeTotal;
+};
+
+static inline unsigned *  Ivy_ObjSim( Ivy_Obj_t * pObj )                                 { return (unsigned *)pObj->pFanout;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeLast( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeRepr( Ivy_Obj_t * pObj )                       { return pObj->pNextFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjClassNodeNext( Ivy_Obj_t * pObj )                       { return pObj->pNextFan1;  }
+static inline Ivy_Obj_t * Ivy_ObjNodeHashNext( Ivy_Obj_t * pObj )                        { return pObj->pPrevFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjEquivListNext( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan0;  }
+static inline Ivy_Obj_t * Ivy_ObjEquivListPrev( Ivy_Obj_t * pObj )                       { return pObj->pPrevFan1;  }
+static inline Ivy_Obj_t * Ivy_ObjFraig( Ivy_Obj_t * pObj )                               { return pObj->pEquiv;     }
+static inline int         Ivy_ObjSatNum( Ivy_Obj_t * pObj )                              { return (int)pObj->pNextFan0;         }
+static inline Vec_Ptr_t * Ivy_ObjFaninVec( Ivy_Obj_t * pObj )                            { return (Vec_Ptr_t *)pObj->pNextFan1; }
+
+static inline void        Ivy_ObjSetSim( Ivy_Obj_t * pObj, unsigned * pSim )             { pObj->pFanout = (Ivy_Obj_t *)pSim; }
+static inline void        Ivy_ObjSetClassNodeLast( Ivy_Obj_t * pObj, Ivy_Obj_t * pLast ) { pObj->pNextFan0 = pLast; }
+static inline void        Ivy_ObjSetClassNodeRepr( Ivy_Obj_t * pObj, Ivy_Obj_t * pRepr ) { pObj->pNextFan0 = pRepr; }
+static inline void        Ivy_ObjSetClassNodeNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pNextFan1 = pNext; }
+static inline void        Ivy_ObjSetNodeHashNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext )  { pObj->pPrevFan0 = pNext; }
+static inline void        Ivy_ObjSetEquivListNext( Ivy_Obj_t * pObj, Ivy_Obj_t * pNext ) { pObj->pPrevFan0 = pNext; }
+static inline void        Ivy_ObjSetEquivListPrev( Ivy_Obj_t * pObj, Ivy_Obj_t * pPrev ) { pObj->pPrevFan1 = pPrev; }
+static inline void        Ivy_ObjSetFraig( Ivy_Obj_t * pObj, Ivy_Obj_t * pNode )         { pObj->pEquiv    = pNode; }
+static inline void        Ivy_ObjSetSatNum( Ivy_Obj_t * pObj, int Num )                  { pObj->pNextFan0 = (Ivy_Obj_t *)Num;     }
+static inline void        Ivy_ObjSetFaninVec( Ivy_Obj_t * pObj, Vec_Ptr_t * vFanins )    { pObj->pNextFan1 = (Ivy_Obj_t *)vFanins; }
+
+static inline unsigned    Ivy_ObjRandomSim()                       { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+
+// iterate through equivalence classes
+#define Ivy_FraigForEachEquivClass( pList, pEnt )                 \
+    for ( pEnt = pList;                                           \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjEquivListNext(pEnt) )
+#define Ivy_FraigForEachEquivClassSafe( pList, pEnt, pEnt2 )      \
+    for ( pEnt = pList,                                           \
+          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL;         \
+          pEnt;                                                   \
+          pEnt = pEnt2,                                           \
+          pEnt2 = pEnt? Ivy_ObjEquivListNext(pEnt): NULL )
+// iterate through nodes in one class
+#define Ivy_FraigForEachClassNode( pClass, pEnt )                 \
+    for ( pEnt = pClass;                                          \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjClassNodeNext(pEnt) )
+#define Ivy_FraigForEachClassNodeSafe( pClass, pEnt, pEnt2 )      \
+    for ( pEnt = pClass,                                          \
+          pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL;         \
+          pEnt;                                                   \
+          pEnt = pEnt2,                                           \
+          pEnt2 = pEnt? Ivy_ObjClassNodeNext(pEnt): NULL )
+// iterate through nodes in the hash table
+#define Ivy_FraigForEachBinNode( pBin, pEnt )                     \
+    for ( pEnt = pBin;                                            \
+          pEnt;                                                   \
+          pEnt = Ivy_ObjNodeHashNext(pEnt) )
+#define Ivy_FraigForEachBinNodeSafe( pBin, pEnt, pEnt2 )          \
+    for ( pEnt = pBin,                                            \
+          pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL;          \
+          pEnt;                                                   \
+          pEnt = pEnt2,                                           \
+          pEnt2 = pEnt? Ivy_ObjNodeHashNext(pEnt): NULL )
+
+static Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams );
+static void          Ivy_FraigPrint( Ivy_Fraig_t * p );
+static void          Ivy_FraigStop( Ivy_Fraig_t * p );
+static void          Ivy_FraigSimulate( Ivy_Fraig_t * p );
+static void          Ivy_FraigSweep( Ivy_Fraig_t * p );
+static Ivy_Obj_t *   Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld );
+static int           Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1, int nBTLimit );
+static void          Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 );
+static int           Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging of the initial AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Ivy_FraigPerform( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_Fraig_t * p;
+    Ivy_Man_t * pManAigNew;
+    int clk;
+clk = clock();
+    assert( Ivy_ManLatchNum(pManAig) == 0 );
+    p = Ivy_FraigStart( pManAig, pParams );
+    Ivy_FraigSimulate( p );
+    Ivy_FraigSweep( p );
+    pManAigNew = p->pManFraig;
+p->timeTotal = clock() - clk;
+    Ivy_FraigStop( p );
+    return pManAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging of the initial AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams )
+{
+    memset( pParams, 0, sizeof(Ivy_FraigParams_t) );
+    pParams->nSimWords =     32;
+    pParams->SimSatur  =  0.005;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Fraig_t * Ivy_FraigStart( Ivy_Man_t * pManAig, Ivy_FraigParams_t * pParams )
+{
+    Ivy_Fraig_t * p;
+    Ivy_Obj_t * pObj;
+    int i, k;
+    // clean the fanout representation
+    Ivy_ManForEachObj( pManAig, pObj, i )
+//        pObj->pEquiv = pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+        assert( !pObj->pEquiv && !pObj->pFanout );
+    // allocat the fraiging manager
+    p = ALLOC( Ivy_Fraig_t, 1 );
+    memset( p, 0, sizeof(Ivy_Fraig_t) );
+    p->pParams   = pParams;
+    p->pManAig   = pManAig;
+    p->pManFraig = Ivy_ManStartFrom( pManAig );
+    // allocate simulation info
+    p->nWords    = pParams->nSimWords;
+    p->pWords    = ALLOC( unsigned, Ivy_ManObjNum(pManAig) * p->nWords ); 
+    k = 0;
+    Ivy_ManForEachObj( pManAig, pObj, i )
+        Ivy_ObjSetSim( pObj, p->pWords + p->nWords * k++ );
+    assert( k == Ivy_ManObjNum(pManAig) );
+    // allocate storage for sim pattern
+    p->nPatWords = Ivy_BitWordNum( Ivy_ManPiNum(pManAig) );
+    p->pPatWords = ALLOC( unsigned, p->nPatWords ); 
+    // set random number generator
+    srand( 0xABCABC );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrint( Ivy_Fraig_t * p )
+{
+    double nMemory;
+    nMemory = (double)Ivy_ManObjNum(p->pManAig)*p->nWords*sizeof(unsigned)/(1<<20);
+    printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nWords, p->nSimRounds, nMemory );
+    printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
+    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
+    printf( "Nodes: Final = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
+        Ivy_ManNodeNum(p->pManFraig), Ivy_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+    if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
+    PRT( "AIG simulation  ", p->timeSim  );
+    PRT( "AIG traversal   ", p->timeTrav  );
+    PRT( "SAT solving     ", p->timeSat   );
+    PRT( "Class refining  ", p->timeRef   );
+    PRT( "TOTAL RUNTIME   ", p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigStop( Ivy_Fraig_t * p )
+{
+    Ivy_FraigPrint( p );
+    if ( p->pSat ) sat_solver_delete( p->pSat );
+    free( p->pPatWords );
+    free( p->pWords );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAssignRandom( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i;
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nWords; i++ )
+        pSims[i] = Ivy_ObjRandomSim();
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAssignConst( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int fConst1 )
+{
+    unsigned * pSims;
+    int i;
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nWords; i++ )
+        pSims[i] = fConst1? ~(unsigned)0 : 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeHasZeroSim( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i;
+    pSims = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nWords; i++ )
+        if ( pSims[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation infos are equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_NodeCompareSims( Ivy_Fraig_t * p, Ivy_Obj_t * pObj0, Ivy_Obj_t * pObj1 )
+{
+    unsigned * pSims0, * pSims1;
+    int i;
+    pSims0 = Ivy_ObjSim(pObj0);
+    pSims1 = Ivy_ObjSim(pObj1);
+    for ( i = 0; i < p->nWords; i++ )
+        if ( pSims0[i] != pSims1[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeSimulate( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+    unsigned * pSims, * pSims0, * pSims1;
+    int fCompl, fCompl0, fCompl1, i;
+    assert( !Ivy_IsComplement(pObj) );
+    // get hold of the simulation information
+    pSims  = Ivy_ObjSim(pObj);
+    pSims0 = Ivy_ObjSim(Ivy_ObjFanin0(pObj));
+    pSims1 = Ivy_ObjSim(Ivy_ObjFanin1(pObj));
+    // get complemented attributes of the children using their random info
+    fCompl  = pObj->fPhase;
+    fCompl0 = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+    fCompl1 = Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+    // simulate
+    if ( fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (pSims0[i] | pSims1[i]);
+        else
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = ~(pSims0[i] | pSims1[i]);
+    }
+    else if ( fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (pSims0[i] | ~pSims1[i]);
+        else
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (~pSims0[i] & pSims1[i]);
+    }
+    else if ( !fCompl0 && fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (~pSims0[i] | pSims1[i]);
+        else
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (pSims0[i] & ~pSims1[i]);
+    }
+    else // if ( !fCompl0 && !fCompl1 )
+    {
+        if ( fCompl )
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = ~(pSims0[i] & pSims1[i]);
+        else
+            for ( i = 0; i < p->nWords; i++ )
+                pSims[i] = (pSims0[i] & pSims1[i]);
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value using simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Ivy_NodeHash( Ivy_Fraig_t * p, Ivy_Obj_t * pObj )
+{
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned uHash, * pSims;
+    int i;
+    assert( p->nWords <= 128 );
+    uHash = 0;
+    pSims  = Ivy_ObjSim(pObj);
+    for ( i = 0; i < p->nWords; i++ )
+        uHash ^= pSims[i] * s_FPrimes[i];
+    return uHash;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSimulateOne( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i, clk;
+clk = clock();
+    Ivy_ManForEachNode( p->pManAig, pObj, i )
+    {
+        Ivy_NodeSimulate( p, pObj );
+/*
+        if ( Ivy_ObjFraig(pObj) == NULL )
+            printf( "%3d --- -- %d  :  ", pObj->Id, pObj->fPhase );
+        else
+            printf( "%3d %3d %2d %d  :  ", pObj->Id, Ivy_Regular(Ivy_ObjFraig(pObj))->Id, Ivy_ObjSatNum(Ivy_Regular(Ivy_ObjFraig(pObj))), pObj->fPhase );
+        Extra_PrintBinary( stdout, Ivy_ObjSim(pObj), 30 );
+        printf( "\n" );
+*/
+    }
+p->timeSim += clock() - clk;
+p->nSimRounds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAssignRandom( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+        Ivy_NodeAssignRandom( p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates AIG manager.]
+
+  Description [Assumes that the PI simulation info is attached.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAssignDist1( Ivy_Fraig_t * p, unsigned * pPat )
+{
+    Ivy_Obj_t * pObj;
+    int i, Limit;
+    Ivy_ManForEachPi( p->pManAig, pObj, i )
+        Ivy_NodeAssignConst( p, pObj, Ivy_InfoHasBit(pPat, i) );
+    Limit = IVY_MIN( Ivy_ManPiNum(p->pManAig), p->nWords * 32 - 1 );
+    for ( i = 0; i < Limit; i++ )
+        Ivy_InfoXorBit( Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), i+1 );
+/*
+    for ( i = 0; i < Limit; i++ )
+        Extra_PrintBinary( stdout, Ivy_ObjSim( Ivy_ManPi(p->pManAig,i) ), 30 ), printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds new nodes to the equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_NodeAddToClass( Ivy_Obj_t * pClass, Ivy_Obj_t * pObj )
+{
+    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+        Ivy_ObjSetClassNodeNext( pClass, pObj );
+    else
+        Ivy_ObjSetClassNodeNext( Ivy_ObjClassNodeLast(pClass), pObj );
+    Ivy_ObjSetClassNodeLast( pClass, pObj );
+    Ivy_ObjSetClassNodeRepr( pObj, pClass );
+    Ivy_ObjSetClassNodeNext( pObj, NULL );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds new nodes to the equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+    if ( p->pClassesHead == NULL )
+    {
+        p->pClassesHead = pClass;
+        p->pClassesTail = pClass;
+        Ivy_ObjSetEquivListPrev( pClass, NULL );
+        Ivy_ObjSetEquivListNext( pClass, NULL ); 
+    }
+    else
+    {
+        Ivy_ObjSetEquivListNext( p->pClassesTail, pClass ); 
+        Ivy_ObjSetEquivListPrev( pClass, p->pClassesTail );
+        Ivy_ObjSetEquivListNext( pClass, NULL ); 
+        p->pClassesTail = pClass;
+    }
+    p->nClasses++;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Updates the list of classes after base class has split.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigInsertClass( Ivy_Fraig_t * p, Ivy_Obj_t * pBase, Ivy_Obj_t * pClass )
+{
+    Ivy_ObjSetEquivListPrev( pClass, pBase );
+    Ivy_ObjSetEquivListNext( pClass, Ivy_ObjEquivListNext(pBase) ); 
+    if ( Ivy_ObjEquivListNext(pBase) )
+        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pBase), pClass );
+    Ivy_ObjSetEquivListNext( pBase, pClass ); 
+    if ( p->pClassesTail == pBase )
+        p->pClassesTail = pClass;
+    p->nClasses++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the list of classes after base class has split.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigRemoveClass( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+    if ( p->pClassesHead == pClass )
+        p->pClassesHead = Ivy_ObjEquivListNext(pClass);
+    if ( p->pClassesTail == pClass )
+        p->pClassesTail = Ivy_ObjEquivListPrev(pClass);
+    if ( Ivy_ObjEquivListPrev(pClass) )
+        Ivy_ObjSetEquivListNext( Ivy_ObjEquivListPrev(pClass), Ivy_ObjEquivListNext(pClass) ); 
+    if ( Ivy_ObjEquivListNext(pClass) )
+        Ivy_ObjSetEquivListPrev( Ivy_ObjEquivListNext(pClass), Ivy_ObjEquivListPrev(pClass) );
+    Ivy_ObjSetEquivListNext( pClass, NULL ); 
+    Ivy_ObjSetEquivListPrev( pClass, NULL );
+    p->nClasses--;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCreateClasses( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t ** pTable;
+    Ivy_Obj_t * pObj, * pConst1, * pBin, * pEntry, * pEntry2;
+    int i, nTableSize;
+    unsigned Hash;
+    pConst1 = Ivy_ManConst1(p->pManAig);
+    // allocate the table
+    nTableSize = Ivy_ManObjNum(p->pManAig) / 2 + 13;
+    pTable = ALLOC( Ivy_Obj_t *, nTableSize ); 
+    memset( pTable, 0, sizeof(Ivy_Obj_t *) * nTableSize );
+    // collect nodes into the table
+    Ivy_ManForEachObj( p->pManAig, pObj, i )
+    {
+        if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsNode(pObj) )
+            continue;
+        Hash = Ivy_NodeHash( p, pObj );
+        if ( Hash == 0 && Ivy_NodeHasZeroSim( p, pObj ) )
+        {
+            Ivy_NodeAddToClass( pConst1, pObj );
+            continue;
+        }
+        // add the node to the table
+        pBin = pTable[Hash % nTableSize];
+        Ivy_FraigForEachBinNode( pBin, pEntry )
+            if ( Ivy_NodeCompareSims( p, pEntry, pObj ) )
+            {
+                Ivy_NodeAddToClass( pEntry, pObj );
+                break;
+            }
+        // check if the entry was added
+        if ( pEntry )
+            continue;
+        Ivy_ObjSetNodeHashNext( pObj, pBin );
+        pTable[Hash % nTableSize] = pObj;
+    }
+    // collect non-trivial classes
+    assert( p->pClassesHead == NULL );
+    if ( Ivy_ObjClassNodeNext(pConst1) )
+    {
+        Ivy_FraigAddClass( p, pConst1 );
+        Ivy_ObjSetClassNodeLast( pConst1, NULL );
+    }
+    for ( i = 0; i < nTableSize; i++ )
+        Ivy_FraigForEachBinNodeSafe( pTable[i], pEntry, pEntry2 )
+            if ( Ivy_ObjClassNodeNext(pEntry) )
+            {
+                Ivy_FraigAddClass( p, pEntry );
+                Ivy_ObjSetClassNodeLast( pEntry, NULL );
+            }
+            else
+                Ivy_ObjSetNodeHashNext( pEntry, NULL );
+    // free the table
+    free( pTable );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively refines the class after simulation.]
+
+  Description [Returns 1 if the class has changed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigRefineClass_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pClassNew, * pListOld, * pListNew, * pNode;
+    // check if there is refinement
+    pListOld = pClass;
+    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClass), pClassNew )
+    {
+        if ( !Ivy_NodeCompareSims(p, pClass, pClassNew) )
+            break;
+        pListOld = pClassNew;
+    }
+    if ( pClassNew == NULL )
+        return 0;
+    // set representative of the new class
+    Ivy_ObjSetClassNodeRepr( pClassNew, NULL );
+    // start the new list
+    pListNew = pClassNew;
+    // go through the remaining nodes and sort them into two groups:
+    // (1) matches of the old node; (2) non-matches of the old node
+    Ivy_FraigForEachClassNode( Ivy_ObjClassNodeNext(pClassNew), pNode )
+        if ( Ivy_NodeCompareSims( p, pClass, pNode ) )
+        {
+            Ivy_ObjSetClassNodeNext( pListOld, pNode );
+            pListOld = pNode;
+        }
+        else
+        {
+            Ivy_ObjSetClassNodeNext( pListNew, pNode );
+            Ivy_ObjSetClassNodeRepr( pNode, pClassNew );
+            pListNew = pNode;
+        }
+    // finish both lists
+    Ivy_ObjSetClassNodeNext( pListNew, NULL );
+    Ivy_ObjSetClassNodeNext( pListOld, NULL );
+    // update the list of classes
+    Ivy_FraigInsertClass( p, pClass, pClassNew );
+    // if the old class is trivial, remove it
+    if ( Ivy_ObjClassNodeNext(pClass) == NULL )
+        Ivy_FraigRemoveClass( p, pClass );
+    // if the new class is trivial, remove it; otherwise, try to refine it
+    if ( Ivy_ObjClassNodeNext(pClassNew) == NULL )
+        Ivy_FraigRemoveClass( p, pClassNew );
+    else
+        Ivy_FraigRefineClass_rec( p, pClassNew );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes after simulation.]
+
+  Description [Assumes that simulation info is assigned. Returns the
+  number of classes refined.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigRefineClasses( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pClass, * pClass2;
+    int clk, RetValue = 0;
+clk = clock();
+    Ivy_FraigForEachEquivClassSafe( p->pClassesHead, pClass, pClass2 )
+        RetValue += Ivy_FraigRefineClass_rec( p, pClass );
+p->timeRef += clock() - clk;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Print the class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrintClass( Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pObj;
+    printf( "Class {" );
+    Ivy_FraigForEachClassNode( pClass, pObj )
+        printf( " %d(%d)%c", pObj->Id, pObj->Level, pObj->fPhase? '+' : '-' );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count the number of elements in the class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCountClassNodes( Ivy_Obj_t * pClass )
+{
+    Ivy_Obj_t * pObj;
+    int Counter = 0;
+    Ivy_FraigForEachClassNode( pClass, pObj )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigCountClasses( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pClass;
+    int Counter = 0;
+    Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
+        Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigPrintSimClasses( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pClass;
+    Ivy_FraigForEachEquivClass( p->pClassesHead, pClass )
+    {
+//        Ivy_FraigPrintClass( pClass );
+        printf( "%d ", Ivy_FraigCountClassNodes( pClass ) );
+    }
+//    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSimulate( Ivy_Fraig_t * p )
+{
+    int nChanges, nClasses;
+    Ivy_FraigAssignRandom( p );
+    Ivy_FraigSimulateOne( p );
+    Ivy_FraigCreateClasses( p );
+//printf( "Starting classes = %5d.\n", p->nClasses );
+    do {
+        Ivy_FraigAssignRandom( p );
+        Ivy_FraigSimulateOne( p );
+        nClasses = p->nClasses;
+        nChanges = Ivy_FraigRefineClasses( p );
+//printf( "Refined classes  = %5d.   Changes = %4d.\n", p->nClasses, nChanges );
+    } while ( (double)nChanges / nClasses > p->pParams->SimSatur );
+//    Ivy_FraigPrintSimClasses( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigResimulate( Ivy_Fraig_t * p )
+{
+    int nChanges;
+    Ivy_FraigAssignDist1( p, p->pPatWords );
+    Ivy_FraigSimulateOne( p );
+    nChanges = Ivy_FraigRefineClasses( p );
+    assert( nChanges >= 1 );
+//printf( "Refined classes! = %5d.   Changes = %4d.\n", p->nClasses, nChanges );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSweep( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+p->nClassesZero = Ivy_ObjIsConst1(p->pClassesHead) ? Ivy_FraigCountClassNodes(p->pClassesHead) : 0;
+p->nClassesBeg  = Ivy_FraigCountClasses(p);
+    // duplicate internal nodes
+    Ivy_ManForEachNode( p->pManAig, pObj, i )
+        pObj->pEquiv = Ivy_FraigAnd( p, pObj );
+p->nClassesEnd = Ivy_FraigCountClasses(p);
+    // add the POs
+    Ivy_ManForEachPo( p->pManAig, pObj, i )
+        Ivy_ObjCreatePo( p->pManFraig, Ivy_ObjChild0Equiv(pObj) );
+    // clean the old manager
+    Ivy_ManForEachObj( p->pManAig, pObj, i )
+        pObj->pFanout = pObj->pNextFan0 = pObj->pNextFan1 = pObj->pPrevFan0 = pObj->pPrevFan1 = NULL;
+    // clean the new manager
+    Ivy_ManForEachObj( p->pManFraig, pObj, i )
+    {
+        if ( Ivy_ObjFaninVec(pObj) )
+            Vec_PtrFree( Ivy_ObjFaninVec(pObj) );
+        pObj->pNextFan0 = pObj->pNextFan1 = NULL;
+    }
+    // remove dangling nodes 
+    Ivy_ManCleanup( p->pManFraig );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Ivy_FraigAnd( Ivy_Fraig_t * p, Ivy_Obj_t * pObjOld )
+{
+    Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew;
+    int RetValue;
+    // get the fraiged fanins
+    pFanin0New = Ivy_ObjChild0Equiv(pObjOld);
+    pFanin1New = Ivy_ObjChild1Equiv(pObjOld);
+    // get the candidate fraig node
+    pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New );
+    // get representative of this class
+    if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL ) // this is a unique node
+    {
+        assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
+        assert( pObjNew != Ivy_Regular(pFanin0New) );
+        assert( pObjNew != Ivy_Regular(pFanin1New) );
+        return pObjNew;
+    }
+    // get the fraiged representative
+    pObjReprNew = Ivy_ObjFraig(Ivy_ObjClassNodeRepr(pObjOld));
+    // if the fraiged nodes are the same return
+    if ( Ivy_Regular(pObjNew) == Ivy_Regular(pObjReprNew) )
+        return pObjNew;
+    // they are different (the counter-example is in p->pPatWords)
+    RetValue = Ivy_FraigNodesAreEquiv( p, Ivy_Regular(pObjReprNew), Ivy_Regular(pObjNew), 1000 );
+    if ( RetValue == 1 )  // proved equivalent
+        return Ivy_NotCond( pObjReprNew, pObjOld->fPhase ^ Ivy_ObjClassNodeRepr(pObjOld)->fPhase );
+    if ( RetValue == -1 ) // failed
+        return pObjNew;
+    // simulate the counter-example and return the new node
+    Ivy_FraigResimulate( p );
+    return pObjNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigSavePattern( Ivy_Fraig_t * p )
+{
+    Ivy_Obj_t * pObj;
+    int i;
+    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
+    Ivy_ManForEachPi( p->pManFraig, pObj, i )
+        if ( p->pSat->model.ptr[Ivy_ObjSatNum(pObj)] == l_True )
+            Ivy_InfoSetBit( p->pPatWords, i );
+/*
+    // print sat variables
+    for ( i = 0; i < p->nSatVars; i++ )
+        printf( "%d=%d ", i, p->pSat->model.ptr[i] );
+    printf( "\n" );
+*/
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigNodesAreEquiv( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew, int nBTLimit )
+{
+    int pLits[4], RetValue, RetValue1, clk, Counter;
+
+//    printf( "Trying to prove nodes %d and %d\n", pOld->Id, pNew->Id );
+
+    // make sure the nodes are not complemented
+    assert( !Ivy_IsComplement(pNew) );
+    assert( !Ivy_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    if ( nBTLimit > 0 && (pOld->fFailTfo || pNew->fFailTfo) )
+    {
+        p->nSatFails++;
+        if ( nBTLimit <= 10 )
+            return -1;
+        nBTLimit = (int)sqrt(nBTLimit);
+    }
+    p->nSatCalls++;
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+    {
+        p->pSat = sat_solver_new();
+        p->nSatVars = 1;
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
+
+    // if the nodes do not have SAT variables, allocate them
+    Ivy_FraigNodeAddToSolver( p, pOld, pNew );
+
+    // prepare variable activity
+clk = clock();
+    Ivy_ManIncrementTravId( p->pManFraig );
+    Counter  = Ivy_FraigMarkConeSetActivity_rec( p, pOld, NULL, 0, NULL, 0 );
+    Counter += Ivy_FraigMarkConeSetActivity_rec( p, pNew, NULL, 0, NULL, 0 );
+//    printf( "%d ", Counter );
+p->timeTrav += clock() - clk;
+
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+clk = clock();
+    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 0 );
+    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        // continue solving the other implication
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+        Ivy_FraigSavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+        // mark the node as the failed node
+        if ( pOld != p->pManFraig->pConst1 ) 
+            pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // if the old node was constant 0, we already know the answer
+    if ( pOld == p->pManFraig->pConst1 )
+    {
+        p->nSatProof++;
+        return 1;
+    }
+
+    // solve under assumptions
+    // A = 0; B = 1     OR     A = 0; B = 0 
+clk = clock();
+    pLits[0] = toLitCond( Ivy_ObjSatNum(pOld), 1 );
+    pLits[1] = toLitCond( Ivy_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+        Ivy_FraigSavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+        // mark the node as the failed node
+        pOld->fFailTfo = 1;
+        pNew->fFailTfo = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClausesMux( Ivy_Fraig_t * p, Ivy_Obj_t * pNode )
+{
+    Ivy_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+    assert( !Ivy_IsComplement( pNode ) );
+    assert( Ivy_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Ivy_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the variable numbers
+    VarF = Ivy_ObjSatNum(pNode);
+    VarI = Ivy_ObjSatNum(pNodeI);
+    VarT = Ivy_ObjSatNum(Ivy_Regular(pNodeT));
+    VarE = Ivy_ObjSatNum(Ivy_Regular(pNodeE));
+    // get the complementation flags
+    fCompT = Ivy_IsComplement(pNodeT);
+    fCompE = Ivy_IsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 1^fCompT);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 0^fCompT);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = toLitCond(VarT, 0^fCompT);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarT, 1^fCompT);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigAddClausesSuper( Ivy_Fraig_t * p, Ivy_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+    Ivy_Obj_t * pFanin;
+    int * pLits, nLits, RetValue, i;
+    assert( !Ivy_IsComplement(pNode) );
+    assert( Ivy_ObjIsNode( pNode ) );
+    // create storage for literals
+    nLits = Vec_PtrSize(vSuper) + 1;
+    pLits = ALLOC( int, nLits );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), Ivy_IsComplement(pFanin));
+        pLits[1] = toLitCond(Ivy_ObjSatNum(pNode), 1);
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+        pLits[i] = toLitCond(Ivy_ObjSatNum(Ivy_Regular(pFanin)), !Ivy_IsComplement(pFanin));
+    pLits[nLits-1] = toLitCond(Ivy_ObjSatNum(pNode), 0);
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+    assert( RetValue );
+    free( pLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigCollectSuper_rec( Ivy_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Ivy_IsComplement(pObj) || Ivy_ObjIsPi(pObj) || (!fFirst && Ivy_ObjRefs(pObj) > 1) || 
+         (fUseMuxes && Ivy_ObjIsMuxType(pObj)) )
+    {
+        Vec_PtrPushUnique( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    Ivy_FraigCollectSuper_rec( Ivy_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Ivy_FraigCollectSuper_rec( Ivy_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ivy_FraigCollectSuper( Ivy_Obj_t * pObj, int fUseMuxes )
+{
+    Vec_Ptr_t * vSuper;
+    assert( !Ivy_IsComplement(pObj) );
+    assert( !Ivy_ObjIsPi(pObj) );
+    vSuper = Vec_PtrAlloc( 4 );
+    Ivy_FraigCollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+    return vSuper;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigObjAddToFrontier( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Ivy_IsComplement(pObj) );
+    if ( Ivy_ObjSatNum(pObj) )
+        return;
+    assert( Ivy_ObjSatNum(pObj) == 0 );
+    assert( Ivy_ObjFaninVec(pObj) == NULL );
+    if ( Ivy_ObjIsConst1(pObj) )
+        return;
+//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
+    Ivy_ObjSetSatNum( pObj, p->nSatVars++ );
+    if ( Ivy_ObjIsNode(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ivy_FraigNodeAddToSolver( Ivy_Fraig_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pNew )
+{
+    Vec_Ptr_t * vFrontier, * vFanins;
+    Ivy_Obj_t * pNode, * pFanin;
+    int i, k, fUseMuxes = 1;
+    // quit if CNF is ready
+    if ( Ivy_ObjFaninVec(pOld) && Ivy_ObjFaninVec(pNew) )
+        return;
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    Ivy_FraigObjAddToFrontier( p, pOld, vFrontier );
+    Ivy_FraigObjAddToFrontier( p, pNew, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( Ivy_ObjSatNum(pNode) );
+        assert( Ivy_ObjFaninVec(pNode) == NULL );
+        if ( fUseMuxes && Ivy_ObjIsMuxType(pNode) )
+        {
+            vFanins = Vec_PtrAlloc( 4 );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin0( Ivy_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( vFanins, Ivy_ObjFanin1( Ivy_ObjFanin1(pNode) ) );
+            Vec_PtrForEachEntry( vFanins, pFanin, k )
+                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+            Ivy_FraigAddClausesMux( p, pNode );
+        }
+        else
+        {
+            vFanins = Ivy_FraigCollectSuper( pNode, fUseMuxes );
+            Vec_PtrForEachEntry( vFanins, pFanin, k )
+                Ivy_FraigObjAddToFrontier( p, Ivy_Regular(pFanin), vFrontier );
+            Ivy_FraigAddClausesSuper( p, pNode, vFanins );
+        }
+        assert( Vec_PtrSize(vFanins) > 1 );
+        Ivy_ObjSetFaninVec( pNode, vFanins );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_FraigMarkConeSetActivity_rec( Ivy_Fraig_t * p, Ivy_Obj_t * pObj, int * pTravIds, int TravId, double * pFactors, int LevelMax )
+{
+    Vec_Ptr_t * vFanins;
+    Ivy_Obj_t * pFanin;
+    int i, Counter;
+    assert( !Ivy_IsComplement(pObj) );
+    if ( Ivy_ObjIsConst1(pObj) )
+        return 0;
+    assert( Ivy_ObjSatNum(pObj) );
+//    if ( pTravIds[Ivy_ObjSatNum(pObj)] == TravId )
+//        return;
+//    pTravIds[Ivy_ObjSatNum(pObj)] = TravId;
+//    pFactors[Ivy_ObjSatNum(pObj)] = pow( 0.97, LevelMax - pObj->Level );
+    if ( Ivy_ObjIsTravIdCurrent(p->pManFraig, pObj) )
+        return 0;
+    Ivy_ObjSetTravIdCurrent(p->pManFraig, pObj);
+    if ( Ivy_ObjIsPi(pObj) )
+        return 0;
+
+    vFanins = Ivy_ObjFaninVec( pObj );
+    Counter = 1;
+    Vec_PtrForEachEntry( vFanins, pFanin, i )
+        Counter += Ivy_FraigMarkConeSetActivity_rec( p, Ivy_Regular(pFanin), pTravIds, TravId, pFactors, LevelMax );
+    return Counter;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/ivy/ivyMan.c

@@ -58,7 +58,7 @@ Ivy_Man_t * Ivy_ManStart()
     Ivy_ManStartMemory( p );
     // create the constant node
     p->pConst1 = Ivy_ManFetchMemory( p );
-//    p->pConst1->fPhase = 1;
+    p->pConst1->fPhase = 1;
     Vec_PtrPush( p->vObjs, p->pConst1 );
     p->nCreated = 1;
     // start the table
@@ -79,6 +79,31 @@ Ivy_Man_t * Ivy_ManStart()
   SeeAlso     []
 
 ***********************************************************************/
+Ivy_Man_t * Ivy_ManStartFrom( Ivy_Man_t * p )
+{
+    Ivy_Man_t * pNew;
+    Ivy_Obj_t * pObj;
+    int i;
+    // create the new manager
+    pNew = Ivy_ManStart();
+    // create the PIs
+    Ivy_ManConst1(p)->pEquiv = Ivy_ManConst1(pNew);
+    Ivy_ManForEachPi( p, pObj, i )
+        pObj->pEquiv = Ivy_ObjCreatePi(pNew);
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ivy_Man_t * Ivy_ManDup( Ivy_Man_t * p )
 {
     Vec_Int_t * vNodes, * vLatches;

src/temp/ivy/ivyObj.c

@@ -96,6 +96,14 @@ Ivy_Obj_t * Ivy_ObjCreate( Ivy_Man_t * p, Ivy_Obj_t * pGhost )
         pObj->Level = Ivy_ObjFanin0(pObj)->Level;
     else if ( !Ivy_ObjIsPi(pObj) )
         assert( 0 );
+    // create phase
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj)) & Ivy_ObjFaninPhase(Ivy_ObjChild1(pObj));
+    else if ( Ivy_ObjIsOneFanin(pObj) )
+        pObj->fPhase = Ivy_ObjFaninPhase(Ivy_ObjChild0(pObj));
+    // set the fail TFO flag
+    if ( Ivy_ObjIsNode(pObj) )
+        pObj->fFailTfo = Ivy_ObjFanin0(pObj)->fFailTfo | Ivy_ObjFanin1(pObj)->fFailTfo;
     // mark the fanins in a special way if the node is EXOR
     if ( Ivy_ObjIsExor(pObj) )
     {

src/temp/ivy/ivyShow.c

@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
+static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,7 +41,7 @@ static void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig );
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
+void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig, Vec_Ptr_t * vBold )
 {
     extern void Abc_ShowFile( char * FileNameDot );
     static Counter = 0;
@@ -58,7 +58,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
     }
     fclose( pFile );
     // generate the file
-    Ivy_WriteDotAig( pMan, FileNameDot, fHaig );
+    Ivy_WriteDotAig( pMan, FileNameDot, fHaig, vBold );
     // visualize the file 
     Abc_ShowFile( FileNameDot );
 }
@@ -75,7 +75,7 @@ void Ivy_ManShow( Ivy_Man_t * pMan, int fHaig )
   SeeAlso     []
 
 ***********************************************************************/
-void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
+void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * vBold )
 {
     FILE * pFile;
     Ivy_Obj_t * pNode, * pTemp, * pPrev;
@@ -92,6 +92,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
         return;
     }
 
+    // mark the nodes
+    if ( vBold )
+        Vec_PtrForEachEntry( vBold, pNode, i )
+            pNode->fMarkB = 1;
+
     // compute levels
     LevelMax = 1 + Ivy_ManSetLevels( pMan, fHaig );
 
@@ -218,6 +223,8 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
                 fprintf( pFile, "  Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, 
                     Ivy_Regular(pNode->pEquiv)->Id, Ivy_IsComplement(pNode->pEquiv)? "\'":"" );
             fprintf( pFile, ", shape = ellipse" );
+            if ( vBold && pNode->fMarkB )
+                fprintf( pFile, ", style = filled" );
             fprintf( pFile, "];\n" );
         }
         fprintf( pFile, "}" );
@@ -316,6 +323,11 @@ void Ivy_WriteDotAig( Ivy_Man_t * pMan, char * pFileName, int fHaig )
     fprintf( pFile, "\n" );
     fprintf( pFile, "\n" );
     fclose( pFile );
+
+    // unmark nodes
+    if ( vBold )
+        Vec_PtrForEachEntry( vBold, pNode, i )
+            pNode->fMarkB = 0;
 }
 
 

src/temp/ivy/satSolver.c

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#include <stdio.h>
+#include <assert.h>
+#include <string.h>
+#include <math.h>
+
+#include "satSolver.h"
+
+//=================================================================================================
+// Debug:
+
+//#define VERBOSEDEBUG
+
+// For derivation output (verbosity level 2)
+#define L_IND    "%-*d"
+#define L_ind    sat_solver_dlevel(s)*3+3,sat_solver_dlevel(s)
+#define L_LIT    "%sx%d"
+#define L_lit(p) lit_sign(p)?"~":"", (lit_var(p))
+
+// Just like 'assert()' but expression will be evaluated in the release version as well.
+static inline void check(int expr) { assert(expr); }
+
+static void printlits(lit* begin, lit* end)
+{
+    int i;
+    for (i = 0; i < end - begin; i++)
+        printf(L_LIT" ",L_lit(begin[i]));
+}
+
+//=================================================================================================
+// Random numbers:
+
+
+// Returns a random float 0 <= x < 1. Seed must never be 0.
+static inline double drand(double* seed) {
+    int q;
+    *seed *= 1389796;
+    q = (int)(*seed / 2147483647);
+    *seed -= (double)q * 2147483647;
+    return *seed / 2147483647; }
+
+
+// Returns a random integer 0 <= x < size. Seed must never be 0.
+static inline int irand(double* seed, int size) {
+    return (int)(drand(seed) * size); }
+
+
+//=================================================================================================
+// Predeclarations:
+
+static void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *));
+
+//=================================================================================================
+// Clause datatype + minor functions:
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int   clause_size       (clause* c)          { return c->size_learnt >> 1; }
+static inline lit*  clause_begin      (clause* c)          { return c->lits; }
+static inline int   clause_learnt     (clause* c)          { return c->size_learnt & 1; }
+static inline float clause_activity   (clause* c)          { return *((float*)&c->lits[c->size_learnt>>1]); }
+static inline void  clause_setactivity(clause* c, float a) { *((float*)&c->lits[c->size_learnt>>1]) = a; }
+
+//=================================================================================================
+// Encode literals in clause pointers:
+
+static clause* clause_from_lit (lit l)     { return (clause*)((unsigned long)l + (unsigned long)l + 1);  }
+static bool    clause_is_lit   (clause* c) { return ((unsigned long)c & 1);                              }
+static lit     clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1);                        }
+
+//=================================================================================================
+// Simple helpers:
+
+static inline int     sat_solver_dlevel(sat_solver* s)            { return veci_size(&s->trail_lim); }
+static inline vecp*   sat_solver_read_wlist(sat_solver* s, lit l) { return &s->wlists[l]; }
+static inline void    vecp_remove(vecp* v, void* e)
+{
+    void** ws = vecp_begin(v);
+    int    j  = 0;
+    for (; ws[j] != e  ; j++);
+    assert(j < vecp_size(v));
+    for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1];
+    vecp_resize(v,vecp_size(v)-1);
+}
+
+//=================================================================================================
+// Variable order functions:
+
+static inline void order_update(sat_solver* s, int v) // updateorder
+{
+    int*    orderpos = s->orderpos;
+    double* activity = s->activity;
+    int*    heap     = veci_begin(&s->order);
+    int     i        = orderpos[v];
+    int     x        = heap[i];
+    int     parent   = (i - 1) / 2;
+
+    assert(s->orderpos[v] != -1);
+
+    while (i != 0 && activity[x] > activity[heap[parent]]){
+        heap[i]           = heap[parent];
+        orderpos[heap[i]] = i;
+        i                 = parent;
+        parent            = (i - 1) / 2;
+    }
+    heap[i]     = x;
+    orderpos[x] = i;
+}
+
+static inline void order_assigned(sat_solver* s, int v) 
+{
+}
+
+static inline void order_unassigned(sat_solver* s, int v) // undoorder
+{
+    int* orderpos = s->orderpos;
+    if (orderpos[v] == -1){
+        orderpos[v] = veci_size(&s->order);
+        veci_push(&s->order,v);
+        order_update(s,v);
+    }
+}
+
+static int  order_select(sat_solver* s, float random_var_freq) // selectvar
+{
+    int*    heap;
+    double* activity;
+    int*    orderpos;
+
+    lbool* values = s->assigns;
+
+    // Random decision:
+    if (drand(&s->random_seed) < random_var_freq){
+        int next = irand(&s->random_seed,s->size);
+        assert(next >= 0 && next < s->size);
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    // Activity based decision:
+
+    heap     = veci_begin(&s->order);
+    activity = s->activity;
+    orderpos = s->orderpos;
+
+
+    while (veci_size(&s->order) > 0){
+        int    next  = heap[0];
+        int    size  = veci_size(&s->order)-1;
+        int    x     = heap[size];
+
+        veci_resize(&s->order,size);
+
+        orderpos[next] = -1;
+
+        if (size > 0){
+            double act   = activity[x];
+
+            int    i     = 0;
+            int    child = 1;
+
+
+            while (child < size){
+                if (child+1 < size && activity[heap[child]] < activity[heap[child+1]])
+                    child++;
+
+                assert(child < size);
+
+                if (act >= activity[heap[child]])
+                    break;
+
+                heap[i]           = heap[child];
+                orderpos[heap[i]] = i;
+                i                 = child;
+                child             = 2 * child + 1;
+            }
+            heap[i]           = x;
+            orderpos[heap[i]] = i;
+        }
+
+        if (values[next] == l_Undef)
+            return next;
+    }
+
+    return var_Undef;
+}
+
+//=================================================================================================
+// Activity functions:
+
+static inline void act_var_rescale(sat_solver* s) {
+    double* activity = s->activity;
+    int i;
+    for (i = 0; i < s->size; i++)
+        activity[i] *= 1e-100;
+    s->var_inc *= 1e-100;
+}
+
+static inline void act_var_bump(sat_solver* s, int v) {
+    double* activity = s->activity;
+    if ((activity[v] += s->var_inc) > 1e100)
+        act_var_rescale(s);
+
+    //printf("bump %d %f\n", v-1, activity[v]);
+
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+
+}
+
+static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
+
+static inline void act_clause_rescale(sat_solver* s) {
+    clause** cs = (clause**)vecp_begin(&s->learnts);
+    int i;
+    for (i = 0; i < vecp_size(&s->learnts); i++){
+        float a = clause_activity(cs[i]);
+        clause_setactivity(cs[i], a * (float)1e-20);
+    }
+    s->cla_inc *= (float)1e-20;
+}
+
+
+static inline void act_clause_bump(sat_solver* s, clause *c) {
+    float a = clause_activity(c) + s->cla_inc;
+    clause_setactivity(c,a);
+    if (a > 1e20) act_clause_rescale(s);
+}
+
+static inline void act_clause_decay(sat_solver* s) { s->cla_inc *= s->cla_decay; }
+
+
+//=================================================================================================
+// Clause functions:
+
+/* pre: size > 1 && no variable occurs twice
+ */
+static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt)
+{
+    int size;
+    clause* c;
+    int i;
+
+    assert(end - begin > 1);
+    assert(learnt >= 0 && learnt < 2);
+    size           = end - begin;
+    c              = (clause*)malloc(sizeof(clause) + sizeof(lit) * size + learnt * sizeof(float));
+    c->size_learnt = (size << 1) | learnt;
+    assert(((unsigned int)c & 1) == 0);
+
+    for (i = 0; i < size; i++)
+        c->lits[i] = begin[i];
+
+    if (learnt)
+        *((float*)&c->lits[size]) = 0.0;
+
+    assert(begin[0] >= 0);
+    assert(begin[0] < s->size*2);
+    assert(begin[1] >= 0);
+    assert(begin[1] < s->size*2);
+
+    assert(lit_neg(begin[0]) < s->size*2);
+    assert(lit_neg(begin[1]) < s->size*2);
+
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c);
+    //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c);
+
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1])));
+    vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0])));
+
+    return c;
+}
+
+
+static void clause_remove(sat_solver* s, clause* c)
+{
+    lit* lits = clause_begin(c);
+    assert(lit_neg(lits[0]) < s->size*2);
+    assert(lit_neg(lits[1]) < s->size*2);
+
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c);
+    //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c);
+
+    assert(lits[0] < s->size*2);
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1])));
+    vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0])));
+
+    if (clause_learnt(c)){
+        s->stats.learnts--;
+        s->stats.learnts_literals -= clause_size(c);
+    }else{
+        s->stats.clauses--;
+        s->stats.clauses_literals -= clause_size(c);
+    }
+
+    free(c);
+}
+
+
+static lbool clause_simplify(sat_solver* s, clause* c)
+{
+    lit*   lits   = clause_begin(c);
+    lbool* values = s->assigns;
+    int i;
+
+    assert(sat_solver_dlevel(s) == 0);
+
+    for (i = 0; i < clause_size(c); i++){
+        lbool sig = !lit_sign(lits[i]); sig += sig - 1;
+        if (values[lit_var(lits[i])] == sig)
+            return l_True;
+    }
+    return l_False;
+}
+
+//=================================================================================================
+// Minor (solver) functions:
+
+void sat_solver_setnvars(sat_solver* s,int n)
+{
+    int var;
+
+    if (s->cap < n){
+
+        while (s->cap < n) s->cap = s->cap*2+1;
+
+        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
+        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
+        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
+        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
+        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
+        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
+        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
+        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
+    }
+
+    for (var = s->size; var < n; var++){
+        vecp_new(&s->wlists[2*var]);
+        vecp_new(&s->wlists[2*var+1]);
+        s->activity [var] = 0;
+        s->assigns  [var] = l_Undef;
+        s->orderpos [var] = veci_size(&s->order);
+        s->reasons  [var] = (clause*)0;
+        s->levels   [var] = 0;
+        s->tags     [var] = l_Undef;
+        
+        /* does not hold because variables enqueued at top level will not be reinserted in the heap
+           assert(veci_size(&s->order) == var); 
+         */
+        veci_push(&s->order,var);
+        order_update(s, var);
+    }
+
+    s->size = n > s->size ? n : s->size;
+}
+
+
+static inline bool enqueue(sat_solver* s, lit l, clause* from)
+{
+    lbool* values = s->assigns;
+    int    v      = lit_var(l);
+    lbool  val    = values[v];
+#ifdef VERBOSEDEBUG
+    printf(L_IND"enqueue("L_LIT")\n", L_ind, L_lit(l));
+#endif
+
+    lbool sig = !lit_sign(l); sig += sig - 1;
+    if (val != l_Undef){
+        return val == sig;
+    }else{
+        // New fact -- store it.
+#ifdef VERBOSEDEBUG
+        printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(l));
+#endif
+        int*     levels  = s->levels;
+        clause** reasons = s->reasons;
+
+        values [v] = sig;
+        levels [v] = sat_solver_dlevel(s);
+        reasons[v] = from;
+        s->trail[s->qtail++] = l;
+
+        order_assigned(s, v);
+        return true;
+    }
+}
+
+
+static inline void assume(sat_solver* s, lit l){
+    assert(s->qtail == s->qhead);
+    assert(s->assigns[lit_var(l)] == l_Undef);
+#ifdef VERBOSEDEBUG
+    printf(L_IND"assume("L_LIT")\n", L_ind, L_lit(l));
+#endif
+    veci_push(&s->trail_lim,s->qtail);
+    enqueue(s,l,(clause*)0);
+}
+
+
+static inline void sat_solver_canceluntil(sat_solver* s, int level) {
+    lit*     trail;   
+    lbool*   values;  
+    clause** reasons; 
+    int      bound;
+    int      c;
+    
+    if (sat_solver_dlevel(s) <= level)
+        return;
+
+    trail   = s->trail;
+    values  = s->assigns;
+    reasons = s->reasons;
+    bound   = (veci_begin(&s->trail_lim))[level];
+
+    for (c = s->qtail-1; c >= bound; c--) {
+        int     x  = lit_var(trail[c]);
+        values [x] = l_Undef;
+        reasons[x] = (clause*)0;
+    }
+
+    for (c = s->qhead-1; c >= bound; c--)
+        order_unassigned(s,lit_var(trail[c]));
+
+    s->qhead = s->qtail = bound;
+    veci_resize(&s->trail_lim,level);
+}
+
+static void sat_solver_record(sat_solver* s, veci* cls)
+{
+    lit*    begin = veci_begin(cls);
+    lit*    end   = begin + veci_size(cls);
+    clause* c     = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
+    enqueue(s,*begin,c);
+
+    assert(veci_size(cls) > 0);
+
+    if (c != 0) {
+        vecp_push(&s->learnts,c);
+        act_clause_bump(s,c);
+        s->stats.learnts++;
+        s->stats.learnts_literals += veci_size(cls);
+    }
+}
+
+
+static double sat_solver_progress(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    int*    levels = s->levels;
+    int     i;
+
+    double  progress = 0;
+    double  F        = 1.0 / s->size;
+    for (i = 0; i < s->size; i++)
+        if (values[i] != l_Undef)
+            progress += pow(F, levels[i]);
+    return progress / s->size;
+}
+
+//=================================================================================================
+// Major methods:
+
+static bool sat_solver_lit_removable(sat_solver* s, lit l, int minl)
+{
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      top     = veci_size(&s->tagged);
+
+    assert(lit_var(l) >= 0 && lit_var(l) < s->size);
+    assert(reasons[lit_var(l)] != 0);
+    veci_resize(&s->stack,0);
+    veci_push(&s->stack,lit_var(l));
+
+    while (veci_size(&s->stack) > 0){
+        clause* c;
+        int v = veci_begin(&s->stack)[veci_size(&s->stack)-1];
+        assert(v >= 0 && v < s->size);
+        veci_resize(&s->stack,veci_size(&s->stack)-1);
+        assert(reasons[v] != 0);
+        c    = reasons[v];
+
+        if (clause_is_lit(c)){
+            int v = lit_var(clause_read_lit(c));
+            if (tags[v] == l_Undef && levels[v] != 0){
+                if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+                    veci_push(&s->stack,v);
+                    tags[v] = l_True;
+                    veci_push(&s->tagged,v);
+                }else{
+                    int* tagged = veci_begin(&s->tagged);
+                    int j;
+                    for (j = top; j < veci_size(&s->tagged); j++)
+                        tags[tagged[j]] = l_Undef;
+                    veci_resize(&s->tagged,top);
+                    return false;
+                }
+            }
+        }else{
+            lit*    lits = clause_begin(c);
+            int     i, j;
+
+            for (i = 1; i < clause_size(c); i++){
+                int v = lit_var(lits[i]);
+                if (tags[v] == l_Undef && levels[v] != 0){
+                    if (reasons[v] != 0 && ((1 << (levels[v] & 31)) & minl)){
+
+                        veci_push(&s->stack,lit_var(lits[i]));
+                        tags[v] = l_True;
+                        veci_push(&s->tagged,v);
+                    }else{
+                        int* tagged = veci_begin(&s->tagged);
+                        for (j = top; j < veci_size(&s->tagged); j++)
+                            tags[tagged[j]] = l_Undef;
+                        veci_resize(&s->tagged,top);
+                        return false;
+                    }
+                }
+            }
+        }
+    }
+
+    return true;
+}
+
+static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt)
+{
+    lit*     trail   = s->trail;
+    lbool*   tags    = s->tags;
+    clause** reasons = s->reasons;
+    int*     levels  = s->levels;
+    int      cnt     = 0;
+    lit      p       = lit_Undef;
+    int      ind     = s->qtail-1;
+    lit*     lits;
+    int      i, j, minl;
+    int*     tagged;
+
+    veci_push(learnt,lit_Undef);
+
+    do{
+        assert(c != 0);
+
+        if (clause_is_lit(c)){
+            lit q = clause_read_lit(c);
+            assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+            if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                tags[lit_var(q)] = l_True;
+                veci_push(&s->tagged,lit_var(q));
+                act_var_bump(s,lit_var(q));
+                if (levels[lit_var(q)] == sat_solver_dlevel(s))
+                    cnt++;
+                else
+                    veci_push(learnt,q);
+            }
+        }else{
+
+            if (clause_learnt(c))
+                act_clause_bump(s,c);
+
+            lits = clause_begin(c);
+            //printlits(lits,lits+clause_size(c)); printf("\n");
+            for (j = (p == lit_Undef ? 0 : 1); j < clause_size(c); j++){
+                lit q = lits[j];
+                assert(lit_var(q) >= 0 && lit_var(q) < s->size);
+                if (tags[lit_var(q)] == l_Undef && levels[lit_var(q)] > 0){
+                    tags[lit_var(q)] = l_True;
+                    veci_push(&s->tagged,lit_var(q));
+                    act_var_bump(s,lit_var(q));
+                    if (levels[lit_var(q)] == sat_solver_dlevel(s))
+                        cnt++;
+                    else
+                        veci_push(learnt,q);
+                }
+            }
+        }
+
+        while (tags[lit_var(trail[ind--])] == l_Undef);
+
+        p = trail[ind+1];
+        c = reasons[lit_var(p)];
+        cnt--;
+
+    }while (cnt > 0);
+
+    *veci_begin(learnt) = lit_neg(p);
+
+    lits = veci_begin(learnt);
+    minl = 0;
+    for (i = 1; i < veci_size(learnt); i++){
+        int lev = levels[lit_var(lits[i])];
+        minl    |= 1 << (lev & 31);
+    }
+
+    // simplify (full)
+    for (i = j = 1; i < veci_size(learnt); i++){
+        if (reasons[lit_var(lits[i])] == 0 || !sat_solver_lit_removable(s,lits[i],minl))
+            lits[j++] = lits[i];
+    }
+
+    // update size of learnt + statistics
+    s->stats.max_literals += veci_size(learnt);
+    veci_resize(learnt,j);
+    s->stats.tot_literals += j;
+
+    // clear tags
+    tagged = veci_begin(&s->tagged);
+    for (i = 0; i < veci_size(&s->tagged); i++)
+        tags[tagged[i]] = l_Undef;
+    veci_resize(&s->tagged,0);
+
+#ifdef DEBUG
+    for (i = 0; i < s->size; i++)
+        assert(tags[i] == l_Undef);
+#endif
+
+#ifdef VERBOSEDEBUG
+    printf(L_IND"Learnt {", L_ind);
+    for (i = 0; i < veci_size(learnt); i++) printf(" "L_LIT, L_lit(lits[i]));
+#endif
+    if (veci_size(learnt) > 1){
+        int max_i = 1;
+        int max   = levels[lit_var(lits[1])];
+        lit tmp;
+
+        for (i = 2; i < veci_size(learnt); i++)
+            if (levels[lit_var(lits[i])] > max){
+                max   = levels[lit_var(lits[i])];
+                max_i = i;
+            }
+
+        tmp         = lits[1];
+        lits[1]     = lits[max_i];
+        lits[max_i] = tmp;
+    }
+#ifdef VERBOSEDEBUG
+    {
+        int lev = veci_size(learnt) > 1 ? levels[lit_var(lits[1])] : 0;
+        printf(" } at level %d\n", lev);
+    }
+#endif
+}
+
+
+clause* sat_solver_propagate(sat_solver* s)
+{
+    lbool*  values = s->assigns;
+    clause* confl  = (clause*)0;
+    lit*    lits;
+
+    //printf("sat_solver_propagate\n");
+    while (confl == 0 && s->qtail - s->qhead > 0){
+        lit  p  = s->trail[s->qhead++];
+        vecp* ws = sat_solver_read_wlist(s,p);
+        clause **begin = (clause**)vecp_begin(ws);
+        clause **end   = begin + vecp_size(ws);
+        clause **i, **j;
+
+        s->stats.propagations++;
+        s->simpdb_props--;
+
+        //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p));
+        for (i = j = begin; i < end; ){
+            if (clause_is_lit(*i)){
+                *j++ = *i;
+                if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){
+                    confl = s->binary;
+                    (clause_begin(confl))[1] = lit_neg(p);
+                    (clause_begin(confl))[0] = clause_read_lit(*i++);
+
+                    // Copy the remaining watches:
+                    while (i < end)
+                        *j++ = *i++;
+                }
+            }else{
+                lit false_lit;
+                lbool sig;
+
+                lits = clause_begin(*i);
+
+                // Make sure the false literal is data[1]:
+                false_lit = lit_neg(p);
+                if (lits[0] == false_lit){
+                    lits[0] = lits[1];
+                    lits[1] = false_lit;
+                }
+                assert(lits[1] == false_lit);
+                //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n");
+
+                // If 0th watch is true, then clause is already satisfied.
+                sig = !lit_sign(lits[0]); sig += sig - 1;
+                if (values[lit_var(lits[0])] == sig){
+                    *j++ = *i;
+                }else{
+                    // Look for new watch:
+                    lit* stop = lits + clause_size(*i);
+                    lit* k;
+                    for (k = lits + 2; k < stop; k++){
+                        lbool sig = lit_sign(*k); sig += sig - 1;
+                        if (values[lit_var(*k)] != sig){
+                            lits[1] = *k;
+                            *k = false_lit;
+                            vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i);
+                            goto next; }
+                    }
+
+                    *j++ = *i;
+                    // Clause is unit under assignment:
+                    if (!enqueue(s,lits[0], *i)){
+                        confl = *i++;
+                        // Copy the remaining watches:
+                        while (i < end)
+                            *j++ = *i++;
+                    }
+                }
+            }
+        next:
+            i++;
+        }
+
+        s->stats.inspects += j - (clause**)vecp_begin(ws);
+        vecp_resize(ws,j - (clause**)vecp_begin(ws));
+    }
+
+    return confl;
+}
+
+static inline int clause_cmp (const void* x, const void* y) {
+    return clause_size((clause*)x) > 2 && (clause_size((clause*)y) == 2 || clause_activity((clause*)x) < clause_activity((clause*)y)) ? -1 : 1; }
+
+void sat_solver_reducedb(sat_solver* s)
+{
+    int      i, j;
+    double   extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity
+    clause** learnts = (clause**)vecp_begin(&s->learnts);
+    clause** reasons = s->reasons;
+
+    sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp);
+
+    for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i])
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+    for (; i < vecp_size(&s->learnts); i++){
+        if (clause_size(learnts[i]) > 2 && reasons[lit_var(*clause_begin(learnts[i]))] != learnts[i] && clause_activity(learnts[i]) < extra_lim)
+            clause_remove(s,learnts[i]);
+        else
+            learnts[j++] = learnts[i];
+    }
+
+    //printf("reducedb deleted %d\n", vecp_size(&s->learnts) - j);
+
+
+    vecp_resize(&s->learnts,j);
+}
+
+static lbool sat_solver_search(sat_solver* s, int nof_conflicts, int nof_learnts)
+{
+    int*    levels          = s->levels;
+    double  var_decay       = 0.95;
+    double  clause_decay    = 0.999;
+    double  random_var_freq = 0.02;
+
+    int     conflictC       = 0;
+    veci    learnt_clause;
+
+    assert(s->root_level == sat_solver_dlevel(s));
+
+    s->stats.starts++;
+    s->var_decay = (float)(1 / var_decay   );
+    s->cla_decay = (float)(1 / clause_decay);
+    veci_resize(&s->model,0);
+    veci_new(&learnt_clause);
+
+    for (;;){
+        clause* confl = sat_solver_propagate(s);
+        if (confl != 0){
+            // CONFLICT
+            int blevel;
+
+#ifdef VERBOSEDEBUG
+            printf(L_IND"**CONFLICT**\n", L_ind);
+#endif
+            s->stats.conflicts++; conflictC++;
+            if (sat_solver_dlevel(s) == s->root_level){
+                veci_delete(&learnt_clause);
+                return l_False;
+            }
+
+            veci_resize(&learnt_clause,0);
+            sat_solver_analyze(s, confl, &learnt_clause);
+            blevel = veci_size(&learnt_clause) > 1 ? levels[lit_var(veci_begin(&learnt_clause)[1])] : s->root_level;
+            blevel = s->root_level > blevel ? s->root_level : blevel;
+            sat_solver_canceluntil(s,blevel);
+            sat_solver_record(s,&learnt_clause);
+            act_var_decay(s);
+            act_clause_decay(s);
+
+        }else{
+            // NO CONFLICT
+            int next;
+
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
+                // Reached bound on number of conflicts:
+                s->progress_estimate = sat_solver_progress(s);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+                return l_Undef; }
+
+            if (sat_solver_dlevel(s) == 0)
+                // Simplify the set of problem clauses:
+                sat_solver_simplify(s);
+
+            if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts)
+                // Reduce the set of learnt clauses:
+                sat_solver_reducedb(s);
+
+            // New variable decision:
+            s->stats.decisions++;
+            next = order_select(s,(float)random_var_freq);
+
+            if (next == var_Undef){
+                // Model found:
+                lbool* values = s->assigns;
+                int i;
+                veci_resize(&s->model, 0);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&s->model,(int)values[i]);
+                sat_solver_canceluntil(s,s->root_level);
+                veci_delete(&learnt_clause);
+
+                /*
+                veci apa; veci_new(&apa);
+                for (i = 0; i < s->size; i++) 
+                    veci_push(&apa,(int)(s->model.ptr[i] == l_True ? toLit(i) : lit_neg(toLit(i))));
+                printf("model: "); printlits((lit*)apa.ptr, (lit*)apa.ptr + veci_size(&apa)); printf("\n");
+                veci_delete(&apa);
+                */
+
+                return l_True;
+            }
+
+            assume(s,lit_neg(toLit(next)));
+        }
+    }
+
+    return l_Undef; // cannot happen
+}
+
+//=================================================================================================
+// External solver functions:
+
+sat_solver* sat_solver_new(void)
+{
+    sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
+    memset( s, 0, sizeof(sat_solver) );
+
+    // initialize vectors
+    vecp_new(&s->clauses);
+    vecp_new(&s->learnts);
+    veci_new(&s->order);
+    veci_new(&s->trail_lim);
+    veci_new(&s->tagged);
+    veci_new(&s->stack);
+    veci_new(&s->model);
+
+    // initialize arrays
+    s->wlists    = 0;
+    s->activity  = 0;
+    s->assigns   = 0;
+    s->orderpos  = 0;
+    s->reasons   = 0;
+    s->levels    = 0;
+    s->tags      = 0;
+    s->trail     = 0;
+
+
+    // initialize other vars
+    s->size                   = 0;
+    s->cap                    = 0;
+    s->qhead                  = 0;
+    s->qtail                  = 0;
+    s->cla_inc                = 1;
+    s->cla_decay              = 1;
+    s->var_inc                = 1;
+    s->var_decay              = 1;
+    s->root_level             = 0;
+    s->simpdb_assigns         = 0;
+    s->simpdb_props           = 0;
+    s->random_seed            = 91648253;
+    s->progress_estimate      = 0;
+    s->binary                 = (clause*)malloc(sizeof(clause) + sizeof(lit)*2);
+    s->binary->size_learnt    = (2 << 1);
+    s->verbosity              = 0;
+
+    s->stats.starts           = 0;
+    s->stats.decisions        = 0;
+    s->stats.propagations     = 0;
+    s->stats.inspects         = 0;
+    s->stats.conflicts        = 0;
+    s->stats.clauses          = 0;
+    s->stats.clauses_literals = 0;
+    s->stats.learnts          = 0;
+    s->stats.learnts_literals = 0;
+    s->stats.max_literals     = 0;
+    s->stats.tot_literals     = 0;
+
+    return s;
+}
+
+
+void sat_solver_delete(sat_solver* s)
+{
+    int i;
+    for (i = 0; i < vecp_size(&s->clauses); i++)
+        free(vecp_begin(&s->clauses)[i]);
+
+    for (i = 0; i < vecp_size(&s->learnts); i++)
+        free(vecp_begin(&s->learnts)[i]);
+
+    // delete vectors
+    vecp_delete(&s->clauses);
+    vecp_delete(&s->learnts);
+    veci_delete(&s->order);
+    veci_delete(&s->trail_lim);
+    veci_delete(&s->tagged);
+    veci_delete(&s->stack);
+    veci_delete(&s->model);
+    free(s->binary);
+
+    // delete arrays
+    if (s->wlists != 0){
+        int i;
+        for (i = 0; i < s->size*2; i++)
+            vecp_delete(&s->wlists[i]);
+
+        // if one is different from null, all are
+        free(s->wlists);
+        free(s->activity );
+        free(s->assigns  );
+        free(s->orderpos );
+        free(s->reasons  );
+        free(s->levels   );
+        free(s->trail    );
+        free(s->tags     );
+    }
+
+    free(s);
+}
+
+
+bool sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
+{
+    lit *i,*j;
+    int maxvar;
+    lbool* values;
+    lit last;
+
+    if (begin == end) return false;
+
+    //printlits(begin,end); printf("\n");
+    // insertion sort
+    maxvar = lit_var(*begin);
+    for (i = begin + 1; i < end; i++){
+        lit l = *i;
+        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
+        for (j = i; j > begin && *(j-1) > l; j--)
+            *j = *(j-1);
+        *j = l;
+    }
+    sat_solver_setnvars(s,maxvar+1);
+
+    //printlits(begin,end); printf("\n");
+    values = s->assigns;
+
+    // delete duplicates
+    last = lit_Undef;
+    for (i = j = begin; i < end; i++){
+        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
+        lbool sig = !lit_sign(*i); sig += sig - 1;
+        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
+            return true;   // tautology
+        else if (*i != last && values[lit_var(*i)] == l_Undef)
+            last = *j++ = *i;
+    }
+
+    //printf("final: "); printlits(begin,j); printf("\n");
+
+    if (j == begin)          // empty clause
+        return false;
+    else if (j - begin == 1) // unit clause
+        return enqueue(s,*begin,(clause*)0);
+
+    // create new clause
+    vecp_push(&s->clauses,clause_new(s,begin,j,0));
+
+
+    s->stats.clauses++;
+    s->stats.clauses_literals += j - begin;
+
+    return true;
+}
+
+
+bool sat_solver_simplify(sat_solver* s)
+{
+    clause** reasons;
+    int type;
+
+    assert(sat_solver_dlevel(s) == 0);
+
+    if (sat_solver_propagate(s) != 0)
+        return false;
+
+    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
+        return true;
+
+    reasons = s->reasons;
+    for (type = 0; type < 2; type++){
+        vecp*    cs  = type ? &s->learnts : &s->clauses;
+        clause** cls = (clause**)vecp_begin(cs);
+
+        int i, j;
+        for (j = i = 0; i < vecp_size(cs); i++){
+            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
+                clause_simplify(s,cls[i]) == l_True)
+                clause_remove(s,cls[i]);
+            else
+                cls[j++] = cls[i];
+        }
+        vecp_resize(cs,j);
+    }
+
+    s->simpdb_assigns = s->qhead;
+    // (shouldn't depend on 'stats' really, but it will do for now)
+    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);
+
+    return true;
+}
+
+
+int sat_solver_solve(sat_solver* s, lit* begin, lit* end)
+{
+    double  nof_conflicts = 100;
+    double  nof_learnts   = sat_solver_nclauses(s) / 3;
+    lbool   status        = l_Undef;
+    lbool*  values        = s->assigns;
+    lit*    i;
+    
+    //printf("solve: "); printlits(begin, end); printf("\n");
+    for (i = begin; i < end; i++){
+        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
+        case 1: /* l_True: */
+            break;
+        case 0: /* l_Undef */
+            assume(s, *i);
+            if (sat_solver_propagate(s) == NULL)
+                break;
+            // falltrough
+        case -1: /* l_False */
+            sat_solver_canceluntil(s, 0);
+            return l_False;
+        }
+    }
+
+    s->root_level = sat_solver_dlevel(s);
+
+    if (s->verbosity >= 1){
+        printf("==================================[MINISAT]===================================\n");
+        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
+        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
+        printf("==============================================================================\n");
+    }
+
+    while (status == l_Undef){
+        double Ratio = (s->stats.learnts == 0)? 0.0 :
+            s->stats.learnts_literals / (double)s->stats.learnts;
+
+        if (s->verbosity >= 1){
+            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
+                (double)s->stats.conflicts,
+                (double)s->stats.clauses, 
+                (double)s->stats.clauses_literals,
+                (double)nof_learnts, 
+                (double)s->stats.learnts, 
+                (double)s->stats.learnts_literals,
+                Ratio,
+                s->progress_estimate*100);
+            fflush(stdout);
+        }
+        status = sat_solver_search(s,(int)nof_conflicts, (int)nof_learnts);
+        nof_conflicts *= 1.5;
+        nof_learnts   *= 1.1;
+    }
+    if (s->verbosity >= 1)
+        printf("==============================================================================\n");
+
+    sat_solver_canceluntil(s,0);
+    return status;
+}
+
+
+int sat_solver_nvars(sat_solver* s)
+{
+    return s->size;
+}
+
+
+int sat_solver_nclauses(sat_solver* s)
+{
+    return vecp_size(&s->clauses);
+}
+
+
+int sat_solver_nconflicts(sat_solver* s)
+{
+    return (int)s->stats.conflicts;
+}
+
+//=================================================================================================
+// Sorting functions (sigh):
+
+static inline void selectionsort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    int     i, j, best_i;
+    void*   tmp;
+
+    for (i = 0; i < size-1; i++){
+        best_i = i;
+        for (j = i+1; j < size; j++){
+            if (comp(array[j], array[best_i]) < 0)
+                best_i = j;
+        }
+        tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp;
+    }
+}
+
+
+static void sortrnd(void** array, int size, int(*comp)(const void *, const void *), double* seed)
+{
+    if (size <= 15)
+        selectionsort(array, size, comp);
+
+    else{
+        void*       pivot = array[irand(seed, size)];
+        void*       tmp;
+        int         i = -1;
+        int         j = size;
+
+        for(;;){
+            do i++; while(comp(array[i], pivot)<0);
+            do j--; while(comp(pivot, array[j])<0);
+
+            if (i >= j) break;
+
+            tmp = array[i]; array[i] = array[j]; array[j] = tmp;
+        }
+
+        sortrnd(array    , i     , comp, seed);
+        sortrnd(&array[i], size-i, comp, seed);
+    }
+}
+
+void sat_solver_sort(void** array, int size, int(*comp)(const void *, const void *))
+{
+    double seed = 91648253;
+    sortrnd(array,size,comp,&seed);
+}

src/temp/ivy/satSolver.h

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satSolver_h
+#define satSolver_h
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+#include "satVec.h"
+
+//=================================================================================================
+// Simple types:
+
+// does not work for c++
+typedef int  bool;
+static const bool  true      = 1;
+static const bool  false     = 0;
+
+typedef int                lit;
+typedef char               lbool;
+
+#ifdef _WIN32
+typedef signed __int64     sint64;   // compatible with MS VS 6.0
+#else
+typedef long long          sint64;
+#endif
+
+static const int   var_Undef = -1;
+static const lit   lit_Undef = -2;
+
+static const lbool l_Undef   =  0;
+static const lbool l_True    =  1;
+static const lbool l_False   = -1;
+
+static inline lit  toLit    (int v)        { return v + v; }
+static inline lit  toLitCond(int v, int c) { return v + v + (c != 0); }
+static inline lit  lit_neg  (lit l)        { return l ^ 1; }
+static inline int  lit_var  (lit l)        { return l >> 1; }
+static inline int  lit_sign (lit l)        { return l & 1; }
+
+
+//=================================================================================================
+// Public interface:
+
+struct sat_solver_t;
+typedef struct sat_solver_t sat_solver;
+
+extern sat_solver* sat_solver_new(void);
+extern void        sat_solver_delete(sat_solver* s);
+
+extern bool        sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
+extern bool        sat_solver_simplify(sat_solver* s);
+extern int         sat_solver_solve(sat_solver* s, lit* begin, lit* end);
+
+extern int         sat_solver_nvars(sat_solver* s);
+extern int         sat_solver_nclauses(sat_solver* s);
+extern int         sat_solver_nconflicts(sat_solver* s);
+
+extern void        sat_solver_setnvars(sat_solver* s,int n);
+
+struct stats_t
+{
+    sint64   starts, decisions, propagations, inspects, conflicts;
+    sint64   clauses, clauses_literals, learnts, learnts_literals, max_literals, tot_literals;
+};
+typedef struct stats_t stats;
+
+extern void        Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars );
+extern void        Sat_SolverPrintStats( FILE * pFile, sat_solver * p );
+
+//=================================================================================================
+// Solver representation:
+
+struct clause_t;
+typedef struct clause_t clause;
+
+struct sat_solver_t
+{
+    int      size;          // nof variables
+    int      cap;           // size of varmaps
+    int      qhead;         // Head index of queue.
+    int      qtail;         // Tail index of queue.
+
+    // clauses
+    vecp     clauses;       // List of problem constraints. (contains: clause*)
+    vecp     learnts;       // List of learnt clauses. (contains: clause*)
+
+    // activities
+    double   var_inc;       // Amount to bump next variable with.
+    double   var_decay;     // INVERSE decay factor for variable activity: stores 1/decay. 
+    float    cla_inc;       // Amount to bump next clause with.
+    float    cla_decay;     // INVERSE decay factor for clause activity: stores 1/decay.
+
+    vecp*    wlists;        // 
+    double*  activity;      // A heuristic measurement of the activity of a variable.
+    lbool*   assigns;       // Current values of variables.
+    int*     orderpos;      // Index in variable order.
+    clause** reasons;       //
+    int*     levels;        //
+    lit*     trail;
+
+    clause*  binary;        // A temporary binary clause
+    lbool*   tags;          //
+    veci     tagged;        // (contains: var)
+    veci     stack;         // (contains: var)
+
+    veci     order;         // Variable order. (heap) (contains: var)
+    veci     trail_lim;     // Separator indices for different decision levels in 'trail'. (contains: int)
+    veci     model;         // If problem is solved, this vector contains the model (contains: lbool).
+
+    int      root_level;    // Level of first proper decision.
+    int      simpdb_assigns;// Number of top-level assignments at last 'simplifyDB()'.
+    int      simpdb_props;  // Number of propagations before next 'simplifyDB()'.
+    double   random_seed;
+    double   progress_estimate;
+    int      verbosity;     // Verbosity level. 0=silent, 1=some progress report, 2=everything
+
+    stats    stats;
+};
+
+#endif

src/temp/ivy/satUtil.c

+/**CFile****************************************************************
+
+  FileName    [satUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [C-language MiniSat solver.]
+
+  Synopsis    [Additional SAT solver procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: satUtil.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <assert.h>
+#include "satSolver.h"
+#include "extra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct clause_t
+{
+    int size_learnt;
+    lit lits[0];
+};
+
+static inline int  clause_size( clause* c )  { return c->size_learnt >> 1; }
+static inline lit* clause_begin( clause* c ) { return c->lits;             }
+
+static void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Write the clauses in the solver into a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverWriteDimacs( sat_solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
+{
+    FILE * pFile;
+    void ** pClauses;
+    int nClauses, i;
+
+    // count the number of clauses
+    nClauses = p->clauses.size + p->learnts.size;
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            nClauses++;
+
+    // start the file
+    pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
+        return;
+    }
+    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
+    fprintf( pFile, "p cnf %d %d\n", p->size, nClauses );
+
+    // write the original clauses
+    nClauses = p->clauses.size;
+    pClauses = p->clauses.ptr;
+    for ( i = 0; i < nClauses; i++ )
+        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+    // write the learned clauses
+    nClauses = p->learnts.size;
+    pClauses = p->learnts.ptr;
+    for ( i = 0; i < nClauses; i++ )
+        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );
+
+    // write zero-level assertions
+    for ( i = 0; i < p->size; i++ )
+        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
+
+    fprintf( pFile, "\n" );
+    fclose( pFile );
+}   
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
+{
+    lit * pLits = clause_begin(pC);
+    int nLits = clause_size(pC);
+    int i;
+
+    for ( i = 0; i < nLits; i++ )
+        fprintf( pFile, "%s%d ", (lit_sign(pLits[i])? "-": ""),  lit_var(pLits[i]) + (int)(fIncrement>0) );
+    if ( fIncrement )
+        fprintf( pFile, "0" );
+    fprintf( pFile, "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Writes the given clause in a file in DIMACS format.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Sat_SolverPrintStats( FILE * pFile, sat_solver * p )
+{
+    printf( "starts        : %d\n", (int)p->stats.starts );
+    printf( "conflicts     : %d\n", (int)p->stats.conflicts );
+    printf( "decisions     : %d\n", (int)p->stats.decisions );
+    printf( "propagations  : %d\n", (int)p->stats.propagations );
+    printf( "inspects      : %d\n", (int)p->stats.inspects );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/temp/ivy/satVec.h

+/**************************************************************************************************
+MiniSat -- Copyright (c) 2005, Niklas Sorensson
+http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+// Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko
+
+#ifndef satVec_h
+#define satVec_h
+
+#include <stdlib.h>
+
+// vector of 32-bit intergers (added for 64-bit portability)
+struct veci_t {
+    int    size;
+    int    cap;
+    int*   ptr;
+};
+typedef struct veci_t veci;
+
+static inline void veci_new (veci* v) {
+    v->size = 0;
+    v->cap  = 4;
+    v->ptr  = (int*)malloc(sizeof(int)*v->cap);
+}
+
+static inline void   veci_delete (veci* v)          { free(v->ptr);   }
+static inline int*   veci_begin  (veci* v)          { return v->ptr;  }
+static inline int    veci_size   (veci* v)          { return v->size; }
+static inline void   veci_resize (veci* v, int k)   { v->size = k;    } // only safe to shrink !!
+static inline void   veci_push   (veci* v, int e)
+{
+    if (v->size == v->cap) {
+        int newsize = v->cap * 2+1;
+        v->ptr = (int*)realloc(v->ptr,sizeof(int)*newsize);
+        v->cap = newsize; }
+    v->ptr[v->size++] = e;
+}
+
+
+// vector of 32- or 64-bit pointers
+struct vecp_t {
+    int    size;
+    int    cap;
+    void** ptr;
+};
+typedef struct vecp_t vecp;
+
+static inline void vecp_new (vecp* v) {
+    v->size = 0;
+    v->cap  = 4;
+    v->ptr  = (void**)malloc(sizeof(void*)*v->cap);
+}
+
+static inline void   vecp_delete (vecp* v)          { free(v->ptr);   }
+static inline void** vecp_begin  (vecp* v)          { return v->ptr;  }
+static inline int    vecp_size   (vecp* v)          { return v->size; }
+static inline void   vecp_resize (vecp* v, int   k) { v->size = k;    } // only safe to shrink !!
+static inline void   vecp_push   (vecp* v, void* e)
+{
+    if (v->size == v->cap) {
+        int newsize = v->cap * 2+1;
+        v->ptr = (void**)realloc(v->ptr,sizeof(void*)*newsize);
+        v->cap = newsize; }
+    v->ptr[v->size++] = e;
+}
+
+
+#endif

src/temp/player/playerToAbc.c

@@ -91,6 +91,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
         Ivy_FastMapPerform( pMan, nLutMax );
         // convert from the extended AIG manager into an SOP network
         pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode );
+//        pNtkNew = NULL;
         Ivy_FastMapStop( pMan );
     }
     else
@@ -104,7 +105,7 @@ void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int f
     }
     Ivy_ManStop( pMan );
     // chech the resulting network
-    if ( !Abc_NtkCheck( pNtkNew ) )
+    if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) )
     {
         printf( "Abc_NtkPlayer: The network check has failed.\n" );
         Abc_NtkDelete( pNtkNew );