From 20c2b197984ad6da0f28eb9ef86f95b362d96335 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 7 Oct 2005 08:01:00 -0700 Subject: Version abc51007 --- src/sat/fraig/fraig.h | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/sat/fraig/fraig.h') diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index dc679907..33ae1e49 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -153,6 +153,9 @@ extern void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams extern Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ); extern void Fraig_ManFree( Fraig_Man_t * pMan ); extern void Fraig_ManPrintStats( Fraig_Man_t * p ); +extern Fraig_NodeVec_t * Fraig_ManGetSimInfo( Fraig_Man_t * p ); +extern int Fraig_ManCheckClauseUsingSimInfo( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2 ); +extern void Fraig_ManAddClause( Fraig_Man_t * p, Fraig_Node_t ** ppNodes, int nNodes ); /*=== fraigDfs.c =============================================================*/ extern Fraig_NodeVec_t * Fraig_Dfs( Fraig_Man_t * pMan, int fEquiv ); @@ -168,6 +171,7 @@ extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * 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 ); +extern int Fraig_ManCheckClauseUsingSat( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ); /*=== fraigVec.c ===============================================================*/ extern Fraig_NodeVec_t * Fraig_NodeVecAlloc( int nCap ); -- cgit v1.2.3