abc/src/sat/bsat/satSolver.c
// internal call to the SAT solver
internal call to the SAT solver
internal call to the SAT solver
int sat_solver_solve_internal(sat_solver* s)
{
    lbool status = l_Undef;
    int restart_iter = 0;
    veci_resize(&s->unit_lits, 0);
    s->nCalls++;
    if (s->verbosity >= 1){
        printf("==================================[MINISAT]===================================\n");
        printf("| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
        printf("|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
        printf("==============================================================================\n");
    }
    while (status == l_Undef){
        ABC_INT64_T nof_conflicts;
        double Ratio = (s->stats.learnts == 0)? 0.0 :
            s->stats.learnts_literals / (double)s->stats.learnts;
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if (s->verbosity >= 1)
        {
            printf("| %9.0f | %7.0f %8.0f | %7.0f %7.0f %8.0f %7.1f | %6.3f %% |\n", 
                (double)s->stats.conflicts,
                (double)s->stats.clauses, 
                (double)s->stats.clauses_literals,
                (double)0, 
                (double)s->stats.learnts, 
                (double)s->stats.learnts_literals,
                Ratio,
                s->progress_estimate*100);
            fflush(stdout);
        }
        nof_conflicts = (ABC_INT64_T)( 100 * luby(2, restart_iter++) );
        status = sat_solver_search(s, nof_conflicts);
        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
            break;
        if ( s->nInsLimit  && s->stats.propagations > s->nInsLimit )
            break;
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if ( s->pFuncStop && s->pFuncStop(s->RunId) )
            break;
    }
    if (s->verbosity >= 1)
        printf("==============================================================================\n");
    sat_solver_canceluntil(s,s->root_level);
    if ( status == l_True && s->user_vars.size )
    {
        int v;
        for ( v = 0; v < s->user_vars.size; v++ )
            veci_push(&s->user_values, sat_solver_var_value(s, s->user_vars.ptr[v]));
    }
    return status;
}
int sat_solver_solve_internal ( sat_solver * s ) { lbool status = l_Undef ; int restart_iter = 0 ; veci_resize ( & s -> unit_lits , 0 ) ; s -> nCalls ++ ; if ( s -> verbosity >= 1 ) { printf ( " \n " ) ; printf ( " \n " ) ; printf ( " \n " ) ; printf ( " \n " ) ; } while ( status == l_Undef ) { ABC_INT64_T nof_conflicts ; double Ratio = ( s -> stats . learnts == 0 ) ? 0.0 : s -> stats . learnts_literals / ( double ) s -> stats . learnts ; if ( s -> nRuntimeLimit && Abc_Clock ( ) > s -> nRuntimeLimit ) break ; if ( s -> verbosity >= 1 ) { printf ( " \n " , ( double ) s -> stats . conflicts , ( double ) s -> stats . clauses , ( double ) s -> stats . clauses_literals , ( double ) 0 , ( double ) s -> stats . learnts , ( double ) s -> stats . learnts_literals , Ratio , s -> progress_estimate * 100 ) ; fflush ( stdout ) ; } nof_conflicts = ( ABC_INT64_T ) ( 100 * luby ( 2 , restart_iter ++ ) ) ; status = sat_solver_search ( s , nof_conflicts ) ; if ( s -> nConfLimit && s -> stats . conflicts > s -> nConfLimit ) break ; if ( s -> nInsLimit && s -> stats . propagations > s -> nInsLimit ) break ; if ( s -> nRuntimeLimit && Abc_Clock ( ) > s -> nRuntimeLimit ) break ; if ( s -> pFuncStop && s -> pFuncStop ( s -> RunId ) ) break ; } if ( s -> verbosity >= 1 ) printf ( " \n " ) ; sat_solver_canceluntil ( s , s -> root_level ) ; if ( status == l_True && s -> user_vars . size ) { int v ; for ( v = 0 ; v < s -> user_vars . size ; v ++ ) veci_push ( & s -> user_values , sat_solver_var_value ( s , s -> user_vars . ptr [ v ] ) ) ; } return status ; }
internal call to the SAT solver
internal call to the SAT solver
// quit the loop if reached an external limit // save variable values