Searched refs:fUseGlucose (Results 1 – 3 of 3) sorted by relevance
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bmc/ |
| H A D | bmc.h | 108 int fUseGlucose; // enables using Glucose 3.0 member
140 int fUseGlucose; // use Glucose 3.0 as the default solver member
|
| H A D | bmcBmc3.c | 721 …_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose ) in Saig_Bmc3ManStart() argument
759 else if ( fUseGlucose ) in Saig_Bmc3ManStart()
1483 …Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose ); in Saig_ManBmcScalable()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/base/abci/ |
| H A D | abc.c | 26670 pPars->fUseGlucose ^= 1; in Abc_CommandBmc3()
26765 …ucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); in Abc_CommandBmc3()
42876 pPars->fUseGlucose = 0; // use Glucose 3.0 in Abc_CommandAbc9SBmc()
42947 pPars->fUseGlucose ^= 1; in Abc_CommandAbc9SBmc()
42974 …pAbc->Status = pPars->fUseGlucose ? Bmcg_ManPerform(pAbc->pGia, pPars) : Bmcs_ManPerform(pAbc->pG… in Abc_CommandAbc9SBmc()
42987 …ose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fUseGlucose? "Glucose" : "… in Abc_CommandAbc9SBmc()
|