satStore.h File Reference

#include "satSolver.h"

Go to the source code of this file.

Data Structures
struct	Sto_Cls_t_
struct	Sto_Man_t_

Macros
#define	STO_MAX(a, b)   ((a) > (b) ? (a) : (b))
	INCLUDES ///. More...
#define	Sto_ManForEachClause(p, pCls)   for( pCls = p->pHead; pCls; pCls = pCls->pNext )
#define	Sto_ManForEachClauseRoot(p, pCls)   for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )

Typedefs
typedef struct Sto_Cls_t_	Sto_Cls_t
	BASIC TYPES ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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 ///. More...
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

#define Sto_ManForEachClause	(		p,
			pCls
	)		for( pCls = p->pHead; pCls; pCls = pCls->pNext )

Definition at line 99 of file satStore.h.

#define Sto_ManForEachClauseRoot	(		p,
			pCls
	)		for( pCls = p->pHead; pCls && pCls->fRoot; pCls = pCls->pNext )

Definition at line 100 of file satStore.h.

#define STO_MAX	(		a,
			b
	)		((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

typedef struct Int_Man_t_ Int_Man_t

Definition at line 123 of file satStore.h.

typedef struct Inta_Man_t_ Inta_Man_t

Definition at line 130 of file satStore.h.

typedef struct Intb_Man_t_ Intb_Man_t

Definition at line 136 of file satStore.h.

typedef struct Intp_Man_t_ Intp_Man_t

Definition at line 142 of file satStore.h.

typedef struct Sto_Cls_t_ Sto_Cls_t

BASIC TYPES ///.

Definition at line 67 of file satStore.h.

typedef struct Sto_Man_t_ Sto_Man_t

Definition at line 81 of file satStore.h.

Function Documentation

Int_Man_t* Int_ManAlloc

(

)

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

void Int_ManFree

(

Int_Man_t *

p

)

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

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

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

int* Int_ManSetGlobalVars	(	Int_Man_t *	p,
		int	nGloVars
	)

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

Synopsis [Allocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file satInter.c.

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

Inta_Man_t* Inta_ManAlloc

(

)

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

void Inta_ManFree

(

Inta_Man_t *

p

)

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

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

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\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 = *Inta_ManAigRead( p, p->pCnf->pTail );
    Aig_ObjCreateCo( pRes, pObj );
    Aig_ManCleanup( pRes );

    p->pAig = NULL;
    return pRes;
    
}

Intb_Man_t* Intb_ManAlloc

(

)

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

void Intb_ManFree

(

Intb_Man_t *

p

)

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

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

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

Intp_Man_t* Intp_ManAlloc

(

)

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

void Intp_ManFree

(

Intp_Man_t *

p

)

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

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

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

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

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

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

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

Sto_Man_t* Sto_ManAlloc

(

)

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

int Sto_ManChangeLastClause

(

Sto_Man_t *

p

)

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

void Sto_ManDumpClauses	(	Sto_Man_t *	p,
		char *	pFileName
	)

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

void Sto_ManFree

(

Sto_Man_t *

p

)

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

Synopsis [Deallocate proof manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file satStore.c.

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

Sto_Man_t* Sto_ManLoadClauses

(

char *

pFileName

)

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

void Sto_ManMarkClausesA

(

Sto_Man_t *

p

)

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

void Sto_ManMarkRoots

(

Sto_Man_t *

p

)

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

int Sto_ManMemoryReport

(

Sto_Man_t *

p

)

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