src/sat/bsat/satSolver.h File Reference

#include "satVec.h"
#include "satMem.h"

Include dependency graph for satSolver.h:

This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Data Structures
struct	stats_t
struct	sat_solver_t
Typedefs
typedef int	lit
typedef char	lbool
typedef long long	sint64
typedef struct sat_solver_t	sat_solver
typedef struct stats_t	stats
typedef struct clause_t	clause
Functions
static lit	toLit (int v)
static lit	toLitCond (int v, int c)
static lit	lit_neg (lit l)
static int	lit_var (lit l)
static int	lit_sign (lit l)
static int	lit_print (lit l)
static lit	lit_read (int s)
sat_solver *	sat_solver_new (void)
void	sat_solver_delete (sat_solver *s)
bool	sat_solver_addclause (sat_solver *s, lit *begin, lit *end)
bool	sat_solver_simplify (sat_solver *s)
int	sat_solver_solve (sat_solver *s, lit *begin, lit *end, sint64 nConfLimit, sint64 nInsLimit, sint64 nConfLimitGlobal, sint64 nInsLimitGlobal)
int	sat_solver_nvars (sat_solver *s)
int	sat_solver_nclauses (sat_solver *s)
int	sat_solver_nconflicts (sat_solver *s)
void	sat_solver_setnvars (sat_solver *s, int n)
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)
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)
Variables
static const bool	true = 1
static const bool	false = 0
static const int	var_Undef = -1
static const lit	lit_Undef = -2
static const lbool	l_Undef = 0
static const lbool	l_True = 1
static const lbool	l_False = -1

---

Typedef Documentation

typedef struct clause_t clause

Definition at line 124 of file satSolver.h.

typedef char lbool

Definition at line 47 of file satSolver.h.

typedef int lit

Definition at line 46 of file satSolver.h.

typedef struct sat_solver_t sat_solver

Definition at line 80 of file satSolver.h.

typedef long long sint64

Definition at line 55 of file satSolver.h.

typedef struct stats_t stats

Definition at line 100 of file satSolver.h.

---

Function Documentation

static lit lit_neg

(

lit

l

)

[inline, static]

Definition at line 69 of file satSolver.h.

{ return l ^ 1; }

static int lit_print

(

lit

l

)

[inline, static]

Definition at line 72 of file satSolver.h.

{ return lit_sign(l)? -lit_var(l)-1 : lit_var(l)+1; }

static lit lit_read

(

int

s

)

[inline, static]

Definition at line 73 of file satSolver.h.

{ return s > 0 ? toLit(s-1) : lit_neg(toLit(-s-1)); }

static int lit_sign

(

lit

l

)

[inline, static]

Definition at line 71 of file satSolver.h.

{ return l & 1; }

static int lit_var

(

lit

l

)

[inline, static]

Definition at line 70 of file satSolver.h.

{ return l >> 1; }

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

Definition at line 1048 of file satSolver.c.

{
    lit *i,*j;
    int maxvar;
    lbool* values;
    lit last;

    if (begin == end) return false;

    //printlits(begin,end); printf("\n");
    // 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);
//    sat_solver_setnvars(s, lit_var(*(end-1))+1 );

    //printlits(begin,end); printf("\n");
    values = s->assigns;

    // 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) ? -values[lit_var(*i)] : values[lit_var(*i)]));
        lbool sig = !lit_sign(*i); sig += sig - 1;
        if (*i == lit_neg(last) || sig == values[lit_var(*i)])
            return true;   // tautology
        else if (*i != last && values[lit_var(*i)] == l_Undef)
            last = *j++ = *i;
    }

    //printf("final: "); printlits(begin,j); printf("\n");

    if (j == begin)          // empty clause
        return false;

    // add clause to internal storage
    if ( s->pStore )
    {
        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
        int RetValue = Sto_ManAddClause( s->pStore, begin, j );
        assert( RetValue );
    }

    if (j - begin == 1) // unit clause
        return enqueue(s,*begin,(clause*)0);

    // create new clause
    vecp_push(&s->clauses,clause_new(s,begin,j,0));


    s->stats.clauses++;
    s->stats.clauses_literals += j - begin;

    return true;
}

void sat_solver_delete

(

sat_solver *

s

)

Definition at line 1001 of file satSolver.c.

