ana::feasible_graph Class Reference

#include <feasible-graph.h>

Inheritance diagram for ana::feasible_graph:

Collaboration diagram for ana::feasible_graph:

Public Types
typedef GraphTraits::node_t	node_t
typedef GraphTraits::edge_t	edge_t
typedef GraphTraits::dump_args_t	dump_args_t
typedef GraphTraits::cluster_t	cluster_t

Public Member Functions
	feasible_graph ()
feasible_node *	add_node (const exploded_node *enode, const feasibility_state &state, unsigned path_length)
void	add_feasibility_problem (feasible_node *src_fnode, const exploded_edge *eedge, std::unique_ptr< rejected_constraint > rc)
std::unique_ptr< exploded_path >	make_epath (feasible_node *fnode) const
void	dump_feasible_path (const feasible_node &dst_fnode, const char *filename) const
unsigned	get_num_infeasible () const
void	log_stats (logger *logger) const
void	dump_dot_to_pp (pretty_printer *pp, cluster_t *root_cluster, const dump_args_t &args) const
void	dump_dot_to_file (FILE *fp, cluster_t *root_cluster, const dump_args_t &args) const
void	dump_dot (const char *path, cluster_t *root_cluster, const dump_args_t &args) const
void	add_node (node_t *node)
void	add_edge (edge_t *edge)

Data Fields
auto_delete_vec< node_t >	m_nodes
auto_delete_vec< edge_t >	m_edges

Private Member Functions
void	dump_feasible_path (const feasible_node &dst_fnode, pretty_printer *pp) const

Private Attributes
unsigned	m_num_infeasible

Detailed Description

A digraph subclass for exploring trees of feasible paths through
the egraph.  This is actually a tree.

The paths within the graph of feasible_nodes express feasible paths
through the graph, and it also captures known infeasible edges,
which is invaluable for debugging.   

Member Typedef Documentation

cluster_t

typedef GraphTraits::cluster_t digraph< fg_traits >::cluster_t

inherited

dump_args_t

typedef GraphTraits::dump_args_t digraph< fg_traits >::dump_args_t

inherited

edge_t

typedef GraphTraits::edge_t digraph< fg_traits >::edge_t

inherited

node_t

typedef GraphTraits::node_t digraph< fg_traits >::node_t

inherited

Constructor & Destructor Documentation

feasible_graph()

ana::feasible_graph::feasible_graph

(

)

Member Function Documentation

add_edge()

void digraph< fg_traits >::add_edge ( edge_t * edge )

inlineinherited

Add EDGE to this digraph, and to the preds/succs of its endpoints.
Take ownership of EDGE.   

add_feasibility_problem()

void ana::feasible_graph::add_feasibility_problem	(	feasible_node *	src_fnode,
		const exploded_edge *	eedge,
		std::unique_ptr< rejected_constraint >	rc )

add_node() [1/2]

feasible_node * ana::feasible_graph::add_node	(	const exploded_node *	enode,
		const feasibility_state &	state,
		unsigned	path_length )

add_node() [2/2]

void digraph< fg_traits >::add_node ( node_t * node )

inlineinherited

Add NODE to this DIGRAPH, taking ownership.   

dump_dot()

void digraph< fg_traits >::dump_dot ( const char * path, cluster_t * root_cluster, const dump_args_t & args ) const

inlineinherited

Write .dot information for this graph to a file at PATH, passing ARGS
to the nodes and edges.
If ROOT_CLUSTER is non-NULL, use it to organize the nodes into clusters.   

dump_dot_to_file()

void digraph< fg_traits >::dump_dot_to_file ( FILE * fp, cluster_t * root_cluster, const dump_args_t & args ) const

inlineinherited

Write .dot information for this graph to FP, passing ARGS to the nodes
and edges.
If ROOT_CLUSTER is non-NULL, use it to organize the nodes into clusters.   

dump_dot_to_pp()

void digraph< fg_traits >::dump_dot_to_pp ( pretty_printer * pp, cluster_t * root_cluster, const dump_args_t & args ) const

inlineinherited

Write .dot information for this graph to PP, passing ARGS to the nodes
and edges.
If ROOT_CLUSTER is non-NULL, use it to organize the nodes into clusters.   

dump_feasible_path() [1/2]

void ana::feasible_graph::dump_feasible_path	(	const feasible_node &	dst_fnode,
		const char *	filename ) const

dump_feasible_path() [2/2]

void ana::feasible_graph::dump_feasible_path ( const feasible_node & dst_fnode, pretty_printer * pp ) const

private

get_num_infeasible()

unsigned ana::feasible_graph::get_num_infeasible ( ) const

inline

References m_num_infeasible.

log_stats()

void ana::feasible_graph::log_stats

(

logger *

logger

)

const

make_epath()

std::unique_ptr< exploded_path > ana::feasible_graph::make_epath

(

feasible_node *

fnode

)

const

Field Documentation

m_edges

auto_delete_vec<edge_t> digraph< fg_traits >::m_edges

inherited

m_nodes

auto_delete_vec<node_t> digraph< fg_traits >::m_nodes

inherited

m_num_infeasible

unsigned ana::feasible_graph::m_num_infeasible

private

Referenced by get_num_infeasible().

---

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

• feasible-graph.h