NuSMV/code/nusmv/core/rbc/clg/clg.h File Reference

#include "nusmv/core/utils/utils.h"

Go to the source code of this file.

Defines
#define	CLG_DIMACS   20
	Clause graphs.
#define	CLG_NUSMV   22
#define	CLG_ZCHAFF   21
Typedefs
typedef void(*	Clg_Commit )(void *, int *, int)
typedef struct ClgManager_TAG *	ClgManager_ptr
Functions
clause_graph	Clg_Conj (ClgManager_ptr clgmgr, clause_graph left, clause_graph right)
	Create a CLG representing a conjunction of two CLGs.
clause_graph	Clg_Disj (ClgManager_ptr clgmgr, clause_graph left, clause_graph right)
	Create a CLG representing a disjunction of two CLGs.
void	Clg_Extract (const NuSMVEnv_ptr env, clause_graph head, int type, Clg_Commit commit, void *data)
	Extract the real clauses from the CLG.
clause_graph	Clg_Lit (ClgManager_ptr clgmgr, int literal)
	Create a CLG representing a single literal.
int	Clg_Size (clause_graph graph)
	Return the number of clauses stored in the CLG.
void	ClgManager_destroy (ClgManager_ptr clgManager)
	Free all CLGs.

---

Define Documentation

#define CLG_DIMACS   20

Clause graphs.

Author:

Dan Sheridan & Marco Roveri Compact data structure for representing sets of clauses with sharing of common structure. The data structure is a graph of conjunctions and disjunctions which are converted using the standard (exponential-size) CNF conversion to obtain the required clauses.

Todo:

Missing synopsis

Todo:

Missing description

#define CLG_NUSMV   22

Todo:

Missing synopsis

Todo:

Missing description

#define CLG_ZCHAFF   21

Todo:

Missing synopsis

Todo:

Missing description

---

Typedef Documentation

typedef void(* Clg_Commit)(void *, int *, int)

Todo:

Missing synopsis

Todo:

Missing description

typedef struct ClgManager_TAG* ClgManager_ptr

---

Function Documentation

clause_graph Clg_Conj	(	ClgManager_ptr	clgmgr,
		clause_graph	left,
		clause_graph	right
	)

Create a CLG representing a conjunction of two CLGs.

clause_graph Clg_Disj	(	ClgManager_ptr	clgmgr,
		clause_graph	left,
		clause_graph	right
	)

Create a CLG representing a disjunction of two CLGs.

void Clg_Extract	(	const NuSMVEnv_ptr	env,
		clause_graph	head,
		int	type,
		Clg_Commit	commit,
		void *	data
	)

Extract the real clauses from the CLG.

Calls commit with each extracted clause as an argument. type indicates the style of clause (eg, ZChaff all-positive integer format); *data is passed to commit as an extra argument.

Clauses have duplicated literals suppressed and clauses with both positive and negative occurrences of the same literal are skipped.

clause_graph Clg_Lit	(	ClgManager_ptr	clgmgr,
		int	literal
	)

Create a CLG representing a single literal.

int Clg_Size

(

clause_graph

graph

)

Return the number of clauses stored in the CLG.

void ClgManager_destroy

(

ClgManager_ptr

clgManager

)

Free all CLGs.