merge

10 files changed, 197 insertions, 26 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 003842f0..2efa041c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -61,6 +61,7 @@
 #include "bool/rpo/rpo.h"
 #include "map/mpm/mpm.h"
 #include "opt/fret/fretime.h"
+#include "opt/nwk/nwkMerge.h"
 
 #ifndef _WIN32
 #include <unistd.h>
@@ -124,7 +125,7 @@ static int Abc_CommandTrace                  ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandSpeedup                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPowerdown              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAddBuffs               ( Abc_Frame_t * pAbc, int argc, char ** argv );
-//static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMerge                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestDec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestNpn                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTestRPO                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -774,7 +775,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "speedup",       Abc_CommandSpeedup,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "powerdown",     Abc_CommandPowerdown,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "addbuffs",      Abc_CommandAddBuffs,         1 );
-//    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "merge",         Abc_CommandMerge,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testdec",       Abc_CommandTestDec,          0 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "testnpn",       Abc_CommandTestNpn,          0 );
     Cmd_CommandAdd( pAbc, "LogiCS",       "testrpo",       Abc_CommandTestRPO,          0 );
@@ -6011,7 +6012,7 @@ usage:
     return 1;
 }
 
-#if 0
+//#if 0
 /**Function*************************************************************
 
   Synopsis    []
@@ -6144,7 +6145,7 @@ usage:
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
 }
-#endif
+//#endif
 
 
 
diff --git a/src/map/scl/scl.c b/src/map/scl/scl.c
index 9d4653a7..27342458 100644
--- a/src/map/scl/scl.c
+++ b/src/map/scl/scl.c
@@ -1823,13 +1823,17 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     FILE * pFile;
     char * pFileName;
+    int fUseNewFormat = 0;
     int c, fVerbose = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'n':
+            fVerbose ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -1850,25 +1854,29 @@ int Scl_CommandReadConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     fclose( pFile );
-//    Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
 
-    if ( pNtk == NULL )
-    {
-        fprintf( pAbc->Err, "There is no current network.\n" );
-        return 1;
-    }
-
-    // input constraint manager
-    if ( pNtk )
+    if ( !fUseNewFormat )
+        Abc_SclReadTimingConstr( pAbc, pFileName, fVerbose );
+    else
     {
-        Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
-        if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
+        if ( pNtk == NULL )
+        {
+            fprintf( pAbc->Err, "There is no current network.\n" );
+            return 1;
+        }
+        // input constraint manager
+        if ( pNtk )
+        {
+            Scl_Con_t * pCon = Scl_ConRead( pFileName, Abc_NtkNameMan(pNtk, 0), Abc_NtkNameMan(pNtk, 1) );
+            if ( pCon ) Scl_ConUpdateMan( pAbc, pCon );
+        }
     }
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_constr [-vh] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_constr [-nvh] <file>\n" );
     fprintf( pAbc->Err, "\t         read file with timing constraints for standard-cell designs\n" );
+    fprintf( pAbc->Err, "\t-n     : toggle using new constraint file format [default = %s]\n", fUseNewFormat? "yes": "no" );
     fprintf( pAbc->Err, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\t<file> : the name of a file to read\n" );
diff --git a/src/map/scl/sclUtil.c b/src/map/scl/sclUtil.c
index 70140044..07e0deb6 100644
--- a/src/map/scl/sclUtil.c
+++ b/src/map/scl/sclUtil.c
@@ -254,21 +254,21 @@ void Abc_SclReadTimingConstr( Abc_Frame_t * pAbc, char * pFileName, int fVerbose
         pToken = strtok( Buffer, " \t\r\n" );
         if ( pToken == NULL )
             continue;
-//        if ( !strcmp(pToken, "set_driving_cell") )
-        if ( !strcmp(pToken, "default_input_cell") )
+        if ( !strcmp(pToken, "set_driving_cell") )
+//        if ( !strcmp(pToken, "default_input_cell") )
         {
             Abc_FrameSetDrivingCell( Abc_UtilStrsav(strtok(NULL, " \t\r\n")) );
             if ( fVerbose ) 
                 printf( "Setting driving cell to be \"%s\".\n", Abc_FrameReadDrivingCell() );
         }
-//        else if ( !strcmp(pToken, "set_load") )
-        else if ( !strcmp(pToken, "default_output_load") )
+        else if ( !strcmp(pToken, "set_load") )
+//        else if ( !strcmp(pToken, "default_output_load") )
         {
             Abc_FrameSetMaxLoad( atof(strtok(NULL, " \t\r\n")) );
             if ( fVerbose ) 
                 printf( "Setting driving cell to be %f.\n", Abc_FrameReadMaxLoad() );
         }
-//        else printf( "Unrecognized token \"%s\".\n", pToken );
+        else printf( "Unrecognized token \"%s\".\n", pToken );
     }
     fclose( pFile );
 }
diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
index 4d86d2ee..5c5b1f2b 100644
--- a/src/opt/sbd/sbd.c
+++ b/src/opt/sbd/sbd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "misc/vec/vecHsh.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
+{
+    int i, k, Entry = 0, Entry2, Count = 0, Below;
+    int Prev = Vec_IntEntry( vSet, 0 );
+    Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
+    {
+        assert( 2*Prev >= Entry );
+        if ( 2*Prev == Entry )
+        {
+            Prev = Entry;
+            continue;
+        }
+        Below = nVars; 
+        Vec_IntForEachEntryStart( vSet, Entry2, k, i )
+            Below += Entry2;
+        Count += Below * (2*Prev - 1);
+        Prev = Entry;
+    }
+    Count += nVars * 2*Prev;
+    return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
+}
+void Sbd_CountTopos()
+{
+    Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
+    Vec_Int_t * vSet = Vec_IntAlloc( 100 );
+    int i, k, e, Start, Stop;
+    Start = Hsh_VecManAdd( p, vSet );
+    for ( i = 1; i < 9; i++ )
+    {
+        Stop = Hsh_VecSize( p );
+        for ( e = Start; e < Stop; e++ )
+        {
+            Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+            Vec_IntClear( vSet );
+            Vec_IntAppend( vSet, vTemp );
+            for ( k = 0; k < Vec_IntSize(vSet); k++ )
+            {
+                // skip if the number of entries on this level is equal to the number of fanins on the previous level
+                if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
+                    continue;
+                Vec_IntAddToEntry( vSet, k, 1 );
+                Hsh_VecManAdd( p, vSet );
+                Vec_IntAddToEntry( vSet, k, -1 );
+            }
+            Vec_IntPush( vSet, 1 );
+            Hsh_VecManAdd( p, vSet );
+        }
+        printf( "%2d : This = %8d  All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
+        if ( 0 )
+        {
+            for ( e = Stop; e < Hsh_VecSize(p); e++ )
+            {
+                Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+                printf( "Params = %3d.  ", Sbd_CountConfigVars(vTemp, 5) );
+                Vec_IntPrint( vTemp );
+            }
+        }
+        Start = Stop;
+    }
+    Vec_IntFree( vSet );
+    Hsh_VecManStop( p );
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 97a8b644..5f8503a5 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1539,9 +1539,37 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
             pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
         if ( pPars->fDumpVabs || pPars->fDumpMabs )
-            Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
+            Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", 
                 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                 Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
+        if ( pPars->fDumpMabs )
+        {
+            {
+                char Command[1000];
+                Abc_FrameSetStatus( -1 );
+                Abc_FrameSetCex( NULL );
+                Abc_FrameSetNFrames( -1 );
+                sprintf( Command, "write_status %s", Extra_FileNameGenericAppend((char *)(p->pPars->pFileVabs ? p->pPars->pFileVabs : "glabs.aig"), ".status"));
+                Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
+            }
+            {
+                // create trivial abstraction map
+                Gia_Obj_t * pObj; 
+                char * pFileName = Ga2_GlaGetFileName(p, 0);
+                Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
+                pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+                Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+                Gia_ManForEachAnd( pAig, pObj, i )
+                    Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
+                Gia_ManForEachRo( pAig, pObj, i )
+                    Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
+                Gia_AigerWrite( pAig, pFileName, 0, 0 );
+                Vec_IntFree( pAig->vGateClasses );
+                pAig->vGateClasses = vMap;
+                if ( p->pPars->fVerbose )
+                    Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+            }
+        }
         Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
     }
     // iterate unrolling
diff --git a/src/sat/satoko/clause.h b/src/sat/satoko/clause.h
index 2be18cd6..9b05868b 100644
--- a/src/sat/satoko/clause.h
+++ b/src/sat/satoko/clause.h
@@ -59,5 +59,19 @@ static inline void clause_print(struct clause *clause)
     printf("}\n");
 }
 
+static inline void clause_dump(FILE *file, struct clause *clause, int no_zero_var) 
+{
+    unsigned i;
+    for (i = 0; i < clause->size; i++) {
+        int var = (clause->data[i].lit >> 1);
+        char pol = (clause->data[i].lit & 1);
+        fprintf(file, "%d ", pol ? -(var + no_zero_var) : (var + no_zero_var));
+    }
+    if (no_zero_var)
+        fprintf(file, "0\n");
+    else
+        fprintf(file, "\n");
+}
+
 ABC_NAMESPACE_HEADER_END
 #endif /* satoko__clause_h */
diff --git a/src/sat/satoko/cnf_reader.c b/src/sat/satoko/cnf_reader.c
index adb9a47b..8223affd 100644
--- a/src/sat/satoko/cnf_reader.c
+++ b/src/sat/satoko/cnf_reader.c
@@ -150,7 +150,7 @@ int satoko_parse_dimacs(char *fname, satoko_t **solver)
     vec_uint_free(lits);
     satoko_free(buffer);
     *solver = p;
-    return satoko_simplify(p);
+    return SATOKO_OK;
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index a0c4d216..6634e68e 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -60,6 +60,7 @@ struct satoko_opts {
     unsigned clause_min_lbd_bin_resol;
     float garbage_max_ratio;
     char verbose;
+    char no_simplify;
 };
 
 typedef struct satoko_stats satoko_stats_t;
@@ -108,6 +109,16 @@ extern void satoko_unbookmark(satoko_t *);
  */
 extern int satoko_final_conflict(satoko_t *, unsigned *);
 
+/* Procedure to dump a DIMACS file.
+ * - It receives as input the solver, a file name string and two integers.
+ * - If the file name string is NULL the solver will dump in stdout.
+ * - The first argument can be either 0 or 1 and is an option to dump learnt 
+ *   clauses. (value 1 will dump them).
+ * - The seccond argument can be either 0 or 1 and is an option to use 0 as a 
+ *   variable ID or not. Keep in mind that if 0 is used as an ID the generated
+ *   file will not be a DIMACS. (value 1 will use 0 as ID).
+ */
+extern void satoko_write_dimacs(satoko_t *, char *, int, int);
 extern satoko_stats_t satoko_stats(satoko_t *);
 
 ABC_NAMESPACE_HEADER_END
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index af3dcffb..42bc6448 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -644,7 +644,7 @@ char solver_search(solver_t *s)
                 solver_cancel_until(s, 0);
                 return SATOKO_UNDEC;
             }
