diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-14 03:13:05 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-03-14 03:13:05 +0700 |
| commit | dc92f89278b17ad61407234a9159ffabc9c81e9e (patch) | |
| tree | 0355655e361d78be356bce71571735b44eb99281 /src/sat | |
| parent | 3146ff40901d034383911d3aeb6048eb141fa246 (diff) | |
| download | abc-dc92f89278b17ad61407234a9159ffabc9c81e9e.tar.gz abc-dc92f89278b17ad61407234a9159ffabc9c81e9e.tar.bz2 abc-dc92f89278b17ad61407234a9159ffabc9c81e9e.zip | |
Adding silent mode to &splitprove.
Diffstat (limited to 'src/sat')
| -rw-r--r-- | src/sat/bmc/bmcFault.c | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c index 7a2a57fb..4912d82c 100644 --- a/src/sat/bmc/bmcFault.c +++ b/src/sat/bmc/bmcFault.c @@ -674,12 +674,18 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c ***********************************************************************/ int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars ) { - Gia_Man_t * pC; + Gia_Man_t * pC;//, * pTemp; Cnf_Dat_t * pCnf2; Gia_Obj_t * pObj; int i, Lit; // derive the cofactor pC = Gia_ManFaultCofactor( pM, vLits ); + // try synthesis +// printf( "\n" ); +// Gia_ManPrintStats( pC, NULL ); +// pC = Gia_ManAigSyn2( pTemp = pC, 0, 1, 0, 100, 0, 0, 0 ); +// Gia_ManStop( pTemp ); +// Gia_ManPrintStats( pC, NULL ); //Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 ); //printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" ); // derive new CNF |