diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-08 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-08 08:01:00 -0700 |
commit | eb4cdcdcb4db6e468aa02a7949217fa6da245217 (patch) | |
tree | 34223999f598d157831c030392666a937b020992 /src/sat/fraig/fraig.h | |
parent | 1260d20cc05fe2d21088cc047c460e85ccdb3b14 (diff) | |
download | abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.tar.gz abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.tar.bz2 abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.zip |
Version abc50908
Diffstat (limited to 'src/sat/fraig/fraig.h')
-rw-r--r-- | src/sat/fraig/fraig.h | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 901bbac9..75dfb812 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -43,6 +43,7 @@ struct Fraig_ParamsStruct_t_ int nPatsRand; // the number of words of random simulation info int nPatsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the timeout for the final proof int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables distance-1 patterns @@ -162,8 +163,8 @@ extern int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pO extern int Fraig_CountLevels( Fraig_Man_t * pMan ); /*=== fraigSat.c =============================================================*/ -extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ); -extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); +extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ); +extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ); extern void Fraig_ManProveMiter( Fraig_Man_t * p ); extern int Fraig_ManCheckMiter( Fraig_Man_t * p ); |