{

#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    int i;
    for (i = 0; i < vecp_size(&s->clauses); i++)
        free(vecp_begin(&s->clauses)[i]);
    for (i = 0; i < vecp_size(&s->learnts); i++)
        free(vecp_begin(&s->learnts)[i]);
#else
    Sat_MmStepStop( s->pMem, 0 );
#endif

    // delete vectors
    vecp_delete(&s->clauses);
    vecp_delete(&s->learnts);
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
    veci_delete(&s->stack);
    veci_delete(&s->model);
    veci_delete(&s->act_vars);
    free(s->binary);

    // delete arrays
    if (s->wlists != 0){
        int i;
        for (i = 0; i < s->size*2; i++)
            vecp_delete(&s->wlists[i]);

        // if one is different from null, all are
        free(s->wlists   );
        free(s->activity );
        free(s->factors  );
        free(s->assigns  );
        free(s->orderpos );
        free(s->reasons  );
        free(s->levels   );
        free(s->trail    );
        free(s->tags     );
    }

    sat_solver_store_free(s);
    free(s);
}

int sat_solver_nclauses

(

sat_solver *

s

)

Definition at line 1254 of file satSolver.c.

{
    return vecp_size(&s->clauses);
}

int sat_solver_nconflicts

(

sat_solver *

s

)

Definition at line 1260 of file satSolver.c.

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

sat_solver* sat_solver_new

(

void

)

Definition at line 935 of file satSolver.c.

