Commit 590ae696 by Baruch Sterin

add a new field to the ABC Frame. The new field is a callback that may be called…

add a new field to the ABC Frame. The new field is a callback that may be called by a BMC-like engine when a frame is done and a PO is either known to be SAT or UNSAT up to a specific frame
parent a1d1a7b8
...@@ -54,6 +54,8 @@ ABC_NAMESPACE_HEADER_START ...@@ -54,6 +54,8 @@ ABC_NAMESPACE_HEADER_START
/// STRUCTURE DEFINITIONS /// /// STRUCTURE DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef void (*Abc_Frame_Callback_BmcFrameDone_Func)(int frame, int po, int status);
struct Abc_Frame_t_ struct Abc_Frame_t_
{ {
// general info // general info
...@@ -146,6 +148,8 @@ struct Abc_Frame_t_ ...@@ -146,6 +148,8 @@ struct Abc_Frame_t_
Gia_Man_t * pGiaMiniLut; Gia_Man_t * pGiaMiniLut;
Vec_Int_t * vCopyMiniAig; Vec_Int_t * vCopyMiniAig;
Vec_Int_t * vCopyMiniLut; Vec_Int_t * vCopyMiniLut;
Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone;
}; };
typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc ); typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment