satStore.h File Reference

#include "satSolver.h"

Include dependency graph for satStore.h:

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

Go to the source code of this file.

Classes
struct	Sto_Cls_t_
struct	Sto_Man_t_

Macros
#define	STO_MAX(a, b)
	INCLUDES ///.
#define	Sto_ManForEachClause(p, pCls)
#define	Sto_ManForEachClauseRoot(p, pCls)

Typedefs
typedef struct Sto_Cls_t_	Sto_Cls_t
	BASIC TYPES ///.
typedef struct Sto_Man_t_	Sto_Man_t
typedef struct Int_Man_t_	Int_Man_t
typedef struct Inta_Man_t_	Inta_Man_t
typedef struct Intb_Man_t_	Intb_Man_t
typedef struct Intp_Man_t_	Intp_Man_t

Functions
Sto_Man_t *	Sto_ManAlloc ()
	MACRO DEFINITIONS ///.
void	Sto_ManFree (Sto_Man_t *p)
int	Sto_ManAddClause (Sto_Man_t *p, lit *pBeg, lit *pEnd)
int	Sto_ManMemoryReport (Sto_Man_t *p)
void	Sto_ManMarkRoots (Sto_Man_t *p)
void	Sto_ManMarkClausesA (Sto_Man_t *p)
void	Sto_ManDumpClauses (Sto_Man_t *p, char *pFileName)
int	Sto_ManChangeLastClause (Sto_Man_t *p)
Sto_Man_t *	Sto_ManLoadClauses (char *pFileName)
Int_Man_t *	Int_ManAlloc ()
	FUNCTION DEFINITIONS ///.
int *	Int_ManSetGlobalVars (Int_Man_t *p, int nGloVars)
void	Int_ManFree (Int_Man_t *p)
int	Int_ManInterpolate (Int_Man_t *p, Sto_Man_t *pCnf, int fVerbose, unsigned **ppResult)
Inta_Man_t *	Inta_ManAlloc ()
	FUNCTION DEFINITIONS ///.
void	Inta_ManFree (Inta_Man_t *p)
void *	Inta_ManInterpolate (Inta_Man_t *p, Sto_Man_t *pCnf, abctime TimeToStop, void *vVarsAB, int fVerbose)
Intb_Man_t *	Intb_ManAlloc ()
	FUNCTION DEFINITIONS ///.
void	Intb_ManFree (Intb_Man_t *p)
void *	Intb_ManInterpolate (Intb_Man_t *p, Sto_Man_t *pCnf, void *vVarsAB, int fVerbose)
Intp_Man_t *	Intp_ManAlloc ()
	FUNCTION DEFINITIONS ///.
void	Intp_ManFree (Intp_Man_t *p)
void *	Intp_ManUnsatCore (Intp_Man_t *p, Sto_Man_t *pCnf, int fLearned, int fVerbose)
void	Intp_ManUnsatCorePrintForBmc (FILE *pFile, Sto_Man_t *pCnf, void *vCore, void *vVarMap)

Macro Definition Documentation

Sto_ManForEachClause

#define Sto_ManForEachClause	(		p,
			pCls )

Value:

for( pCls = p->pHead; pCls; pCls = pCls->pNext )

Definition at line 99 of file satStore.h.

Sto_ManForEachClauseRoot

#define Sto_ManForEachClauseRoot	(		p,
			pCls )

Value:

for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )

Definition at line 100 of file satStore.h.

STO_MAX

#define STO_MAX	(		a,
			b )

Value:

((a) > (b) ? (a) : (b))

INCLUDES ///.

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

FileName [satStore.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Proof recording.]

Synopsis [External declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id

pr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp

] PARAMETERS ///

Definition at line 48 of file satStore.h.

Typedef Documentation

Int_Man_t

typedef struct Int_Man_t_ Int_Man_t

Definition at line 123 of file satStore.h.

Inta_Man_t

typedef struct Inta_Man_t_ Inta_Man_t

Definition at line 130 of file satStore.h.

Intb_Man_t

typedef struct Intb_Man_t_ Intb_Man_t

Definition at line 136 of file satStore.h.

Intp_Man_t

