diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-18 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-18 08:01:00 -0700 |
| commit | 655a50101e18176f1163ccfc67cf69d86623d1f2 (patch) | |
| tree | dd31c20fe95145cdc23d30eb0b65ff727881b57b /src/aig/fra | |
| parent | ce690b29075a23a07673d0a4727f0bf9557ec882 (diff) | |
| download | abc-655a50101e18176f1163ccfc67cf69d86623d1f2.tar.gz abc-655a50101e18176f1163ccfc67cf69d86623d1f2.tar.bz2 abc-655a50101e18176f1163ccfc67cf69d86623d1f2.zip | |
Version abc80918
Diffstat (limited to 'src/aig/fra')
| -rw-r--r-- | src/aig/fra/fra.h | 1 | ||||
| -rw-r--r-- | src/aig/fra/fraLcr.c | 5 |
2 files changed, 4 insertions, 2 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 91689196..eceda480 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -123,6 +123,7 @@ struct Fra_Sec_t_ int fInterpolation; // enables interpolation int fReachability; // enables BDD based reachability int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove + int fUseNewProver; // the new prover int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index f597e090..d3be9842 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -629,16 +629,17 @@ clk2 = clock(); pAigTemp = Fra_FraigEquivence( pAigPart, nConfMax, 0 ); p->timeFraig += clock() - clk2; Vec_PtrPush( p->vFraigs, pAigTemp ); +/* { char Name[1000]; sprintf( Name, "part%04d.blif", i ); Aig_ManDumpBlif( pAigPart, Name, NULL, NULL ); } - Aig_ManStop( pAigPart ); - printf( "Finished part %4d (out of %4d). ", i, Vec_PtrSize(p->vParts) ); PRT( "Time", clock() - clk3 ); +*/ + Aig_ManStop( pAigPart ); } Fra_ClassNodesUnmark( p ); // report the intermediate results |