intInter.c

Go to the documentation of this file.

 
#include "intInt.h"
 
ABC_NAMESPACE_IMPL_START
 



Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
{
    Aig_Man_t * pInterC;
    assert( Aig_ManCiNum(pInter) <= Aig_ManCiNum(pOther) );
    pInterC = Aig_ManDupSimple( pInter );
    Aig_IthVar( pInterC, Aig_ManCiNum(pOther)-1 );
    assert( Aig_ManCiNum(pInterC) == Aig_ManCiNum(pOther) );
    return pInterC;
}

void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
{
    extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
    Aig_Man_t * pLower, * pUpper, * pInterC;
    int RetValue1, RetValue2;
 
    pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
    pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
    Aig_ManFlipFirstPo( pUpper );
 
    pInterC = Inter_ManDupExpand( pInter, pLower );
    RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
    Aig_ManStop( pInterC );
 
    pInterC = Inter_ManDupExpand( pInter, pUpper );
    RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
    Aig_ManStop( pInterC );
    
    if ( RetValue1 && RetValue2 )
        printf( "Im is correct.\n" );
    if ( !RetValue1 )
        printf( "Property A => Im fails.\n" );
    if ( !RetValue2 )
        printf( "Property Im => !B fails.\n" );
 
    Aig_ManStop( pLower );
    Aig_ManStop( pUpper );
}

void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
{
    extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
    Aig_Man_t * pLower, * pUpper, * pInterC;
    int RetValue1, RetValue2;
 
    pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
    pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
    Aig_ManFlipFirstPo( pUpper );
 
    pInterC = Inter_ManDupExpand( pInter, pLower );
//Aig_ManPrintStats( pLower );
//Aig_ManPrintStats( pUpper );
//Aig_ManPrintStats( pInterC );
//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
    RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
    Aig_ManStop( pInterC );
 
    pInterC = Inter_ManDupExpand( pInter, pUpper );
    RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
    Aig_ManStop( pInterC );
    
    if ( RetValue1 && RetValue2 )
        printf( "Ip is correct.\n" );
    if ( !RetValue1 )
        printf( "Property A => Ip fails.\n" );
    if ( !RetValue2 )
        printf( "Property Ip => !B fails.\n" );
 
    Aig_ManStop( pLower );
    Aig_ManStop( pUpper );
}

 
 
ABC_NAMESPACE_IMPL_END