diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-14 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-10-14 08:01:00 -0700 |
| commit | a4bca405978e500b7ef2b987d159e3b11b95905f (patch) | |
| tree | e94a9b0c2c252ffdd0f56d287e71526aba53aa36 /src/aig/fra/fra.h | |
| parent | e917dda1d363cf56274d0595c97cecf3c59eca75 (diff) | |
| download | abc-a4bca405978e500b7ef2b987d159e3b11b95905f.tar.gz abc-a4bca405978e500b7ef2b987d159e3b11b95905f.tar.bz2 abc-a4bca405978e500b7ef2b987d159e3b11b95905f.zip | |
Version abc81014
Diffstat (limited to 'src/aig/fra/fra.h')
| -rw-r--r-- | src/aig/fra/fra.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index dc98adc9..e7cd0550 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -118,6 +118,8 @@ struct Fra_Sec_t_ int nFramesMax; // the max number of frames used for induction int nBTLimit; // the conflict limit at a node int nBTLimitGlobal; // the global conflict limit + int nBTLimitInter; // the conflict limit for interpolation + int nBddVarsMax; // the state space limit for BDD reachability int nBddMax; // the max number of BDD nodes int nBddIterMax; // the limit on the number of BDD iterations int fPhaseAbstract; // enables phase abstraction @@ -361,7 +363,7 @@ extern int Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, extern int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew ); /*=== fraSec.c ========================================================*/ extern void Fra_SecSetDefaultParams( Fra_Sec_t * p ); -extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec ); +extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult ); /*=== fraSim.c ========================================================*/ extern int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize ); extern int Fra_SmlNodeIsConst( Aig_Obj_t * pObj ); |