fraClau.c

Go to the documentation of this file.

 
#include "fra.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
 
ABC_NAMESPACE_IMPL_START
 
 
/*
    This code is inspired by the paper: Aaron Bradley and Zohar Manna, 
    "Checking safety by inductive generalization of counterexamples to 
    induction", FMCAD '07.
*/

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


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

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_ManCoNum(pMan) );
    Aig_ManForEachCo( pMan, pObj, i )
        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
    return vVars;
}

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_ManCiNum(pMan) - nStarting );
    Aig_ManForEachCi( pMan, pObj, i )
    {
        if ( i < nStarting )
            continue;
        Vec_IntPush( vVars, pCnf->pVarNums[pObj->Id] );
    }
    return vVars;
}

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 = 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_ClauStop( Cla_Man_t * p )
{
    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 );
}

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

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

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

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, (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_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), 
        (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;
}

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

int Fra_ClauCheckClause( Cla_Man_t * p, Vec_Int_t * vClause, Vec_Int_t * vCex )
{
    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;
}

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

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

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

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

int Fra_Clau( Aig_Man_t * pMan, int nIters, int fVerbose, int fVeryVerbose )
{
    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;
}
 

 
 
ABC_NAMESPACE_IMPL_END