NuSMV/code/nusmv/core/bmc/bmcDump.h File Reference

#include <stdio.h>
#include "nusmv/core/enc/be/BeEnc.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/prop/Prop.h"

Go to the source code of this file.

Enumerations
enum	Bmc_DumpType { BMC_DUMP_NONE, BMC_DUMP_DIMACS, BMC_DUMP_DA_VINCI, BMC_DUMP_GDL }
	Public interface for dumping functionalities, like dimacs. More...
Functions
void	Bmc_Dump_DimacsInvarProblem (const BeEnc_ptr be_enc, const Be_Cnf_ptr cnf, FILE *dimacsfile)
	Dumps the given invar problem in the given file.
int	Bmc_Dump_DimacsInvarProblemFilename (const BeEnc_ptr be_enc, const Be_Cnf_ptr cnf, const char *filename)
	Opens a new file named filename, than dumps the given invar problem in DIMACS format.
void	Bmc_Dump_DimacsProblem (const BeEnc_ptr be_enc, const Be_Cnf_ptr cnf, const int k, FILE *dimacsfile)
	Dumps the given LTL problem in the given file.
int	Bmc_Dump_DimacsProblemFilename (const BeEnc_ptr be_enc, const Be_Cnf_ptr cnf, const char *filename, const int k)
	Opens a new file named filename, than dumps the given LTL problem in DIMACS format.
void	Bmc_Dump_WriteProblem (const BeEnc_ptr be_enc, const Be_Cnf_ptr cnf, Prop_ptr prop, const int k, const int loop, const Bmc_DumpType dump_type, const char *dump_fname_template)
	Dumps a cnf in different formats.

---

Enumeration Type Documentation

enum Bmc_DumpType

Public interface for dumping functionalities, like dimacs.

Author:

Roberto Cavada

Todo:

: Missing description

Enumerator:

BMC_DUMP_NONE
BMC_DUMP_DIMACS
BMC_DUMP_DA_VINCI
BMC_DUMP_GDL

---

Function Documentation

void Bmc_Dump_DimacsInvarProblem	(	const BeEnc_ptr	be_enc,
		const Be_Cnf_ptr	cnf,
		FILE *	dimacsfile
	)

Dumps the given invar problem in the given file.

dimacsfile must be writable

int Bmc_Dump_DimacsInvarProblemFilename	(	const BeEnc_ptr	be_enc,
		const Be_Cnf_ptr	cnf,
		const char *	filename
	)

Opens a new file named filename, than dumps the given invar problem in DIMACS format.

void Bmc_Dump_DimacsProblem	(	const BeEnc_ptr	be_enc,
		const Be_Cnf_ptr	cnf,
		const int	k,
		FILE *	dimacsfile
	)

Dumps the given LTL problem in the given file.

dimacsfile must be writable

int Bmc_Dump_DimacsProblemFilename	(	const BeEnc_ptr	be_enc,
		const Be_Cnf_ptr	cnf,
		const char *	filename,
		const int	k
	)

Opens a new file named filename, than dumps the given LTL problem in DIMACS format.

void Bmc_Dump_WriteProblem	(	const BeEnc_ptr	be_enc,
		const Be_Cnf_ptr	cnf,
		Prop_ptr	prop,
		const int	k,
		const int	loop,
		const Bmc_DumpType	dump_type,
		const char *	dump_fname_template
	)

Dumps a cnf in different formats.

AutomaticStart

None