satSolver.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satVec.h"
#include "satClause.h"
#include "misc/util/utilDouble.h"

Include dependency graph for satSolver.h:

Go to the source code of this file.

Classes
struct	sat_solver_t

Typedefs
typedef struct sat_solver_t	sat_solver
typedef struct varinfo_t	varinfo

Functions
sat_solver *	sat_solver_new (void)
sat_solver *	zsat_solver_new_seed (double seed)
void	sat_solver_delete (sat_solver *s)
int	sat_solver_addclause (sat_solver *s, lit *begin, lit *end)
int	sat_solver_clause_new (sat_solver *s, lit *begin, lit *end, int learnt)
int	sat_solver_simplify (sat_solver *s)
int	sat_solver_solve (sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
int	sat_solver_solve_internal (sat_solver *s)
int	sat_solver_solve_lexsat (sat_solver *s, int *pLits, int nLits)
int	sat_solver_minimize_assumptions (sat_solver *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver_minimize_assumptions2 (sat_solver *s, int *pLits, int nLits, int nConfLimit)
int	sat_solver_push (sat_solver *s, int p)
void	sat_solver_pop (sat_solver *s)
void	sat_solver_set_resource_limits (sat_solver *s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
void	sat_solver_restart (sat_solver *s)
void	zsat_solver_restart_seed (sat_solver *s, double seed)
void	sat_solver_rollback (sat_solver *s)
int	sat_solver_nvars (sat_solver *s)
int	sat_solver_nclauses (sat_solver *s)
int	sat_solver_nconflicts (sat_solver *s)
double	sat_solver_memory (sat_solver *s)
int	sat_solver_count_assigned (sat_solver *s)
int	sat_solver_addvar (sat_solver *s)
void	sat_solver_setnvars (sat_solver *s, int n)
int	sat_solver_get_var_value (sat_solver *s, int v)
void	sat_solver_set_var_activity (sat_solver *s, int *pVars, int nVars)
void	Sat_SolverWriteDimacs (sat_solver *p, char *pFileName, lit *assumptionsBegin, lit *assumptionsEnd, int incrementVars)
void	Sat_SolverPrintStats (FILE *pFile, sat_solver *p)
int *	Sat_SolverGetModel (sat_solver *p, int *pVars, int nVars)
void	Sat_SolverDoubleClauses (sat_solver *p, int iVar)
void	Sat_SolverTraceStart (sat_solver *pSat, char *pName)
	DECLARATIONS ///.
void	Sat_SolverTraceStop (sat_solver *pSat)
void	Sat_SolverTraceWrite (sat_solver *pSat, int *pBeg, int *pEnd, int fRoot)
void	sat_solver_store_alloc (sat_solver *s)
void	sat_solver_store_write (sat_solver *s, char *pFileName)
void	sat_solver_store_free (sat_solver *s)
void	sat_solver_store_mark_roots (sat_solver *s)
void	sat_solver_store_mark_clauses_a (sat_solver *s)
void *	sat_solver_store_release (sat_solver *s)

Typedef Documentation

sat_solver

typedef struct sat_solver_t sat_solver

Definition at line 41 of file satSolver.h.

varinfo

typedef struct varinfo_t varinfo

Definition at line 98 of file satSolver.h.

Function Documentation

sat_solver_addclause()

int sat_solver_addclause ( sat_solver * s, lit * begin, lit * end )

extern

Definition at line 1735 of file satSolver.c.

{
    lit *i,*j;
    int maxvar;
    lit last;
    assert( begin < end );
    if ( s->fPrintClause )
    {
        for ( i = begin; i < end; i++ )
            printf( "%s%d ", (*i)&1 ? "!":"", (*i)>>1 );
        printf( "\n" );
    }
 
    veci_resize( &s->temp_clause, 0 );
    for ( i = begin; i < end; i++ )
        veci_push( &s->temp_clause, *i );
    begin = veci_begin( &s->temp_clause );
    end = begin + veci_size( &s->temp_clause );
 
    // insertion sort
    maxvar = lit_var(*begin);
    for (i = begin + 1; i < end; i++){
        lit l = *i;
        maxvar = lit_var(l) > maxvar ? lit_var(l) : maxvar;
        for (j = i; j > begin && *(j-1) > l; j--)
            *j = *(j-1);
        *j = l;
    }
    sat_solver_setnvars(s,maxvar+1);

    // add clause to internal storage
    if ( s->pStore )
    {
        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, begin, end );
        assert( RetValue );
        (void) RetValue;
    }
 
    // delete duplicates
    last = lit_Undef;
    for (i = j = begin; i < end; i++){
        //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]));
        if (*i == lit_neg(last) || var_value(s, lit_var(*i)) == lit_sign(*i))
            return true;   // tautology
        else if (*i != last && var_value(s, lit_var(*i)) == varX)
            last = *j++ = *i;
    }
//    j = i;
 
    if (j == begin)          // empty clause
        return false;
 
    if (j - begin == 1) // unit clause
        return sat_solver_enqueue(s,*begin,0);
 
    // create new clause
    sat_solver_clause_new(s,begin,j,0);
    return true;
}

Here is the call graph for this function:

sat_solver_addvar()

int sat_solver_addvar ( sat_solver * s )

extern

Definition at line 1267 of file satSolver.c.

{
    sat_solver_setnvars(s, s->size+1);
    return s->size-1;
}

Here is the call graph for this function:

sat_solver_clause_new()

int sat_solver_clause_new ( sat_solver * s, lit * begin, lit * end, int learnt )

extern

Definition at line 533 of file satSolver.c.

{
    int fUseBinaryClauses = 1;
    int size;
    clause* c;
    int h;
 
    assert(end - begin > 1);
    assert(learnt >= 0 && learnt < 2);
    size           = end - begin;
 
    // do not allocate memory for the two-literal problem clause
    if ( fUseBinaryClauses && size == 2 && !learnt )
    {
        veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(clause_from_lit(begin[1])));
        veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(clause_from_lit(begin[0])));
        s->stats.clauses++;
        s->stats.clauses_literals += size;
        return 0;
    }
 
    // create new clause
//    h = Vec_SetAppend( &s->Mem, NULL, size + learnt + 1 + 1 ) << 1;
    h = Sat_MemAppend( &s->Mem, begin, size, learnt, 0 );
    assert( !(h & 1) );
    if ( s->hLearnts == -1 && learnt )
        s->hLearnts = h;
    if (learnt)
    {
        c = clause_read( s, h );
        c->lbd = sat_clause_compute_lbd( s, c );
        assert( clause_id(c) == veci_size(&s->act_clas) );
//        veci_push(&s->learned, h);
//        act_clause_bump(s,clause_read(s, h));
        if ( s->ClaActType == 0 )
            veci_push(&s->act_clas, (1<<10));
        else
            veci_push(&s->act_clas, s->cla_inc);
        s->stats.learnts++;
        s->stats.learnts_literals += size;
    }
    else
    {
        s->stats.clauses++;
        s->stats.clauses_literals += size;
    }
 
    assert(begin[0] >= 0);
    assert(begin[0] < s->size*2);
    assert(begin[1] >= 0);
    assert(begin[1] < s->size*2);
 
    assert(lit_neg(begin[0]) < s->size*2);
    assert(lit_neg(begin[1]) < s->size*2);
 
    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),c);
    //veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),c);
    veci_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(size > 2 ? h : clause_from_lit(begin[1])));
    veci_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(size > 2 ? h : clause_from_lit(begin[0])));
 
    return h;
}

