NuSMV/code/nusmv/core/enc/encInt.h File Reference

#include "nusmv/core/enc/utils/OrdGroups.h"
#include "nusmv/core/enc/bool/BoolEnc.h"
#include "nusmv/core/utils/utils.h"
#include "nusmv/core/node/node.h"
#include "nusmv/core/opt/opt.h"
#include "nusmv/core/dd/dd.h"

Go to the source code of this file.

Functions
void	Enc_append_bit_to_sorted_list (SymbTable_ptr symb_table, NodeList_ptr sorted_list, node_ptr var, node_ptr *sorting_cache)
	Given a boolean variable or a bit the function inserts it into the sorted list at proper position.
OrdGroups_ptr	enc_utils_create_vars_ord_groups (BoolEnc_ptr bool_enc, NodeList_ptr vars)
	Given a list of variables representing a new variable ordering, produces an OrdGroups instance.
OrdGroups_ptr	enc_utils_parse_ordering_file (const NuSMVEnv_ptr env, const char *order_filename, const BoolEnc_ptr bool_enc)
	Parses the given ordering file, and produces an OrdGroups instance.
Variables
node_ptr	boolean_range
int	nusmv_yylineno
	Internal API for the enc package.

---

Function Documentation

void Enc_append_bit_to_sorted_list	(	SymbTable_ptr	symb_table,
		NodeList_ptr	sorted_list,
		node_ptr	var,
		node_ptr *	sorting_cache
	)

Given a boolean variable or a bit the function inserts it into the sorted list at proper position.

The higher bits are added to the beginning of the list and lower bits are added at the end. The boolean variables are added at the beginning of the list before the bits.

A new element is added at the end of the group of equal elements, e.g. a boolean var is added after existing boolean vars but before the bit vars.

Parameter 'sorting_cache' is used to speed up insertion (sorting a list will be linear instead of quadratic). Initially 'sorting_cache' has to point to a pointer which points to Nil and sorted_list has to be an empty list. It is the invoker responsibility to free the sorted list and cache (with free_list) after last invoking Enc_append_bit_to_sorted_list (the same sorting_cache and sorted_list can be used for several runs of this function).

OrdGroups_ptr enc_utils_create_vars_ord_groups	(	BoolEnc_ptr	bool_enc,
		NodeList_ptr	vars
	)

Given a list of variables representing a new variable ordering, produces an OrdGroups instance.

The returned instance belongs to the caller. It is a caller's responsability to destroy it.

OrdGroups_ptr enc_utils_parse_ordering_file	(	const NuSMVEnv_ptr	env,
		const char *	order_filename,
		const BoolEnc_ptr	bool_enc
	)

Parses the given ordering file, and produces an OrdGroups instance.

The returned instance belongs to the caller. It is a caller's responsability to destroy it. order_filename can be NULL

---

Variable Documentation

node_ptr boolean_range

int nusmv_yylineno

Internal API for the enc package.

Author:

Roberto Cavada

Todo:

: Missing description