satSolver2.h File Reference

#include <stdio.h>
#include <stdlib.h>
#include <string.h>
#include <assert.h>
#include "satVec.h"
#include "satClause.h"
#include "misc/vec/vecSet.h"
#include "satProof2.h"

Include dependency graph for satSolver2.h:

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

Go to the source code of this file.

Classes
struct	sat_solver2_t

Typedefs
typedef struct sat_solver2_t	sat_solver2
typedef struct Int2_Man_t_	Int2_Man_t
typedef struct varinfo2_t	varinfo2

Functions
sat_solver2 *	sat_solver2_new (void)
void	sat_solver2_delete (sat_solver2 *s)
int	sat_solver2_addclause (sat_solver2 *s, lit *begin, lit *end, int Id)
int	sat_solver2_simplify (sat_solver2 *s)
int	sat_solver2_solve (sat_solver2 *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
void	sat_solver2_rollback (sat_solver2 *s)
void	sat_solver2_reducedb (sat_solver2 *s)
double	sat_solver2_memory (sat_solver2 *s, int fAll)
double	sat_solver2_memory_proof (sat_solver2 *s)
void	sat_solver2_setnvars (sat_solver2 *s, int n)
void	Sat_Solver2WriteDimacs (sat_solver2 *p, char *pFileName, lit *assumptionsBegin, lit *assumptionsEnd, int incrementVars)
void	Sat_Solver2PrintStats (FILE *pFile, sat_solver2 *p)
int *	Sat_Solver2GetModel (sat_solver2 *p, int *pVars, int nVars)
void	Sat_Solver2DoubleClauses (sat_solver2 *p, int iVar)
int	var_is_assigned (sat_solver2 *s, int v)
int	var_is_partA (sat_solver2 *s, int v)
void	var_set_partA (sat_solver2 *s, int v, int partA)
void *	Sat_ProofCore (sat_solver2 *s)
void *	Sat_ProofInterpolant (sat_solver2 *s, void *pGloVars)
word *	Sat_ProofInterpolantTruth (sat_solver2 *s, void *pGloVars)
void	Sat_ProofCheck (sat_solver2 *s)
Int2_Man_t *	Int2_ManStart (sat_solver2 *pSat, int *pGloVars, int nGloVars)
	FUNCTION DEFINITIONS ///.
void	Int2_ManStop (Int2_Man_t *p)
int	Int2_ManChainStart (Int2_Man_t *p, clause *c)
int	Int2_ManChainResolve (Int2_Man_t *p, clause *c, int iLit, int varA)
void *	Int2_ManReadInterpolant (sat_solver2 *s)

Typedef Documentation

Int2_Man_t

typedef struct Int2_Man_t_ Int2_Man_t

Definition at line 45 of file satSolver2.h.

sat_solver2

typedef struct sat_solver2_t sat_solver2

Definition at line 44 of file satSolver2.h.

varinfo2

typedef struct varinfo2_t varinfo2

Definition at line 88 of file satSolver2.h.

Function Documentation

Int2_ManChainResolve()

int Int2_ManChainResolve ( Int2_Man_t * p, clause * c, int iLit, int varA )

extern

Definition at line 134 of file satSolver2i.c.

{
    int iLit2 = Int2_ManChainStart( p, c );
    assert( iLit >= 0 );
    if ( varA )
        iLit = Gia_ManHashOr( p->pGia, iLit, iLit2 );
    else
        iLit = Gia_ManHashAnd( p->pGia, iLit, iLit2 );
    return iLit;
}

Here is the call graph for this function:

Int2_ManChainStart()

int Int2_ManChainStart ( Int2_Man_t * p, clause * c )

extern

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

Synopsis [Computing interpolant for a clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 108 of file satSolver2i.c.

{
    if ( c->lrn )
        return veci_begin(&p->pSat->claProofs)[clause_id(c)];
    if ( !c->partA )
        return 1;
    if ( c->lits[c->size] < 0 )
    {
        int i, Var, CiId, Res = 0;
        for ( i = 0; i < (int)c->size; i++ )
        {
            // get ID of the global variable
            if ( Abc_Lit2Var(c->lits[i]) >= Vec_IntSize(p->vVar2Glo) )
                continue;
            Var = Vec_IntEntry( p->vVar2Glo, Abc_Lit2Var(c->lits[i]) );
            if ( Var < 0 )
                continue;
            // get literal of the AIG node
            CiId = Gia_ObjId( p->pGia, Gia_ManCi(p->pGia, Var) );
            // compute interpolant of the clause
            Res = Gia_ManHashOr( p->pGia, Res, Abc_Var2Lit(CiId, Abc_LitIsCompl(c->lits[i])) );
        }
        c->lits[c->size] = Res;
    }
    return c->lits[c->size];
}

Here is the call graph for this function:

Here is the caller graph for this function:

Int2_ManReadInterpolant()

void * Int2_ManReadInterpolant ( sat_solver2 * s )

extern

Definition at line 80 of file satSolver2i.c.

{
    Int2_Man_t * p = pSat->pInt2;
    Gia_Man_t * pTemp, * pGia = p->pGia; p->pGia = NULL;
    // return NULL, if the interpolant is not ready (for example, when the solver returned 'sat')
    if ( pSat->hProofLast == -1 )
        return NULL;
    // create AIG with one primary output
    assert( Gia_ManPoNum(pGia) == 0 );
    Gia_ManAppendCo( pGia, pSat->hProofLast );  
    pSat->hProofLast = -1;
    // cleanup the resulting AIG
    pGia = Gia_ManCleanup( pTemp = pGia );
    Gia_ManStop( pTemp );
    return (void *)pGia;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Int2_ManStart()

Int2_Man_t * Int2_ManStart ( sat_solver2 * pSat, int * pGloVars, int nGloVars )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Managing interpolation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file satSolver2i.c.

{
    Int2_Man_t * p;
    int i;
    p = ABC_CALLOC( Int2_Man_t, 1 );
    p->pSat     = pSat;
    p->vGloVars = Vec_IntAllocArrayCopy( pGloVars, nGloVars );
    p->vVar2Glo = Vec_IntInvert( p->vGloVars, -1 );
    p->pGia     = Gia_ManStart( 10 * Vec_IntSize(p->vGloVars) );
    p->pGia->pName = Abc_UtilStrsav( "interpolant" );
    for ( i = 0; i < nGloVars; i++ )
        Gia_ManAppendCi( p->pGia );
    Gia_ManHashStart( p->pGia );
    return p;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Int2_ManStop()

void Int2_ManStop ( Int2_Man_t * p )

extern

Definition at line 71 of file satSolver2i.c.

{
    if ( p == NULL )
        return;
    Gia_ManStopP( &p->pGia );
    Vec_IntFree( p->vGloVars );
    Vec_IntFree( p->vVar2Glo );
    ABC_FREE( p );
}

Here is the call graph for this function:

Sat_ProofCheck()

void Sat_ProofCheck ( sat_solver2 * s )

extern

Sat_ProofCore()

void * Sat_ProofCore ( sat_solver2 * s )

extern

Definition at line 1985 of file satSolver2.c.

{
    extern void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot );
    if ( s->pPrf1 )
        return Proof_DeriveCore( s->pPrf1, s->hProofLast );
    if ( s->pPrf2 )
    {
        s->dPrfMemory = Abc_MaxDouble( s->dPrfMemory, Prf_ManMemory(s->pPrf2) );
        return Prf_ManUnsatCore( s->pPrf2 );
    }
    return NULL;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sat_ProofInterpolant()

void * Sat_ProofInterpolant ( sat_solver2 * s, void * pGloVars )

extern

Here is the caller graph for this function:

Sat_ProofInterpolantTruth()

word * Sat_ProofInterpolantTruth ( sat_solver2 * s, void * pGloVars )

extern

sat_solver2_addclause()

int sat_solver2_addclause ( sat_solver2 * s, lit * begin, lit * end, int Id )

extern

Definition at line 1287 of file satSolver2.c.

{
    cla Cid;
    lit *i,*j,*iFree = NULL;
    int maxvar, count, temp;
    assert( solver2_dlevel(s) == 0 );
    assert( begin < end );
    assert( Id != 0 );
 
    // copy clause into storage
    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_solver2_setnvars(s,maxvar+1);
 
 
    // delete duplicates
    for (i = j = begin + 1; i < end; i++)
    {
        if ( *(i-1) == lit_neg(*i) ) // tautology
            return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
        if ( *(i-1) != *i )
            *j++ = *i;
    }
    end = j;
    assert( begin < end );
 
    // coount the number of 0-literals
    count = 0;
    for ( i = begin; i < end; i++ )
    {
        // make sure all literals are unique
        assert( i == begin || lit_var(*(i-1)) != lit_var(*i) );
        // consider the value of this literal
        if ( var_value(s, lit_var(*i)) == lit_sign(*i) ) // this clause is always true
            return clause2_create_new( s, begin, end, 0, 0 ); // add it anyway, to preserve proper clause count       
        if ( var_value(s, lit_var(*i)) == varX ) // unassigned literal
            iFree = i;
        else
            count++; // literal is 0
    }
    assert( count < end-begin ); // the clause cannot be UNSAT
 
    // swap variables to make sure the clause is watched using unassigned variable
    temp   = *iFree;
    *iFree = *begin;
    *begin = temp;
 
    // create a new clause
    Cid = clause2_create_new( s, begin, end, 0, 0 );
    if ( Id )
        clause2_set_id( s, Cid, Id );
 
    // handle unit clause
    if ( count+1 == end-begin )
    {
        if ( s->fProofLogging )
        {
            if ( count == 0 ) // original learned clause
            {
                var_set_unit_clause( s, lit_var(begin[0]), Cid );
                if ( !solver2_enqueue(s,begin[0],0) )
                    assert( 0 );
            }
            else
            {
                // Log production of top-level unit clause:
                int x, k, proof_id, CidNew;
                clause* c = clause2_read(s, Cid);
                proof_chain_start( s, c );
                clause_foreach_var( c, x, k, 1 )
                    proof_chain_resolve( s, NULL, x );
                proof_id = proof_chain_stop( s );
                // generate a new clause
                CidNew = clause2_create_new( s, begin, begin+1, 1, proof_id );
                var_set_unit_clause( s, lit_var(begin[0]), CidNew );
                if ( !solver2_enqueue(s,begin[0],Cid) )
                    assert( 0 );
            }
        }
    }
    return Cid;
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_delete()

void sat_solver2_delete ( sat_solver2 * s )

extern

Definition at line 1225 of file satSolver2.c.

{
    int fVerify = 0;
    if ( fVerify )
    {
        veci * pCore = (veci *)Sat_ProofCore( s );
//        Abc_Print(1, "UNSAT core contains %d clauses (%6.2f %%).\n", veci_size(pCore), 100.0*veci_size(pCore)/veci_size(&s->clauses) );
        veci_delete( pCore );
        ABC_FREE( pCore );
//        if ( s->fProofLogging )
//            Sat_ProofCheck( s );
    }
 
    // report statistics
//    Abc_Print(1, "Used %6.2f MB for proof-logging.   Unit clauses = %d.\n", 1.0 * Vec_ReportMemory(&s->Proofs) / (1<<20), s->nUnits );
 
    // delete vectors
    veci_delete(&s->order);
    veci_delete(&s->trail_lim);
    veci_delete(&s->tagged);
    veci_delete(&s->stack);
    veci_delete(&s->temp_clause);
    veci_delete(&s->temp_proof);
    veci_delete(&s->conf_final);
    veci_delete(&s->mark_levels);
    veci_delete(&s->min_lit_order);
    veci_delete(&s->min_step_order);
//    veci_delete(&s->learnt_live);
    veci_delete(&s->act_clas);
    veci_delete(&s->claProofs);
//    veci_delete(&s->clauses);
//    veci_delete(&s->lrns);
    Sat_MemFree_( &s->Mem );
//    veci_delete(&s->proofs);
    Vec_SetFree( s->pPrf1 );
    Prf_ManStop( s->pPrf2 );
    Int2_ManStop( s->pInt2 );
 
    // delete arrays
    if (s->vi != 0){
        int i;
        if ( s->wlists )
            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->trail    );
        ABC_FREE(s->orderpos );
        ABC_FREE(s->reasons  );
        ABC_FREE(s->units    );
        ABC_FREE(s->activity );
        ABC_FREE(s->activity2);
        ABC_FREE(s->model    );
    }
    ABC_FREE(s);
 
//    Abc_PrintTime( 1, "Time", Time );
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_memory()

double sat_solver2_memory ( sat_solver2 * s, int fAll )

extern

Definition at line 1692 of file satSolver2.c.

{
    int i;
    double Mem = sizeof(sat_solver2);
    if ( fAll )
        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->act_clas.cap * sizeof(int);
    Mem += s->claProofs.cap * sizeof(int);
//    Mem += s->cap * sizeof(char);     // ABC_FREE(s->polarity );
//    Mem += s->cap * sizeof(char);     // ABC_FREE(s->tags     );
    Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi       );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->levels   );
    Mem += s->cap * sizeof(char);     // ABC_FREE(s->assigns  );
#ifdef USE_FLOAT_ACTIVITY2
    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
    Mem += s->cap * sizeof(lit);      // ABC_FREE(s->trail    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->orderpos );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->reasons  );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->units    );
    Mem += s->cap * sizeof(int);      // ABC_FREE(s->model    );
    Mem += s->tagged.cap * sizeof(int);
    Mem += s->stack.cap * sizeof(int);
    Mem += s->order.cap * sizeof(int);
    Mem += s->trail_lim.cap * sizeof(int);
    Mem += s->temp_clause.cap * sizeof(int);
    Mem += s->conf_final.cap * sizeof(int);
    Mem += s->mark_levels.cap * sizeof(int);
    Mem += s->min_lit_order.cap * sizeof(int);
    Mem += s->min_step_order.cap * sizeof(int);
    Mem += s->temp_proof.cap * sizeof(int);
    Mem += Sat_MemMemoryAll( &s->Mem );
//    Mem += Vec_ReportMemory( s->pPrf1 );
    return Mem;
}

Here is the caller graph for this function:

sat_solver2_memory_proof()

double sat_solver2_memory_proof ( sat_solver2 * s )

extern

Definition at line 1733 of file satSolver2.c.

{
    double Mem = s->dPrfMemory;
    if ( s->pPrf1 )
        Mem += Vec_ReportMemory( s->pPrf1 );
    return Mem;
}

Here is the caller graph for this function:

sat_solver2_new()

sat_solver2 * sat_solver2_new ( void )

extern

Definition at line 1109 of file satSolver2.c.

{
    sat_solver2* s = (sat_solver2 *)ABC_CALLOC( char, sizeof(sat_solver2) );
 
#ifdef USE_FLOAT_ACTIVITY2
    s->var_inc        = 1;
    s->cla_inc        = 1;
    s->var_decay      = (float)(1 / 0.95  );
    s->cla_decay      = (float)(1 / 0.999 );
//    s->cla_decay      = 1;
//    s->var_decay      = 1;
#else
    s->var_inc        = (1 <<  5);
    s->cla_inc        = (1 << 11);
#endif
    s->random_seed    = 91648253;
 
#ifdef SAT_USE_PROOF_LOGGING
    s->fProofLogging  =  1;
#else
    s->fProofLogging  =  0;
#endif
    s->fSkipSimplify  =  1;
    s->fNotUseRandom  =  0;
    s->fVerbose       =  0;
 
    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->stack);
    veci_new(&s->temp_clause);
    veci_new(&s->temp_proof);
    veci_new(&s->conf_final);
    veci_new(&s->mark_levels);
    veci_new(&s->min_lit_order);
    veci_new(&s->min_step_order);
//    veci_new(&s->learnt_live);
    Sat_MemAlloc_( &s->Mem, 14 );
    veci_new(&s->act_clas);  
    // proof-logging
    veci_new(&s->claProofs);
//    s->pPrf1 = Vec_SetAlloc( 20 );
    s->tempInter = -1;
 
    // initialize clause pointers
    s->hLearntLast            = -1; // the last learnt clause 
    s->hProofLast             = -1; // the last proof ID
    // initialize rollback
    s->iVarPivot              =  0; // the pivot for variables
    s->iTrailPivot            =  0; // the pivot for trail
    s->hProofPivot            =  1; // the pivot for proof records
    return s;
}

Here is the caller graph for this function:

sat_solver2_reducedb()

void sat_solver2_reducedb ( sat_solver2 * s )

extern

Definition at line 1406 of file satSolver2.c.

{
    static abctime TimeTotal = 0;
    Sat_Mem_t * pMem = &s->Mem;
    clause * c = NULL;
    int nLearnedOld = veci_size(&s->act_clas);
    int * act_clas = veci_begin(&s->act_clas);
    int * pPerm, * pSortValues, nCutoffValue, * pClaProofs;
    int i, j, k, Id, nSelected;//, LastSize = 0;
    int Counter, CounterStart;
    abctime clk = Abc_Clock();
    static int Count = 0;
    Count++;
    assert( s->nLearntMax );
    s->nDBreduces++;
//    printf( "Calling reduceDB with %d clause limit and parameters (%d %d %d).\n", s->nLearntMax, s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
 
/*
    // find the new limit
    s->nLearntMax = s->nLearntMax * 11 / 10;
    // preserve 1/10 of last clauses
    CounterStart  = s->stats.learnts - (s->nLearntMax / 10);
    // preserve 1/10 of most active clauses
    pSortValues = veci_begin(&s->act_clas);
    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
    nCutoffValue = pSortValues[pPerm[nLearnedOld*9/10]];
    ABC_FREE( pPerm );
//    nCutoffValue = ABC_INFINITY;
*/
 
 
    // find the new limit
    s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
    // preserve 1/20 of last clauses
    CounterStart  = nLearnedOld - (s->nLearntMax / 20);
    // preserve 3/4 of most active clauses
    nSelected = nLearnedOld*s->nLearntRatio/100;
    // create sorting values
    pSortValues = ABC_ALLOC( int, nLearnedOld );
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        Id = clause_id(c);
        pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4));
//        pSortValues[Id] = act_clas[Id];
        assert( pSortValues[Id] >= 0 );
    }
    // find non-decreasing permutation
    pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
    assert( pSortValues[pPerm[0]] <= pSortValues[pPerm[nLearnedOld-1]] );
    nCutoffValue = pSortValues[pPerm[nLearnedOld-nSelected]];
    ABC_FREE( pPerm );
