satSolver.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satVec.h"
#include "satClause.h"

Go to the source code of this file.

Data Structures
struct	sat_solver_t

Typedefs
typedef struct sat_solver_t	sat_solver
typedef struct varinfo_t	varinfo

Functions
sat_solver *	sat_solver_new (void)
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)
void	sat_solver_restart (sat_solver *s)
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)
void	sat_solver_setnvars (sat_solver *s, int n)
int	sat_solver_get_var_value (sat_solver *s, int v)
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 ///. More...
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)
static clause *	clause_read (sat_solver *s, cla h)
static int	sat_solver_var_value (sat_solver *s, int v)
static int	sat_solver_var_literal (sat_solver *s, int v)
static void	sat_solver_act_var_clear (sat_solver *s)
static void	sat_solver_compress (sat_solver *s)
static int	sat_solver_final (sat_solver *s, int **ppArray)
static abctime	sat_solver_set_runtime_limit (sat_solver *s, abctime Limit)
static int	sat_solver_set_random (sat_solver *s, int fNotUseRandom)
static void	sat_solver_bookmark (sat_solver *s)
static void	sat_solver_set_pivot_variables (sat_solver *s, int *pPivots, int nPivots)
static int	sat_solver_count_usedvars (sat_solver *s)
static int	sat_solver_add_const (sat_solver *pSat, int iVar, int fCompl)
static int	sat_solver_add_buffer (sat_solver *pSat, int iVarA, int iVarB, int fCompl)
static int	sat_solver_add_buffer_enable (sat_solver *pSat, int iVarA, int iVarB, int iVarEn, int fCompl)
static int	sat_solver_add_and (sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl)
static int	sat_solver_add_xor (sat_solver *pSat, int iVarA, int iVarB, int iVarC, int fCompl)
static int	sat_solver_add_mux (sat_solver *pSat, int iVarC, int iVarT, int iVarE, int iVarZ)
static int	sat_solver_add_mux41 (sat_solver *pSat, int iVarC0, int iVarC1, int iVarD0, int iVarD1, int iVarD2, int iVarD3, int iVarZ)
static int	sat_solver_add_xor_and (sat_solver *pSat, int iVarF, int iVarA, int iVarB, int iVarC)
static int	sat_solver_add_constraint (sat_solver *pSat, int iVar, int iVar2, int fCompl)

Typedef Documentation

typedef struct sat_solver_t sat_solver

Definition at line 42 of file satSolver.h.

typedef struct varinfo_t varinfo

Definition at line 89 of file satSolver.h.

Function Documentation

static clause* clause_read ( sat_solver *  s, cla  h  )

inlinestatic

Definition at line 195 of file satSolver.h.

{ 
    return Sat_MemClauseHand( &s->Mem, h );      
}

static void sat_solver_act_var_clear ( sat_solver *  s )

static

Definition at line 210 of file satSolver.h.

{
    int i;
    for (i = 0; i < s->size; i++)
        s->activity[i] = 0;
    s->var_inc = 1;
}

static int sat_solver_add_and ( sat_solver *  pSat, int  iVar, int  iVar0, int  iVar1, int  fCompl0, int  fCompl1, int  fCompl  )

inlinestatic

Definition at line 324 of file satSolver.h.

{
    lit Lits[3];
    int Cid;

    Lits[0] = toLitCond( iVar, !fCompl );
    Lits[1] = toLitCond( iVar0, fCompl0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );

    Lits[0] = toLitCond( iVar, !fCompl );
    Lits[1] = toLitCond( iVar1, fCompl1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );

    Lits[0] = toLitCond( iVar, fCompl );
    Lits[1] = toLitCond( iVar0, !fCompl0 );
    Lits[2] = toLitCond( iVar1, !fCompl1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );
    return 3;
}

static int sat_solver_add_buffer ( sat_solver *  pSat, int  iVarA, int  iVarB, int  fCompl  )

inlinestatic

Definition at line 288 of file satSolver.h.

{
    lit Lits[2];
    int Cid;
    assert( iVarA >= 0 && iVarB >= 0 );

    Lits[0] = toLitCond( iVarA, 0 );
    Lits[1] = toLitCond( iVarB, !fCompl );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );

    Lits[0] = toLitCond( iVarA, 1 );
    Lits[1] = toLitCond( iVarB, fCompl );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );
    return 2;
}

static int sat_solver_add_buffer_enable ( sat_solver *  pSat, int  iVarA, int  iVarB, int  iVarEn, int  fCompl  )

inlinestatic

Definition at line 305 of file satSolver.h.

{
    lit Lits[3];
    int Cid;
    assert( iVarA >= 0 && iVarB >= 0 && iVarEn >= 0 );

    Lits[0] = toLitCond( iVarA, 0 );
    Lits[1] = toLitCond( iVarB, !fCompl );
    Lits[2] = toLitCond( iVarEn, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarA, 1 );
    Lits[1] = toLitCond( iVarB, fCompl );
    Lits[2] = toLitCond( iVarEn, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );
    return 2;
}

static int sat_solver_add_const ( sat_solver *  pSat, int  iVar, int  fCompl  )

inlinestatic

Definition at line 277 of file satSolver.h.

{
    lit Lits[1];
    int Cid;
    assert( iVar >= 0 );

    Lits[0] = toLitCond( iVar, fCompl );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 1 );
    assert( Cid );
    return 1;
}

static int sat_solver_add_constraint ( sat_solver *  pSat, int  iVar, int  iVar2, int  fCompl  )

inlinestatic

Definition at line 526 of file satSolver.h.

{
    lit Lits[2];
    int Cid;
    assert( iVar >= 0 );

    Lits[0] = toLitCond( iVar, fCompl );
    Lits[1] = toLitCond( iVar2, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );

    Lits[0] = toLitCond( iVar, fCompl );
    Lits[1] = toLitCond( iVar2, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );
    return 2;
}

static int sat_solver_add_mux ( sat_solver *  pSat, int  iVarC, int  iVarT, int  iVarE, int  iVarZ  )

inlinestatic

Definition at line 377 of file satSolver.h.

{
    lit Lits[3];
    int Cid;
    assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );

    Lits[0] = toLitCond( iVarC, 1 );
    Lits[1] = toLitCond( iVarT, 1 );
    Lits[2] = toLitCond( iVarZ, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarC, 1 );
    Lits[1] = toLitCond( iVarT, 0 );
    Lits[2] = toLitCond( iVarZ, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarC, 0 );
    Lits[1] = toLitCond( iVarE, 1 );
    Lits[2] = toLitCond( iVarZ, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarC, 0 );
    Lits[1] = toLitCond( iVarE, 0 );
    Lits[2] = toLitCond( iVarZ, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    if ( iVarT == iVarE )
        return 4;

    Lits[0] = toLitCond( iVarT, 0 );
    Lits[1] = toLitCond( iVarE, 0 );
    Lits[2] = toLitCond( iVarZ, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarT, 1 );
    Lits[1] = toLitCond( iVarE, 1 );
    Lits[2] = toLitCond( iVarZ, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );
    return 6;
}

static int sat_solver_add_mux41 ( sat_solver *  pSat, int  iVarC0, int  iVarC1, int  iVarD0, int  iVarD1, int  iVarD2, int  iVarD3, int  iVarZ  )

inlinestatic

Definition at line 423 of file satSolver.h.

{
    lit Lits[4];
    int Cid;
    assert( iVarC0 >= 0 && iVarC1 >= 0 && iVarD0 >= 0 && iVarD1 >= 0 && iVarD2 >= 0 && iVarD3 >= 0 && iVarZ >= 0 );

    Lits[0] = toLitCond( iVarD0, 1 );
    Lits[1] = toLitCond( iVarC0, 0 );
    Lits[2] = toLitCond( iVarC1, 0 );
    Lits[3] = toLitCond( iVarZ,  0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD1, 1 );
    Lits[1] = toLitCond( iVarC0, 1 );
    Lits[2] = toLitCond( iVarC1, 0 );
    Lits[3] = toLitCond( iVarZ,  0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD2, 1 );
    Lits[1] = toLitCond( iVarC0, 0 );
    Lits[2] = toLitCond( iVarC1, 1 );
    Lits[3] = toLitCond( iVarZ,  0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD3, 1 );
    Lits[1] = toLitCond( iVarC0, 1 );
    Lits[2] = toLitCond( iVarC1, 1 );
    Lits[3] = toLitCond( iVarZ,  0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );


    Lits[0] = toLitCond( iVarD0, 0 );
    Lits[1] = toLitCond( iVarC0, 0 );
    Lits[2] = toLitCond( iVarC1, 0 );
    Lits[3] = toLitCond( iVarZ,  1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD1, 0 );
    Lits[1] = toLitCond( iVarC0, 1 );
    Lits[2] = toLitCond( iVarC1, 0 );
    Lits[3] = toLitCond( iVarZ,  1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD2, 0 );
    Lits[1] = toLitCond( iVarC0, 0 );
    Lits[2] = toLitCond( iVarC1, 1 );
    Lits[3] = toLitCond( iVarZ,  1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarD3, 0 );
    Lits[1] = toLitCond( iVarC0, 1 );
    Lits[2] = toLitCond( iVarC1, 1 );
    Lits[3] = toLitCond( iVarZ,  1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );
    return 8;
}

