NuSMV/code/nusmv/core/utils/bmc_profiler.h File Reference

#include "nusmv/core/cinit/NuSMVEnv.h"
#include "nusmv/core/utils/error.h"

Defines
#define	BMC_PROFILER_DEINIT_ENV(env)
	Remove the data structure kept in the environment.
#define	BMC_PROFILER_DISABLE(env)
	Disable the profiling of the BMC algorithms.
#define	BMC_PROFILER_ENABLE(env, file)
	Enable the profiling of the different calls to the sat solver during a BMC execution.
#define	BMC_PROFILER_GET_OUT_FILE(env) (char*) NULL
	Returns the string of the profiler file.
#define	BMC_PROFILER_INIT_ENV(env)
	Defines the macros used to wrap a profiler library for BMC problems.
#define	BMC_PROFILER_INITIALIZE(env)
	Initialize the BMC profiler library.
#define	BMC_PROFILER_IS_ENABLED(env) false
	Check if the profiler is enabled.
#define	BMC_PROFILER_SAMPLING_SOLVE_END(env, bmc_step)
	Log the end of a BMC sat check at depth bmc_step.
#define	BMC_PROFILER_SAMPLING_SOLVE_START(env, bmc_step)
	Log the beginning of a BMC sat check at depth bmc_step.

Define Documentation

#define BMC_PROFILER_DEINIT_ENV ( env )

Remove the data structure kept in the environment.

If the library is not linked the macro does nothing.

#define BMC_PROFILER_DISABLE ( env )

Disable the profiling of the BMC algorithms.

The macro takes as input the environment where the BMC is executed. The macro has to be called only after calling BMC_PROFILER_ENABLE. Calling this macro will cause to close the current handle to the output file used for printing the profiling information.

If the library is not linked the macro will do nothing.

#define BMC_PROFILER_ENABLE	(	env,
		file		)

Enable the profiling of the different calls to the sat solver during a BMC execution.

The macro takes as input the environment where the BMC is executed and a name (const char*) of the file used to output the statistics. The file is rewritten if exists and it has to be closed calling BMC_PROFILER_DISABLE.

If the library is not linked the macro will do nothing.

#define BMC_PROFILER_GET_OUT_FILE ( env ) (char*) NULL

Returns the string of the profiler file.

Returns the string of the profiler file. If the library is not linked the macro returns false.

#define BMC_PROFILER_INIT_ENV ( env )

Defines the macros used to wrap a profiler library for BMC problems.

Author:: Sergio Mover Defines a set of macros that wrap the calls to a profiler library for BMC problems. The profiler library allows to write on a file the statistics (time) took to solve an instance of the BMC problem.

Initialize the data structure used to keep the status of the profiler library (on the NuSMV side) If the library is not linked the macro does nothing.

#define BMC_PROFILER_INITIALIZE ( env )

Initialize the BMC profiler library.

The macro intializes the BMC profiler library. If the library is not linked the macro will do nothing.

#define BMC_PROFILER_IS_ENABLED ( env ) false

Check if the profiler is enabled.

The macro returns true iff the profiler is enabled. If the library is not linked the macro returns false.

#define BMC_PROFILER_SAMPLING_SOLVE_END	(	env,
		bmc_step		)

Log the end of a BMC sat check at depth bmc_step.

Log the end of a BMC sat check at depth bmc_step. This will print in the profiling file a message that contains the information about the end of the bmc_step BMC sat check and the current timestamp.

The macro takes as input the environment where the BMC is executed and the current step (a non-negative integer value). The macro has to be called only after calling BMC_PROFILER_ENABLE.

If the library is not linked the macro will do nothing.

#define BMC_PROFILER_SAMPLING_SOLVE_START	(	env,
		bmc_step		)

Log the beginning of a BMC sat check at depth bmc_step.

Log the beginning of a BMC sat check at depth bmc_step. This will print in the profiling file a message that contains the information about the start of the bmc_step BMC sat check and the current timestamp.

The macro takes as input the environment where the BMC is executed and the current step (a non-negative integer value). The macro has to be called only after calling BMC_PROFILER_ENABLE.

If the library is not linked the macro will do nothing.