intInt.h File Reference

#include "aig/saig/saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"
#include "int.h"

Go to the source code of this file.

Data Structures
struct	Inter_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_HEADER_START struct Inter_Man_t_	Inter_Man_t
	INCLUDES ///. More...
typedef struct Inter_Check_t_	Inter_Check_t

Functions
Inter_Check_t *	Inter_CheckStart (Aig_Man_t *pTrans, int nFramesK)
	MACRO DEFINITIONS ///. More...
void	Inter_CheckStop (Inter_Check_t *p)
int	Inter_CheckPerform (Inter_Check_t *p, Cnf_Dat_t *pCnf, abctime nTimeNewOut)
int	Inter_ManCheckContainment (Aig_Man_t *pNew, Aig_Man_t *pOld)
	FUNCTION DEFINITIONS ///. More...
int	Inter_ManCheckEquivalence (Aig_Man_t *pNew, Aig_Man_t *pOld)
int	Inter_ManCheckInductiveContainment (Aig_Man_t *pTrans, Aig_Man_t *pInter, int nSteps, int fBackward)
void *	Inter_ManGetCounterExample (Aig_Man_t *pAig, int nFrames, int fVerbose)
Aig_Man_t *	Inter_ManStartInitState (int nRegs)
	DECLARATIONS ///. More...
Aig_Man_t *	Inter_ManStartDuplicated (Aig_Man_t *p)
Aig_Man_t *	Inter_ManStartOneOutput (Aig_Man_t *p, int fAddFirstPo)
Aig_Man_t *	Inter_ManFramesInter (Aig_Man_t *pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames)
	DECLARATIONS ///. More...
Inter_Man_t *	Inter_ManCreate (Aig_Man_t *pAig, Inter_ManParams_t *pPars)
	DECLARATIONS ///. More...
void	Inter_ManClean (Inter_Man_t *p)
void	Inter_ManStop (Inter_Man_t *p, int fProved)
int	Inter_ManPerformOneStep (Inter_Man_t *p, int fUseBias, int fUseBackward, abctime nTimeNewOut)
int	Inter_ManCheckInitialState (Aig_Man_t *p)
	DECLARATIONS ///. More...
int	Inter_ManCheckAllStates (Aig_Man_t *p)

Typedef Documentation

typedef struct Inter_Check_t_ Inter_Check_t

Definition at line 84 of file intInt.h.

typedef typedefABC_NAMESPACE_HEADER_START struct Inter_Man_t_ Inter_Man_t

INCLUDES ///.

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

FileName [intInt.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Internal declarations.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 49 of file intInt.h.

Function Documentation

int Inter_CheckPerform	(	Inter_Check_t *	p,
		Cnf_Dat_t *	pCnfInt,
		abctime	nTimeNewOut
	)

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

Synopsis [Perform the checking.]

Description [Returns 1 if the check has passed.]

SideEffects []

SeeAlso []

Definition at line 220 of file intCheck.c.

{
    Aig_Obj_t * pObj, * pObj2;
    int i, f, VarA, VarB, RetValue, Entry, status;
    int nRegs = Aig_ManCiNum(pCnfInt->pMan);
    assert( Aig_ManCoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
    assert( Aig_ManCoNum(pCnfInt->pMan) == 1 );

    // set runtime limit
    if ( nTimeNewOut )
        sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );

    // add clauses to the SAT solver
    Cnf_DataLift( pCnfInt, p->nVars );
    for ( f = 0; f <= p->nFramesK; f++ )
    {
        // add clauses to the solver
        for ( i = 0; i < pCnfInt->nClauses; i++ )
        {
            RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
            assert( RetValue );
        }
        // add equality clauses for the flop variables
        Aig_ManForEachCi( pCnfInt->pMan, pObj, i )
        {
            pObj2 = f ? Aig_ManCo(p->pFrames, i + (f-1) * nRegs) : Aig_ManCi(p->pFrames, i);
            Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
        }
        // add final clauses
        if ( f < p->nFramesK )
        {
            if ( f == Vec_IntSize(p->vOrLits) ) // find time here
            {
                // add literal to this frame
                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                Vec_IntPush( p->vOrLits, VarB );
            }
            else
            {
                // add OR gate for this frame
                VarA = Vec_IntEntry( p->vOrLits, f );
                VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
                Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
                Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
            }
        }
        else
        {
            // add AND gate for this frame
            VarB = pCnfInt->pVarNums[ Aig_ManCo(pCnfInt->pMan, 0)->Id ];
            Vec_IntPush( p->vAndLits, VarB );
        }
        // update variable IDs
        Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
        p->nVars += pCnfInt->nVars + 1;
    }
    Cnf_DataLift( pCnfInt, -p->nVars );
    assert( Vec_IntSize(p->vOrLits) == p->nFramesK );

    // collect the assumption literals
    Vec_IntClear( p->vAssLits );
    Vec_IntForEachEntry( p->vOrLits, Entry, i )
        Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
    Vec_IntForEachEntry( p->vAndLits, Entry, i )
        Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
/*
    if ( pCnfInt->nLiterals == 3635 )
    {
        int s = 0;
    }
*/
    // call the SAT solver
    status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits), 
        Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits), 
        (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );

    return status == l_False;
}

Inter_Check_t* Inter_CheckStart	(	Aig_Man_t *	pTrans,
		int	nFramesK
	)

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

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

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 105 of file intCheck.c.

{
    Inter_Check_t * p;
    // create solver
    p = ABC_CALLOC( Inter_Check_t, 1 );
    p->vOrLits  = Vec_IntAlloc( 100 );
    p->vAndLits = Vec_IntAlloc( 100 );
    p->vAssLits = Vec_IntAlloc( 100 );
    // generate the timeframes 
    p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
    assert( Aig_ManCiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
    assert( Aig_ManCoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
    // convert to CNF
    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) ); 
    p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
    // assign parameters
    p->nFramesK = nFramesK;
    p->nVars    = p->pCnf->nVars;
    return p;
}

void Inter_CheckStop

(

Inter_Check_t *

p

)

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

Synopsis [This procedure sets default values of interpolation parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file intCheck.c.

{
    if ( p == NULL )
        return;
    Vec_IntFree( p->vOrLits );
    Vec_IntFree( p->vAndLits );
    Vec_IntFree( p->vAssLits );
    Cnf_DataFree( p->pCnf );
    Aig_ManStop( p->pFrames );
    sat_solver_delete( p->pSat );
    ABC_FREE( p );
}

int Inter_ManCheckAllStates

(

Aig_Man_t *

p

)

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

Synopsis [Returns 1 if the property holds in all states.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file intUtil.c.

{
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    int status;
    abctime clk = Abc_Clock();
    pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    Cnf_DataFree( pCnf );
    if ( pSat == NULL )
        return 1;
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    sat_solver_delete( pSat );
    ABC_PRT( "Time", Abc_Clock() - clk );
    return status == l_False;
}

int Inter_ManCheckContainment	(	Aig_Man_t *	pNew,
		Aig_Man_t *	pOld
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Checks constainment of two interpolants.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file intContain.c.

{
    Aig_Man_t * pMiter, * pAigTemp;
    int RetValue;
    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
//    Aig_ManStop( pAigTemp );
    RetValue = Fra_FraigMiterStatus( pMiter );
    if ( RetValue == -1 )
    {
        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
        RetValue = Fra_FraigMiterStatus( pAigTemp );
        Aig_ManStop( pAigTemp );
//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
    }
    assert( RetValue != -1 );
    Aig_ManStop( pMiter );
    return RetValue;
}

int Inter_ManCheckEquivalence	(	Aig_Man_t *	pNew,
		Aig_Man_t *	pOld
	)

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

Synopsis [Checks constainment of two interpolants.]

Description []

SideEffects []

SeeAlso []

Definition at line 78 of file intContain.c.

{
    Aig_Man_t * pMiter, * pAigTemp;
    int RetValue;
    pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
//    Aig_ManStop( pAigTemp );
    RetValue = Fra_FraigMiterStatus( pMiter );
    if ( RetValue == -1 )
    {
        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
        RetValue = Fra_FraigMiterStatus( pAigTemp );
        Aig_ManStop( pAigTemp );
//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
    }
    assert( RetValue != -1 );
    Aig_ManStop( pMiter );
    return RetValue;
}

int Inter_ManCheckInductiveContainment	(	Aig_Man_t *	pTrans,
		Aig_Man_t *	pInter,
		int	nSteps,
		int	fBackward
	)

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

Synopsis [Checks constainment of two interpolants inductively.]

Description []

SideEffects []

SeeAlso []

Definition at line 190 of file intContain.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t ** ppNodes;
    Vec_Ptr_t * vMapRegs;
    Cnf_Dat_t * pCnf;
    sat_solver * pSat;
    int f, nRegs, status;
    nRegs = Saig_ManRegNum(pTrans);
    assert( nRegs > 0 );
    // generate the timeframes 
    pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs );
    assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
    // add main constraints to the timeframes
    ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
    if ( !fBackward )
    { 
        // forward inductive check: p -> p -> ... -> !p
        for ( f = 0; f < nSteps; f++ )
            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
    }
    else
    {
        // backward inductive check: p -> !p -> ... -> !p
        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
        for ( f = 1; f <= nSteps; f++ )
            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
    }
    Vec_PtrFree( vMapRegs );
    Aig_ManCleanup( pFrames );

    // convert to CNF
    pCnf = Cnf_Derive( pFrames, 0 ); 
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
//    Cnf_DataFree( pCnf );
//    Aig_ManStop( pFrames );

    if ( pSat == NULL )
    {
        Cnf_DataFree( pCnf );
        Aig_ManStop( pFrames );
        return 1;
    }

     // solve the problem
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );

//    Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );

    Cnf_DataFree( pCnf );
    Aig_ManStop( pFrames );

    sat_solver_delete( pSat );
    return status == l_False;
}

int Inter_ManCheckInitialState

(

Aig_Man_t *

p

)

DECLARATIONS ///.

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

FileName [intUtil.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Various interpolation utilities.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:

intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Returns 1 if the property fails in the initial state.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file intUtil.c.

{
    Cnf_Dat_t * pCnf;
    Aig_Obj_t * pObj;
    sat_solver * pSat;
    int i, status;
    //abctime clk = Abc_Clock();
    pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
    if ( pSat == NULL )
    {
        Cnf_DataFree( pCnf );
        return 0;
    }
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    //ABC_PRT( "Time", Abc_Clock() - clk );
    if ( status == l_True )
    {
        p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
        Saig_ManForEachPi( p, pObj, i )
            if ( sat_solver_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pObj)] ) )
                Abc_InfoSetBit( p->pSeqModel->pData, Aig_ManRegNum(p) + i );
    }
    Cnf_DataFree( pCnf );
    sat_solver_delete( pSat );
    return status == l_True;
}

void Inter_ManClean

(

Inter_Man_t *

p

)

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

Synopsis [Cleans the interpolation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file intMan.c.

{
    if ( p->vInters )
    {
        Aig_Man_t * pMan;
        int i;
        Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i )
            Aig_ManStop( pMan );
        Vec_PtrClear( p->vInters );
    }
    if ( p->pCnfInter )
        Cnf_DataFree( p->pCnfInter );
    if ( p->pCnfFrames )
        Cnf_DataFree( p->pCnfFrames );
    if ( p->pInter )
        Aig_ManStop( p->pInter );
    if ( p->pFrames )
        Aig_ManStop( p->pFrames );
}

Inter_Man_t* Inter_ManCreate	(	Aig_Man_t *	pAig,
		Inter_ManParams_t *	pPars
	)

DECLARATIONS ///.

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

FileName [intMan.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Interpolation manager procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:

intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Creates the interpolation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file intMan.c.

{
    Inter_Man_t * p;
    // create interpolation manager
    p = ABC_ALLOC( Inter_Man_t, 1 );
    memset( p, 0, sizeof(Inter_Man_t) );
    p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
    p->nConfLimit = pPars->nBTLimit;
    p->fVerbose = pPars->fVerbose;
    p->pFileName = pPars->pFileName;
    p->pAig = pAig;
    if ( pPars->fDropInvar )
        p->vInters = Vec_PtrAlloc( 100 );
    return p;
}

Aig_Man_t* Inter_ManFramesInter	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	fAddRegOuts,
		int	fUseTwoFrames
	)

DECLARATIONS ///.

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

FileName [intFrames.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Sequential AIG unrolling for interpolation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:

intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Create timeframes of the manager for interpolation.]

Description [The resulting manager is combinational. The primary inputs corresponding to register outputs are ordered first. The only POs of the manager is the property output of the last timeframe.]

SideEffects []

SeeAlso []

Definition at line 47 of file intFrames.c.

{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    Aig_Obj_t * pLastPo = NULL;
    int i, f;
    assert( Saig_ManRegNum(pAig) > 0 );
    assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
    // create variables for register outputs
    if ( fAddRegOuts )
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_ManConst0( pFrames );
    }
    else
    {
        Saig_ManForEachLo( pAig, pObj, i )
            pObj->pData = Aig_ObjCreateCi( pFrames );
    }
    // add timeframes
    for ( f = 0; f < nFrames; f++ )
    {
        // create PI nodes for this frame
        Saig_ManForEachPi( pAig, pObj, i )
            pObj->pData = Aig_ObjCreateCi( pFrames );
        // add internal nodes of this frame
        Aig_ManForEachNode( pAig, pObj, i )
            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
        // add outputs for constraints
        Saig_ManForEachPo( pAig, pObj, i )
        {
            if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
                continue;
            Aig_ObjCreateCo( pFrames, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
        }
        if ( f == nFrames - 1 )
            break;
        // remember the last PO
        pObj = Aig_ManCo( pAig, 0 );
        pLastPo = Aig_ObjChild0Copy(pObj);
        // save register inputs
        Saig_ManForEachLi( pAig, pObj, i )
            pObj->pData = Aig_ObjChild0Copy(pObj);
        // transfer to register outputs
        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
            pObjLo->pData = pObjLi->pData;
    }
    // create POs for each register output
    if ( fAddRegOuts )
    {
        Saig_ManForEachLi( pAig, pObj, i )
            Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
    }
    // create the only PO of the manager
    else
    {
        pObj = Aig_ManCo( pAig, 0 );
        // add the last PO
        if ( pLastPo == NULL || !fUseTwoFrames )
            pLastPo = Aig_ObjChild0Copy(pObj);
        else
            pLastPo = Aig_Or( pFrames, pLastPo, Aig_ObjChild0Copy(pObj) );
        Aig_ObjCreateCo( pFrames, pLastPo );
    }
    Aig_ManCleanup( pFrames );
    return pFrames;
}

void* Inter_ManGetCounterExample	(	Aig_Man_t *	pAig,
		int	nFrames,
		int	fVerbose
	)

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

Synopsis [Run the SAT solver on the unrolled instance.]

Description []

SideEffects []

SeeAlso []

Definition at line 95 of file intCtrex.c.

{
    int nConfLimit = 1000000;
    Abc_Cex_t * pCtrex = NULL;
    Aig_Man_t * pFrames;
    sat_solver * pSat;
    Cnf_Dat_t * pCnf;
    int status;
    abctime clk = Abc_Clock();
    Vec_Int_t * vCiIds;
    // create timeframes
    assert( Saig_ManPoNum(pAig) == 1 );
    pFrames = Inter_ManFramesBmc( pAig, nFrames );
    // derive CNF
    pCnf = Cnf_Derive( pFrames, 0 );
    Cnf_DataTranformPolarity( pCnf, 0 );
    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
    Aig_ManStop( pFrames );
    // convert into SAT solver
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
    Cnf_DataFree( pCnf );
    if ( pSat == NULL )
    {
        printf( "Counter-example generation in command \"int\" has failed.\n" );
        printf( "Use command \"bmc2\" to produce a valid counter-example.\n" );
        Vec_IntFree( vCiIds );
        return NULL;
    }
    // simplify the problem
    status = sat_solver_simplify(pSat);
    if ( status == 0 )
    {
        Vec_IntFree( vCiIds );
        sat_solver_delete( pSat );
        return NULL;
    }
    // solve the miter
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    // if the problem is SAT, get the counterexample
    if ( status == l_True )
    {
        int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
        pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
        pCtrex->iFrame = nFrames - 1;
        pCtrex->iPo = 0;
        for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
            if ( pModel[i] )
                Abc_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
        ABC_FREE( pModel );
    }
    // free the sat_solver
    sat_solver_delete( pSat );
    Vec_IntFree( vCiIds );
    // verify counter-example
    status = Saig_ManVerifyCex( pAig, pCtrex );
    if ( status == 0 )
        printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
    // report the results
    if ( fVerbose )
    {
        ABC_PRT( "Total ctrex generation time", Abc_Clock() - clk );
    }
    return pCtrex;

}