//    nCutoffValue = ABC_INFINITY;
 
    // count how many clauses satisfy the condition
    Counter = j = 0;
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        assert( c->mark == 0 );
        if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
        {
        }
        else
            j++;
        if ( j >= nLearnedOld / 6 )
            break;
    }
    if ( j < nLearnedOld / 6 )
    {
        ABC_FREE( pSortValues );
        return;
    }
 
    // mark learned clauses to remove
    Counter = j = 0;
    pClaProofs = veci_size(&s->claProofs) ? veci_begin(&s->claProofs) : NULL;
    Sat_MemForEachLearned( pMem, c, i, k )
    {
        assert( c->mark == 0 );
        if ( Counter++ > CounterStart || clause_size(c) < 2 || pSortValues[clause_id(c)] >= nCutoffValue || s->reasons[lit_var(c->lits[0])] == Sat_MemHand(pMem, i, k) )
        {
            pSortValues[j] = pSortValues[clause_id(c)];
            if ( pClaProofs ) 
                pClaProofs[j] = pClaProofs[clause_id(c)];
            if ( s->pPrf2 )
                Prf_ManAddSaved( s->pPrf2, clause_id(c), j );
            j++;
        }
        else // delete
        {
            c->mark = 1;
            s->stats.learnts_literals -= clause_size(c);
            s->stats.learnts--;
        }
    }
    ABC_FREE( pSortValues );
    if ( s->pPrf2 )
        Prf_ManCompact( s->pPrf2, j );
