Added test package (new files).

abclib.dsp

@@ -674,6 +674,14 @@ SOURCE=.\src\base\ver\verParse.c
 SOURCE=.\src\base\ver\verStream.c
 # End Source File
 # End Group
+# Begin Group "test"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\test\test.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 

src/base/abci/abc.c

@@ -8706,9 +8706,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-
 */
 
+
 {
 //    extern void Au_Sat3DeriveImpls();
 //    Au_Sat3DeriveImpls();

src/base/test/module.make

+SRC +=    src/base/test/test.c

src/base/test/test.c

+/**CFile****************************************************************
+
+  FileName    [test.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Template package.]
+
+  Synopsis    []
+
+  Author      []
+  
+  Affiliation []
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: test.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "main.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Test_Init( Abc_Frame_t * pAbc )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Test_End( Abc_Frame_t * pAbc )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/sat/bsat/satSolver.c

@@ -1482,6 +1482,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
     }
 
     while (status == l_Undef){
+//        int nConfs = 0;
         double Ratio = (s->stats.learnts == 0)? 0.0 :
             s->stats.learnts_literals / (double)s->stats.learnts;
 
@@ -1500,7 +1501,11 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
         }
         nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
 //printf( "%d ", (int)nof_conflicts );
+//        nConfs = s->stats.conflicts;
         status = sat_solver_search(s, nof_conflicts, nof_learnts);
+//        if ( status == l_True )
+//            printf( "%d ", s->stats.conflicts - nConfs );
+
 //        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
         nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;