typedef struct Intp_Man_t_ Intp_Man_t

Definition at line 142 of file satStore.h.

Sto_Cls_t

typedef struct Sto_Cls_t_ Sto_Cls_t

BASIC TYPES ///.

Definition at line 67 of file satStore.h.

Sto_Man_t

typedef struct Sto_Man_t_ Sto_Man_t

Definition at line 81 of file satStore.h.

Function Documentation

Int_ManAlloc()

Int_Man_t * Int_ManAlloc ( )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 107 of file satInter.c.

{
    Int_Man_t * p;
    // allocate the manager
    p = (Int_Man_t *)ABC_ALLOC( char, sizeof(Int_Man_t) );
    memset( p, 0, sizeof(Int_Man_t) );
    // verification
    p->nResLitsAlloc = (1<<16);
    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Int_ManFree()

void Int_ManFree ( Int_Man_t * p )

extern

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file satInter.c.

{
/*
    printf( "Runtime stats:\n" );
ABC_PRT( "BCP     ", p->timeBcp   );
ABC_PRT( "Trace   ", p->timeTrace );
ABC_PRT( "TOTAL   ", p->timeTotal );
*/
    ABC_FREE( p->pInters );
    ABC_FREE( p->pProofNums );
    ABC_FREE( p->pTrail );
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pSeens );
    ABC_FREE( p->pVarTypes );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pWatches );
    ABC_FREE( p->pResLits );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Int_ManInterpolate()

int Int_ManInterpolate ( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned ** ppResult )

extern

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

Synopsis [Computes interpolant for the given CNF.]

Description [Returns the number of common variable found and interpolant. Returns 0, if something did not work.]

SideEffects []

SeeAlso []

Definition at line 1005 of file satInter.c.

{
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();
 
    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    *ppResult = NULL;
 
    // adjust the manager
    Int_ManResize( p );
 
    // prepare the interpolant computation
    Int_ManPrepareInter( p );
 
    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }
 
    // write the root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Int_ManProofWriteOne( p, pClause );
 
    // propagate root level assignments
    if ( Int_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Int_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }
 
    // stop the proof
    if ( p->fProofWrite )
    {
        fclose( p->pFile );
        p->pFile = NULL;    
    }
 
    if ( fVerbose )
    {
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += Abc_Clock() - clkTotal;
    }
 
    *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
    return p->nVarsAB;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Int_ManSetGlobalVars()

int * Int_ManSetGlobalVars ( Int_Man_t * p, int nGloVars )

extern

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file satInter.c.

{
    p->nGloVars = nGloVars;
    return p->pGloVars;
}

Here is the caller graph for this function:

Inta_ManAlloc()

Inta_Man_t * Inta_ManAlloc ( )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file satInterA.c.

{
    Inta_Man_t * p;
    // allocate the manager
    p = (Inta_Man_t *)ABC_ALLOC( char, sizeof(Inta_Man_t) );
    memset( p, 0, sizeof(Inta_Man_t) );
    // verification
    p->vResLits = Vec_IntAlloc( 1000 );
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Inta_ManFree()

void Inta_ManFree ( Inta_Man_t * p )

extern

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 250 of file satInterA.c.

{
/*
    printf( "Runtime stats:\n" );
ABC_PRT( "BCP     ", p->timeBcp   );
ABC_PRT( "Trace   ", p->timeTrace );
ABC_PRT( "TOTAL   ", p->timeTotal );
*/
    ABC_FREE( p->pInters );
    ABC_FREE( p->pProofNums );
    ABC_FREE( p->pTrail );
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pSeens );
    ABC_FREE( p->pVarTypes );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pWatches );
    Vec_IntFree( p->vResLits );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Inta_ManInterpolate()

void * Inta_ManInterpolate ( Inta_Man_t * p, Sto_Man_t * pCnf, abctime TimeToStop, void * vVarsAB, int fVerbose )

extern

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

Synopsis [Computes interpolant for the given CNF.]

Description [Takes the interpolation manager, the CNF deriving by the SAT solver, which includes ClausesA, ClausesB, and learned clauses. Additional arguments are the vector of variables common to AB and the verbosiness flag. Returns the AIG manager with a single output, containing the interpolant.]