//    if ( j == nLearnedOld )
//        return;
 
    assert( s->stats.learnts == (unsigned)j );
    assert( Counter == nLearnedOld );
    veci_resize(&s->act_clas,j);
    if ( veci_size(&s->claProofs) )
        veci_resize(&s->claProofs,j);
 
    // update ID of each clause to be its new handle
    Counter = Sat_MemCompactLearned( pMem, 0 );
    assert( Counter == (int)s->stats.learnts );
 
    // update reasons
    for ( i = 0; i < s->size; i++ )
    {
        if ( !s->reasons[i] ) // no reason
            continue;
        if ( clause_is_lit(s->reasons[i]) ) // 2-lit clause
            continue;
        if ( !clause_learnt_h(pMem, s->reasons[i]) ) // problem clause
            continue;
        assert( c->lrn );
        c = clause2_read( s, s->reasons[i] );
        assert( c->mark == 0 );
        s->reasons[i] = clause_id(c); // updating handle here!!!
    }
 
    // update watches
    for ( i = 0; i < s->size*2; i++ )
    {
        int * pArray = veci_begin(&s->wlists[i]);
        for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
        {
            if ( clause_is_lit(pArray[k]) ) // 2-lit clause
                pArray[j++] = pArray[k];
            else if ( !clause_learnt_h(pMem, pArray[k]) ) // problem clause
                pArray[j++] = pArray[k];
            else 
            {
                assert( c->lrn );
                c = clause2_read(s, pArray[k]);
                if ( !c->mark ) // useful learned clause
                   pArray[j++] = clause_id(c); // updating handle here!!!
            }
        }
        veci_resize(&s->wlists[i],j);
    }
 
    // compact units
    if ( s->fProofLogging )
        for ( i = 0; i < s->size; i++ )
            if ( s->units[i] && clause_learnt_h(pMem, s->units[i]) )
            {
                assert( c->lrn );
                c = clause2_read( s, s->units[i] );
                assert( c->mark == 0 );
                s->units[i] = clause_id(c);
            }
 
    // perform final move of the clauses
    Counter = Sat_MemCompactLearned( pMem, 1 );
    assert( Counter == (int)s->stats.learnts );
 
    // compact proof (compacts 'proofs' and update 'claProofs')
    if ( s->pPrf1 )
    {
        extern int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot );
        s->hProofPivot = Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
    }
 
    // report the results
    TimeTotal += Abc_Clock() - clk;
    if ( s->fVerbose )
    {
        Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
            s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );
        Abc_PrintTime( 1, "Time", TimeTotal );
    }
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_rollback()

