abc/src/sat/bsat/satSolver.c
// pushing one assumption to the stack of assumptions
pushing one assumption to the stack of assumptions
pushing one assumption to the stack of assumptions
int sat_solver_push(sat_solver* s, int p)
{
    assert(lit_var(p) < s->size);
    veci_push(&s->trail_lim,s->qtail);
    s->root_level++;
    if (!sat_solver_enqueue(s,p,0))
    {
        int h = s->reasons[lit_var(p)];
        if (h)
        {
            if (clause_is_lit(h))
            {
                (clause_begin(s->binary))[1] = lit_neg(p);
                (clause_begin(s->binary))[0] = clause_read_lit(h);
                h = s->hBinary;
            }
            sat_solver_analyze_final(s, h, 1);
            veci_push(&s->conf_final, lit_neg(p));
        }
        else
        {
            veci_resize(&s->conf_final,0);
            veci_push(&s->conf_final, lit_neg(p));
            if (var_level(s, lit_var(p)) > 0)
                veci_push(&s->conf_final, p);
        }
        return false; 
    }
    else
    {
        int fConfl = sat_solver_propagate(s);
        if (fConfl){
            sat_solver_analyze_final(s, fConfl, 0);
            return false; }
    }
    return true;
}
int sat_solver_push ( sat_solver * s , int p ) { assert ( lit_var ( p ) < s -> size ) ; veci_push ( & s -> trail_lim , s -> qtail ) ; s -> root_level ++ ; if ( ! sat_solver_enqueue ( s , p , 0 ) ) { int h = s -> reasons [ lit_var ( p ) ] ; if ( h ) { if ( clause_is_lit ( h ) ) { ( clause_begin ( s -> binary ) ) [ 1 ] = lit_neg ( p ) ; ( clause_begin ( s -> binary ) ) [ 0 ] = clause_read_lit ( h ) ; h = s -> hBinary ; } sat_solver_analyze_final ( s , h , 1 ) ; veci_push ( & s -> conf_final , lit_neg ( p ) ) ; } else { veci_resize ( & s -> conf_final , 0 ) ; veci_push ( & s -> conf_final , lit_neg ( p ) ) ; if ( var_level ( s , lit_var ( p ) ) > 0 ) veci_push ( & s -> conf_final , p ) ; } return false ; } else { int fConfl = sat_solver_propagate ( s ) ; if ( fConfl ) { sat_solver_analyze_final ( s , fConfl , 0 ) ; return false ; } } return true ; }
pushing one assumption to the stack of assumptions
pushing one assumption to the stack of assumptions
// the two lines below are a bug fix by Siert Wieringa  //sat_solver_canceluntil(s, 0); //assert(s->conf_final.size > 0); //sat_solver_canceluntil(s, 0);