From b8dea8ff0510ee7be465f5fe50994ecb58b9b30a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 2 Aug 2008 20:01:00 -0700 Subject: Version abc80802_2 --- src/aig/dch/dchCore.c | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) (limited to 'src/aig/dch/dchCore.c') 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 -- cgit v1.2.3