void sat_solver2_rollback ( sat_solver2 * s )

extern

Definition at line 1586 of file satSolver2.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 );
    assert( s->pPrf1 == NULL || (s->hProofPivot >= 1 && s->hProofPivot <= Vec_SetHandCurrent(s->pPrf1)) );
    // reset implication queue
    solver2_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);
    if ( s->pPrf1 ) 
    {
        veci_resize(&s->claProofs, s->stats.learnts);
        Vec_SetShrink(s->pPrf1, s->hProofPivot); 
        // some weird bug here, which shows only on 64-bits!
        // temporarily, perform more general proof reduction
//        Sat_ProofReduce( s->pPrf1, &s->claProofs, s->hProofPivot );
    }
    assert( s->pPrf2 == NULL );
//    if ( s->pPrf2 )
//        Prf_ManShrink( s->pPrf2, 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_ACTIVITY2
        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 clause pointers
        s->hLearntLast            = -1; // the last learnt clause 
        s->hProofLast             = -1; // the last proof ID
 
        // 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_solver2_setnvars()

void sat_solver2_setnvars ( sat_solver2 * s, int n )

extern

Definition at line 1170 of file satSolver2.c.

{
    int var;
 
    if (s->cap < n){
        int old_cap = s->cap;
        while (s->cap < n) s->cap = s->cap*2+1;
 
        s->wlists    = ABC_REALLOC(veci,     s->wlists,   s->cap*2);
        s->vi        = ABC_REALLOC(varinfo2, s->vi,       s->cap);
        s->levels    = ABC_REALLOC(int,      s->levels,   s->cap);
        s->assigns   = ABC_REALLOC(char,     s->assigns,  s->cap);
        s->trail     = ABC_REALLOC(lit,      s->trail,    s->cap);
        s->orderpos  = ABC_REALLOC(int,      s->orderpos, s->cap);
        s->reasons   = ABC_REALLOC(cla,      s->reasons,  s->cap);
        if ( s->fProofLogging )
        s->units     = ABC_REALLOC(cla,      s->units,    s->cap);
#ifdef USE_FLOAT_ACTIVITY2
        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->model     = ABC_REALLOC(int,      s->model,    s->cap);
        memset( s->wlists + 2*old_cap, 0, 2*(s->cap-old_cap)*sizeof(vecp) );
    }
 
    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]);
        *((int*)s->vi + var) = 0; //s->vi[var].val = varX;
        s->levels  [var] = 0;
        s->assigns [var] = varX;
        s->reasons [var] = 0;
        if ( s->fProofLogging )
        s->units   [var] = 0;
