diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-31 16:27:07 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-31 16:27:07 +0700 |
| commit | 6f598455bcdf55bdd997bfeb82129d770f745e35 (patch) | |
| tree | f17c7d7ab3f7087ba27fd6619c4f73e6948cdca2 /src/sat/bmc | |
| parent | 5ebe403a8770d51994e9a89cb44a90327e2551f4 (diff) | |
| download | abc-6f598455bcdf55bdd997bfeb82129d770f745e35.tar.gz abc-6f598455bcdf55bdd997bfeb82129d770f745e35.tar.bz2 abc-6f598455bcdf55bdd997bfeb82129d770f745e35.zip | |
Updating command &satfx.
Diffstat (limited to 'src/sat/bmc')
| -rw-r--r-- | src/sat/bmc/bmcFx.c | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/src/sat/bmc/bmcFx.c b/src/sat/bmc/bmcFx.c index 1d3a9802..5482dcd3 100644 --- a/src/sat/bmc/bmcFx.c +++ b/src/sat/bmc/bmcFx.c @@ -670,11 +670,9 @@ void Bmc_FxAddClauses( sat_solver * pSat, Vec_Int_t * vDivs, int iCiVarBeg, int else assert( 0 ); } } -int Bmc_FxComputeOne( Gia_Man_t * p ) +int Bmc_FxComputeOne( Gia_Man_t * p, int nIterMax, int nDiv2Add ) { int Extra = 1000; - int nIterMax = 5; - int nDiv2Add = 15; // create SAT solver Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 ); sat_solver * pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); |