Adding support for cardinality constraints in &fftest (switches -K and -k).

3 files changed, 84 insertions, 6 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 286ec39d..8b96bba1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36342,7 +36342,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Gia_ParFfSetDefault( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "ATNSGsbfdeuvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfdeuvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -36379,6 +36379,17 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nIterCheck < 0 )
                 goto usage;
             break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nCardConstr = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nCardConstr <= 0 )
+                goto usage;
+            break;
         case 'S':
             if ( globalUtilOptind >= argc )
             {
@@ -36397,12 +36408,15 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             pFileName = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
-        case 's':
-            pPars->fStartPats ^= 1;
+        case 'k':
+            pPars->fNonStrict ^= 1;
             break;
         case 'b':
             pPars->fBasic ^= 1;
             break;
+        case 's':
+            pPars->fStartPats ^= 1;
+            break;
         case 'f':
             pPars->fFfOnly ^= 1;
             break;
@@ -36493,7 +36507,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fftest [-ATN num] [-sbfdeuvh] <file> [-G file] [-S str]\n" );
+    Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeuvh] <file> [-G file] [-S str]\n" );
     Abc_Print( -2, "\t          performs functional fault test generation\n" );
     Abc_Print( -2, "\t-A num  : selects fault model for all gates [default = %d]\n", pPars->Algo );
     Abc_Print( -2, "\t                0: fault model is not selected (use -S str)\n" );
@@ -36503,8 +36517,10 @@ usage:
     Abc_Print( -2, "\t                4: functionally observable fault\n" );
     Abc_Print( -2, "\t-T num  : specifies approximate runtime limit in seconds [default = %d]\n",        pPars->nTimeOut );
     Abc_Print( -2, "\t-N num  : specifies iteration to check for fixed parameters [default = %d]\n",     pPars->nIterCheck );
+    Abc_Print( -2, "\t-K num  : specifies cardinality constraint (num > 0) [default = unused]\n" );
+    Abc_Print( -2, "\t-k      : toggles non-strict cardinality (n <= K, instead of n == K) [default = %s]\n",pPars->fNonStrict?  "yes": "no" );
+    Abc_Print( -2, "\t-b      : toggles testing for single faults (the same as \"-K 1\") [default = %s]\n", pPars->fBasic?      "yes": "no" );
     Abc_Print( -2, "\t-s      : toggles starting with the all-0 and all-1 patterns [default = %s]\n",    pPars->fStartPats?  "yes": "no" );
-    Abc_Print( -2, "\t-b      : toggles testing for single faults only [default = %s]\n",                pPars->fBasic?      "yes": "no" );
     Abc_Print( -2, "\t-f      : toggles faults at flop inputs only with \"-A 1\" and \"-S str\" [default = %s]\n",          pPars->fFfOnly?     "yes": "no" );
     Abc_Print( -2, "\t-d      : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump?       "yes": "no" );
     Abc_Print( -2, "\t-e      : toggles dumping test pattern pairs (delay faults only) [default = %s]\n", pPars->fDumpDelay? "yes": "no" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 75529f7b..14ffec12 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -130,6 +130,8 @@ struct Bmc_ParFf_t_
     int        fStartPats;
     int        nTimeOut;
     int        nIterCheck;
+    int        nCardConstr;
+    int        fNonStrict;
     int        fBasic;
     int        fFfOnly;
     int        fDump;
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index 50477f21..e91c76ac 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -65,6 +65,56 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Adds a general cardinality constraint in terms of vVars.]
+
+  Description [Strict is "exactly K out of N". Non-strict is 
+  "less or equal than K out of N".]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cnf_AddCardinVar( int Level, int Base, Vec_Int_t * vVars, int k )
+{
+    return Level ? Base + k : Vec_IntEntry( vVars, k );
+}
+static inline void Cnf_AddCardinConstrGeneral( sat_solver * p, Vec_Int_t * vVars, int K, int fStrict )
+{
+    int i, k, iCur, iNext, iVar, Lit;
+    int nVars = sat_solver_nvars(p);
+    int nBits = Vec_IntSize(vVars);
+    Vec_IntForEachEntry( vVars, iVar, i )
+        assert( iVar >= 0 && iVar < nVars );
+    sat_solver_setnvars( p, nVars + nBits * nBits );
+    for ( i = 0; i < nBits; i++ )
+    {
+        iCur = nVars + nBits * (i-1);
+        iNext = nVars + nBits * i;
+        if ( i & 1 )
+            sat_solver_add_buffer( p, iNext, Cnf_AddCardinVar(i, iCur, vVars, 0), 0 );
+        for ( k = i & 1; k + 1 < nBits; k += 2 )
+        {
+            sat_solver_add_and( p, iNext+k  , Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 1, 1, 1 );
+            sat_solver_add_and( p, iNext+k+1, Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 0, 0, 0 );
+        }
+        if ( k == nBits - 1 )
+            sat_solver_add_buffer( p, iNext + nBits-1, Cnf_AddCardinVar(i, iCur, vVars, nBits-1), 0 );
+    }
+    // add final constraint
+    assert( K > 0 && K < nBits );
+    Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K, 1 );
+    if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
+        assert( 0 );
+    if ( fStrict )
+    {
+        Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K - 1, 0 );
+        if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
+            assert( 0 );
+    }
+}
+/**Function*************************************************************
+
   Synopsis    [Add constraint that no more than 1 variable is 1.]
 
   Description []
@@ -99,17 +149,19 @@ static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
 }
 void Cnf_AddCardinConstrTest()
 {
-    int i, status, nVars = 7;
+    int i, status, Count = 1, nVars = 6;
     Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
     sat_solver * pSat = sat_solver_new();
     sat_solver_setnvars( pSat, nVars );
     Cnf_AddCardinConstr( pSat, vVars );
+    //Cnf_AddCardinConstrGeneral( pSat, vVars, 1, 1 );
     while ( 1 )
     {
         status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
         if ( status != l_True )
             break;
         Vec_IntClear( vVars );
+        printf( "%3d : ", Count++ );
         for ( i = 0; i < nVars; i++ )
         {
             Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
@@ -1078,6 +1130,14 @@ int Gia_ManFaultPrepare( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars, int
                 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
         Cnf_AddCardinConstr( pSat, vLits );
     }
+    else if ( pPars->nCardConstr )
+    {
+        Vec_IntClear( vLits );
+        Gia_ManForEachPi( pM, pObj, i )
+            if ( i >= nFuncVars )
+                Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
+        Cnf_AddCardinConstrGeneral( pSat, vLits, pPars->nCardConstr, !pPars->fNonStrict );
+    }
 
     // add available test-patterns
     if ( Vec_IntSize(vTests) > 0 )