Version abc80130

1 files changed, 0 insertions, 759 deletions

diff --git a/src/aig/fra/fraClau.c b/src/aig/fra/fraClau.c
deleted file mode 100644
index fc239a40..00000000
--- a/src/aig/fra/fraClau.c
+++ /dev/null
@@ -1,759 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "fra.h"
-#include "cnf.h"
-#include "satSolver.h"
-
-/*
-    This code is inspired by the paper: Aaron Bradley and Zohar Manna, 
-    "Checking safety by inductive generalization of counterexamples to 
-    induction", FMCAD '07.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Cla_Man_t_    Cla_Man_t;
-struct Cla_Man_t_
-{
-    // SAT solvers
-    sat_solver *     pSatMain;
-    sat_solver *     pSatTest;
-    sat_solver *     pSatBmc;
-    // CNF for the test solver
-//    Cnf_Dat_t *      pCnfTest;
-    // SAT variables
-    Vec_Int_t *      vSatVarsMainCs;
-    Vec_Int_t *      vSatVarsTestCs;
-    Vec_Int_t *      vSatVarsTestNs;
-    Vec_Int_t *      vSatVarsBmcNs;
-    // helper variables
-    int              nSatVarsTestBeg;
-    int              nSatVarsTestCur;
-    // counter-examples
-    Vec_Int_t *      vCexMain0;
-    Vec_Int_t *      vCexMain;
-    Vec_Int_t *      vCexTest;
-    Vec_Int_t *      vCexBase;
-    Vec_Int_t *      vCexAssm;
-    Vec_Int_t *      vCexBmc;
-    // mapping of CS into NS var numbers
-    int *            pMapCsMainToCsTest; 
-    int *            pMapCsTestToCsMain; 
-    int *            pMapCsTestToNsTest; 
-    int *            pMapCsTestToNsBmc;  
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Saves variables corresponding to latch outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_ClauSaveLatchVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int fCsVars )
-{
-    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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Saves variables corresponding to latch outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_ClauSaveOutputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf )
-{
-    Vec_Int_t * vVars;
-    Aig_Obj_t * pObj;
-    int i;
-    vVars = Vec_IntAlloc( Aig_ManPoNum(pMan) );
-    Aig_ManForEachPo( pMan, pObj, i )
-        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
-    return vVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Saves variables corresponding to latch outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_ClauSaveInputVars( Aig_Man_t * pMan, Cnf_Dat_t * pCnf, int nStarting )
-{
-    Vec_Int_t * vVars;
-    Aig_Obj_t * pObj;
-    int i;
-    vVars = Vec_IntAlloc( Aig_ManPiNum(pMan) - nStarting );
-    Aig_ManForEachPi( pMan, pObj, i )
-    {
-        if ( i < nStarting )
-            continue;
-        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
-    }
-    return vVars;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Saves variables corresponding to latch outputs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int * Fra_ClauCreateMapping( Vec_Int_t * vSatVarsFrom, Vec_Int_t * vSatVarsTo, int nVarsMax )
-{
-    int * pMapping, Var, i;
-    assert( Vec_IntSize(vSatVarsFrom) == Vec_IntSize(vSatVarsTo) );
-    pMapping = 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;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Deletes the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClauStop( Cla_Man_t * p )
-{
-    free( p->pMapCsMainToCsTest );
-    free( p->pMapCsTestToCsMain );
-    free( p->pMapCsTestToNsTest );
-    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 );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Takes the AIG with the single output to be checked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Cla_Man_t * Fra_ClauStart( Aig_Man_t * pMan )
-{
-    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_ManPoNum(pMan) - Aig_ManRegNum(pMan) == 1 );
-
-    // start the manager
-    p = 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_ManPoNum(pFramesMain) == 2 );
-    Aig_ObjChild0Flip( Aig_ManPo(pFramesMain, 0) ); // complement the first output
-    pCnfMain = Cnf_DeriveSimple( pFramesMain, 0 );
-//Cnf_DataWriteIntoFile( pCnfMain, "temp.cnf", 1 );
-    p->pSatMain = 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_ManPoNum(pFramesTest) == Aig_ManRegNum(pMan) );
-    pCnfTest = Cnf_DeriveSimple( pFramesTest, Aig_ManRegNum(pMan) );
-    p->pSatTest = 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_ManPoNum(pFramesBmc) == Aig_ManRegNum(pMan) );
-    pCnfBmc = Cnf_DeriveSimple( pFramesBmc, Aig_ManRegNum(pMan) );
-    p->pSatBmc = Cnf_DataWriteIntoSolver( pCnfBmc, 1, 0 );
-
-    // create variable sets
-    p->vSatVarsMainCs = Fra_ClauSaveInputVars( pFramesMain, pCnfMain, 2 * (Aig_ManPiNum(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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Splits off second half and returns it as a new vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Vec_Int_t * Vec_IntSplitHalf( Vec_Int_t * vVec )
-{
-    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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Appends the contents of the second vector.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
-{
-    int Entry, i;
-    Vec_IntForEachEntry( vVec2, Entry, i )
-        Vec_IntPush( vVec1, Entry );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Complements all literals in the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Vec_IntComplement( Vec_Int_t * vVec )
-{
-    int i;
-    for ( i = 0; i < Vec_IntSize(vVec); i++ )
-        vVec->pArray[i] = lit_neg( vVec->pArray[i] );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the property holds. Returns counter-example if not.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClauCheckProperty( Cla_Man_t * p, Vec_Int_t * vCex )
-{
-    int nBTLimit = 0;
-    int RetValue, iVar, i;
-    sat_solver_act_var_clear( p->pSatMain );
-    RetValue = sat_solver_solve( p->pSatMain, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the clause holds using BMC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClauCheckBmc( Cla_Man_t * p, Vec_Int_t * vClause )
-{
-    int nBTLimit = 0;
-    int RetValue;
-    RetValue = sat_solver_solve( p->pSatBmc, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause), 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-    if ( RetValue == l_False )
-        return 1;
-    assert( RetValue == l_True );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Lifts the clause to depend on NS variables.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClauRemapClause( int * pMap, Vec_Int_t * vClause, Vec_Int_t * vRemapped, int fInv )
-{
-    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 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks if the clause holds. Returns counter example if not.]
-
-  Description [Uses test SAT solver.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
-{
-    int nBTLimit = 0;
-    int RetValue, iVar, i;
-    int nClauseSize = Vec_IntSize( vClause );
-    // 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), 
-        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)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;
-}
-
-/**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     []
-
-***********************************************************************/
-void Fra_ClauReduceClause( Vec_Int_t * vMain, Vec_Int_t * vNew )
-{
-    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 );
-}
-
-/**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     []
-
-***********************************************************************/
-void Fra_ClauMinimizeClause_rec( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
-{
-    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 );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Minimizes the clauses using a simple method.]
-
-  Description [The input and output clause are in vExtra.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClauMinimizeClause( Cla_Man_t * p, Vec_Int_t * vBasis, Vec_Int_t * vExtra )
-{
-    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 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the clause.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClauPrintClause( Vec_Int_t * vSatCsVars, Vec_Int_t * vCex )
-{
-    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) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Takes the AIG with the single output to be checked.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
-{
-    Cla_Man_t * p;
-    int Iter, RetValue, fFailed, i;
-    assert( Aig_ManPoNum(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;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-