{
    sat_solver* s = (sat_solver*)malloc(sizeof(sat_solver));
    memset( s, 0, sizeof(sat_solver) );

    // initialize vectors
    vecp_new(&s->clauses);
    vecp_new(&s->learnts);
    veci_new(&s->order);
    veci_new(&s->trail_lim);
    veci_new(&s->tagged);
    veci_new(&s->stack);
    veci_new(&s->model);
    veci_new(&s->act_vars);

    // initialize arrays
    s->wlists    = 0;
    s->activity  = 0;
    s->factors   = 0;
    s->assigns   = 0;
    s->orderpos  = 0;
    s->reasons   = 0;
    s->levels    = 0;
    s->tags      = 0;
    s->trail     = 0;


    // initialize other vars
    s->size                   = 0;
    s->cap                    = 0;
    s->qhead                  = 0;
    s->qtail                  = 0;
    s->cla_inc                = 1;
    s->cla_decay              = 1;
    s->var_inc                = 1;
    s->var_decay              = 1;
    s->root_level             = 0;
    s->simpdb_assigns         = 0;
    s->simpdb_props           = 0;
    s->random_seed            = 91648253;
    s->progress_estimate      = 0;
    s->binary                 = (clause*)malloc(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.max_literals     = 0;
    s->stats.tot_literals     = 0;

#ifdef SAT_USE_SYSTEM_MEMORY_MANAGEMENT
    s->pMem = NULL;
#else
    s->pMem = Sat_MmStepStart( 10 );
#endif
    return s;
}

int sat_solver_nvars

(

sat_solver *

s

)

Definition at line 1248 of file satSolver.c.

{
    return s->size;
}

void sat_solver_setnvars	(	sat_solver *	s,
		int	n
	)

Definition at line 362 of file satSolver.c.

{
    int var;

    if (s->cap < n){

        while (s->cap < n) s->cap = s->cap*2+1;

        s->wlists    = (vecp*)   realloc(s->wlists,   sizeof(vecp)*s->cap*2);
        s->activity  = (double*) realloc(s->activity, sizeof(double)*s->cap);
        s->factors   = (double*) realloc(s->factors,  sizeof(double)*s->cap);
        s->assigns   = (lbool*)  realloc(s->assigns,  sizeof(lbool)*s->cap);
        s->orderpos  = (int*)    realloc(s->orderpos, sizeof(int)*s->cap);
        s->reasons   = (clause**)realloc(s->reasons,  sizeof(clause*)*s->cap);
        s->levels    = (int*)    realloc(s->levels,   sizeof(int)*s->cap);
        s->tags      = (lbool*)  realloc(s->tags,     sizeof(lbool)*s->cap);
        s->trail     = (lit*)    realloc(s->trail,    sizeof(lit)*s->cap);
    }

    for (var = s->size; var < n; var++){
        vecp_new(&s->wlists[2*var]);
        vecp_new(&s->wlists[2*var+1]);
        s->activity [var] = 0;
        s->factors  [var] = 0;
        s->assigns  [var] = l_Undef;
        s->orderpos [var] = veci_size(&s->order);
        s->reasons  [var] = (clause*)0;
        s->levels   [var] = 0;
        s->tags     [var] = l_Undef;
        
        /* 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;
}

bool sat_solver_simplify

(

sat_solver *

s

)

Definition at line 1113 of file satSolver.c.

{
    clause** reasons;
    int type;

    assert(sat_solver_dlevel(s) == 0);

    if (sat_solver_propagate(s) != 0)
        return false;

    if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
        return true;

    reasons = s->reasons;
    for (type = 0; type < 2; type++){
        vecp*    cs  = type ? &s->learnts : &s->clauses;
        clause** cls = (clause**)vecp_begin(cs);

        int i, j;
        for (j = i = 0; i < vecp_size(cs); i++){
            if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
                clause_simplify(s,cls[i]) == l_True)
                clause_remove(s,cls[i]);
            else
                cls[j++] = cls[i];
        }
        vecp_resize(cs,j);
    }

    s->simpdb_assigns = s->qhead;
    // (shouldn't depend on 'stats' really, but it will do for now)
    s->simpdb_props   = (int)(s->stats.clauses_literals + s->stats.learnts_literals);

    return true;
}

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

Definition at line 1150 of file satSolver.c.

{
    sint64  nof_conflicts = 100;
    sint64  nof_learnts   = sat_solver_nclauses(s) / 3;
    lbool   status        = l_Undef;
    lbool*  values        = s->assigns;
    lit*    i;

    // set the external limits
    s->nCalls++;
    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;
    if ( nConfLimitGlobal && (s->nConfLimit == 0 || s->nConfLimit > nConfLimitGlobal) )
        s->nConfLimit = nConfLimitGlobal;
    if ( nInsLimitGlobal && (s->nInsLimit == 0 || s->nInsLimit > nInsLimitGlobal) )
        s->nInsLimit = nInsLimitGlobal;

    //printf("solve: "); printlits(begin, end); printf("\n");
    for (i = begin; i < end; i++){
        switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){
        case 1: /* l_True: */
            break;
        case 0: /* l_Undef */
            assume(s, *i);
            if (sat_solver_propagate(s) == NULL)
                break;
            // fallthrough
        case -1: /* l_False */
            sat_solver_canceluntil(s, 0);
            return l_False;
        }
    }
    s->nCalls2++;

    s->root_level = sat_solver_dlevel(s);

    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){
        double Ratio = (s->stats.learnts == 0)? 0.0 :
            s->stats.learnts_literals / (double)s->stats.learnts;

        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)nof_learnts, 
                (double)s->stats.learnts, 
                (double)s->stats.learnts_literals,
                Ratio,
                s->progress_estimate*100);
            fflush(stdout);
        }
        status = sat_solver_search(s, nof_conflicts, nof_learnts);
        nof_conflicts = nof_conflicts * 3 / 2; //*= 1.5;
        nof_learnts   = nof_learnts * 11 / 10; //*= 1.1;

        // quit the loop if reached an external limit
        if ( s->nConfLimit && s->stats.conflicts > s->nConfLimit )
        {
//            printf( "Reached the limit on the number of conflicts (%d).\n", s->nConfLimit );
            break;
        }
        if ( s->nInsLimit  && s->stats.inspects > s->nInsLimit )
        {
//            printf( "Reached the limit on the number of implications (%d).\n", s->nInsLimit );
            break;
        }
    }
    if (s->verbosity >= 1)
        printf("==============================================================================\n");

    sat_solver_canceluntil(s,0);

    if ( status == l_False && s->pStore )
    {
        extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
        int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
        assert( RetValue );
    }
    return status;
}

void sat_solver_store_alloc

(

sat_solver *

s

)

Definition at line 1268 of file satSolver.c.

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

void sat_solver_store_free

(

sat_solver *

s

)

Definition at line 1281 of file satSolver.c.

{
    extern void Sto_ManFree( void * p );
    if ( s->pStore ) Sto_ManFree( s->pStore );
    s->pStore = NULL;
}

void sat_solver_store_mark_clauses_a

(

sat_solver *

s

)

Definition at line 1294 of file satSolver.c.

{
    extern void Sto_ManMarkClausesA( void * p );
    if ( s->pStore ) Sto_ManMarkClausesA( s->pStore );
}

void sat_solver_store_mark_roots

(

sat_solver *

s

)

Definition at line 1288 of file satSolver.c.

{
    extern void Sto_ManMarkRoots( void * p );
    if ( s->pStore ) Sto_ManMarkRoots( s->pStore );
}