SideEffects []

SeeAlso []

Definition at line 944 of file satInterA.c.

{
    Aig_Man_t * pRes;
    Aig_Obj_t * pObj;
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();
 
    if ( TimeToStop && Abc_Clock() > TimeToStop )
        return NULL;
 
    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    p->vVarsAB = (Vec_Int_t *)vVarsAB;
    p->pAig = pRes = Aig_ManStart( 10000 );
    Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
 
    // adjust the manager
    Inta_ManResize( p );
 
    // prepare the interpolant computation
    Inta_ManPrepareInter( p );
 
    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }
 
    // write the root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
    {
        Inta_ManProofWriteOne( p, pClause );
        if ( TimeToStop && Abc_Clock() > TimeToStop )
        {
            Aig_ManStop( pRes );
            p->pAig = NULL;
            return NULL;
        }
    }
 
    // propagate root level assignments
    if ( Inta_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Inta_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
            if ( TimeToStop && Abc_Clock() > TimeToStop )
            {
                Aig_ManStop( pRes );
                p->pAig = NULL;
                return NULL;
            }
        }
    }
 
    // stop the proof
    if ( p->fProofWrite )
    { 
        fclose( p->pFile );
//        Sat_ProofChecker( "proof.cnf_" );
        p->pFile = NULL;    
    }
 
    if ( fVerbose )
    {
//        ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB  ", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
p->timeTotal += Abc_Clock() - clkTotal;
    }
 
    pObj = *Inta_ManAigRead( p, p->pCnf->pTail );
    Aig_ObjCreateCo( pRes, pObj );
    Aig_ManCleanup( pRes );
 
    p->pAig = NULL;
    return pRes;
    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Intb_ManAlloc()

Intb_Man_t * Intb_ManAlloc ( )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file satInterB.c.

{
    Intb_Man_t * p;
    // allocate the manager
    p = (Intb_Man_t *)ABC_ALLOC( char, sizeof(Intb_Man_t) );
    memset( p, 0, sizeof(Intb_Man_t) );
    // verification
    p->nResLitsAlloc = (1<<16);
    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

Here is the call graph for this function:

Intb_ManFree()

void Intb_ManFree ( Intb_Man_t * p )

extern

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 255 of file satInterB.c.

{
/*
    printf( "Runtime stats:\n" );
ABC_PRT( "BCP     ", p->timeBcp   );
ABC_PRT( "Trace   ", p->timeTrace );
ABC_PRT( "TOTAL   ", p->timeTotal );
*/
    ABC_FREE( p->pInters );
    ABC_FREE( p->pProofNums );
    ABC_FREE( p->pTrail );
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pSeens );
    ABC_FREE( p->pVarTypes );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pWatches );
    ABC_FREE( p->pResLits );
    ABC_FREE( p );
}

Intb_ManInterpolate()

void * Intb_ManInterpolate ( Intb_Man_t * p, Sto_Man_t * pCnf, void * vVarsAB, int fVerbose )

extern

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

Synopsis [Computes interpolant for the given CNF.]

Description [Takes the interpolation manager, the CNF deriving by the SAT solver, which includes ClausesA, ClausesB, and learned clauses. Additional arguments are the vector of variables common to AB and the verbosiness flag. Returns the AIG manager with a single output, containing the interpolant.]

SideEffects []

SeeAlso []

Definition at line 987 of file satInterB.c.

{
    Aig_Man_t * pRes;
    Aig_Obj_t * pObj;
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();
 
    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
    p->vVarsAB = (Vec_Int_t *)vVarsAB;
    p->pAig = pRes = Aig_ManStart( 10000 );
    Aig_IthVar( p->pAig, Vec_IntSize(p->vVarsAB) - 1 );
 
    // adjust the manager
    Intb_ManResize( p );
 
    // prepare the interpolant computation
    Intb_ManPrepareInter( p );
 
    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }
 
    // write the root clauses
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Intb_ManProofWriteOne( p, pClause );
 
    // propagate root level assignments
    if ( Intb_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Intb_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }
 
    // stop the proof
    if ( p->fProofWrite )
    { 
        fclose( p->pFile );
//        Sat_ProofChecker( "proof.cnf_" );
        p->pFile = NULL;    
    }
 
    if ( fVerbose )
    {
//        ABC_PRT( "Interpo", Abc_Clock() - clkTotal );
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += Abc_Clock() - clkTotal;
    }
 
    pObj = *Intb_ManAigRead( p, p->pCnf->pTail );
    Aig_ObjCreateCo( pRes, pObj );
    Aig_ManCleanup( pRes );
 
    p->pAig = NULL;
    return pRes;
    
}