-            if (solver_dlevel(s) == 0)
+            if (!s->opts.no_simplify && solver_dlevel(s) == 0)
                 satoko_simplify(s);
 
             /* Reduce the set of learnt clauses */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index 3cb9f3d3..dada33cc 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -152,6 +152,7 @@ void satoko_default_opts(satoko_opts_t *opts)
 {
     memset(opts, 0, sizeof(satoko_opts_t));
     opts->verbose = 0;
+    opts->no_simplify = 0;
     /* Limits */
     opts->conf_limit = 0;
     opts->prop_limit  = 0;
@@ -290,6 +291,10 @@ int satoko_solve(solver_t *s)
     //if (s->opts.verbose)
     //    print_opts(s);
 
+    if (!s->opts.no_simplify)
+        if (satoko_simplify(s) != SATOKO_OK)
+            return SATOKO_UNDEC;
+
     while (status == SATOKO_UNDEC) {
         status = solver_search(s);
         if (solver_check_limits(s) == 0)
@@ -297,6 +302,7 @@ int satoko_solve(solver_t *s)
     }
     if (s->opts.verbose)
         print_stats(s);
+    
     solver_cancel_until(s, vec_uint_size(s->assumptions));
     return status;
 }
@@ -309,7 +315,6 @@ int satoko_final_conflict(solver_t *s, unsigned *out)
     memcpy(out, vec_uint_data(s->final_conflict),
            sizeof(unsigned) * vec_uint_size(s->final_conflict));
     return vec_uint_size(s->final_conflict);
-
 }
 
 satoko_stats_t satoko_stats(satoko_t *s)
@@ -324,6 +329,7 @@ void satoko_bookmark(satoko_t *s)
     s->book_cl_lrnt = vec_uint_size(s->learnts);
     s->book_vars = vec_char_size(s->assigns);
     s->book_trail = vec_uint_size(s->trail);
+    s->opts.no_simplify = 1;
 }
 
 void satoko_unbookmark(satoko_t *s)
@@ -333,6 +339,7 @@ void satoko_unbookmark(satoko_t *s)
     s->book_cdb = 0;
     s->book_vars = 0;
     s->book_trail = 0;
+    s->opts.no_simplify = 0;
 }
 
 void satoko_reset(satoko_t *s)
@@ -442,4 +449,43 @@ void satoko_unmark_cone(satoko_t *s, int *pvars, int n_vars)
         var_clean_mark(s, pvars[i]);
 }
 
+void satoko_write_dimacs(satoko_t *s, char *fname, int wrt_lrnt, int zero_var)
+{
+    FILE *file;
+    unsigned i;
+    unsigned n_vars = vec_act_size(s->activity);
+    unsigned n_orig = vec_uint_size(s->originals) + vec_uint_size(s->assumptions);
+    unsigned n_lrnts = vec_uint_size(s->learnts);
+    unsigned *array;
+
+    assert(wrt_lrnt == 0 || wrt_lrnt == 1);
+    assert(zero_var == 0 || zero_var == 1);
+    if (fname != NULL)
+        file = fopen(fname, "w");
+    else
+        file = stdout;
+    
+    if (file == NULL) {
+        printf( "Error: Cannot open output file.\n");
+        return;
+    }
+    fprintf(file, "p cnf %d %d\n", n_vars, wrt_lrnt ? n_orig + n_lrnts : n_orig);
+    array = vec_uint_data(s->assumptions);
+    for (i = 0; i < vec_uint_size(s->assumptions); i++)
+        fprintf(file, "%d\n", array[i] & 1 ? -(array[i] + !zero_var) : array[i] + !zero_var);
+    
+    array = vec_uint_data(s->originals);
+    for (i = 0; i < vec_uint_size(s->originals); i++)
+        clause_dump(file, clause_read(s, array[i]), !zero_var);
+    
+    if (wrt_lrnt) {
+        printf(" Lertns %u", n_lrnts);
+        array = vec_uint_data(s->learnts);
+        for (i = 0; i < n_lrnts; i++)
+            clause_dump(file, clause_read(s, array[i]), !zero_var);
+    }
+
+}
+
+
 ABC_NAMESPACE_IMPL_END