void* sat_solver_store_release

(

sat_solver *

s

)

Definition at line 1300 of file satSolver.c.

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

void sat_solver_store_write	(	sat_solver *	s,
		char *	pFileName
	)

Definition at line 1275 of file satSolver.c.

{
    extern void Sto_ManDumpClauses( void * p, char * pFileName );
    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
}

void Sat_SolverDoubleClauses	(	sat_solver *	p,
		int	iVar
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 193 of file satUtil.c.

{
    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 = 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;
    }
}

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

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

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 169 of file satUtil.c.

{
    int * pModel;
    int i;
    pModel = ALLOC( int, nVars );
    for ( i = 0; i < nVars; i++ )
    {
        assert( pVars[i] >= 0 && pVars[i] < p->size );
        pModel[i] = (int)(p->model.ptr[pVars[i]] == l_True);
    }
    return pModel;    
}

void Sat_SolverPrintStats	(	FILE *	pFile,
		sat_solver *	p
	)

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

Synopsis [Writes the given clause in a file in DIMACS format.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file satUtil.c.

{
//    printf( "calls         : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 );
    printf( "starts        : %8d\n", (int)p->stats.starts );
    printf( "conflicts     : %8d\n", (int)p->stats.conflicts );
    printf( "decisions     : %8d\n", (int)p->stats.decisions );
    printf( "propagations  : %8d\n", (int)p->stats.propagations );
    printf( "inspects      : %8d\n", (int)p->stats.inspects );
//    printf( "inspects2     : %8d\n", (int)p->stats.inspects2 );
}

void Sat_SolverTraceStart	(	sat_solver *	pSat,
		char *	pName
	)

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

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

Synopsis [Start the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file satTrace.c.

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

void Sat_SolverTraceStop

(

sat_solver *

pSat

)

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

Synopsis [Stops the trace recording.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 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;
}

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

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

Synopsis [Writes one clause into the trace file.]

Description []

SideEffects []

SeeAlso []

Definition at line 94 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" );
}

void Sat_SolverWriteDimacs	(	sat_solver *	p,
		char *	pFileName,
		lit *	assumptionsBegin,
		lit *	assumptionsEnd,
		int	incrementVars
	)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file satUtil.c.

{
    FILE * pFile;
    void ** pClauses;
    int nClauses, i;

    // count the number of clauses
    nClauses = p->clauses.size + p->learnts.size;
    for ( i = 0; i < p->size; i++ )
        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
            nClauses++;

    // start the file
    pFile = fopen( pFileName, "wb" );
    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, nClauses );

    // write the original clauses
    nClauses = p->clauses.size;
    pClauses = p->clauses.ptr;
    for ( i = 0; i < nClauses; i++ )
        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );

    // write the learned clauses
    nClauses = p->learnts.size;
    pClauses = p->learnts.ptr;
    for ( i = 0; i < nClauses; i++ )
        Sat_SolverClauseWriteDimacs( pFile, pClauses[i], incrementVars );

    // write zero-level assertions
    for ( i = 0; i < p->size; i++ )
        if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
            fprintf( pFile, "%s%d%s\n",
                     (p->assigns[i] == l_False)? "-": "",
                     i + (int)(incrementVars>0),
                     (incrementVars) ? " 0" : "");

    // write the assumptions
    if (assumptionsBegin) {
        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
            fprintf( pFile, "%s%d%s\n",
                     lit_sign(*assumptionsBegin)? "-": "",
                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
                     (incrementVars) ? " 0" : "");
        }
    }

    fprintf( pFile, "\n" );
    fclose( pFile );
}   

static lit toLit

(

int

v

)

[inline, static]

Definition at line 67 of file satSolver.h.

{ return v + v; }

static lit toLitCond	(	int	v,
		int	c
	)			[inline, static]

Definition at line 68 of file satSolver.h.

{ return v + v + (c != 0); }

---

Variable Documentation

const bool false = 0 [static]

Definition at line 44 of file satSolver.h.

const lbool l_False = -1 [static]

Definition at line 65 of file satSolver.h.

const lbool l_True = 1 [static]

Definition at line 64 of file satSolver.h.

const lbool l_Undef = 0 [static]

Definition at line 63 of file satSolver.h.

const lit lit_Undef = -2 [static]

Definition at line 61 of file satSolver.h.

const bool true = 1 [static]

Definition at line 43 of file satSolver.h.

const int var_Undef = -1 [static]

Definition at line 60 of file satSolver.h.