static int sat_solver_add_xor ( sat_solver *  pSat, int  iVarA, int  iVarB, int  iVarC, int  fCompl  )

inlinestatic

Definition at line 346 of file satSolver.h.

{
    lit Lits[3];
    int Cid;
    assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );

    Lits[0] = toLitCond( iVarA, !fCompl );
    Lits[1] = toLitCond( iVarB, 1 );
    Lits[2] = toLitCond( iVarC, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarA, !fCompl );
    Lits[1] = toLitCond( iVarB, 0 );
    Lits[2] = toLitCond( iVarC, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarA, fCompl );
    Lits[1] = toLitCond( iVarB, 1 );
    Lits[2] = toLitCond( iVarC, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarA, fCompl );
    Lits[1] = toLitCond( iVarB, 0 );
    Lits[2] = toLitCond( iVarC, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );
    return 4;
}

static int sat_solver_add_xor_and ( sat_solver *  pSat, int  iVarF, int  iVarA, int  iVarB, int  iVarC  )

inlinestatic

Definition at line 487 of file satSolver.h.

{
    // F = (a (+) b) * c
    lit Lits[4];
    int Cid;
    assert( iVarF >= 0 && iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );

    Lits[0] = toLitCond( iVarF, 1 );
    Lits[1] = toLitCond( iVarA, 1 );
    Lits[2] = toLitCond( iVarB, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarF, 1 );
    Lits[1] = toLitCond( iVarA, 0 );
    Lits[2] = toLitCond( iVarB, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
    assert( Cid );

    Lits[0] = toLitCond( iVarF, 1 );
    Lits[1] = toLitCond( iVarC, 0 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
    assert( Cid );

    Lits[0] = toLitCond( iVarF, 0 );
    Lits[1] = toLitCond( iVarA, 1 );
    Lits[2] = toLitCond( iVarB, 0 );
    Lits[3] = toLitCond( iVarC, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );

    Lits[0] = toLitCond( iVarF, 0 );
    Lits[1] = toLitCond( iVarA, 0 );
    Lits[2] = toLitCond( iVarB, 1 );
    Lits[3] = toLitCond( iVarC, 1 );
    Cid = sat_solver_addclause( pSat, Lits, Lits + 4 );
    assert( Cid );
    return 5;
}

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

Definition at line 1492 of file satSolver.c.

{
    int fVerbose = 0;
    lit *i,*j;
    int maxvar;
    lit last;
    assert( begin < end );
    if ( fVerbose )
    {
        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;
}

static void sat_solver_bookmark ( sat_solver *  s )

inlinestatic

Definition at line 247 of file satSolver.h.

{
    assert( s->qhead == s->qtail );
    s->iVarPivot    = s->size;
    s->iTrailPivot  = s->qhead;
    Sat_MemBookMark( &s->Mem );
    if ( s->activity2 )
    {
        s->var_inc2 = s->var_inc;
        memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
    }
}

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

Definition at line 402 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));
        veci_push(&s->act_clas, (1<<10));
        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;
}

static void sat_solver_compress ( sat_solver *  s )

static

Definition at line 217 of file satSolver.h.

{
    if ( s->qtail != s->qhead )
    {
        int RetValue = sat_solver_simplify(s);
        assert( RetValue != 0 );
        (void) RetValue;
    }
}

