ConjSet Struct Reference

Public interface of class 'ConjSet'. More...

#include <ConjSet.h>

Related Functions
(Note that these are not member functions.)
void	ConjSet_add_var_assign (ConjSet_ptr self, Rbc_t *var, Rbc_t *expr)
	Adds a new variable assignment to set.
Rbc_t *	ConjSet_conjoin (ConjSet_ptr self, Rbc_t *f)
	Returns the conjuction of self with the given formula.
ConjSet_ptr	ConjSet_copy (const ConjSet_ptr self)
	Copy constructor.
ConjSet_ptr	ConjSet_create (Rbc_Manager_t *rbcm)
	The ConjSet class constructor.
void	ConjSet_destroy (ConjSet_ptr self)
	The ConjSet class destructor.
void	ConjSet_flattenize (ConjSet_ptr self)
	Makes the ConjSet flattened.
void	ConjSet_inherit_from (ConjSet_ptr self, const ConjSet_ptr other)
	Inherits as much as possible (provided that what it inherits is not worse than what it has collected so far) from the given ConjSet.
void	ConjSet_print (const ConjSet_ptr self, FILE *file)
	Prints debugging information about self.
Rbc_t *	ConjSet_substitute (ConjSet_ptr self, Rbc_t *f)
	Substitutes all variables occurring into f that belong to self with the corresponding expression.

---

Detailed Description

Public interface of class 'ConjSet'.

Author:

Roberto Cavada

Todo:

: Missing description

Definition of the public accessor for class ConjSet A ConjSet holds the associations between variables and the corresponding expression each variable can be substituted with. A ConjSet is internally used by RBC inlining. In particular it is used by class InlineResult

---

Friends And Related Function Documentation

void ConjSet_add_var_assign	(	ConjSet_ptr	self,
		Rbc_t *	var,
		Rbc_t *	expr
	)			[related]

Adds a new variable assignment to set.

Will be kept onlt if 'better' then the possibly previous assigment

Rbc_t * ConjSet_conjoin	(	ConjSet_ptr	self,
		Rbc_t *	f
	)			[related]

Returns the conjuction of self with the given formula.

Returns a formula like: for all v,exp belonging to self, (/\ (v <-> exp)) /\ f

ConjSet_ptr ConjSet_copy

(

const ConjSet_ptr

self

)

[related]

Copy constructor.

ConjSet_ptr ConjSet_create

(

Rbc_Manager_t *

rbcm

)

[related]

The ConjSet class constructor.

AutomaticStart

The ConjSet class constructor

See also:

ConjSet_destroy

void ConjSet_destroy

(

ConjSet_ptr

self

)

[related]

The ConjSet class destructor.

The ConjSet class destructor

See also:

ConjSet_create

void ConjSet_flattenize

(

ConjSet_ptr

self

)

[related]

Makes the ConjSet flattened.

Flattens the ConjSet, making minimal the graph of dependencies. A flatten ConjSet can then be used to substitute an expression

void ConjSet_inherit_from	(	ConjSet_ptr	self,
		const ConjSet_ptr	other
	)			[related]

Inherits as much as possible (provided that what it inherits is not worse than what it has collected so far) from the given ConjSet.

void ConjSet_print	(	const ConjSet_ptr	self,
		FILE *	file
	)			[related]

Prints debugging information about self.

Rbc_t * ConjSet_substitute	(	ConjSet_ptr	self,
		Rbc_t *	f
	)			[related]

Substitutes all variables occurring into f that belong to self with the corresponding expression.

If self was previously flattened, the resulting RBC will be flattened as well, but only about those parts that has the same language of self

---

The documentation for this struct was generated from the following file:

• NuSMV/code/nusmv/core/rbc/ConjSet.h