Enabled skipping random decisions in PBA, which are performed by default.

7 files changed, 24 insertions, 9 deletions

diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 2432bdbf..16fe9c35 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -379,7 +379,7 @@ int Gia_ManPbaPerform( Gia_Man_t * pGia, int nStart, int nFrames, int nConfLimit
 ***********************************************************************/
 int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 {
-    extern Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
+    extern Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses, * vGateClassesOld = NULL;
     Aig_Man_t * pAig;
@@ -397,7 +397,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
     // perform abstraction
     pAig = Gia_ManToAigSimple( pGia );
     assert( vGateClassesOld == NULL || Vec_IntSize(vGateClassesOld) == Aig_ManObjNumMax(pAig) );
-    vGateClasses = Aig_Gla1ManTest( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
+    vGateClasses = Aig_Gla1ManPerform( pAig, vGateClassesOld, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, fNaiveCnf, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the map
@@ -419,7 +419,7 @@ int Gia_ManGlaCbaPerform( Gia_Man_t * pGia, void * pPars, int fNaiveCnf )
 ***********************************************************************/
 int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
 {
-    extern Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose );
+    extern Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose );
     Saig_ParBmc_t * p = (Saig_ParBmc_t *)pPars;
     Vec_Int_t * vGateClasses;
     Aig_Man_t * pAig;
@@ -440,7 +440,7 @@ int Gia_ManGlaPbaPerform( Gia_Man_t * pGia, void * pPars )
     }
 
     // perform abstraction
-    vGateClasses = Aig_Gla2ManTest( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fVerbose );
+    vGateClasses = Aig_Gla2ManPerform( pAig, p->nStart, p->nFramesMax, p->nConfLimit, p->nTimeOut, p->fSkipRand, p->fVerbose );
     Aig_ManStop( pAig );
 
     // update the BMC depth
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 9f98a8f9..99928a66 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -68,6 +68,7 @@ struct Saig_ParBmc_t_
     int         fSolveAll;      // does not stop at the first SAT output
     int         fDropSatOuts;   // replace sat outputs by constant 0
     int         nFfToAddMax;    // max number of flops to add during CBA
+    int         fSkipRand;      // skip random decisions
     int         fVerbose;       // verbose 
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
diff --git a/src/aig/saig/saigGlaCba.c b/src/aig/saig/saigGlaCba.c
index d0fd2db3..9140c7bf 100644
--- a/src/aig/saig/saigGlaCba.c
+++ b/src/aig/saig/saigGlaCba.c
@@ -676,7 +676,7 @@ void Aig_Gla1ExtendIncluded( Aig_Gla1Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_Gla1ManTest( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
+Vec_Int_t * Aig_Gla1ManPerform( Aig_Man_t * pAig, Vec_Int_t * vGateClassesOld, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fNaiveCnf, int fVerbose )
 {
     Vec_Int_t * vResult = NULL;
     Aig_Gla1Man_t * p;
diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 00e04346..fce2372f 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -553,7 +553,7 @@ Vec_Int_t * Aig_Gla2ManCollect( Aig_Gla2Man_t * p, Vec_Int_t * vCore )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fVerbose )
+Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nConfLimit, int TimeLimit, int fSkipRand, int fVerbose )
 {
     Aig_Gla2Man_t * p;
     Vec_Int_t * vCore, * vResult;
@@ -578,6 +578,7 @@ Vec_Int_t * Aig_Gla2ManTest( Aig_Man_t * pAig, int nStart, int nFramesMax, int n
         Aig_Gla2ManStop( p );
         return NULL;
     }
+    sat_solver_set_random( p->pSat, fSkipRand );
     p->timePre += Abc_Clock(1,0);
 
     // set runtime limit
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ed23abfd..81b82f73 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29093,8 +29093,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->nStart     =  0;  //(pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
     pPars->nFramesMax = 10; //pPars->nStart + 10;
     pPars->nConfLimit =  0;
+    pPars->fSkipRand  =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -29142,6 +29143,9 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 ) 
                 goto usage;
             break;
+        case 'r':
+            pPars->fSkipRand ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -29185,12 +29189,13 @@ int Abc_CommandAbc9GlaPba( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-vh]\n" );
+    Abc_Print( -2, "usage: &gla_pba [-SFCT num] [-rvh]\n" );
     Abc_Print( -2, "\t         refines abstracted object map with proof-based abstraction\n" );
     Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
     Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts (0=unused) [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-T num : an approximate timeout, in seconds [default = %d]\n", pPars->nTimeOut );
+    Abc_Print( -2, "\t-r     : toggle using random decisiont during SAT solving [default = %s]\n", !pPars->fSkipRand? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index ac2202dc..d4726b81 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -967,7 +967,7 @@ static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT
     int*    levels          = s->levels;
     double  var_decay       = 0.95;
     double  clause_decay    = 0.999;
-    double  random_var_freq = 0.02;
+    double  random_var_freq = s->fNotUseRandom ? 0.0 : 0.02;
 
     ABC_INT64_T  conflictC       = 0;
     veci    learnt_clause;
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index a33c7240..a67e829a 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -175,6 +175,7 @@ struct sat_solver_t
     Sat_MmStep_t * pMem;
 
     int      fSkipSimplify; // set to one to skip simplification of the clause database
+    int      fNotUseRandom; // do not allow random decisions with a fixed probability
 
     int *    pGlobalVars;   // for experiments with global vars during interpolation
     // clause store
@@ -228,6 +229,13 @@ static int sat_solver_set_runtime_limit(sat_solver* s, int Limit)
     return nRuntimeLimit;
 }
 
+static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
+{
+    int fNotUseRandomOld = s->fNotUseRandom;
+    s->fNotUseRandom = fNotUseRandom;
+    return fNotUseRandomOld;
+}
+
 ABC_NAMESPACE_HEADER_END
 
 #endif