Multi-output property solver.

src/misc/extra/extraZddTrunc.c

+/**CFile****************************************************************
+
+  FileName    [extraZddTrunc.c]
+
+  PackageName [extra]
+
+  Synopsis    [Procedure to truncate a ZDD using variable probabilities.]
+
+  Author      [Alan Mishchenko]
+
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraZddTrunc.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
+
+***********************************************************************/
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/st/st.h"
+#include "bdd/cudd/cuddInt.h"
+
+#ifdef _WIN32
+#define inline __inline // compatible with MS VS 6.0
+#endif
+
+ABC_NAMESPACE_IMPL_START
+
+
+#define TEST_VAR_MAX 10
+#define TEST_SET_MAX 10
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+
+// dynamic vector of intergers
+typedef struct Vec_Int_t_       Vec_Int_t;
+struct Vec_Int_t_ 
+{
+    int              nCap;
+    int              nSize;
+    int *            pArray;
+};
+static inline Vec_Int_t * Vec_IntAlloc( int nCap )
+{
+    Vec_Int_t * p;
+    p = ABC_ALLOC( Vec_Int_t, 1 );
+    if ( nCap > 0 && nCap < 16 )
+        nCap = 16;
+    p->nSize  = 0;
+    p->nCap   = nCap;
+    p->pArray = p->nCap? ABC_ALLOC( int, p->nCap ) : NULL;
+    return p;
+}
+static inline void Vec_IntFree( Vec_Int_t * p )
+{
+    ABC_FREE( p->pArray );
+    ABC_FREE( p );
+}
+static inline int * Vec_IntReleaseArray( Vec_Int_t * p )
+{
+    int * pArray = p->pArray;
+    p->nCap = 0;
+    p->nSize = 0;
+    p->pArray = NULL;
+    return pArray;
+}
+static inline int Vec_IntAddToEntry( Vec_Int_t * p, int i, int Addition )
+{
+    assert( i >= 0 && i < p->nSize );
+    return p->pArray[i] += Addition;
+}
+static inline void Vec_IntGrow( Vec_Int_t * p, int nCapMin )
+{
+    if ( p->nCap >= nCapMin )
+        return;
+    p->pArray = ABC_REALLOC( int, p->pArray, nCapMin ); 
+    assert( p->pArray );
+    p->nCap   = nCapMin;
+}
+static inline int Vec_IntPop( Vec_Int_t * p )
+{
+    assert( p->nSize > 0 );
+    return p->pArray[--p->nSize];
+}
+static inline void Vec_IntPush( Vec_Int_t * p, int Entry )
+{
+    if ( p->nSize == p->nCap )
+    {
+        if ( p->nCap < 16 )
+            Vec_IntGrow( p, 16 );
+        else
+            Vec_IntGrow( p, 2 * p->nCap );
+    }
+    p->pArray[p->nSize++] = Entry;
+}
+static inline void Vec_IntAppend( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
+{
+    int i;
+    for ( i = 0; i < vVec2->nSize; i++ )
+        Vec_IntPush( vVec1, vVec2->pArray[i] );
+}
+
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Compute the set of subsets whose probability is more than ProbLimit.]
+
+  Description [The resulting array has the following form:  The first integer entry 
+  is the number of resulting subsets.  The following integer entries in the array
+  contain as many subsets. Each subset is an array of integers followed by -1. 
+  See how subsets are printed in the included test procedure below.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_zddTruncate_rec(
+  DdManager * dd, 
+  DdNode * zFunc,       // zFunc is the ZDD to be truncated
+  double * pVarProbs,    // pVarProbs is probabilities of each variable (should have at least dd->sizeZ entries)
+  double ProbLimit,      // ProbLimit is the limit on the probabilities (only those more than this will be collected)
+  double ProbThis,       // current path probability
+  Vec_Int_t * vSubset,  // current subset under construction
+  Vec_Int_t * vResult ) // resulting subsets to be returned to the user
+{
+    // quit if probability of the path is less then the limit
+    if ( ProbThis < ProbLimit )
+        return;
+    // quit if there is no subsets
+    if ( zFunc == Cudd_ReadZero(dd) ) 
+        return;
+    // quit and save a new subset if there is one
+    if ( zFunc == Cudd_ReadOne(dd) ) 
+    {
+        Vec_IntAddToEntry( vResult, 0, 1 );
+        Vec_IntAppend( vResult, vSubset );
+        Vec_IntPush( vResult, -1 );
+        return;
+    }
+    // call recursively for the set without the given variable
+    Extra_zddTruncate_rec( dd, cuddE(zFunc), pVarProbs, ProbLimit, ProbThis, vSubset, vResult );
+    // call recursively for the set with the given variable
+    Vec_IntPush( vSubset, Cudd_NodeReadIndex(zFunc) );
+    Extra_zddTruncate_rec( dd, cuddT(zFunc), pVarProbs, ProbLimit, ProbThis * pVarProbs[Cudd_NodeReadIndex(zFunc)], vSubset, vResult );
+    Vec_IntPop( vSubset );
+}
+int * Extra_zddTruncate( 
+  DdManager * dd, 
+  DdNode * zFunc,       // zFunc is the ZDD to be truncated
+  double * pVarProbs,    // pVarProbs is probabilities of each variable (should have at least dd->sizeZ entries)
+  double ProbLimit )     // ProbLimit is the limit on the probabilities (only those more than this will be collected)
+{
+    Vec_Int_t * vSubset, * vResult;
+    int i, sizeZ = Cudd_ReadZddSize(dd);
+    int * pResult;
+    // check that probabilities are reasonable
+    assert( ProbLimit > 0 && ProbLimit <= 1 );
+    for ( i = 0; i < sizeZ; i++ )
+        assert( pVarProbs[i] > 0 && pVarProbs[i] <= 1 );
+    // enumerate assignments satisfying the probability limit
+    vSubset = Vec_IntAlloc( sizeZ );
+    vResult = Vec_IntAlloc( 10 * sizeZ );
+    Vec_IntPush( vResult, 0 );
+    Extra_zddTruncate_rec( dd, zFunc, pVarProbs, ProbLimit, 1, vSubset, vResult );
+    Vec_IntFree( vSubset );
+    pResult = Vec_IntReleaseArray( vResult );
+    Vec_IntFree( vResult );
+    return pResult;
+} // end of Extra_zddTruncate 
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the combination composed of a single ZDD variable.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Extra_zddVariable( DdManager * dd, int iVar )
+{
+    DdNode * zRes;
+    do {
+        dd->reordered = 0;
+        zRes = cuddZddGetNode( dd, iVar, Cudd_ReadOne(dd), Cudd_ReadZero(dd) ); 
+    } while (dd->reordered == 1);
+    return zRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Creates ZDD representing a given set of subsets.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_zddCreateSubsets(
+  DdManager * dd,
+  int pSubsets[][TEST_VAR_MAX+1],
+  int nSubsets )
+{
+    int i, k;
+    DdNode * zOne, * zVar, * zRes, * zTemp;
+    zRes = Cudd_ReadZero(dd); Cudd_Ref( zRes );
+    for ( i = 0; i < nSubsets; i++ )
+    {
+        zOne = Cudd_ReadOne(dd); Cudd_Ref( zOne );
+        for ( k = 0; pSubsets[i][k] != -1; k++ )
+        {
+            assert( pSubsets[i][k] < TEST_VAR_MAX );
+            zVar = Extra_zddVariable( dd, pSubsets[i][k] );
+            zOne = Cudd_zddUnateProduct( dd, zTemp = zOne, zVar ); Cudd_Ref( zOne );
+            Cudd_RecursiveDerefZdd( dd, zTemp );
+        }
+        zRes = Cudd_zddUnion( dd, zRes, zOne ); Cudd_Ref( zRes );
+        Cudd_RecursiveDerefZdd( dd, zOne );
+    }
+    Cudd_Deref( zRes );
+    return zRes;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Prints a set of subsets represented using as an array.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_zddPrintSubsets( int * pSubsets )
+{
+    int i, k, Counter = 0;
+    printf( "The set contains %d subsets:\n", pSubsets[0] );
+    for ( i = k = 0; i < pSubsets[0]; i++ )
+    {
+        printf( "Subset %3d : {", Counter );
+        for ( k++; pSubsets[k] != -1; k++ )
+            printf( " %d", pSubsets[k] );
+        printf( " }\n" );
+        Counter++;
+    }
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Testbench for the above truncation procedure.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_zddTruncateTest()
+{
+    // input data
+    int nSubsets = 5;
+    int pSubsets[TEST_SET_MAX][TEST_VAR_MAX+1] = { {0, 3, 5, -1}, {1, 2, 3, 6, 9, -1}, {1, 5, 7, 8, -1}, {2, 4, -1}, {0, 5, 6, 9, -1} };
+    // varible probabilities
+    double pVarProbs[TEST_VAR_MAX] = { 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1, 0.1 };
+    double ProbLimit = 0.001;
+    // output data
+    int * pOutput;
+    // start the manager and create ZDD representing the input subsets
+    DdManager * dd = Cudd_Init( 0, TEST_VAR_MAX, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS , 0 );
+    DdNode * zFunc = Extra_zddCreateSubsets( dd, pSubsets, nSubsets );  Cudd_Ref( zFunc );
+    assert( nSubsets <= TEST_SET_MAX );
+    // print the input ZDD
+    printf( "The initial ZDD representing %d subsets:\n", nSubsets );
+    Cudd_zddPrintMinterm( dd, zFunc );
+    // compute the result of truncation
+    pOutput = Extra_zddTruncate( dd, zFunc, pVarProbs, ProbLimit );
+    // print the resulting ZDD
+    printf( "The resulting ZDD representing %d subsets:\n", pOutput[0] );
+    // print the resulting subsets
+    Extra_zddPrintSubsets( pOutput );
+    // cleanup
+    ABC_FREE( pOutput );
+    Cudd_RecursiveDerefZdd( dd, zFunc );
+    Cudd_Quit( dd );
+} 
+
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                           END OF FILE                            ///
+////////////////////////////////////////////////////////////////////////
+ABC_NAMESPACE_IMPL_END
+

src/sat/bmc/bmcMulti.c

+/**CFile****************************************************************
+
+  FileName    [bmcMulti.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Proving multi-output properties.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcMulti.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "proof/ssw/ssw.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Divides outputs into solved and unsolved.]
+
+  Description [Return array of unsolved outputs to extract into a new AIG.
+  Updates the resulting CEXes (vCexesOut) and current output map (vOutMap).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Gia_ManProcessOutputs( Vec_Ptr_t * vCexesIn, Vec_Ptr_t * vCexesOut, Vec_Int_t * vOutMap )
+{
+    Abc_Cex_t * pCex; 
+    Vec_Int_t * vLeftOver;
+    int i, iOut;
+    assert( Vec_PtrSize(vCexesIn) == Vec_IntSize(vOutMap) );
+    vLeftOver = Vec_IntAlloc( Vec_PtrSize(vCexesIn) );
+    Vec_IntForEachEntry( vOutMap, iOut, i )
+    {
+        assert( Vec_PtrEntry(vCexesOut, iOut) == NULL );
+        pCex = (Abc_Cex_t *)Vec_PtrEntry( vCexesIn, i );
+        if ( pCex ) // found a CEX for output iOut
+        {
+            Vec_PtrWriteEntry( vCexesIn, i, NULL );
+            Vec_PtrWriteEntry( vCexesOut, iOut, pCex );
+        }
+        else // still unsolved
+        {
+            Vec_IntWriteEntry( vOutMap, Vec_IntSize(vLeftOver), iOut );
+            Vec_IntPush( vLeftOver, i );
+        }
+    }
+    Vec_IntShrink( vOutMap, Vec_IntSize(vLeftOver) );
+    return vLeftOver;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManMultiReport( Aig_Man_t * p, char * pStr, int nTotalPo, int nTotalSize, abctime clkStart )
+{
+    printf( "%3s : ", pStr );
+    printf( "PI =%6d  ", Saig_ManPiNum(p) );
+    printf( "PO =%6d  ", Saig_ManPoNum(p) );
+    printf( "FF =%7d  ", Saig_ManRegNum(p) );
+    printf( "ND =%7d  ", Aig_ManNodeNum(p) );
+    printf( "Solved =%7d (%5.1f %%)  ", nTotalPo-Saig_ManPoNum(p), 100.0*(nTotalPo-Saig_ManPoNum(p))/Abc_MaxInt(1, nTotalPo) );
+    printf( "Size   =%7d (%5.1f %%)  ", Aig_ManObjNum(p),          100.0*Aig_ManObjNum(p)/Abc_MaxInt(1, nTotalSize) );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Gia_ManMultiProveAig( Aig_Man_t * p, int TimeOutGlo, int TimeOutLoc, int TimeOutInc, int fVerbose )
+{
+    Ssw_RarPars_t ParsSim, * pParsSim = &ParsSim;
+    Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
+    Vec_Int_t * vOutMap, * vLeftOver;
+    Vec_Ptr_t * vCexes;
+    Aig_Man_t * pTemp;
+    abctime clkStart = Abc_Clock();
+    int nTimeToStop  = TimeOutGlo ? TimeOutGlo * CLOCKS_PER_SEC + Abc_Clock(): 0;
+    int nTotalPo     = Saig_ManPoNum(p);
+    int nTotalSize   = Aig_ManObjNum(p);
+    int i, RetValue  = -1;
+    // create output map
+    vOutMap = Vec_IntStartNatural( Saig_ManPoNum(p) ); // maps current outputs into their original IDs
+    vCexes  = Vec_PtrStart( Saig_ManPoNum(p) );        // maps solved outputs into their CEXes (or markers)
+    for ( i = 0; i < 1000; i++ )
+    {
+        // synthesize
+//        p = Gia_ManMultiProveSyn( pTemp = p );
+//        Aig_ManStop( pTemp );
+//        if ( fVerbose )
+//            Gia_ManMultiReport( p, "SYN", nTotalPo, nTotalSize, clkStart );
+
+        // perform SIM3
+        Ssw_RarSetDefaultParams( pParsSim );
+        pParsSim->fSolveAll = 1;
+        pParsSim->fNotVerbose = 1;
+        pParsSim->fSilent = 1;
+        pParsSim->TimeOut = TimeOutLoc;
+        pParsSim->nRandSeed = (i * 17) % 500;
+        RetValue *= Ssw_RarSimulate( p, pParsSim );
+        // sort outputs
+        if ( p->vSeqModelVec )
+        {
+            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
+            if ( Vec_IntSize(vLeftOver) == 0 )
+                break;
+            // remove solved        
+            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
+            Vec_IntFree( vLeftOver );
+            Aig_ManStop( pTemp );
+        }
+//        if ( fVerbose )
+            Gia_ManMultiReport( p, "SIM", nTotalPo, nTotalSize, clkStart );
+
+        // perform BMC
+        Saig_ParBmcSetDefaultParams( pParsBmc );
+        pParsBmc->fSolveAll = 1;
+        pParsBmc->fNotVerbose = 1;
+        pParsBmc->fSilent = 1;
+        pParsBmc->nTimeOut = TimeOutLoc;
+        RetValue *= Saig_ManBmcScalable( p, pParsBmc );
+        // sort outputs
+        if ( p->vSeqModelVec )
+        {
+            vLeftOver = Gia_ManProcessOutputs( p->vSeqModelVec, vCexes, vOutMap );
+            if ( Vec_IntSize(vLeftOver) == 0 )
+                break;
+            // remove solved        
+            p = Saig_ManDupCones( pTemp = p, Vec_IntArray(vLeftOver), Vec_IntSize(vLeftOver) );
+            Vec_IntFree( vLeftOver );
+            Aig_ManStop( pTemp );
+        }
+//        if ( fVerbose )
+            Gia_ManMultiReport( p, "BMC", nTotalPo, nTotalSize, clkStart );
+
+        // increase timeout
+        TimeOutLoc *= TimeOutInc;
+        if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+        {
+            printf( "Global timeout (%d sec) is reached.\n", TimeOutGlo );
+            break;
+        }
+    }
+    Vec_IntFree( vOutMap );
+    Aig_ManStop( p );
+    return vCexes;
+}
+int Gia_ManMultiProve( Gia_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pAig;
+    if ( p->vSeqModelVec )
+        Vec_PtrFreeFree( p->vSeqModelVec ), p->vSeqModelVec = NULL;
+    pAig = Gia_ManToAig( p, 0 );
+    p->vSeqModelVec = Gia_ManMultiProveAig( pAig, 30, 2, 2, fVerbose );
+    assert( Vec_PtrSize(p->vSeqModelVec) == Gia_ManPoNum(p) );
+//    Aig_ManStop( pAig );
+    return Vec_PtrCountZero(p->vSeqModelVec) == Vec_PtrSize(p->vSeqModelVec) ? -1 : 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+