Added test package (new files).

5 files changed, 85 insertions, 1 deletions

diff --git a/abclib.dsp b/abclib.dsp
index d98a8a91..f4d8fb96 100644
--- a/abclib.dsp
+++ b/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"
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 89d8cca3..c0c0d71e 100644
--- a/src/base/abci/abc.c
+++ b/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();
diff --git a/src/base/test/module.make b/src/base/test/module.make
new file mode 100644
index 00000000..45da1fb4
--- /dev/null
+++ b/src/base/test/module.make
@@ -0,0 +1 @@
+SRC +=    src/base/test/test.c
diff --git a/src/base/test/test.c b/src/base/test/test.c
new file mode 100644
index 00000000..f603befd
--- /dev/null
+++ b/src/base/test/test.c
@@ -0,0 +1,70 @@
+/**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
+
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1ad903c1..aa8c7f08 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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;