Here is the caller graph for this function:

sat_solver_count_assigned()

int sat_solver_count_assigned ( sat_solver * s )

extern

Definition at line 744 of file satSolver.c.

{
    // count top-level assignments
    int i, Count = 0;
    assert(sat_solver_dl(s) == 0);
    for ( i = 0; i < s->size; i++ )
        if (var_value(s, i) != varX)
            Count++;
    return Count;
}

sat_solver_delete()

void sat_solver_delete ( sat_solver * s )

extern

Definition at line 1341 of file satSolver.c.

{
//    Vec_SetFree_( &s->Mem );
    Sat_MemFree_( &s->Mem );
 
    // delete vectors
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
//    veci_delete(&s->learned);
    veci_delete(&s->act_clas);
    veci_delete(&s->stack);
//    veci_delete(&s->model);
    veci_delete(&s->act_vars);
    veci_delete(&s->unit_lits);
    veci_delete(&s->pivot_vars);
    veci_delete(&s->temp_clause);
    veci_delete(&s->conf_final);
 
    veci_delete(&s->user_vars);
    veci_delete(&s->user_values);
 
    // delete arrays
    if (s->reasons != 0){
        int i;
        for (i = 0; i < s->cap*2; i++)
            veci_delete(&s->wlists[i]);
        ABC_FREE(s->wlists   );
//        ABC_FREE(s->vi       );
        ABC_FREE(s->levels   );
        ABC_FREE(s->assigns  );
        ABC_FREE(s->polarity );
        ABC_FREE(s->tags     );
        ABC_FREE(s->loads    );
        ABC_FREE(s->activity );
        ABC_FREE(s->activity2);
        ABC_FREE(s->pFreqs   );
        ABC_FREE(s->factors  );
        ABC_FREE(s->orderpos );
        ABC_FREE(s->reasons  );
        ABC_FREE(s->trail    );
        ABC_FREE(s->model    );
    }
 
    sat_solver_store_free(s);
    ABC_FREE(s);
}

Here is the call graph for this function:

sat_solver_get_var_value()

int sat_solver_get_var_value ( sat_solver * s, int v )

extern

Definition at line 118 of file satSolver.c.

{
    if ( var_value(s, v) == var0 )
        return l_False;
    if ( var_value(s, v) == var1 )
        return l_True;
    if ( var_value(s, v) == varX )
        return l_Undef;
    assert( 0 );
    return 0;
}

Here is the caller graph for this function:

sat_solver_memory()

double sat_solver_memory ( sat_solver * s )

extern

Definition at line 1479 of file satSolver.c.

{
    int i;
    double Mem = sizeof(sat_solver);
    for (i = 0; i < s->cap*2; i++)
        Mem += s->wlists[i].cap * sizeof(int);
    Mem += s->cap * sizeof(veci);     // ABC_FREE(s->wlists   );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->levels   );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->loads    );
    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
    if ( s->activity2 )
    Mem += s->cap * sizeof(word);     // ABC_FREE(s->activity );
    if ( s->factors )
    Mem += s->cap * sizeof(double);   // ABC_FREE(s->factors  );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
    Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->model    );
 
    Mem += s->order.cap * sizeof(int);
    Mem += s->trail_lim.cap * sizeof(int);
    Mem += s->tagged.cap * sizeof(int);
//    Mem += s->learned.cap * sizeof(int);
    Mem += s->stack.cap * sizeof(int);
    Mem += s->act_vars.cap * sizeof(int);
    Mem += s->unit_lits.cap * sizeof(int);
    Mem += s->act_clas.cap * sizeof(int);
    Mem += s->temp_clause.cap * sizeof(int);
    Mem += s->conf_final.cap * sizeof(int);
    Mem += Sat_MemMemoryAll( &s->Mem );
    return Mem;
}

Here is the caller graph for this function:

sat_solver_minimize_assumptions()

int sat_solver_minimize_assumptions ( sat_solver * s, int * pLits, int nLits, int nConfLimit )

extern

Definition at line 2209 of file satSolver.c.

{
    int i, k, nLitsL, nLitsR, nResL, nResR, status;
    if ( nLits == 1 )
    {
        // since the problem is UNSAT, we will try to solve it without assuming the last literal
        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
        if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
        status = sat_solver_solve_internal( s );
        //printf( "%c", status == l_False ? 'u' : 's' );
        return (int)(status != l_False); // return 1 if the problem is not UNSAT
    }
    assert( nLits >= 2 );
    nLitsL = nLits / 2;
    nLitsR = nLits - nLitsL;
    // assume the left lits
    for ( i = 0; i < nLitsL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve with these assumptions
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) // these are enough
    {
        for ( i = 0; i < nLitsL; i++ )
            sat_solver_pop(s);
        return sat_solver_minimize_assumptions( s, pLits, nLitsL, nConfLimit );
    }
    // solve for the right lits
    nResL = nLitsR == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver_pop(s);
    // swap literals
//    assert( nResL <= nLitsL );
//    for ( i = 0; i < nResL; i++ )
//        ABC_SWAP( int, pLits[i], pLits[nLitsL+i] );
    veci_resize( &s->temp_clause, 0 );
    for ( i = 0; i < nLitsL; i++ )
        veci_push( &s->temp_clause, pLits[i] );
    for ( i = 0; i < nResL; i++ )
        pLits[i] = pLits[nLitsL+i];
    for ( i = 0; i < nLitsL; i++ )
        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
    // assume the right lits
    for ( i = 0; i < nResL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
            return sat_solver_minimize_assumptions( s, pLits, i+1, nConfLimit );
        }
    // solve with these assumptions
    if ( nConfLimit ) s->nConfLimit = s->stats.conflicts + nConfLimit;
    status = sat_solver_solve_internal( s );
    if ( status == l_False ) // these are enough
    {
        for ( i = 0; i < nResL; i++ )
            sat_solver_pop(s);
        return nResL;
    }
    // solve for the left lits
    nResR = nLitsL == 1 ? 1 : sat_solver_minimize_assumptions( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_minimize_assumptions2()

int sat_solver_minimize_assumptions2 ( sat_solver * s, int * pLits, int nLits, int nConfLimit )

extern

Definition at line 2284 of file satSolver.c.

{
    int i, k, nLitsL, nLitsR, nResL, nResR;
    if ( nLits == 1 )
    {
        // since the problem is UNSAT, we will try to solve it without assuming the last literal
        // if the result is UNSAT, the last literal can be dropped; otherwise, it is needed
        int RetValue = 1, LitNot = Abc_LitNot(pLits[0]);
        int status = l_False;
        int Temp = s->nConfLimit; 
        s->nConfLimit = nConfLimit;
 
        RetValue = sat_solver_push( s, LitNot ); assert( RetValue );
        status = sat_solver_solve_internal( s );
        sat_solver_pop( s );
 
        // if the problem is UNSAT, add clause
        if ( status == l_False )
        {
            RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
            assert( RetValue );
        }
 
        s->nConfLimit = Temp;
        return (int)(status != l_False); // return 1 if the problem is not UNSAT
    }
    assert( nLits >= 2 );
    nLitsL = nLits / 2;
    nLitsR = nLits - nLitsL;
    // assume the left lits
    for ( i = 0; i < nLitsL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nLitsL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the right lits
    nResL = sat_solver_minimize_assumptions2( s, pLits + nLitsL, nLitsR, nConfLimit );
    for ( i = 0; i < nLitsL; i++ )
        sat_solver_pop(s);
    // swap literals
//    assert( nResL <= nLitsL );
    veci_resize( &s->temp_clause, 0 );
    for ( i = 0; i < nLitsL; i++ )
        veci_push( &s->temp_clause, pLits[i] );
    for ( i = 0; i < nResL; i++ )
        pLits[i] = pLits[nLitsL+i];
    for ( i = 0; i < nLitsL; i++ )
        pLits[nResL+i] = veci_begin(&s->temp_clause)[i];
    // assume the right lits
    for ( i = 0; i < nResL; i++ )
        if ( !sat_solver_push(s, pLits[i]) )
        {
            for ( k = i; k >= 0; k-- )
                sat_solver_pop(s);
 
            // add clauses for these literal
            for ( k = i+1; k > nResL; k++ )
            {
                int LitNot = Abc_LitNot(pLits[i]);
                int RetValue = sat_solver_addclause( s, &LitNot, &LitNot+1 );
                assert( RetValue );
            }
 
            return sat_solver_minimize_assumptions2( s, pLits, i+1, nConfLimit );
        }
    // solve for the left lits
    nResR = sat_solver_minimize_assumptions2( s, pLits + nResL, nLitsL, nConfLimit );
    for ( i = 0; i < nResL; i++ )
        sat_solver_pop(s);
    return nResL + nResR;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_nclauses()

int sat_solver_nclauses ( sat_solver * s )

extern

Definition at line 2375 of file satSolver.c.

{
    return s->stats.clauses;
}

Here is the caller graph for this function:

sat_solver_nconflicts()

int sat_solver_nconflicts ( sat_solver * s )

extern

Definition at line 2381 of file satSolver.c.

{
    return (int)s->stats.conflicts;
}

Here is the caller graph for this function:

sat_solver_new()

sat_solver * sat_solver_new ( void )

extern

Definition at line 1137 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
//    Vec_SetAlloc_(&s->Mem, 15);
    Sat_MemAlloc_(&s->Mem, 17);
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    s->nLearntStart = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
    s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
    s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
    s->nLearntMax   = s->nLearntStart;
 
    // initialize vectors
    veci_new(&s->order);
    veci_new(&s->trail_lim);
    veci_new(&s->tagged);
//    veci_new(&s->learned);
    veci_new(&s->act_clas);
    veci_new(&s->stack);
//    veci_new(&s->model);
    veci_new(&s->unit_lits);
    veci_new(&s->temp_clause);
    veci_new(&s->conf_final);
 
    // initialize arrays
    s->wlists    = 0;
    s->activity  = 0;
    s->orderpos  = 0;
    s->reasons   = 0;
    s->trail     = 0;
 
    // initialize other vars
    s->size                   = 0;
    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_new(&s->act_vars);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = 91648253;
    s->progress_estimate      = 0;
//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
//    s->binary->size_learnt    = (2 << 1);
    s->verbosity              = 0;
 
    s->stats.starts           = 0;
    s->stats.decisions        = 0;
    s->stats.propagations     = 0;
    s->stats.inspects         = 0;
    s->stats.conflicts        = 0;
    s->stats.clauses          = 0;
    s->stats.clauses_literals = 0;
    s->stats.learnts          = 0;
    s->stats.learnts_literals = 0;
    s->stats.tot_literals     = 0;
    return s;
}

sat_solver_nvars()

int sat_solver_nvars ( sat_solver * s )

extern

Definition at line 2369 of file satSolver.c.

{
    return s->size;
}

sat_solver_pop()

void sat_solver_pop ( sat_solver * s )

extern

Definition at line 2045 of file satSolver.c.

{
    assert( sat_solver_dl(s) > 0 );
    sat_solver_canceluntil(s, --s->root_level);
}

Here is the caller graph for this function:

sat_solver_push()

int sat_solver_push ( sat_solver * s, int p )

extern

Definition at line 2002 of file satSolver.c.

{
    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));
            // the two lines below are a bug fix by Siert Wieringa 
            if (var_level(s, lit_var(p)) > 0)
                veci_push(&s->conf_final, p);
        }
        //sat_solver_canceluntil(s, 0);
        return false; 
    }
    else
    {
        int fConfl = sat_solver_propagate(s);
        if (fConfl){
            sat_solver_analyze_final(s, fConfl, 0);
            //assert(s->conf_final.size > 0);
            //sat_solver_canceluntil(s, 0);
            return false; }
    }
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_restart()

void sat_solver_restart ( sat_solver * s )

extern

Definition at line 1389 of file satSolver.c.

{
    int i;
    Sat_MemRestart( &s->Mem );
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    veci_resize(&s->trail_lim, 0);
    veci_resize(&s->order, 0);
    for ( i = 0; i < s->size*2; i++ )
        s->wlists[i].size = 0;
 
    s->nDBreduces = 0;
 
    // initialize other vars
    s->size                   = 0;
//    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
 
    // variable activities
    solver_init_activities(s);
    veci_resize(&s->act_clas, 0);
 
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = 91648253;
    s->progress_estimate      = 0;
    s->verbosity              = 0;
 
    s->stats.starts           = 0;
    s->stats.decisions        = 0;
    s->stats.propagations     = 0;
    s->stats.inspects         = 0;
    s->stats.conflicts        = 0;
    s->stats.clauses          = 0;
    s->stats.clauses_literals = 0;
    s->stats.learnts          = 0;
    s->stats.learnts_literals = 0;
    s->stats.tot_literals     = 0;
}

Here is the caller graph for this function:

sat_solver_rollback()

void sat_solver_rollback ( sat_solver * s )

extern

Definition at line 1643 of file satSolver.c.

{
    Sat_Mem_t * pMem = &s->Mem;
    int i, k, j;
    static int Count = 0;
    Count++;
    assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
    assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
    // reset implication queue
    sat_solver_canceluntil_rollback( s, s->iTrailPivot );
    // update order 
    if ( s->iVarPivot < s->size )
    { 
        if ( s->activity2 )
        {
            s->var_inc = s->var_inc2;
            memcpy( s->activity, s->activity2, sizeof(word) * s->iVarPivot );
        }
        veci_resize(&s->order, 0);
        for ( i = 0; i < s->iVarPivot; i++ )
        {
            if ( var_value(s, i) != varX )
                continue;
            s->orderpos[i] = veci_size(&s->order);
            veci_push(&s->order,i);
            order_update(s, i);
        }
    }
    // compact watches
    for ( i = 0; i < s->iVarPivot*2; i++ )
    {
        cla* pArray = veci_begin(&s->wlists[i]);
        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
        {
            if ( clause_is_lit(pArray[k]) )
            {
                if ( clause_read_lit(pArray[k]) < s->iVarPivot*2 )
                    pArray[j++] = pArray[k];
            }
            else if ( Sat_MemClauseUsed(pMem, pArray[k]) )
                pArray[j++] = pArray[k];
        }
        veci_resize(&s->wlists[i],j);
    }
    // reset watcher lists
    for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
        s->wlists[i].size = 0;
 
    // reset clause counts
    s->stats.clauses = pMem->BookMarkE[0];
    s->stats.learnts = pMem->BookMarkE[1];
    // rollback clauses
    Sat_MemRollBack( pMem );
 
    // resize learned arrays
    veci_resize(&s->act_clas,  s->stats.learnts);
 
    // initialize other vars
    s->size = s->iVarPivot;
    if ( s->size == 0 )
    {
    //    s->size                   = 0;
    //    s->cap                    = 0;
        s->qhead                  = 0;
        s->qtail                  = 0;
 
        solver_init_activities(s);
 
        s->root_level             = 0;
        s->random_seed            = 91648253;
        s->progress_estimate      = 0;
        s->verbosity              = 0;
 
        s->stats.starts           = 0;
        s->stats.decisions        = 0;
        s->stats.propagations     = 0;
        s->stats.inspects         = 0;
        s->stats.conflicts        = 0;
        s->stats.clauses          = 0;
        s->stats.clauses_literals = 0;
        s->stats.learnts          = 0;
        s->stats.learnts_literals = 0;
        s->stats.tot_literals     = 0;
 
        // initialize rollback
        s->iVarPivot              =  0; // the pivot for variables
        s->iTrailPivot            =  0; // the pivot for trail
        s->hProofPivot            =  1; // the pivot for proof records
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_set_resource_limits()

void sat_solver_set_resource_limits ( sat_solver * s, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal )

extern

Definition at line 2051 of file satSolver.c.

{
    // set the external limits
    s->nRestarts  = 0;
    s->nConfLimit = 0;
    s->nInsLimit  = 0;
    if ( nConfLimit )
        s->nConfLimit = s->stats.conflicts + nConfLimit;
    if ( nInsLimit )
//        s->nInsLimit = s->stats.inspects + nInsLimit;
        s->nInsLimit = s->stats.propagations + nInsLimit;
    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
        s->nConfLimit = nConfLimitGlobal;
    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
        s->nInsLimit = nInsLimitGlobal;
}

Here is the caller graph for this function:

sat_solver_set_var_activity()

void sat_solver_set_var_activity ( sat_solver * s, int * pVars, int nVars )

extern

Definition at line 218 of file satSolver.c.

{
    int i;
    for (i = 0; i < s->size; i++)
        s->activity[i] = 0;
    if ( s->VarActType == 0 )
    {
        s->var_inc            = (1 <<  5);
        s->var_decay          = -1;
        for ( i = 0; i < nVars; i++ )
        {
            int iVar = pVars ? pVars[i] : i;
            s->activity[iVar] = s->var_inc*(nVars-i);
            if (s->orderpos[iVar] != -1)
                order_update( s, iVar );
        }
    }
    else if ( s->VarActType == 1 )
    {
        s->var_inc = Abc_Dbl2Word(1);
        for ( i = 0; i < nVars; i++ )
        {
            int iVar = pVars ? pVars[i] : i;
            s->activity[iVar] = Abc_Dbl2Word(nVars-i);
            if (s->orderpos[iVar] != -1)
                order_update( s, iVar );
        }
    }
    else assert( 0 );
}

sat_solver_setnvars()

void sat_solver_setnvars ( sat_solver * s, int n )

extern

Definition at line 1272 of file satSolver.c.

{
    int var;
 
    if (s->cap < n){
        int old_cap = s->cap;
        while (s->cap < n) s->cap = s->cap*2+1;
        if ( s->cap < 50000 )
            s->cap = 50000;
 
        s->wlists    = ABC_REALLOC(veci,   s->wlists,   s->cap*2);
//        s->vi        = ABC_REALLOC(varinfo,s->vi,       s->cap);
        s->levels    = ABC_REALLOC(int,    s->levels,   s->cap);
        s->assigns   = ABC_REALLOC(char,   s->assigns,  s->cap);
        s->polarity  = ABC_REALLOC(char,   s->polarity, s->cap);
        s->tags      = ABC_REALLOC(char,   s->tags,     s->cap);
        s->loads     = ABC_REALLOC(char,   s->loads,    s->cap);
        s->activity  = ABC_REALLOC(word,   s->activity, s->cap);
        s->activity2 = ABC_REALLOC(word,   s->activity2,s->cap);
        s->pFreqs    = ABC_REALLOC(char,   s->pFreqs,   s->cap);
 
        if ( s->factors )
        s->factors   = ABC_REALLOC(double, s->factors,  s->cap);
        s->orderpos  = ABC_REALLOC(int,    s->orderpos, s->cap);
        s->reasons   = ABC_REALLOC(int,    s->reasons,  s->cap);
        s->trail     = ABC_REALLOC(lit,    s->trail,    s->cap);
        s->model     = ABC_REALLOC(int,    s->model,    s->cap);
        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(veci) );
    } 
 
    for (var = s->size; var < n; var++){
        assert(!s->wlists[2*var].size);
        assert(!s->wlists[2*var+1].size);
        if ( s->wlists[2*var].ptr == NULL )
            veci_new(&s->wlists[2*var]);
        if ( s->wlists[2*var+1].ptr == NULL )
            veci_new(&s->wlists[2*var+1]);
 
        if ( s->VarActType == 0 )
            s->activity[var] = (1<<10);
        else if ( s->VarActType == 1 )
            s->activity[var] = 0;
        else if ( s->VarActType == 2 )
            s->activity[var] = 0;
        else assert(0);
 
        s->pFreqs[var]   = 0;
        if ( s->factors )
        s->factors [var] = 0;
//        *((int*)s->vi + var) = 0; s->vi[var].val = varX;
        s->levels  [var] = 0;
        s->assigns [var] = varX;
        s->polarity[var] = 0;
        s->tags    [var] = 0;
        s->loads   [var] = 0;
        s->orderpos[var] = veci_size(&s->order);
        s->reasons [var] = 0;
        s->model   [var] = 0; 
        
        /* does not hold because variables enqueued at top level will not be reinserted in the heap
           assert(veci_size(&s->order) == var); 
         */
        veci_push(&s->order,var);
        order_update(s, var);
    }
 
    s->size = n > s->size ? n : s->size;
}

Here is the call graph for this function:

sat_solver_simplify()

int sat_solver_simplify ( sat_solver * s )

extern

Definition at line 1515 of file satSolver.c.

{
    assert(sat_solver_dl(s) == 0);
    if (sat_solver_propagate(s) != 0)
        return false;
    return true;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_solve()

int sat_solver_solve ( sat_solver * s, lit * begin, lit * end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal )

extern

Definition at line 2068 of file satSolver.c.

{
    lbool status;
    lit * i;
    if ( s->fSolved )
    {
        if ( s->pStore )
        {
            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
            assert( RetValue );
            (void) RetValue;
        }
        return l_False;
    }
 
    if ( s->fVerbose )
        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
 
    sat_solver_set_resource_limits( s, nConfLimit, nInsLimit, nConfLimitGlobal, nInsLimitGlobal );
 
#ifdef SAT_USE_ANALYZE_FINAL
    // Perform assumptions:
    s->root_level = 0;
    for ( i = begin; i < end; i++ )
        if ( !sat_solver_push(s, *i) )
        {
            sat_solver_canceluntil(s,0);
            s->root_level = 0;
            return l_False;
        }
    assert(s->root_level == sat_solver_dl(s));
#else
    //printf("solve: "); printlits(begin, end); printf("\n");
    for (i = begin; i < end; i++){
//        switch (lit_sign(*i) ? -s->assignss[lit_var(*i)] : s->assignss[lit_var(*i)]){
        switch (var_value(s, *i)) {
        case var1: // l_True: 
            break;
        case varX: // l_Undef
            sat_solver_decision(s, *i);
            if (sat_solver_propagate(s) == 0)
                break;
            // fallthrough
        case var0: // l_False 
            sat_solver_canceluntil(s, 0);
            return l_False;
        }
    }
    s->root_level = sat_solver_dl(s);
#endif
 
    status = sat_solver_solve_internal(s);
 
    sat_solver_canceluntil(s,0);
    s->root_level = 0;

    if ( status == l_False && s->pStore )
    {
        int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
        assert( RetValue );
        (void) RetValue;
    }
    return status;
}

Here is the call graph for this function:

sat_solver_solve_internal()

int sat_solver_solve_internal ( sat_solver * s )

extern

Definition at line 1942 of file satSolver.c.

{
    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;
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        if (s->verbosity >= 1)
        {
            double Ratio = (s->stats.learnts == 0)? 0.0 :
                s->stats.learnts_literals / (double)s->stats.learnts;
            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);
        // quit the loop if reached an external limit
        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);
    // save variable values
    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;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_solve_lexsat()

int sat_solver_solve_lexsat ( sat_solver * s, int * pLits, int nLits )

extern

Definition at line 2143 of file satSolver.c.

{
    int i, iLitFail = -1;
    lbool status;
    assert( nLits > 0 );
    // help the SAT solver by setting desirable polarity
    sat_solver_set_literal_polarity( s, pLits, nLits );
    // check if there exists a satisfying assignment
    status = sat_solver_solve_internal( s );
    if ( status != l_True ) // no assignment
        return status;
    // there is at least one satisfying assignment
    assert( status == l_True );
    // find the first mismatching literal
    for ( i = 0; i < nLits; i++ )
        if ( pLits[i] != sat_solver_var_literal(s, Abc_Lit2Var(pLits[i])) )
            break;
    if ( i == nLits ) // no mismatch - the current assignment is the minimum one!
        return l_True;
    // mismatch happens in literal i
    iLitFail = i;
    // create assumptions up to this literal (as in pLits) - including this literal!
    for ( i = 0; i <= iLitFail; i++ )
        if ( !sat_solver_push(s, pLits[i]) ) // can become UNSAT while adding the last assumption
            break;
    if ( i < iLitFail + 1 ) // the solver became UNSAT while adding assumptions
        status = l_False;
    else // solve under the assumptions
        status = sat_solver_solve_internal( s );
    if ( status == l_True )
    {
        // we proved that there is a sat assignment with literal (iLitFail) having polarity as in pLits
        // continue solving recursively
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
    }
    else if ( status == l_False )
    {
        // we proved that there is no assignment with iLitFail having polarity as in pLits
        assert( Abc_LitIsCompl(pLits[iLitFail]) ); // literal is 0 
        // (this assert may fail only if there is a sat assignment smaller than one originally given in pLits)
        // now we flip this literal (make it 1), change the last assumption
        // and contiue looking for the 000...0-assignment of other literals
        sat_solver_pop( s );
        pLits[iLitFail] = Abc_LitNot(pLits[iLitFail]);
        if ( !sat_solver_push(s, pLits[iLitFail]) )
            printf( "sat_solver_solve_lexsat(): A satisfying assignment should exist.\n" ); // because we know that the problem is satisfiable
        // update other literals to be 000...0
        for ( i = iLitFail + 1; i < nLits; i++ )
            pLits[i] = Abc_LitNot( Abc_LitRegular(pLits[i]) );
        // continue solving recursively
        if ( iLitFail + 1 < nLits )
            status = sat_solver_solve_lexsat( s, pLits + iLitFail + 1, nLits - iLitFail - 1 );
        else
            status = l_True;
    }
    // undo the assumptions
    for ( i = iLitFail; i >= 0; i-- )
        sat_solver_pop( s );
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_alloc()

void sat_solver_store_alloc ( sat_solver * s )

extern

Definition at line 2389 of file satSolver.c.

{
    assert( s->pStore == NULL );
    s->pStore = Sto_ManAlloc();
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_free()

void sat_solver_store_free ( sat_solver * s )

extern

Definition at line 2400 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManFree( (Sto_Man_t *)s->pStore );
    s->pStore = NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_mark_clauses_a()

void sat_solver_store_mark_clauses_a ( sat_solver * s )

extern

Definition at line 2417 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManMarkClausesA( (Sto_Man_t *)s->pStore );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_mark_roots()

void sat_solver_store_mark_roots ( sat_solver * s )

extern

Definition at line 2412 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManMarkRoots( (Sto_Man_t *)s->pStore );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver_store_release()

void * sat_solver_store_release ( sat_solver * s )

extern

Definition at line 2422 of file satSolver.c.

{
    void * pTemp;
    if ( s->pStore == NULL )
        return NULL;
    pTemp = s->pStore;
    s->pStore = NULL;
    return pTemp;
}

Here is the caller graph for this function:

sat_solver_store_write()

void sat_solver_store_write ( sat_solver * s, char * pFileName )

extern

Definition at line 2395 of file satSolver.c.

{
    if ( s->pStore ) Sto_ManDumpClauses( (Sto_Man_t *)s->pStore, pFileName );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sat_SolverDoubleClauses()

void Sat_SolverDoubleClauses ( sat_solver * p, int iVar )

extern

Function*************************************************************

Synopsis [Duplicates all clauses, complements unit clause of the given var.]

Description []

SideEffects []

SeeAlso []

Definition at line 312 of file satUtil.c.

{
    assert( 0 );
/*
    clause * pClause;
    lit Lit, * pLits;
    int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
    // get the number of variables
    nVarsOld = p->size;
    nLitsOld = 2 * p->size;
    // extend the solver to depend on two sets of variables
    sat_solver_setnvars( p, 2 * p->size );
    // duplicate implications
    for ( v = 0; v < nVarsOld; v++ )
        if ( p->assigns[v] != l_Undef )
        {
            Lit = nLitsOld + toLitCond( v, p->assigns[v]==l_False );
            if ( v == iVar )
                Lit = lit_neg(Lit);
            RetValue = sat_solver_addclause( p, &Lit, &Lit + 1 );
            assert( RetValue );
        }
    // duplicate clauses
    nClauses = vecp_size(&p->clauses);
    for ( c = 0; c < nClauses; c++ )
    {
        pClause = (clause *)p->clauses.ptr[c];
        nLits = clause_size(pClause);
        pLits = clause_begin(pClause);
        for ( v = 0; v < nLits; v++ )
            pLits[v] += nLitsOld;
        RetValue = sat_solver_addclause( p, pLits, pLits + nLits );
        assert( RetValue );
        for ( v = 0; v < nLits; v++ )
            pLits[v] -= nLitsOld;
    }
*/
}

Here is the caller graph for this function:

Sat_SolverGetModel()

int * Sat_SolverGetModel ( sat_solver * p, int * pVars, int nVars )

extern

Function*************************************************************

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file satUtil.c.

{
    int * pModel;
    int i;
    pModel = ABC_CALLOC( int, nVars+1 );
    for ( i = 0; i < nVars; i++ )
        pModel[i] = sat_solver_var_value(p, pVars[i]);
    return pModel;    
}

Here is the caller graph for this function:

Sat_SolverPrintStats()

void Sat_SolverPrintStats ( FILE * pFile, sat_solver * p )

extern

Definition at line 193 of file satUtil.c.

{
    printf( "starts        : %16.0f\n", Sat_Wrd2Dbl(p->stats.starts) );
    printf( "conflicts     : %16.0f\n", Sat_Wrd2Dbl(p->stats.conflicts) );
    printf( "decisions     : %16.0f\n", Sat_Wrd2Dbl(p->stats.decisions) );
    printf( "propagations  : %16.0f\n", Sat_Wrd2Dbl(p->stats.propagations) );
//    printf( "inspects      : %10d\n", (int)p->stats.inspects );
//    printf( "inspects2     : %10d\n", (int)p->stats.inspects2 );
}

Here is the caller graph for this function:

Sat_SolverTraceStart()

void Sat_SolverTraceStart ( sat_solver * pSat, char * pName )

extern

DECLARATIONS ///.

CFile****************************************************************

FileName [satTrace.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT sat_solver.]

Synopsis [Records the trace of SAT solving in the CNF form.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id

satTrace.c,v 1.4 2005/09/16 22:55:03 casem Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Start the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 53 of file satTrace.c.

{
    assert( pSat->pFile == NULL );
    pSat->pFile = fopen( pName, "w" );
    fprintf( pSat->pFile, "                                        \n" );
    pSat->nClauses = 0;
    pSat->nRoots = 0;
}   

Sat_SolverTraceStop()

void Sat_SolverTraceStop ( sat_solver * pSat )

extern

Function*************************************************************

Synopsis [Stops the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file satTrace.c.

{
    if ( pSat->pFile == NULL )
        return;
    rewind( pSat->pFile );
    fprintf( pSat->pFile, "p %d %d %d", sat_solver_nvars(pSat), pSat->nClauses, pSat->nRoots );
    fclose( pSat->pFile );
    pSat->pFile = NULL;
}

Here is the call graph for this function:

Sat_SolverTraceWrite()

void Sat_SolverTraceWrite ( sat_solver * pSat, int * pBeg, int * pEnd, int fRoot )

extern

Function*************************************************************

Synopsis [Writes one clause into the trace file.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file satTrace.c.

{
    if ( pSat->pFile == NULL )
        return;
    pSat->nClauses++;
    pSat->nRoots += fRoot;
    for ( ; pBeg < pEnd ; pBeg++ )
        fprintf( pSat->pFile, " %d", lit_print(*pBeg) );
    fprintf( pSat->pFile, " 0\n" );
}

Sat_SolverWriteDimacs()

void Sat_SolverWriteDimacs ( sat_solver * p, char * pFileName, lit * assumpBegin, lit * assumpEnd, int incrementVars )

extern

Function*************************************************************

Synopsis [Write the clauses in the solver into a file in DIMACS format.]

Description [This procedure by default does not print binary clauses. To enable printing of binary clauses, please set fUseBinaryClauses to 0 in the body of procedure sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt) in file "satSolver.c".]

SideEffects []

SeeAlso []

Definition at line 74 of file satUtil.c.

{
    Sat_Mem_t * pMem = &p->Mem;
    FILE * pFile;
    clause * c;
    int i, k, nUnits;
 
    // count the number of unit clauses
    nUnits = 0;
    for ( i = 0; i < p->size; i++ )
        if ( p->levels[i] == 0 && p->assigns[i] != 3 )
            nUnits++;
 
    // start the file
    pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
    if ( pFile == NULL )
    {
        printf( "Sat_SolverWriteDimacs(): Cannot open the ouput file.\n" );
        return;
    }
//    fprintf( pFile, "c CNF generated by ABC on %s\n", Extra_TimeStamp() );
    fprintf( pFile, "p cnf %d %d\n", p->size, Sat_MemEntryNum(&p->Mem, 0)-1+Sat_MemEntryNum(&p->Mem, 1)+nUnits+(int)(assumpEnd-assumpBegin) );
 
    // write the original clauses
    Sat_MemForEachClause( pMem, c, i, k )
        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
    // write the learned clauses
//    Sat_MemForEachLearned( pMem, c, i, k )
//        Sat_SolverClauseWriteDimacs( pFile, c, incrementVars );
 
    // write zero-level assertions
    for ( i = 0; i < p->size; i++ )
        if ( p->levels[i] == 0 && p->assigns[i] != 3 ) // varX
            fprintf( pFile, "%s%d%s\n",
                     (p->assigns[i] == 1)? "-": "",    // var0
                     i + (int)(incrementVars>0),
                     (incrementVars) ? " 0" : "");
 
    // write the assump
    if (assumpBegin) {
        for (; assumpBegin != assumpEnd; assumpBegin++) {
            fprintf( pFile, "%s%d%s\n",
                     lit_sign(*assumpBegin)? "-": "",
                     lit_var(*assumpBegin) + (int)(incrementVars>0),
                     (incrementVars) ? " 0" : "");
        }
    }
 
    fprintf( pFile, "\n" );
    if ( pFileName ) fclose( pFile );
} 

Here is the caller graph for this function:

zsat_solver_new_seed()

sat_solver * zsat_solver_new_seed ( double seed )

extern

Definition at line 1202 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)ABC_CALLOC( char, sizeof(sat_solver));
 
//    Vec_SetAlloc_(&s->Mem, 15);
    Sat_MemAlloc_(&s->Mem, 15);
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    s->nLearntStart = LEARNT_MAX_START_DEFAULT;  // starting learned clause limit
    s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT;  // delta of learned clause limit
    s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT;  // ratio of learned clause limit
    s->nLearntMax   = s->nLearntStart;
 
    // initialize vectors
    veci_new(&s->order);
    veci_new(&s->trail_lim);
    veci_new(&s->tagged);
//    veci_new(&s->learned);
    veci_new(&s->act_clas);
    veci_new(&s->stack);
//    veci_new(&s->model);
    veci_new(&s->unit_lits);
    veci_new(&s->temp_clause);
    veci_new(&s->conf_final);
 
    // initialize arrays
    s->wlists    = 0;
    s->activity  = 0;
    s->orderpos  = 0;
    s->reasons   = 0;
    s->trail     = 0;
 
    // initialize other vars
    s->size                   = 0;
    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_new(&s->act_vars);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = seed;
    s->progress_estimate      = 0;
//    s->binary                 = (clause*)ABC_ALLOC( char, sizeof(clause) + sizeof(lit)*2);
//    s->binary->size_learnt    = (2 << 1);
    s->verbosity              = 0;
 
    s->stats.starts           = 0;
    s->stats.decisions        = 0;
    s->stats.propagations     = 0;
    s->stats.inspects         = 0;
    s->stats.conflicts        = 0;
    s->stats.clauses          = 0;
    s->stats.clauses_literals = 0;
    s->stats.learnts          = 0;
    s->stats.learnts_literals = 0;
    s->stats.tot_literals     = 0;
    return s;
}

Here is the caller graph for this function:

zsat_solver_restart_seed()

void zsat_solver_restart_seed ( sat_solver * s, double seed )

extern

Definition at line 1435 of file satSolver.c.

{
    int i;
    Sat_MemRestart( &s->Mem );
    s->hLearnts = -1;
    s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0, 0 );
    s->binary = clause_read( s, s->hBinary );
 
    veci_resize(&s->trail_lim, 0);
    veci_resize(&s->order, 0);
    for ( i = 0; i < s->size*2; i++ )
        s->wlists[i].size = 0;
 
    s->nDBreduces = 0;
 
    // initialize other vars
    s->size                   = 0;
//    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
 
    solver_init_activities(s);
    veci_resize(&s->act_clas, 0);
 
    s->root_level             = 0;
//    s->simpdb_assigns         = 0;
//    s->simpdb_props           = 0;
    s->random_seed            = seed;
    s->progress_estimate      = 0;
    s->verbosity              = 0;
 
    s->stats.starts           = 0;
    s->stats.decisions        = 0;
    s->stats.propagations     = 0;
    s->stats.inspects         = 0;
    s->stats.conflicts        = 0;
    s->stats.clauses          = 0;
    s->stats.clauses_literals = 0;
    s->stats.learnts          = 0;
    s->stats.learnts_literals = 0;
    s->stats.tot_literals     = 0;
}

Here is the caller graph for this function: