Version abc70727

1 files changed, 205 insertions, 0 deletions

diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
new file mode 100644
index 00000000..1bfe1cb4
--- /dev/null
+++ b/src/aig/fra/fraInd.c
@@ -0,0 +1,205 @@
+/**CFile****************************************************************
+
+  FileName    [fraInd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Inductive prover.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
+{
+    Aig_Man_t * pManFraig;
+    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjReprNew, * pMiter;
+    Aig_Obj_t ** pLatches;
+    int i, k, f;
+    assert( p->pManFraig == NULL );
+    assert( Aig_ManInitNum(p->pManAig) > 0 );
+    assert( Aig_ManInitNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
+
+    // start the fraig package
+    pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFrames );
+    pManFraig->vInits = Vec_IntDup(p->pManAig->vInits);
+    // create PI nodes for the frames
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
+        Aig_ManForEachPiSeq( p->pManAig, pObj, i )
+            Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
+    }
+    // create latches for the first frame
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
+
+    // add timeframes
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManInitNum(p->pManAig) );
+    for ( f = 0; f < p->nFrames - 1; f++ )
+    {
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pManAig, pObj, i )
+        {
+            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
+            Fra_ObjSetFraig( pObj, f, pObjNew );
+            // skip nodes without representative
+            if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
+                continue;
+            assert( pObjRepr->Id < pObj->Id );
+            // get the new node of the representative
+            pObjReprNew = Fra_ObjFraig( pObjRepr, f );
+            // if this is the same node, no need to add constraints
+            if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+                continue;
+            // these are different nodes
+            // perform speculative reduction
+            Fra_ObjSetFraig( pObj, f, Aig_NotCond(pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase) );
+            // add the constraint
+            pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
+            pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
+            Aig_ObjCreatePo( pManFraig, pMiter );
+        }
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+            pLatches[k++] = Fra_ObjChild0Fra(pObj,f);
+        assert( k == Aig_ManInitNum(p->pManAig) );
+        // insert them to the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+            Fra_ObjSetFraig( pObj, f+1, pLatches[k++] );
+        assert( k == Aig_ManInitNum(p->pManAig) );
+    }
+    free( pLatches );
+    // mark the asserts
+    pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
+    // add the POs for the latch inputs
+    Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+        Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f) );
+
+    // set the pointer to the manager
+    Aig_ManForEachObj( p->pManAig, pObj, i )
+        pObj->pData = p;
+    // set the pointers to the manager
+    Aig_ManForEachObj( pManFraig, pObj, i )
+        pObj->pData = p;
+    // make sure the satisfying assignment is node assigned
+    assert( pManFraig->pData == NULL );
+    return pManFraig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs choicing of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_Induction( Aig_Man_t * pManAig, int nFrames, int fVerbose )
+{
+    Fra_Man_t * p;
+    Fra_Par_t Pars, * pPars = &Pars; 
+    Aig_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pManAigNew;
+    int nIter, i;
+
+    if ( Aig_ManNodeNum(pManAig) == 0 )
+        return Aig_ManDup(pManAig, 1);
+    assert( Aig_ManLatchNum(pManAig) == 0 );
+    assert( Aig_ManInitNum(pManAig) > 0 );
+
+    // get parameters
+    Fra_ParamsDefaultSeq( pPars );
+    pPars->nTimeFrames = nFrames;
+    pPars->fVerbose = fVerbose;
+
+    // start the fraig manager for this run
+    p = Fra_ManStart( pManAig, pPars );
+    // derive and refine e-classes using the 1st init frame
+    Fra_Simulate( p, 1 );
+
+    // refine e-classes using sequential simulation
+
+    // iterate the inductive case
+    p->pCla->fRefinement = 1;
+    for ( nIter = 0; p->pCla->fRefinement; nIter++ )
+    {
+        // mark the classes as non-refined
+        p->pCla->fRefinement = 0;
+        // derive non-init K-timeframes while implementing e-classes
+        p->pManFraig = Fra_FramesWithClasses( p );
+        if ( fVerbose )
+            printf( "Iter = %3d.  Original = %6d. Reduced = %6d.\n", 
+                nIter, Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
+
+        // perform AIG rewriting on the speculated frames
+
+        // convert the manager to SAT solver (the last nLatches outputs are inputs)
+        pCnf = Cnf_Derive( p->pManFraig, Aig_ManInitNum(p->pManFraig) );
+        p->pSat = Cnf_DataWriteIntoSolver( pCnf );
+        // transfer variable numbers
+        Aig_ManForEachPi( p->pManAig, pObj, i )
+            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+        Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+        {
+            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+            Fra_ObjSetFaninVec( pObj, (void *)1 );
+        }
+        Cnf_DataFree( pCnf );
+
+        // perform sweeping
+        Fra_FraigSweep( p );
+        assert( Vec_PtrSize(p->vTimeouts) == 0 );
+        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
+        sat_solver_delete( p->pSat );  p->pSat = NULL;
+    }
+
+    // move the classes into representatives
+    Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
+    // implement the classes
+    pManAigNew = Aig_ManDupRepr( pManAig );
+    Fra_ManStop( p );
+    return pManAigNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+