#ifdef USE_FLOAT_ACTIVITY2
        s->activity[var] = 0;
#else
        s->activity[var] = (1<<10);
#endif
        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); 
        s->orderpos[var] = veci_size(&s->order);
        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:

Here is the caller graph for this function:

sat_solver2_simplify()

int sat_solver2_simplify ( sat_solver2 * s )

extern

Definition at line 996 of file satSolver2.c.

{
    assert(solver2_dlevel(s) == 0);
    return (solver2_propagate(s) == NULL);
}

Here is the call graph for this function:

Here is the caller graph for this function:

sat_solver2_solve()

int sat_solver2_solve ( sat_solver2 * 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 1835 of file satSolver2.c.

{
    int restart_iter = 0;
    ABC_INT64_T  nof_conflicts;
    lbool status = l_Undef;
    int proof_id;
    lit * i;
 
    s->hLearntLast = -1;
    s->hProofLast = -1;
 
    // 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;
 
/*
    // Perform assumptions:
    root_level = assumps.size();
    for (int i = 0; i < assumps.size(); i++){
        Lit p = assumps[i];
        assert(var(p) < nVars());
        if (!solver2_assume(p)){
            GClause r = reason[var(p)];
            if (r != Gclause2_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());
*/
 
    // 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 (!solver2_enqueue(s,p,0))
        {
            clause* r = clause2_read(s, lit_reason(s,p));
            if (r != NULL)
            {
                clause* confl = r;
                proof_id = solver2_analyze_final(s, confl, 1);
                veci_push(&s->conf_final, lit_neg(p));
            }
            else
            {
//                assert( 0 );
//                r = var_unit_clause( s, lit_var(p) );
//                assert( r != NULL );
//                proof_id = clause2_proofid(s, r, 0);
                proof_id = -1; // the only case when ProofId is not assigned (conflicting assumptions)
                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);
            }
            s->hProofLast = proof_id;
            solver2_canceluntil(s, 0);
            return l_False;
        }
        else
        {
            clause* confl = solver2_propagate(s);
            if (confl != NULL){
                proof_id = solver2_analyze_final(s, confl, 0);
                assert(s->conf_final.size > 0);
                s->hProofLast = proof_id;
                solver2_canceluntil(s, 0);
                return l_False;
            }
        }
    }
    assert(s->root_level == solver2_dlevel(s));
 
    if (s->verbosity >= 1){
        Abc_Print(1,"==================================[MINISAT]===================================\n");
        Abc_Print(1,"| Conflicts |     ORIGINAL     |              LEARNT              | Progress |\n");
        Abc_Print(1,"|           | Clauses Literals |   Limit Clauses Literals  Lit/Cl |          |\n");
        Abc_Print(1,"==============================================================================\n");
    }
 
    while (status == l_Undef){
        if (s->verbosity >= 1)
        {
            Abc_Print(1,"| %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)s->nLearntMax,
                (double)s->stats.learnts,
                (double)s->stats.learnts_literals,
                (s->stats.learnts == 0)? 0.0 : (double)s->stats.learnts_literals / s->stats.learnts,
                s->progress_estimate*100);
            fflush(stdout);
        }
        if ( s->nRuntimeLimit && Abc_Clock() > s->nRuntimeLimit )
            break;
        // reduce the set of learnt clauses
        if ( s->nLearntMax && veci_size(&s->act_clas) >= s->nLearntMax && s->pPrf2 == NULL )
            sat_solver2_reducedb(s);
        // perform next run
        nof_conflicts = (ABC_INT64_T)( 100 * luby2(2, restart_iter++) );
        status = solver2_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->verbosity >= 1)
        Abc_Print(1,"==============================================================================\n");
 
    solver2_canceluntil(s,0);