int sat_solver_count_assigned

(

sat_solver *

s

)

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

static int sat_solver_count_usedvars ( sat_solver *  s )

inlinestatic

Definition at line 265 of file satSolver.h.

{
    int i, nVars = 0;
    for ( i = 0; i < s->size; i++ )
        if ( s->pFreqs[i] )
        {
            s->pFreqs[i] = 0;
            nVars++;
        }
    return nVars;
}

void sat_solver_delete

(

sat_solver *

s

)

Definition at line 1141 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);

    // 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);
}

static int sat_solver_final ( sat_solver *  s, int **  ppArray  )

static

Definition at line 227 of file satSolver.h.

{
    *ppArray = s->conf_final.ptr;
    return s->conf_final.size;
}

int sat_solver_get_var_value	(	sat_solver *	s,
		int	v
	)

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

double sat_solver_memory

(

sat_solver *

s

)

Definition at line 1236 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    );
#ifdef USE_FLOAT_ACTIVITY
    Mem += s->cap * sizeof(double);   // ABC_FREE(s->activity );
#else
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
    if ( s->activity2 )
    Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
#endif
    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;
}

int sat_solver_nclauses

(

sat_solver *

s

)

Definition at line 1902 of file satSolver.c.

{
    return s->stats.clauses;
}

int sat_solver_nconflicts

(

sat_solver *

s

)

Definition at line 1908 of file satSolver.c.

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

sat_solver* sat_solver_new

(

void

)

Definition at line 1001 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->act_vars);
    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;
#ifdef USE_FLOAT_ACTIVITY
    s->var_inc                = 1;
    s->cla_inc                = 1;
    s->var_decay              = (float)(1 / 0.95 );
    s->cla_decay              = (float)(1 / 0.999);
#else
    s->var_inc                = (1 <<  5);
    s->cla_inc                = (1 << 11);
#endif
    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;
}

int sat_solver_nvars

(

sat_solver *

s

)

Definition at line 1896 of file satSolver.c.

{
    return s->size;
}

void sat_solver_restart

(

sat_solver *

s

)

Definition at line 1186 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->act_clas, 0);
    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;
#ifdef USE_FLOAT_ACTIVITY
    s->var_inc                = 1;
    s->cla_inc                = 1;
    s->var_decay              = (float)(1 / 0.95  );
    s->cla_decay              = (float)(1 / 0.999 );
#else
    s->var_inc                = (1 <<  5);
    s->cla_inc                = (1 << 11);
#endif
    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;
}

void sat_solver_rollback

(

sat_solver *

s

)

Definition at line 1401 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(unsigned) * 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 ( 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;
#ifdef USE_FLOAT_ACTIVITY
        s->var_inc                = 1;
        s->cla_inc                = 1;
        s->var_decay              = (float)(1 / 0.95  );
        s->cla_decay              = (float)(1 / 0.999 );
#else
        s->var_inc                = (1 <<  5);
        s->cla_inc                = (1 << 11);
#endif
        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
    }
}

static void sat_solver_set_pivot_variables ( sat_solver *  s, int *  pPivots, int  nPivots  )

inlinestatic

Definition at line 259 of file satSolver.h.

{
    s->pivot_vars.cap = nPivots;
    s->pivot_vars.size = nPivots;
    s->pivot_vars.ptr = pPivots;
}

static int sat_solver_set_random ( sat_solver *  s, int  fNotUseRandom  )

static

Definition at line 240 of file satSolver.h.

{
    int fNotUseRandomOld = s->fNotUseRandom;
    s->fNotUseRandom = fNotUseRandom;
    return fNotUseRandomOld;
}

static abctime sat_solver_set_runtime_limit ( sat_solver *  s, abctime  Limit  )

static

Definition at line 233 of file satSolver.h.

{
    abctime nRuntimeLimit = s->nRuntimeLimit;
    s->nRuntimeLimit = Limit;
    return nRuntimeLimit;
}

void sat_solver_setnvars	(	sat_solver *	s,
		int	n
	)

Definition at line 1072 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);
#ifdef USE_FLOAT_ACTIVITY
        s->activity  = ABC_REALLOC(double,   s->activity, s->cap);
#else
        s->activity  = ABC_REALLOC(unsigned, s->activity, s->cap);
        s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
#endif
        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]);
#ifdef USE_FLOAT_ACTIVITY
        s->activity[var] = 0;
#else
        s->activity[var] = (1<<10);
#endif
        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;
}

int sat_solver_simplify

(

sat_solver *

s

)

Definition at line 1276 of file satSolver.c.

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

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
	)

Definition at line 1700 of file satSolver.c.

{
    int restart_iter = 0;
    ABC_INT64_T  nof_conflicts;
//    ABC_INT64_T  nof_learnts   = sat_solver_nclauses(s) / 3;
    lbool   status        = l_Undef;
    lit*    i;

    if ( s->fVerbose )
        printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );

    ////////////////////////////////////////////////
    if ( s->fSolved )
    {
        if ( s->pStore )
        {
            int RetValue = Sto_ManAddClause( (Sto_Man_t *)s->pStore, NULL, NULL );
            assert( RetValue );
            (void) RetValue;
        }
        return l_False;
    }
    ////////////////////////////////////////////////
    veci_resize(&s->unit_lits, 0);

    // 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;
        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;

#ifndef SAT_USE_ANALYZE_FINAL

    //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_assume(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

/*
    // Perform assumptions:
    root_level = assumps.size();
    for (int i = 0; i < assumps.size(); i++){
        Lit p = assumps[i];
        assert(var(p) < nVars());
        if (!sat_solver_assume(p)){
            GClause r = reason[var(p)];
            if (r != GClause_NULL){
                Clause* confl;
                if (r.isLit()){
                    confl = propagate_tmpbin;
                    (*confl)[1] = ~p;
                    (*confl)[0] = r.lit();
                }else
                    confl = r.clause();
                analyzeFinal(confl, true);
                conflict.push(~p);
            }else
                conflict.clear(),
                conflict.push(~p);
            cancelUntil(0);
            return false; }
        Clause* confl = propagate();
        if (confl != NULL){
            analyzeFinal(confl), assert(conflict.size() > 0);
            cancelUntil(0);
            return false; }
    }
    assert(root_level == decisionLevel());
*/

#ifdef SAT_USE_ANALYZE_FINAL
    // Perform assumptions:
    s->root_level = end - begin;
    for ( i = begin; i < end; i++ )
    {
        lit p = *i;
        assert(lit_var(p) < s->size);
        veci_push(&s->trail_lim,s->qtail);
        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 l_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 l_False; }
        }
    }
    assert(s->root_level == sat_solver_dl(s));
#endif

    s->nCalls2++;

    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->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)nof_learnts, 
                (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);
//        nof_learnts    = nof_learnts * 11 / 10; //*= 1.1;
        // 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->verbosity >= 1)
        printf("==============================================================================\n");

    sat_solver_canceluntil(s,0);

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

void sat_solver_store_alloc

(

sat_solver *

s

)

Definition at line 1916 of file satSolver.c.

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

void sat_solver_store_free

(

sat_solver *

s

)

Definition at line 1927 of file satSolver.c.

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

void sat_solver_store_mark_clauses_a

(

sat_solver *

s

)

Definition at line 1944 of file satSolver.c.

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

void sat_solver_store_mark_roots

(

sat_solver *

s

)

Definition at line 1939 of file satSolver.c.

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

void* sat_solver_store_release

(

sat_solver *

s

)

Definition at line 1949 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 1922 of file satSolver.c.

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

static int sat_solver_var_literal ( sat_solver *  s, int  v  )

static

Definition at line 205 of file satSolver.h.

{
    assert( v >= 0 && v < s->size );
    return toLitCond( v, s->model[v] != l_True );
}

static int sat_solver_var_value ( sat_solver *  s, int  v  )

static

Definition at line 200 of file satSolver.h.

{
    assert( v >= 0 && v < s->size );
    return (int)(s->model[v] == l_True);
}

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 308 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;
    }
*/
}

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

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

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

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

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 188 of file satUtil.c.

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

void Sat_SolverTraceStart	(	sat_solver *	pSat,
		char *	pName
	)

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

void Sat_SolverTraceStop

(

sat_solver *

pSat

)

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

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 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" );
}

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

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 71 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 = 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, 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" );
    fclose( pFile );
}