Options for nanotrav. More...

#include <ntr.h>

Data Fields
long	initialTime

int	verify

char *	file1

char *	file2

int	second

int	traverse

int	depend

int	image

double	imageClip

int	approx

int	threshold

int	from

int	groupnsps

int	closure

double	closureClip

int	envelope

int	scc

int	zddtest

int	printcover

int	maxflow

int	shortPath

int	selectiveTrace

char *	sinkfile

int	partition

int	char2vect

int	density

double	quality

int	decomp

int	cofest

double	clip

int	dontcares

int	closestCube

int	clauses

int	noBuild

int	stateOnly

char *	node

int	locGlob

int	progress

int	cacheSize

size_t	maxMemory

size_t	maxMemHard

unsigned int	maxLive

int	slots

int	ordering

char *	orderPiPs

Cudd_ReorderingType	reordering

int	autoDyn

Cudd_ReorderingType	autoMethod

char *	treefile

int	firstReorder

int	countDead

int	maxGrowth

Cudd_AggregationType	groupcheck

int	arcviolation

int	symmviolation

int	recomb

int	nodrop

int	signatures

int	gaOnOff

int	populationSize

int	numberXovers

int	bdddump

int	dumpFmt

char *	dumpfile

int	store

char *	storefile

int	load

char *	loadfile

int	verb

int32_t	seed

Detailed Description

Options for nanotrav.

Field Documentation

int NtrOptions::approx

under or over approximation

int NtrOptions::arcviolation

percent violation of arcs in extended symmetry check

int NtrOptions::autoDyn

ON OFF

Cudd_ReorderingType NtrOptions::autoMethod

RANDOM PIVOT SIFTING CONVERGE ...

int NtrOptions::bdddump

ON OFF

int NtrOptions::cacheSize

computed table initial size

int NtrOptions::char2vect

test char-to-vect decomposition

int NtrOptions::clauses

test extraction of two-literal clauses

double NtrOptions::clip

test clipping functions

int NtrOptions::closestCube

test Cudd_bddClosestCube

int NtrOptions::closure

use transitive closure

double NtrOptions::closureClip

clipping depth in closure computation

int NtrOptions::cofest

test cofactor estimation

int NtrOptions::countDead

count dead nodes toward triggering reordering

int NtrOptions::decomp

test decomposition functions

int NtrOptions::density

test density-related functions

int NtrOptions::depend

do latch dependence analysis

int NtrOptions::dontcares

test equivalence and containment with DCs

char* NtrOptions::dumpfile

filename for dump

int NtrOptions::dumpFmt

0 -> dot 1 -> blif 2 ->daVinci 3 -> DDcal 4 -> factored form

int NtrOptions::envelope

compute outer envelope

char* NtrOptions::file1

first network file name

char* NtrOptions::file2

second network file name

int NtrOptions::firstReorder

when to do first reordering

int NtrOptions::from

method to compute from states

int NtrOptions::gaOnOff

whether to run GA at the end

Cudd_AggregationType NtrOptions::groupcheck

grouping function

int NtrOptions::groupnsps

group present state and next state vars

int NtrOptions::image

monolithic, partitioned, or clip

double NtrOptions::imageClip

clipping depth in image computation

long NtrOptions::initialTime

this is here for convenience

int NtrOptions::load

load initial states from file

char* NtrOptions::loadfile

filename for loading states

int NtrOptions::locGlob

build global or local BDDs

int NtrOptions::maxflow

compute maximum flow in network

int NtrOptions::maxGrowth

maximum growth during reordering (%)

unsigned int NtrOptions::maxLive

maximum number of nodes

size_t NtrOptions::maxMemHard

maximum allowed memory

size_t NtrOptions::maxMemory

target maximum memory

int NtrOptions::noBuild

do not build BDDs; just echo order

char* NtrOptions::node

only node for which to build BDD

int NtrOptions::nodrop

don't drop intermediate BDDs ASAP

int NtrOptions::numberXovers

number of crossovers for GA

int NtrOptions::ordering

FANIN DFS ...

char* NtrOptions::orderPiPs

file for externally provided order

int NtrOptions::partition

test McMillan conjunctive partitioning

int NtrOptions::populationSize

population size for GA

int NtrOptions::printcover

print ISOP covers when testing ZDDs

int NtrOptions::progress

report output names while building BDDs

double NtrOptions::quality

quality parameter for density functions

int NtrOptions::recomb

recombination parameter for grouping

Cudd_ReorderingType NtrOptions::reordering

NONE RANDOM PIVOT SIFTING ...

int NtrOptions::scc

compute strongly connected components

int NtrOptions::second

a second network is given

int32_t NtrOptions::seed

seed for random number generator

int NtrOptions::selectiveTrace

use selective trace in shortest paths

int NtrOptions::shortPath

compute shortest paths in network

int NtrOptions::signatures

computation of signatures

char* NtrOptions::sinkfile

file for externally provided sink node

int NtrOptions::slots

unique subtable initial slots

int NtrOptions::stateOnly

ignore primary outputs

int NtrOptions::store

iteration at which to store Reached

char* NtrOptions::storefile

filename for storing Reached

int NtrOptions::symmviolation

percent symm violation in extended symmetry check

int NtrOptions::threshold

approximation threshold

int NtrOptions::traverse

do reachability analysis

char* NtrOptions::treefile

file name for variable tree

int NtrOptions::verb

level of verbosity

int NtrOptions::verify

read two networks and compare them

int NtrOptions::zddtest

do zdd test

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

nanotrav/ntr.h

Data Fields

Detailed Description

Field Documentation