From 070ae52a46559db0c23c089e0330f5682907d1aa Mon Sep 17 00:00:00 2001 From: Carmine50 Date: Wed, 18 Dec 2024 19:36:50 +0100 Subject: [PATCH] [CEC][SimGen][Custom Parameters] Added custom parameters for SimGen CEC algo --- src/proof/cec/cec.h | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index 10101e6c0..e14ecabe2 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -201,6 +201,27 @@ struct Cec_ParSeq_t_ int fVerbose; // verbose stats }; +// CEC SimGen parameters +typedef struct Cec_ParSimGen_t_ Cec_ParSimGen_t; +struct Cec_ParSimGen_t_ +{ + int fVerbose; // verbose flag + int fVeryVerbose; // verbose flag + int bitwidthOutgold; // bitwidth of the output gold + int bitwidthSim; // bitwidth of the simulation vectors + int nMaxStep; // maximum number of SimGen steps + int nMaxIter; // maximum number of iterations + char * outGold; // data containing outgold + float timeOutSim; // timeout for simulation + int fUseWatchlist; // use watchlist + float fImplicationTime; // time spent in implication + int nImplicationExecution; // number of times implication was executed + int nImplicationSuccess; // number of times implication was successful + int nImplicationTotalChecks; // number of times implication was checked + int nImplicationSuccessChecks; // number of times implication was successful + Cec_ParFra_t * pCECPars; // parameters of CEC +}; + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// ////////////////////////////////////////////////////////////////////////