Merged in msoeken/abc-exact (pull request #66)

Fixes in exact synthesis and small fix in xsat and satoko.

src/base/abci/abcExact.c

@@ -1195,7 +1195,7 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
 {
     extern int Extra_TruthVarsSymm( unsigned * pTruth, int nVars, int iVar0, int iVar1 );
 
-    int h, i, j, k, t, ii, jj, kk, p, q;
+    int h, i, j, k, t, ii, jj, kk, iii, p, q;
     int pLits[3];
     Vec_Int_t * vLits = NULL;
 
@@ -1419,6 +1419,18 @@ static int Ses_ManCreateClauses( Ses_Man_t * pSes )
                         pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, k, pSes->nSpecVars + i ), 1 );
                         sat_solver_addclause( pSes->pSat, pLits, pLits + 2 );
                     }
+    if ( pSes->nGates > 2 )
+        for ( i = 0; i < pSes->nGates - 2; ++i )
+            for ( ii = i + 1; ii < pSes->nGates - 1; ++ii )
+                for ( iii = ii + 1; iii < pSes->nGates; ++iii )
+                    for ( k = 1; k < pSes->nSpecVars + i; ++k )
+                        for ( j = 0; j < k; ++j )
+                            {
+                                pLits[0] = Abc_Var2Lit( Ses_ManSelectVar( pSes, i, j, k ), 1 );
+                                pLits[1] = Abc_Var2Lit( Ses_ManSelectVar( pSes, ii, j, k ), 1 );
+                                pLits[2] = Abc_Var2Lit( Ses_ManSelectVar( pSes, iii, i, ii ), 1 );
+                                sat_solver_addclause( pSes->pSat, pLits, pLits + 3 );
+                            }
 
     /* EXTRA clauses: co-lexicographic order */
     for ( i = 0; i < pSes->nGates - 1; ++i )
@@ -1595,6 +1607,9 @@ static inline int Ses_ManSolve( Ses_Man_t * pSes )
         pSes->timeSatUndef += timeDelta;
         if ( pSes->fSatVerbose )
         {
+            //Sat_SolverWriteDimacs( pSes->pSat, "/tmp/test.cnf", Vec_IntArray( pSes->vAssump ), Vec_IntLimit( pSes->vAssump ), 1 );
+            //exit( 42 );
+
             printf( "resource limit reached\n" );
         }
         return 2;
@@ -1906,7 +1921,7 @@ static inline void Ses_ManPrintFuncs( Ses_Man_t * pSes )
     for ( h = 0; h < pSes->nSpecFunc; ++h )
     {
         printf( "  func %d: ", h + 1 );
-        Abc_TtPrintHexRev( stdout, &pSes->pSpec[h >> 2], pSes->nSpecVars );
+        Abc_TtPrintHexRev( stdout, &pSes->pSpec[h << 2], pSes->nSpecVars );
         printf( "\n" );
     }
 
@@ -2342,6 +2357,29 @@ static char * Ses_ManFindMinimumSizeTopDown( Ses_Man_t * pSes, int nMinGates )
 static char * Ses_ManFindMinimumSize( Ses_Man_t * pSes )
 {
     char * pSol = NULL;
+    int i = pSes->nStartGates + 1, fRes;
+
+    /* if more than one function, no CEGAR */
+    if ( pSes->nSpecFunc > 1 )
+    {
+      while ( true )
+      {
+        if ( pSes->fVerbose )
+        {
+          printf( "try with %d gates\n", i );
+        }
+
+        memset( pSes->pTtValues, ~0, 4 * sizeof( word ) );
+        fRes = Ses_ManFindNetworkExact( pSes, i++ );
+        if ( fRes == 2 ) continue;
+        if ( fRes == 0 ) break;
+
+        pSol = Ses_ManExtractSolution( pSes );
+        break;
+      }
+
+      return pSol;
+    }
 
     /* do the arrival times allow for a network? */
     if ( pSes->nMaxDepth != -1 && pSes->pArrTimeProfile )

src/sat/satoko/solver.c

@@ -437,7 +437,7 @@ static inline void solver_reduce_cdb(solver_t *s)
 
     limit = (unsigned)(n_learnts * s->opts.learnt_ratio);
 
-    satoko_sort((void *)learnts_cls, n_learnts,
+    satoko_sort((void **)learnts_cls, n_learnts,
             (int (*)(const void *, const void *)) clause_compare);
 
     if (learnts_cls[n_learnts / 2]->lbd <= 3)

src/sat/xsat/xsatSolver.c

@@ -790,7 +790,7 @@ void xSAT_SolverReduceDB( xSAT_Solver_t * s )
 
     limit = nLearnedOld / 2;
 
-    xSAT_UtilSort((void *) learnts_cls, nLearnedOld,
+    xSAT_UtilSort((void **) learnts_cls, nLearnedOld,
                   (int (*)( const void *, const void * )) xSAT_ClauseCompare);
 
     if ( learnts_cls[nLearnedOld / 2]->nLBD <= 3 )