//    assert( s->qhead == s->qtail );
//    if ( status == l_True )
//        sat_solver2_verify( s );
    return status;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sat_Solver2DoubleClauses()

void Sat_Solver2DoubleClauses ( sat_solver2 * p, int iVar )

extern

Sat_Solver2GetModel()

int * Sat_Solver2GetModel ( sat_solver2 * p, int * pVars, int nVars )

extern

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

Synopsis [Returns a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file satUtil.c.

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

Here is the caller graph for this function:

Sat_Solver2PrintStats()

void Sat_Solver2PrintStats ( FILE * pFile, sat_solver2 * s )

extern

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 214 of file satUtil.c.

{
    printf( "starts        : %10d\n", (int)s->stats.starts );
    printf( "conflicts     : %10d\n", (int)s->stats.conflicts );
    printf( "decisions     : %10d\n", (int)s->stats.decisions );
    printf( "propagations  : %10d\n", (int)s->stats.propagations );
//    printf( "inspects      : %10d\n", (int)s->stats.inspects );
//    printf( "inspects2     : %10d\n", (int)s->stats.inspects2 );
/*
    printf( "memory for variables %.1f MB (free %6.2f %%) and clauses %.1f MB (free %6.2f %%)\n", 
        1.0 * Sat_Solver2GetVarMem(s) * s->size / (1<<20),
        100.0 * (s->cap - s->size) / s->cap,
        4.0 * (s->clauses.cap + s->learnts.cap) / (1<<20),
        100.0 * (s->clauses.cap - s->clauses.size + 
                 s->learnts.cap - s->learnts.size) / 
                (s->clauses.cap + s->learnts.cap) );
*/
}

Here is the caller graph for this function:

Sat_Solver2WriteDimacs()

void Sat_Solver2WriteDimacs ( sat_solver2 * p, char * pFileName, lit * assumptionsBegin, lit * assumptionsEnd, int incrementVars )

extern

Definition at line 126 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_MemForEachClause2( 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 );
}   

var_is_assigned()

int var_is_assigned ( sat_solver2 * s, int v )

extern

Definition at line 83 of file satSolver2.c.

{ return s->assigns[v] != varX; }

Here is the caller graph for this function:

var_is_partA()

int var_is_partA ( sat_solver2 * s, int v )

extern

Definition at line 84 of file satSolver2.c.

{ return s->vi[v].partA;        }

var_set_partA()

void var_set_partA ( sat_solver2 * s, int v, int partA )

extern

Definition at line 85 of file satSolver2.c.

{ s->vi[v].partA = partA;       }

Here is the caller graph for this function: