intContain.c 10.5 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
/**CFile****************************************************************

  FileName    [intContain.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Interpolation engine.]

  Synopsis    [Interpolant containment checking.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

  Revision    [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "intInt.h"
22
#include "proof/fra/fra.h"
Alan Mishchenko committed
23

24 25
ABC_NAMESPACE_IMPL_START

Alan Mishchenko committed
26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames );

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    [Checks constainment of two interpolants.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
{
    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 );
60
//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
Alan Mishchenko committed
61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90
    }
    assert( RetValue != -1 );
    Aig_ManStop( pMiter );
    return RetValue;
}

/**Function*************************************************************

  Synopsis    [Checks constainment of two interpolants.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
{
    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 );
91
//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
Alan Mishchenko committed
92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
    }
    assert( RetValue != -1 );
    Aig_ManStop( pMiter );
    return RetValue;
}


/**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.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
{
    Aig_Man_t * pFrames;
    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
    int i, f;
    assert( Saig_ManRegNum(pAig) > 0 );
    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
    // map the constant node
    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
    // create variables for register outputs
    *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
    Saig_ManForEachLo( pAig, pObj, i )
    {
124
        pObj->pData = Aig_ObjCreateCi( pFrames );
Alan Mishchenko committed
125 126 127 128 129 130 131
        Vec_PtrPush( *pvMapReg, pObj->pData );
    }
    // add timeframes
    for ( f = 0; f < nFrames; f++ )
    {
        // create PI nodes for this frame
        Saig_ManForEachPi( pAig, pObj, i )
132
            pObj->pData = Aig_ObjCreateCi( pFrames );
Alan Mishchenko committed
133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163
        // add internal nodes of this frame
        Aig_ManForEachNode( pAig, pObj, i )
            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(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;
            Vec_PtrPush( *pvMapReg, pObjLo->pData );
        }
    }
    return pFrames;
}

/**Function*************************************************************

  Synopsis    [Duplicates AIG while mapping PIs into the given array.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
{
    Aig_Obj_t * pObj;
    int i;
164
    assert( Aig_ManCoNum(pOld) == 1 );
Alan Mishchenko committed
165 166 167
    // create the PIs
    Aig_ManCleanData( pOld );
    Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
168
    Aig_ManForEachCi( pOld, pObj, i )
Alan Mishchenko committed
169 170 171 172 173
        pObj->pData = ppNewPis[i];
    // duplicate internal nodes
    Aig_ManForEachNode( pOld, pObj, i )
        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
    // add one PO to new
174
    pObj = Aig_ManCo( pOld, 0 );
175
    Aig_ObjCreateCo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
Alan Mishchenko committed
176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
}


/**Function*************************************************************

  Synopsis    [Checks constainment of two interpolants inductively.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward )
{
    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);
Alan Mishchenko committed
205 206 207 208
    if ( !fBackward )
    { 
        // forward inductive check: p -> p -> ... -> !p
        for ( f = 0; f < nSteps; f++ )
Alan Mishchenko committed
209
            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
Alan Mishchenko committed
210
        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
Alan Mishchenko committed
211 212 213
    }
    else
    {
Alan Mishchenko committed
214 215 216
        // backward inductive check: p -> !p -> ... -> !p
        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
        for ( f = 1; f <= nSteps; f++ )
Alan Mishchenko committed
217 218 219 220 221 222 223
            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
    }
    Vec_PtrFree( vMapRegs );
    Aig_ManCleanup( pFrames );

    // convert to CNF
    pCnf = Cnf_Derive( pFrames, 0 ); 
224
    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
Alan Mishchenko committed
225 226 227 228 229 230 231 232 233 234 235
//    Cnf_DataFree( pCnf );
//    Aig_ManStop( pFrames );

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

     // solve the problem
Alan Mishchenko committed
236
    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
Alan Mishchenko committed
237 238 239 240 241 242 243 244 245

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

    Cnf_DataFree( pCnf );
    Aig_ManStop( pFrames );

    sat_solver_delete( pSat );
    return status == l_False;
}
246
ABC_NAMESPACE_IMPL_END
Alan Mishchenko committed
247

248
#include "proof/fra/fra.h"
Alan Mishchenko committed
249

250 251 252
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276
/**Function*************************************************************

  Synopsis    [Check if cex satisfies uniqueness constraints.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames )
{
    extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 );
    extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
    extern void Fra_SmlSimulateOne( Fra_Sml_t * p );

    Fra_Sml_t * pSml;
    Vec_Int_t * vPis;
    Aig_Obj_t * pObj, * pObj0;
    int i, k, v, iBit, * pCounterEx;
    int Counter;
    if ( nFrames == 1 )
        return 1;
277 278 279 280 281 282
//    if ( pSat->model.size == 0 )
    
    // possible consequences here!!!
    assert( 0 );

    if ( sat_solver_nvars(pSat) == 0 )
Alan Mishchenko committed
283 284 285
        return 1;
//    assert( Saig_ManPoNum(p) == 1 );
    assert( Aig_ManRegNum(p) > 0 );
286
    assert( Aig_ManRegNum(p) < Aig_ManCiNum(p) );
Alan Mishchenko committed
287 288 289

    // get the counter-example
    vPis = Vec_IntAlloc( 100 );
290
    Aig_ManForEachCi( pCnf->pMan, pObj, k )
Alan Mishchenko committed
291 292 293 294 295 296 297 298 299 300 301 302 303 304 305
        Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
    assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
    pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
    Vec_IntFree( vPis );

    // start a new sequential simulator
    pSml = Fra_SmlStart( p, 0, nFrames, 1 );
    // assign simulation info for the registers
    iBit = 0;
    Aig_ManForEachLoSeq( p, pObj, i )
        Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 );
    // assign simulation info for the primary inputs
    for ( i = 0; i < nFrames; i++ )
        Aig_ManForEachPiSeq( p, pObj, k )
            Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
306
    assert( iBit == Aig_ManCiNum(pCnf->pMan) );
Alan Mishchenko committed
307 308 309 310
    // run simulation
    Fra_SmlSimulateOne( pSml );

    // check if the given output has failed
311
//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManCo(pAig, 0) );
Alan Mishchenko committed
312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330
//    assert( RetValue );

    // check values at the internal nodes
    Counter = 0;
    for ( i = 0; i < nFrames; i++ )
    for ( k = i+1; k < nFrames; k++ )
    {
        for ( v = 0; v < Aig_ManRegNum(p); v++ )
        {
            pObj0 = Aig_ManLo(p, v);
            if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) )
                break;
        }
        if ( v == Aig_ManRegNum(p) )
            Counter++;
    }
    printf( "Uniquness does not hold in %d frames.\n", Counter );

    Fra_SmlStop( pSml );
Alan Mishchenko committed
331
    ABC_FREE( pCounterEx );
Alan Mishchenko committed
332 333 334 335 336 337 338 339
    return 1;
}

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


340 341
ABC_NAMESPACE_IMPL_END