int Inter_ManPerformOneStep	(	Inter_Man_t *	p,
		int	fUseBias,
		int	fUseBackward,
		abctime	nTimeNewOut
	)

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

Synopsis [Performs one SAT run with interpolation.]

Description [Returns 1 if proven. 0 if failed. -1 if undecided.]

SideEffects []

SeeAlso []

Definition at line 203 of file intM114.c.

{
    sat_solver * pSat;
    void * pSatCnf = NULL;
    Inta_Man_t * pManInterA; 
//    Intb_Man_t * pManInterB; 
    int * pGlobalVars;
    int status, RetValue;
    int i, Var;
    abctime clk;
//    assert( p->pInterNew == NULL );

    // derive the SAT solver
    pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
    if ( pSat == NULL )
    {
        p->pInterNew = NULL;
        return 1;
    }

    // set runtime limit
    if ( nTimeNewOut )
        sat_solver_set_runtime_limit( pSat, nTimeNewOut );

    // collect global variables
    pGlobalVars = ABC_CALLOC( int, sat_solver_nvars(pSat) );
    Vec_IntForEachEntry( p->vVarsAB, Var, i )
        pGlobalVars[Var] = 1;
    pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;

    // solve the problem
clk = Abc_Clock();
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    p->nConfCur = pSat->stats.conflicts;
p->timeSat += Abc_Clock() - clk;

    pSat->pGlobalVars = NULL;
    ABC_FREE( pGlobalVars );
    if ( status == l_False )
    {
        pSatCnf = sat_solver_store_release( pSat );
        RetValue = 1;
    }
    else if ( status == l_True )
    {
        RetValue = 0;
    } 
    else
    {
        RetValue = -1;
    }
    sat_solver_delete( pSat );
    if ( pSatCnf == NULL )
        return RetValue;

    // create the resulting manager
clk = Abc_Clock();
/*
    if ( !fUseIp )
    {
        pManInterA = Inta_ManAlloc();
        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
        Inta_ManFree( pManInterA );
    }
    else
    {
        Aig_Man_t * pInterNew2;
        int RetValue;

        pManInterA = Inta_ManAlloc();
        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
//        Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
        Inta_ManFree( pManInterA );

        pManInterB = Intb_ManAlloc();
        pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
        Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
        Intb_ManFree( pManInterB );

        // check relationship
        RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
        if ( RetValue )
            printf( "Equivalence \"Ip == Im\" holds\n" );
        else
        {
//            printf( "Equivalence \"Ip == Im\" does not hold\n" );
            RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
            if ( RetValue )
                printf( "Containment \"Ip -> Im\" holds\n" );
            else
                printf( "Containment \"Ip -> Im\" does not hold\n" );

            RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
            if ( RetValue )
                printf( "Containment \"Im -> Ip\" holds\n" );
            else
                printf( "Containment \"Im -> Ip\" does not hold\n" );
        }

        Aig_ManStop( pInterNew2 );
    }
*/

    pManInterA = Inta_ManAlloc();
    p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 );
    Inta_ManFree( pManInterA );

p->timeInt += Abc_Clock() - clk;
    Sto_ManFree( (Sto_Man_t *)pSatCnf );
    if ( p->pInterNew == NULL )
        RetValue = -1;
    return RetValue;
}

Aig_Man_t* Inter_ManStartDuplicated

(

Aig_Man_t *

p

)

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

Synopsis [Duplicate the AIG w/o POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 73 of file intDup.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj;
    int i;
    assert( Aig_ManRegNum(p) > 0 );
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
        pObj->pData = Aig_ObjCreateCi( pNew );
    // set registers
    pNew->nTruePis = p->nTruePis;
    pNew->nTruePos = Saig_ManConstrNum(p);
    pNew->nRegs    = p->nRegs;
    // duplicate internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );

    // create constraint outputs
    Saig_ManForEachPo( p, pObj, i )
    {
        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
            continue;
        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
    }

    // create register inputs with MUXes
    Saig_ManForEachLi( p, pObj, i )
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    Aig_ManCleanup( pNew );
    return pNew;
}

Aig_Man_t* Inter_ManStartInitState

(

int

nRegs

)

DECLARATIONS ///.

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

FileName [intDup.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Interpolation engine.]

Synopsis [Specialized AIG duplication procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 24, 2008.]

Revision [

Id:

intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

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

Synopsis [Create trivial AIG manager for the init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file intDup.c.

{
    Aig_Man_t * p;
    Aig_Obj_t * pRes;
    Aig_Obj_t ** ppInputs;
    int i;
    assert( nRegs > 0 );
    ppInputs = ABC_ALLOC( Aig_Obj_t *, nRegs );
    p = Aig_ManStart( nRegs );
    for ( i = 0; i < nRegs; i++ )
        ppInputs[i] = Aig_Not( Aig_ObjCreateCi(p) );
    pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
    Aig_ObjCreateCo( p, pRes );
    ABC_FREE( ppInputs );
    return p;
}

Aig_Man_t* Inter_ManStartOneOutput	(	Aig_Man_t *	p,
		int	fAddFirstPo
	)

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

Synopsis [Duplicate the AIG w/o POs and transforms to transit into init state.]

Description []

SideEffects []

SeeAlso []

Definition at line 122 of file intDup.c.

{
    Aig_Man_t * pNew;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
    int i;
    assert( Aig_ManRegNum(p) > 0 );
    // create the new manager
    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    // create the PIs
    Aig_ManCleanData( p );
    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
    Aig_ManForEachCi( p, pObj, i )
    {
        if ( i == Saig_ManPiNum(p) )
            pCtrl = Aig_ObjCreateCi( pNew );
        pObj->pData = Aig_ObjCreateCi( pNew );
    }
    // set registers
    pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
    pNew->nTruePis = fAddFirstPo? Aig_ManCiNum(p) + 1 : p->nTruePis + 1;
    pNew->nTruePos = fAddFirstPo + Saig_ManConstrNum(p);
    // duplicate internal nodes
    Aig_ManForEachNode( p, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );

    // create constraint outputs
    Saig_ManForEachPo( p, pObj, i )
    {
        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
            continue;
        Aig_ObjCreateCo( pNew, Aig_Not( Aig_ObjChild0Copy(pObj) ) );
    }

    // add the PO
    if ( fAddFirstPo )
    {
        pObj = Aig_ManCo( p, 0 );
        Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
    }
    else
    {
        // create register inputs with MUXes
        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
        {
            pObj = Aig_Mux( pNew, pCtrl, (Aig_Obj_t *)pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
    //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
            Aig_ObjCreateCo( pNew, pObj );
        }
    }
    Aig_ManCleanup( pNew );
    return pNew;
}

void Inter_ManStop	(	Inter_Man_t *	p,
		int	fProved
	)

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

Synopsis [Frees the interpolation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file intMan.c.

{
    if ( p->fVerbose )
    {
        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
        printf( "Runtime statistics:\n" );
        ABC_PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
        ABC_PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
        ABC_PRTP( "SAT solving", p->timeSat,   p->timeTotal );
        ABC_PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
        ABC_PRTP( "Containment", p->timeEqu,   p->timeTotal );
        ABC_PRTP( "Other      ", p->timeOther, p->timeTotal );
        ABC_PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
    }

    if ( p->vInters )
        Inter_ManInterDump( p, fProved );

    if ( p->pCnfAig )
        Cnf_DataFree( p->pCnfAig );
    if ( p->pAigTrans )
        Aig_ManStop( p->pAigTrans );
    if ( p->pInterNew )
        Aig_ManStop( p->pInterNew );
    Inter_ManClean( p );
    Vec_PtrFreeP( &p->vInters );
    Vec_IntFreeP( &p->vVarsAB );
    ABC_FREE( p );
}