diff options
Diffstat (limited to 'src/aig/dch/dchCore.c')
-rw-r--r-- | src/aig/dch/dchCore.c | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index b73fceb3..76813d1a 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -42,11 +42,15 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) { memset( p, 0, sizeof(Dch_Pars_t) ); - p->nWords = 4; // the number of simulation words - p->nBTLimit = 100; // conflict limit at a node - p->nSatVarMax = 10000; // the max number of SAT variables - p->fSynthesis = 1; // derives three snapshots - p->fVerbose = 1; // verbose stats + p->nWords = 8; // the number of simulation words + p->nBTLimit = 1000; // conflict limit at a node + p->nSatVarMax = 5000; // the max number of SAT variables + p->fSynthesis = 1; // derives three snapshots + p->fPolarFlip = 1; // uses polarity adjustment + p->fSimulateTfo = 1; // simulate TFO + p->fVerbose = 0; // verbose stats + p->nNodesAhead = 1000; // the lookahead in terms of nodes + p->nCallsRecycle = 100; // calls to perform before recycling SAT solver } /**Function************************************************************* @@ -66,6 +70,8 @@ Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) Aig_Man_t * pResult; int clk, clkTotal = clock(); assert( Vec_PtrSize(vAigs) > 0 ); + // reset random numbers + Aig_ManRandom(1); // start the choicing manager p = Dch_ManCreate( vAigs, pPars ); // compute candidate equivalence classes |