fraClau.c File Reference

#include "fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"

Go to the source code of this file.

Data Structures
struct	Cla_Man_t_

Typedefs
typedef typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_	Cla_Man_t
	DECLARATIONS ///. More...

Functions
Vec_Int_t *	Fra_ClauSaveLatchVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int fCsVars)
	FUNCTION DEFINITIONS ///. More...
Vec_Int_t *	Fra_ClauSaveOutputVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf)
Vec_Int_t *	Fra_ClauSaveInputVars (Aig_Man_t *pMan, Cnf_Dat_t *pCnf, int nStarting)
int *	Fra_ClauCreateMapping (Vec_Int_t *vSatVarsFrom, Vec_Int_t *vSatVarsTo, int nVarsMax)
void	Fra_ClauStop (Cla_Man_t *p)
Cla_Man_t *	Fra_ClauStart (Aig_Man_t *pMan)
static Vec_Int_t *	Vec_IntSplitHalf (Vec_Int_t *vVec)
static void	Vec_IntComplement (Vec_Int_t *vVec)
int	Fra_ClauCheckProperty (Cla_Man_t *p, Vec_Int_t *vCex)
int	Fra_ClauCheckBmc (Cla_Man_t *p, Vec_Int_t *vClause)
void	Fra_ClauRemapClause (int *pMap, Vec_Int_t *vClause, Vec_Int_t *vRemapped, int fInv)
int	Fra_ClauCheckClause (Cla_Man_t *p, Vec_Int_t *vClause, Vec_Int_t *vCex)
void	Fra_ClauReduceClause (Vec_Int_t *vMain, Vec_Int_t *vNew)
void	Fra_ClauMinimizeClause_rec (Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
void	Fra_ClauMinimizeClause (Cla_Man_t *p, Vec_Int_t *vBasis, Vec_Int_t *vExtra)
void	Fra_ClauPrintClause (Vec_Int_t *vSatCsVars, Vec_Int_t *vCex)
int	Fra_Clau (Aig_Man_t *pMan, int nIters, int fVerbose, int fVeryVerbose)

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Cla_Man_t_ Cla_Man_t

DECLARATIONS ///.

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

FileName [fraClau.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis [Induction with clause strengthening.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:

fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

]

Definition at line 38 of file fraClau.c.

Function Documentation

int Fra_Clau	(	Aig_Man_t *	pMan,
		int	nIters,
		int	fVerbose,
		int	fVeryVerbose
	)

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

Synopsis [Takes the AIG with the single output to be checked.]

Description []

SideEffects []

SeeAlso []

Definition at line 637 of file fraClau.c.

{
    Cla_Man_t * p;
    int Iter, RetValue, fFailed, i;
    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
    // create the manager
    p = Fra_ClauStart( pMan );
    if ( p == NULL )
    {
        printf( "The property is trivially inductive.\n" );
        return 1;
    }
    // generate counter-examples and expand them
    for ( Iter = 0; !Fra_ClauCheckProperty( p, p->vCexMain0 ) && Iter < nIters; Iter++ )
    {
        if ( fVerbose )
            printf( "%4d : ", Iter );
        // remap clause into the test manager
        Fra_ClauRemapClause( p->pMapCsMainToCsTest, p->vCexMain0, p->vCexMain, 0 );
        if ( fVerbose && fVeryVerbose )
            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
        // the main counter-example is in p->vCexMain
        // intermediate counter-examples are in p->vCexTest
        // generate the reduced counter-example to the inductive property
        fFailed = 0;
        for ( i = 0; !Fra_ClauCheckClause( p, p->vCexMain, p->vCexTest ); i++ )
        {
            Fra_ClauReduceClause( p->vCexMain, p->vCexTest );
            Fra_ClauRemapClause( p->pMapCsTestToNsBmc, p->vCexMain, p->vCexBmc, 0 );

//            if ( !Fra_ClauCheckBmc(p, p->vCexBmc) )
            if ( Vec_IntSize(p->vCexMain) < 1 )
            {
                Vec_IntComplement( p->vCexMain0 ); 
                RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexMain0), Vec_IntArray(p->vCexMain0) + Vec_IntSize(p->vCexMain0) );
                if ( RetValue == 0 )
                {
                    printf( "\nProperty is proved after %d iterations.\n", Iter+1 );
                    return 0;
                }
                fFailed = 1;
                break;
            }
        }
        if ( fFailed )
        {
            if ( fVerbose )
                printf( " Reducing failed after %d iterations (BMC failed).\n", i );
            continue;
        }
        if ( Vec_IntSize(p->vCexMain) == 0 )
        {
            if ( fVerbose )
                printf( " Reducing failed after %d iterations (nothing left).\n", i );
            continue;
        }
        if ( fVerbose )
            printf( "  " );
        if ( fVerbose && fVeryVerbose )
            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
        if ( fVerbose )
            printf( " LitsInd = %3d.  ", Vec_IntSize(p->vCexMain) );
        // minimize the inductive property
        Vec_IntClear( p->vCexBase );
        if ( Vec_IntSize(p->vCexMain) > 1 )
//        Fra_ClauMinimizeClause_rec( p, p->vCexBase, p->vCexMain );
            Fra_ClauMinimizeClause( p, p->vCexBase, p->vCexMain );
        assert( Vec_IntSize(p->vCexMain) > 0 );
        if ( fVerbose && fVeryVerbose )
            Fra_ClauPrintClause( p->vSatVarsTestCs, p->vCexMain );
        if ( fVerbose )
            printf( " LitsRed = %3d.  ", Vec_IntSize(p->vCexMain) );
        if ( fVerbose )
            printf( "\n" );
        // add the clause to the solver
        Fra_ClauRemapClause( p->pMapCsTestToCsMain, p->vCexMain, p->vCexAssm, 1 );
        RetValue = sat_solver_addclause( p->pSatMain, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm) );
        if ( RetValue == 0 )
        {
            Iter++;
            break;
        }
        if ( p->pSatMain->qtail != p->pSatMain->qhead )
        {
            RetValue = sat_solver_simplify(p->pSatMain);
            assert( RetValue != 0 );
            assert( p->pSatMain->qtail == p->pSatMain->qhead );
        }
    }

    // report the results
    if ( Iter == nIters )
    {
        printf( "Property is not proved after %d iterations.\n", nIters );
        return 0;
    }
    printf( "Property is proved after %d iterations.\n", Iter );
    Fra_ClauStop( p );
    return 1;
}

int Fra_ClauCheckBmc	(	Cla_Man_t *	p,
		Vec_Int_t *	vClause
	)

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

Synopsis [Checks if the clause holds using BMC.]

Description []

SideEffects []

SeeAlso []

Definition at line 379 of file fraClau.c.

{
    int nBTLimit = 0;
    int RetValue;
    RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( RetValue == l_False )
        return 1;
    assert( RetValue == l_True );
    return 0;
}

int Fra_ClauCheckClause	(	Cla_Man_t *	p,
		Vec_Int_t *	vClause,
		Vec_Int_t *	vCex
	)

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

Synopsis [Checks if the clause holds. Returns counter example if not.]

Description [Uses test SAT solver.]

SideEffects []

SeeAlso []

Definition at line 425 of file fraClau.c.

{
    int nBTLimit = 0;
    int RetValue, iVar, i;
    // complement literals
    Vec_IntPush( vClause, toLit( p->nSatVarsTestCur++ ) ); // helper positive
    Vec_IntComplement( vClause ); // helper negative (the clause is C v h')
    // add the clause
    RetValue = sat_solver_addclause( p->pSatTest, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
    assert( RetValue == 1 );
    // complement all literals
    Vec_IntPop( vClause );  // helper removed
    Vec_IntComplement( vClause ); 
    // create the assumption in terms of NS variables
    Fra_ClauRemapClause( p->pMapCsTestToNsTest, vClause, p->vCexAssm, 0 );
    // add helper literals
    for ( i = p->nSatVarsTestBeg; i < p->nSatVarsTestCur - 1; i++ )
        Vec_IntPush( p->vCexAssm, toLitCond(i,1) ); // other helpers negative
    Vec_IntPush( p->vCexAssm, toLitCond(i,0) ); // positive helper
    // try to solve
    RetValue = sat_solver_solve( p->pSatTest, Vec_IntArray(p->vCexAssm), Vec_IntArray(p->vCexAssm) + Vec_IntSize(p->vCexAssm), 
        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    if ( vCex )
        Vec_IntClear( vCex );
    if ( RetValue == l_False )
        return 1;
    assert( RetValue == l_True );
    if ( vCex )
    {
        Vec_IntForEachEntry( p->vSatVarsTestCs, iVar, i )
            Vec_IntPush( vCex, sat_solver_var_literal(p->pSatTest, iVar) );
    }
    return 0;
}

int Fra_ClauCheckProperty	(	Cla_Man_t *	p,
		Vec_Int_t *	vCex
	)

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

Synopsis [Checks if the property holds. Returns counter-example if not.]

Description []

SideEffects []

SeeAlso []

Definition at line 345 of file fraClau.c.

{
    int nBTLimit = 0;
    int RetValue, iVar, i;
    sat_solver_act_var_clear( p->pSatMain );
    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
    Vec_IntClear( vCex );
    if ( RetValue == l_False )
        return 1;
    assert( RetValue == l_True );
    Vec_IntForEachEntry( p->vSatVarsMainCs, iVar, i )
        Vec_IntPush( vCex, sat_solver_var_literal(p->pSatMain, iVar) );
/*
    {
        int i;
        for (i = 0; i < p->pSatMain->size; i++)
            printf( "%d=%d ", i, p->pSatMain->model.ptr[i] == l_True );
        printf( "\n" );
    }
*/
    return 0;
}

int* Fra_ClauCreateMapping	(	Vec_Int_t *	vSatVarsFrom,
		Vec_Int_t *	vSatVarsTo,
		int	nVarsMax
	)

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

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 154 of file fraClau.c.

{
    int * pMapping, Var, i;
    assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
    pMapping = ABC_ALLOC( int, nVarsMax );
    for ( i = 0; i < nVarsMax; i++ )
        pMapping[i] = -1;
    Vec_IntForEachEntry( vSatVarsFrom, Var, i )
        pMapping[Var] = Vec_IntEntry(vSatVarsTo,i);
    return pMapping;
}

void Fra_ClauMinimizeClause	(	Cla_Man_t *	p,
		Vec_Int_t *	vBasis,
		Vec_Int_t *	vExtra
	)

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

Synopsis [Minimizes the clauses using a simple method.]

Description [The input and output clause are in vExtra.]

SideEffects []

SeeAlso []

Definition at line 566 of file fraClau.c.

{
    int iLit, iLit2, i, k;
    Vec_IntForEachEntryReverse( vExtra, iLit, i )
    {
        // copy literals without the given one
        Vec_IntClear( vBasis );
        Vec_IntForEachEntry( vExtra, iLit2, k )
            if ( k != i )
                Vec_IntPush( vBasis, iLit2 );
        // try whether it is inductive
        if ( !Fra_ClauCheckClause( p, vBasis, NULL ) )
            continue;
        // the clause is inductive
        // remove the literal
        for ( k = i; k < Vec_IntSize(vExtra)-1; k++ )
            Vec_IntWriteEntry( vExtra, k, Vec_IntEntry(vExtra,k+1) );
        Vec_IntShrink( vExtra, Vec_IntSize(vExtra)-1 );
    }
}

void Fra_ClauMinimizeClause_rec	(	Cla_Man_t *	p,
		Vec_Int_t *	vBasis,
		Vec_Int_t *	vExtra
	)

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

Synopsis [Computes the minimal invariant that holds.]

Description [On entrace, vBasis does not hold, vBasis+vExtra holds but is not minimal. On exit, vBasis is unchanged, vBasis+vExtra is minimal.]

SideEffects []

SeeAlso []

Definition at line 515 of file fraClau.c.

{
    Vec_Int_t * vExtra2;
    int nSizeOld;
    if ( Vec_IntSize(vExtra) == 1 )
        return;
    nSizeOld = Vec_IntSize( vBasis );
    vExtra2 = Vec_IntSplitHalf( vExtra );

    // try the first half
    Vec_IntAppend( vBasis, vExtra );
    if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
    {
        Vec_IntShrink( vBasis, nSizeOld );
        Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
        return;
    }
    Vec_IntShrink( vBasis, nSizeOld );

    // try the second half
    Vec_IntAppend( vBasis, vExtra2 );
    if ( Fra_ClauCheckClause( p, vBasis, NULL ) )
    {
        Vec_IntShrink( vBasis, nSizeOld );
        Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
        return;
    }
//    Vec_IntShrink( vBasis, nSizeOld );

    // find the smallest with the second half added
    Fra_ClauMinimizeClause_rec( p, vBasis, vExtra );
    Vec_IntShrink( vBasis, nSizeOld );
    Vec_IntAppend( vBasis, vExtra );
    // find the smallest with the second half added
    Fra_ClauMinimizeClause_rec( p, vBasis, vExtra2 );
    Vec_IntShrink( vBasis, nSizeOld );
    Vec_IntAppend( vExtra, vExtra2 );
    Vec_IntFree( vExtra2 );
}

void Fra_ClauPrintClause	(	Vec_Int_t *	vSatCsVars,
		Vec_Int_t *	vCex
	)

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

Synopsis [Prints the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 598 of file fraClau.c.

{
    int LitM, VarM, VarN, i, j, k;
    assert( Vec_IntSize(vCex) <= Vec_IntSize(vSatCsVars) );
    for ( i = j = k = 0; i < Vec_IntSize(vCex) && j < Vec_IntSize(vSatCsVars); )
    {
        LitM = Vec_IntEntry( vCex, i );
        VarM = lit_var( LitM );
        VarN = Vec_IntEntry( vSatCsVars, j );
        if ( VarM < VarN )
        {
            assert( 0 );
        }
        else if ( VarM > VarN )
        {
            j++;
            printf( "-" );
        }
        else // if ( VarM == VarN )
        {
            i++;
            j++;
            printf( "%d", !lit_sign(LitM) );
        }
    }
    assert( i == Vec_IntSize(vCex) );
}

void Fra_ClauReduceClause	(	Vec_Int_t *	vMain,
		Vec_Int_t *	vNew
	)

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

Synopsis [Reduces the counter-example by removing complemented literals.]

Description [Removes literals from vMain that differ from those in the counter-example (vNew). Relies on the fact that the PI variables are assigned in the increasing order.]

SideEffects []

SeeAlso []

Definition at line 473 of file fraClau.c.

{
    int LitM, LitN, VarM, VarN, i, j, k;
    assert( Vec_IntSize(vMain) <= Vec_IntSize(vNew) );
    for ( i = j = k = 0; i < Vec_IntSize(vMain) && j < Vec_IntSize(vNew); )
    {
        LitM = Vec_IntEntry( vMain, i );
        LitN = Vec_IntEntry( vNew, j );
        VarM = lit_var( LitM );
        VarN = lit_var( LitN );
        if ( VarM < VarN )
        {
            assert( 0 );
        }
        else if ( VarM > VarN )
        {
            j++;
        }
        else // if ( VarM == VarN )
        {
            i++;
            j++;
            if ( LitM == LitN )
                Vec_IntWriteEntry( vMain, k++, LitM );
        }
    }
    assert( i == Vec_IntSize(vMain) );
    Vec_IntShrink( vMain, k );
}

void Fra_ClauRemapClause	(	int *	pMap,
		Vec_Int_t *	vClause,
		Vec_Int_t *	vRemapped,
		int	fInv
	)

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

Synopsis [Lifts the clause to depend on NS variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 402 of file fraClau.c.

{
    int iLit, i;
    Vec_IntClear( vRemapped );
    Vec_IntForEachEntry( vClause, iLit, i )
    {
        assert( pMap[lit_var(iLit)] >= 0 );
        iLit = toLitCond( pMap[lit_var(iLit)], lit_sign(iLit) ^ fInv );
        Vec_IntPush( vRemapped, iLit );
    }
}

Vec_Int_t* Fra_ClauSaveInputVars	(	Aig_Man_t *	pMan,
		Cnf_Dat_t *	pCnf,
		int	nStarting
	)

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

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 128 of file fraClau.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj;
    int i;
    vVars = Vec_IntAlloc( Aig_ManCiNum(pMan) - nStarting );
    Aig_ManForEachCi( pMan, pObj, i )
    {
        if ( i < nStarting )
            continue;
        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
    }
    return vVars;
}

Vec_Int_t* Fra_ClauSaveLatchVars	(	Aig_Man_t *	pMan,
		Cnf_Dat_t *	pCnf,
		int	fCsVars
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 84 of file fraClau.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObjLo, * pObjLi;
    int i;
    vVars = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    Aig_ManForEachLiLoSeq( pMan, pObjLi, pObjLo, i )
        Vec_IntPush( vVars, pCnf->pVarNums[fCsVars? pObjLo->Id : pObjLi->Id] );
    return vVars;
}

Vec_Int_t* Fra_ClauSaveOutputVars	(	Aig_Man_t *	pMan,
		Cnf_Dat_t *	pCnf
	)

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

Synopsis [Saves variables corresponding to latch outputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file fraClau.c.

{
    Vec_Int_t * vVars;
    Aig_Obj_t * pObj;
    int i;
    vVars = Vec_IntAlloc( Aig_ManCoNum(pMan) );
    Aig_ManForEachCo( pMan, pObj, i )
        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
    return vVars;
}

Cla_Man_t* Fra_ClauStart

(

Aig_Man_t *

pMan

)

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

Synopsis [Takes the AIG with the single output to be checked.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file fraClau.c.

{
    Cla_Man_t * p;
    Cnf_Dat_t * pCnfMain;
    Cnf_Dat_t * pCnfTest;
    Cnf_Dat_t * pCnfBmc;
    Aig_Man_t * pFramesMain;
    Aig_Man_t * pFramesTest;
    Aig_Man_t * pFramesBmc;
    assert( Aig_ManCoNum(pMan) - Aig_ManRegNum(pMan) == 1 );

    // start the manager
    p = ABC_ALLOC( Cla_Man_t, 1 );
    memset( p, 0, sizeof(Cla_Man_t) );
    p->vCexMain0 = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    p->vCexMain  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    p->vCexTest  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    p->vCexBase  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    p->vCexAssm  = Vec_IntAlloc( Aig_ManRegNum(pMan) );
    p->vCexBmc   = Vec_IntAlloc( Aig_ManRegNum(pMan) );

    // derive two timeframes to be checked
    pFramesMain = Aig_ManFrames( pMan, 2, 0, 1, 0, 0, NULL ); // nFrames, fInit, fOuts, fRegs
//Aig_ManShow( pFramesMain, 0, NULL );
    assert( Aig_ManCoNum(pFramesMain) == 2 );
    Aig_ObjChild0Flip( Aig_ManCo(pFramesMain, 0) ); // complement the first output
    pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
    p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfMain, 1, 0 );
/*
    {
        int i;
        Aig_Obj_t * pObj;
        Aig_ManForEachObj( pFramesMain, pObj, i )
            printf( "%d -> %d  \n", pObj->Id, pCnfMain->pVarNums[pObj->Id] );
        printf( "\n" );
    }
*/

    // derive one timeframe to be checked
    pFramesTest = Aig_ManFrames( pMan, 1, 0, 0, 1, 0, NULL );
    assert( Aig_ManCoNum(pFramesTest) == Aig_ManRegNum(pMan) );
    pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
    p->pSatTest = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfTest, 1, 0 );
    p->nSatVarsTestBeg = p->nSatVarsTestCur = sat_solver_nvars( p->pSatTest );

    // derive one timeframe to be checked for BMC
    pFramesBmc = Aig_ManFrames( pMan, 1, 1, 0, 1, 0, NULL );
//Aig_ManShow( pFramesBmc, 0, NULL );
    assert( Aig_ManCoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
    pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
    p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );

    // create variable sets
    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManCiNum(pMan)-Aig_ManRegNum(pMan)) );
    p->vSatVarsTestCs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 1 );
    p->vSatVarsTestNs = Fra_ClauSaveLatchVars( pFramesTest, pCnfTest, 0 );
    p->vSatVarsBmcNs  = Fra_ClauSaveOutputVars( pFramesBmc, pCnfBmc );
    assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsMainCs) );
    assert( Vec_IntSize(p->vSatVarsTestCs) == Vec_IntSize(p->vSatVarsBmcNs) );

    // create mapping of CS into NS vars
    p->pMapCsMainToCsTest = Fra_ClauCreateMapping( p->vSatVarsMainCs, p->vSatVarsTestCs, Aig_ManObjNumMax(pFramesMain) );
    p->pMapCsTestToCsMain = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsMainCs, Aig_ManObjNumMax(pFramesTest) );
    p->pMapCsTestToNsTest = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsTestNs, Aig_ManObjNumMax(pFramesTest) );
    p->pMapCsTestToNsBmc  = Fra_ClauCreateMapping( p->vSatVarsTestCs, p->vSatVarsBmcNs,  Aig_ManObjNumMax(pFramesTest) );

    // cleanup
    Cnf_DataFree( pCnfMain );
    Cnf_DataFree( pCnfTest );
    Cnf_DataFree( pCnfBmc );
    Aig_ManStop( pFramesMain );
    Aig_ManStop( pFramesTest );
    Aig_ManStop( pFramesBmc );
    if ( p->pSatMain == NULL || p->pSatTest == NULL || p->pSatBmc == NULL )
    {
        Fra_ClauStop( p );
        return NULL;
    }
    return p;
}

void Fra_ClauStop

(

Cla_Man_t *

p

)

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

Synopsis [Deletes the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 178 of file fraClau.c.

{
    ABC_FREE( p->pMapCsMainToCsTest );
    ABC_FREE( p->pMapCsTestToCsMain );
    ABC_FREE( p->pMapCsTestToNsTest );
    ABC_FREE( p->pMapCsTestToNsBmc  );
    Vec_IntFree( p->vSatVarsMainCs );
    Vec_IntFree( p->vSatVarsTestCs );
    Vec_IntFree( p->vSatVarsTestNs );
    Vec_IntFree( p->vSatVarsBmcNs );
    Vec_IntFree( p->vCexMain0 );
    Vec_IntFree( p->vCexMain );
    Vec_IntFree( p->vCexTest );
    Vec_IntFree( p->vCexBase );
    Vec_IntFree( p->vCexAssm );
    Vec_IntFree( p->vCexBmc  );
    if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
    if ( p->pSatTest ) sat_solver_delete( p->pSatTest );
    if ( p->pSatBmc )  sat_solver_delete( p->pSatBmc );
    ABC_FREE( p );
}

static void Vec_IntComplement ( Vec_Int_t *  vVec )

static

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

Synopsis [Complements all literals in the clause.]

Description []

SideEffects []

SeeAlso []

Definition at line 327 of file fraClau.c.

{
    int i;
    for ( i = 0; i < Vec_IntSize(vVec); i++ )
        vVec->pArray[i] = lit_neg( vVec->pArray[i] );
}

static Vec_Int_t* Vec_IntSplitHalf ( Vec_Int_t *  vVec )

static

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

Synopsis [Splits off second half and returns it as a new vector.]

Description []

SideEffects []

SeeAlso []

Definition at line 304 of file fraClau.c.

{
    Vec_Int_t * vPart;
    int Entry, i;
    assert( Vec_IntSize(vVec) > 1 );
    vPart = Vec_IntAlloc( Vec_IntSize(vVec) / 2 + 1 );
    Vec_IntForEachEntryStart( vVec, Entry, i, Vec_IntSize(vVec) / 2 )
        Vec_IntPush( vPart, Entry );
    Vec_IntShrink( vVec, Vec_IntSize(vVec) / 2 );
    return vPart;
}