From 590ae696526823709bd6c38726c1c21695babe15 Mon Sep 17 00:00:00 2001 From: Baruch Sterin Date: Wed, 9 Aug 2017 12:00:59 -0700 Subject: 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 --- src/base/main/mainInt.h | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index efc5fc7f..5f330e4a 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -54,6 +54,8 @@ ABC_NAMESPACE_HEADER_START /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +typedef void (*Abc_Frame_Callback_BmcFrameDone_Func)(int frame, int po, int status); + struct Abc_Frame_t_ { // general info @@ -146,6 +148,8 @@ struct Abc_Frame_t_ Gia_Man_t * pGiaMiniLut; Vec_Int_t * vCopyMiniAig; Vec_Int_t * vCopyMiniLut; + + Abc_Frame_Callback_BmcFrameDone_Func pFuncOnFrameDone; }; typedef void (*Abc_Frame_Initialization_Func)( Abc_Frame_t * pAbc ); -- cgit v1.2.3