Here is the call graph for this function:

Intp_ManAlloc()

Intp_Man_t * Intp_ManAlloc ( )

extern

FUNCTION DEFINITIONS ///.

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 96 of file satInterP.c.

{
    Intp_Man_t * p;
    // allocate the manager
    p = (Intp_Man_t *)ABC_ALLOC( char, sizeof(Intp_Man_t) );
    memset( p, 0, sizeof(Intp_Man_t) );
    // verification
    p->nResLitsAlloc = (1<<16);
    p->pResLits = ABC_ALLOC( lit, p->nResLitsAlloc );
    // proof recording
//    p->vAnties = Vec_IntAlloc( 1000 );
//    p->vBreaks = Vec_IntAlloc( 1000 );
    p->vAntClas = Vec_PtrAlloc( 1000 );
    p->nAntStart = 0;
    // parameters
    p->fProofWrite = 0;
    p->fProofVerif = 1;
    return p;    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Intp_ManFree()

void Intp_ManFree ( Intp_Man_t * p )

extern

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file satInterP.c.

{
/*
    printf( "Runtime stats:\n" );
ABC_PRT( "BCP     ", p->timeBcp   );
ABC_PRT( "Trace   ", p->timeTrace );
ABC_PRT( "TOTAL   ", p->timeTotal );
*/
//    Vec_IntFree( p->vAnties );
//    Vec_IntFree( p->vBreaks );
    Vec_VecFree( (Vec_Vec_t *)p->vAntClas );
//    ABC_FREE( p->pInters );
    ABC_FREE( p->pProofNums );
    ABC_FREE( p->pTrail );
    ABC_FREE( p->pAssigns );
    ABC_FREE( p->pSeens );
//    ABC_FREE( p->pVarTypes );
    ABC_FREE( p->pReasons );
    ABC_FREE( p->pWatches );
    ABC_FREE( p->pResLits );
    ABC_FREE( p );
}

Here is the caller graph for this function:

Intp_ManUnsatCore()

void * Intp_ManUnsatCore ( Intp_Man_t * p, Sto_Man_t * pCnf, int fLearned, int fVerbose )

extern

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

Synopsis [Computes UNSAT core of the satisfiablity problem.]

Description [Takes the interpolation manager, the CNF derived by the SAT solver, which includes the root clauses and the learned clauses. Returns the array of integers representing the number of root clauses that are in the UNSAT core.]

SideEffects []

SeeAlso []

Definition at line 963 of file satInterP.c.

{
    Vec_Int_t * vCore;
    Vec_Str_t * vVisited;
    Sto_Cls_t * pClause;
    int RetValue = 1;
    abctime clkTotal = Abc_Clock();
 
    // check that the CNF makes sense
    assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
    p->pCnf = pCnf;
    p->fVerbose = fVerbose;
 
    // adjust the manager
    Intp_ManResize( p ); 
 
    // construct proof for each clause
    // start the proof
    if ( p->fProofWrite )
    {
        p->pFile = fopen( "proof.cnf_", "w" );
        p->Counter = 0;
    }
 
    // write the root clauses
//    Vec_IntClear( p->vAnties );
//    Vec_IntFill( p->vBreaks, p->pCnf->nRoots, 0 );
    Vec_PtrClear( p->vAntClas );
    p->nAntStart = p->pCnf->nRoots;
 
    Sto_ManForEachClauseRoot( p->pCnf, pClause )
        Intp_ManProofWriteOne( p, pClause );
 
    // propagate root level assignments
    if ( Intp_ManProcessRoots( p ) )
    {
        // if there is no conflict, consider learned clauses
        Sto_ManForEachClause( p->pCnf, pClause )
        {
            if ( pClause->fRoot )
                continue;
            if ( !Intp_ManProofRecordOne( p, pClause ) )
            {
                RetValue = 0;
                break;
            }
        }
    }
 
    // add the last breaker
//    assert( p->pCnf->pEmpty->Id == Vec_IntSize(p->vBreaks) - 1 );
//    Vec_IntPush( p->vBreaks, Vec_IntSize(p->vAnties) );
    assert( p->pCnf->pEmpty->Id - p->nAntStart == Vec_PtrSize(p->vAntClas) - 1 );
    Vec_PtrPush( p->vAntClas, Vec_IntAlloc(0) );
 
    // stop the proof
    if ( p->fProofWrite )
    {
        fclose( p->pFile );
//        Sat_ProofChecker( "proof.cnf_" );
        p->pFile = NULL;    
    }
 
    if ( fVerbose )
    {
//        ABC_PRT( "Core", Abc_Clock() - clkTotal );
    printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f MB\n", 
        p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
        1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
        1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
p->timeTotal += Abc_Clock() - clkTotal;
    }
 
    // derive the UNSAT core
    vCore = Vec_IntAlloc( 1000 );
    vVisited = Vec_StrStart( p->pCnf->pEmpty->Id+1 );
    Intp_ManUnsatCore_rec( p->vAntClas, p->pCnf->pEmpty->Id, vCore, p->pCnf->nRoots, vVisited, fLearned );
    Vec_StrFree( vVisited );
    if ( fVerbose )
        printf( "Root clauses = %d. Learned clauses = %d. UNSAT core size = %d.\n", 
            p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, Vec_IntSize(vCore) );
//    Intp_ManUnsatCoreVerify( p->pCnf, vCore );
    return vCore;   
}

Here is the call graph for this function:

Here is the caller graph for this function:

Intp_ManUnsatCorePrintForBmc()

void Intp_ManUnsatCorePrintForBmc ( FILE * pFile, Sto_Man_t * pCnf, void * vCore0, void * vVarMap0 )

extern

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

Synopsis [Prints learned clauses in terms of original problem varibles.]

Description []

SideEffects []

SeeAlso []

Definition at line 1059 of file satInterP.c.

{
    Vec_Int_t * vCore   = (Vec_Int_t *)vCore0;
    Vec_Int_t * vVarMap = (Vec_Int_t *)vVarMap0;
    Vec_Ptr_t * vClaMap;
    Sto_Cls_t * pClause;
    int v, i, iClause, fCompl, iObj, iFrame;
    // create map of clause
    vClaMap = Vec_PtrAlloc( pCnf->nClauses );
    Sto_ManForEachClause( pCnf, pClause )
        Vec_PtrPush( vClaMap, pClause );
    // print clauses
    fprintf( pFile, "UNSAT contains %d learned clauses:\n", Vec_IntSize(vCore) );
    Vec_IntForEachEntry( vCore, iClause, i )
    {
        pClause = (Sto_Cls_t *)Vec_PtrEntry(vClaMap, iClause);
        fprintf( pFile, "%6d : %6d : ", i, iClause - pCnf->nRoots );
        for ( v = 0; v < (int)pClause->nLits; v++ )
        {
            fCompl = Abc_LitIsCompl(pClause->pLits[v]);
            iObj   = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v]));
            iFrame = Vec_IntEntry(vVarMap, 2*Abc_Lit2Var(pClause->pLits[v])+1);
            fprintf( pFile, "%s%d(%d) ", fCompl ? "!":"", iObj, iFrame );
        }
        if ( pClause->nLits == 0 )
            fprintf( pFile, "Empty" );
        fprintf( pFile, "\n" );
    }
    Vec_PtrFree( vClaMap );
}

Here is the caller graph for this function:

Sto_ManAddClause()

int Sto_ManAddClause ( Sto_Man_t * p, lit * pBeg, lit * pEnd )

extern

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

Synopsis [Adds one clause to the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 160 of file satStore.c.

{
    Sto_Cls_t * pClause;
    lit Lit, * i, * j;
    int nSize;
 
    // process the literals
    if ( pBeg < pEnd )
    {
        // insertion sort
        for ( i = pBeg + 1; i < pEnd; i++ )
        {
            Lit = *i;
            for ( j = i; j > pBeg && *(j-1) > Lit; j-- )
                *j = *(j-1);
            *j = Lit;
        }
        // make sure there is no duplicated variables
        for ( i = pBeg + 1; i < pEnd; i++ )
            if ( lit_var(*(i-1)) == lit_var(*i) )
            {
                printf( "The clause contains two literals of the same variable: %d and %d.\n", *(i-1), *i );
                return 0;
            }
        // check the largest var size
        p->nVars = STO_MAX( p->nVars, lit_var(*(pEnd-1)) + 1 );
    }
 
    // get memory for the clause
    nSize = sizeof(Sto_Cls_t) + sizeof(lit) * (pEnd - pBeg);
    nSize = (nSize / sizeof(char*) + ((nSize % sizeof(char*)) > 0)) * sizeof(char*); // added by Saurabh on Sep 3, 2009
    pClause = (Sto_Cls_t *)Sto_ManMemoryFetch( p, nSize );
    memset( pClause, 0, sizeof(Sto_Cls_t) );
 
    // assign the clause
    pClause->Id = p->nClauses++;
    pClause->nLits = pEnd - pBeg;
    memcpy( pClause->pLits, pBeg, sizeof(lit) * (pEnd - pBeg) );
//    assert( pClause->pLits[0] >= 0 );
 
    // add the clause to the list
    if ( p->pHead == NULL )
        p->pHead = pClause;
    if ( p->pTail == NULL )
        p->pTail = pClause;
    else
    {
        p->pTail->pNext = pClause;
        p->pTail = pClause;
    }
 
    // add the empty clause
    if ( pClause->nLits == 0 )
    {
        if ( p->pEmpty )
        {
            printf( "More than one empty clause!\n" );
            return 0;
        }
        p->pEmpty = pClause;
    }
    return 1;
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sto_ManAlloc()

Sto_Man_t * Sto_ManAlloc ( )

extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 121 of file satStore.c.

{
    Sto_Man_t * p;
    // allocate the manager
    p = (Sto_Man_t *)ABC_ALLOC( char, sizeof(Sto_Man_t) );
    memset( p, 0, sizeof(Sto_Man_t) );
    // memory management
    p->nChunkSize = (1<<16); // use 64K chunks
    return p;    
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sto_ManChangeLastClause()

int Sto_ManChangeLastClause ( Sto_Man_t * p )

extern

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

Synopsis [Returns the literal of the last clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file satStore.c.

{
    Sto_Cls_t * pClause, * pPrev;
    pPrev = NULL;
    Sto_ManForEachClause( p, pClause )
        pPrev = pClause;
    assert( pPrev != NULL );
    assert( pPrev->fA == 1 );
    assert( pPrev->nLits == 1 );
    p->nClausesA--;
    pPrev->fA = 0;
    return pPrev->pLits[0] >> 1;
}

Here is the caller graph for this function:

Sto_ManDumpClauses()

void Sto_ManDumpClauses ( Sto_Man_t * p, char * pFileName )

extern

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

Synopsis [Writes the stored clauses into a file.]

Description []

SideEffects []

SeeAlso []

Definition at line 305 of file satStore.c.

{
    FILE * pFile;
    Sto_Cls_t * pClause;
    int i;
    // start the file
    pFile = fopen( pFileName, "w" );
    if ( pFile == NULL )
    {
        printf( "Error: Cannot open output file (%s).\n", pFileName );
        return;
    }
    // write the data
    fprintf( pFile, "p %d %d %d %d\n", p->nVars, p->nClauses, p->nRoots, p->nClausesA );
    Sto_ManForEachClause( p, pClause )
    {
        for ( i = 0; i < (int)pClause->nLits; i++ )
            fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
        fprintf( pFile, " 0\n" );
    }
//    fprintf( pFile, " 0\n" );
    fclose( pFile );
}

Here is the caller graph for this function:

Sto_ManFree()

void Sto_ManFree ( Sto_Man_t * p )

extern

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file satStore.c.

{
    Sto_ManMemoryStop( p );
    ABC_FREE( p );
}

Here is the call graph for this function:

Here is the caller graph for this function:

Sto_ManLoadClauses()

Sto_Man_t * Sto_ManLoadClauses ( char * pFileName )

extern

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

Synopsis [Reads CNF from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file satStore.c.

{
    FILE * pFile;
    Sto_Man_t * p;
    Sto_Cls_t * pClause;
    char pBuffer[1024];
    int nLits, nLitsAlloc, Counter, Number;
    lit * pLits;
 
    // start the file
    pFile = fopen( pFileName, "r" );
    if ( pFile == NULL )
    {
        printf( "Error: Cannot open input file (%s).\n", pFileName );
        return NULL;
    }
 
    // create the manager
    p = Sto_ManAlloc();
 
    // alloc the array of literals
    nLitsAlloc = 1024;
    pLits = (lit *)ABC_ALLOC( char, sizeof(lit) * nLitsAlloc );
 
    // read file header
    p->nVars = p->nClauses = p->nRoots = p->nClausesA = 0;
    while ( fgets( pBuffer, 1024, pFile ) )
    {
        if ( pBuffer[0] == 'c' )
            continue;
        if ( pBuffer[0] == 'p' )
        {
            sscanf( pBuffer + 1, "%d %d %d %d", &p->nVars, &p->nClauses, &p->nRoots, &p->nClausesA );
            break;
        }
        printf( "Warning: Skipping line: \"%s\"\n", pBuffer );
    }
 
    // read the clauses
    nLits = 0;
    while ( Sto_ManLoadNumber(pFile, &Number) )
    {
        if ( Number == 0 )
        {
            int RetValue;
            RetValue = Sto_ManAddClause( p, pLits, pLits + nLits );
            assert( RetValue );
            nLits = 0;
            continue;
        }
        if ( nLits == nLitsAlloc )
        {
            nLitsAlloc *= 2;
            pLits = ABC_REALLOC( lit, pLits, nLitsAlloc );
        }
        pLits[ nLits++ ] = lit_read(Number);
    }
    if ( nLits > 0 )
        printf( "Error: The last clause was not saved.\n" );
 
    // count clauses
    Counter = 0;
    Sto_ManForEachClause( p, pClause )
        Counter++;
 
    // check the number of clauses
    if ( p->nClauses != Counter )
    {
        printf( "Error: The actual number of clauses (%d) is different than declared (%d).\n", Counter, p->nClauses );
        Sto_ManFree( p );
        return NULL;
    }
 
    ABC_FREE( pLits );
    fclose( pFile );
    return p;
}

Here is the call graph for this function:

Sto_ManMarkClausesA()

void Sto_ManMarkClausesA ( Sto_Man_t * p )

extern

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

Synopsis [Mark all clauses added so far as clause of A.]

Description []

SideEffects []

SeeAlso []

Definition at line 257 of file satStore.c.

{
    Sto_Cls_t * pClause;
    p->nClausesA = 0;
    Sto_ManForEachClause( p, pClause )
    {
        pClause->fA = 1;
        p->nClausesA++;
    }
}

Here is the caller graph for this function:

Sto_ManMarkRoots()

void Sto_ManMarkRoots ( Sto_Man_t * p )

extern

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

Synopsis [Mark all clauses added so far as root clauses.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file satStore.c.

{
    Sto_Cls_t * pClause;
    p->nRoots = 0;
    Sto_ManForEachClause( p, pClause )
    {
        pClause->fRoot = 1;
        p->nRoots++;
    }
}

Here is the caller graph for this function:

Sto_ManMemoryReport()

int Sto_ManMemoryReport ( Sto_Man_t * p )

extern

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

Synopsis [Reports memory usage in bytes.]

Description []

SideEffects []

SeeAlso []

Definition at line 97 of file satStore.c.

{
    int Total;
    char * pMem, * pNext;
    if ( p->pChunkLast == NULL )
        return 0;
    Total = p->nChunkUsed; 
    for ( pMem = p->pChunkLast; (pNext = *(char **)pMem); pMem = pNext )
        Total += p->nChunkSize;
    return Total;
}

Here is the caller graph for this function: