diff options
| -rw-r--r-- | src/base/abci/abcExact.c | 42 | ||||
| -rw-r--r-- | src/sat/satoko/solver.c | 2 | ||||
| -rw-r--r-- | src/sat/xsat/xsatSolver.c | 2 |
3 files changed, 42 insertions, 4 deletions
diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c index adb64d79..2fbf63dd 100644 --- a/src/base/abci/abcExact.c +++ b/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 ) diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c index 42bc6448..18d00ba2 100644 --- a/src/sat/satoko/solver.c +++ b/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) diff --git a/src/sat/xsat/xsatSolver.c b/src/sat/xsat/xsatSolver.c index 9807e1b7..4844ca1d 100644 --- a/src/sat/xsat/xsatSolver.c +++ b/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 ) |