The OnnxDriver class reads the onnx file. More...

#include <Driver.h>

Inheritance diagram for dlinear::onnx::OnnxDriver:

Public Member Functions
	OnnxDriver (Context &context)
	Construct a new parser driver context.

bool	ParseStreamCore (std::istream &in) override
	Parse the stream.

bool	ParseFile (const std::string &filename) override
	Invoke the scanner and parser on a file.

const std::unordered_map< std::string, Tensor > &	variables () const
	Get read-only access to the variables of the Driver.

const std::unordered_map< std::string, Tensor > &	available_inputs () const
	Get read-only access to the available_inputs of the Driver.

const ::onnx::ModelProto &	model () const
	Get read-only access to the model of the Driver.

const ::onnx::GraphProto &	graph () const
	Get read-only access to the graph of the Driver.

Public Member Functions inherited from dlinear::Driver
	Driver (Context &context, const std::string &class_name="Driver")
	construct a new parser driver context

bool	ParseStream (std::istream &in, const std::string &sname="stream input")
	Invoke the scanner and parser for a stream.

bool	ParseString (const std::string &input, const std::string &sname="string stream")
	Invoke the scanner and parser on an input string.

void	Push (int n)
	Push the current context to the stack.

void	Pop (int n)
	Restore a previously pushed context from the stack.

void	CheckSat ()
	Call context_.CheckSat() and print proper output messages to the standard output.

void	GetModel ()
	Return a model computed by the solver in response to an invocation of the check-sat.

void	GetAssertions () const
	Callback for the command `get-assertions`.

void	GetOption (const std::string &key) const
	Callback for the command `get-option`.

void	GetInfo (const std::string &key) const
	Callback for the command `get-info`.

void	SetInfo (const std::string &key, const std::string &value)
	Callback for the command `set-info`.

void	SetOption (const std::string &key, const std::string &value)
	Callback for the command `set-option`.

void	SetLogic (const Logic logic)
	Callback for the command `set-logic`.

void	Maximize (const Expression &f)
	Maximize the objective function `f`.

void	Minimize (const Expression &f)
	Minimize the objective function `f`.

void	Exit ()
	Callback for the command `exit`.

bool	trace_scanning () const
	Check whether the scanner debugger is enabled.

bool	trace_parsing () const
	Check whether the trace debugger is enabled.

const Context &	context () const
	Get read-only access to the enabled of the Driver.

const std::string &	stream_name () const
	Get read-only access to the stream name of the input being parsed.

std::string &	m_stream_name ()
	Get read-write access to the stream name of the input being parsed.

const Stats &	stats () const
	Statistics for the driver.

Private Member Functions
template<IsAnyOf< bool, float, std::int64_t, std::string, std::vector< float >, std::vector< std::int64_t >, std::vector< std::string >, const ::onnx::TensorProto * > T>
T	GetAttribute (const ::onnx::NodeProto &node, const std::string &name, const std::optional< T > &default_value={}) const
	Get the attribute `name` from the `node`.

void	ParseGraph ()
	Parse the model_ 's graph.

void	AddNodes ()
	Go through all the nodes in the graph and construct the final assertions.

bool	AddNode (const ::onnx::NodeProto &node)
	Go through a specific node and add the corresponding assertions.

void	AddValueInfo (const ::onnx::ValueInfoProto &value_info, bool is_input=false)
	Add the input and output to the Context.

void	AddValueInfoTensor (const ::onnx::ValueInfoProto &value_info, bool is_input=false)
	Add the input and output to the Context.

void	AddInitializer (const ::onnx::TensorProto &tensor)
	Add an initializer to the available_inputs_.

void	AddFormula (const std::string &output)
	Add the formulas to the Context.

template<NodeOpType T>
void	AddNode (const ::onnx::NodeProto &node)
	Add a node to the context.

const Variable &	ToEqualVar (const Expression &expression)
	Associate to a linear expression a fresh variable.

Private Attributes
::onnx::ModelProto	model_ {}
	The onnx model obtained from the file.

std::unordered_map< std::string, Tensor >	variables_
	Variables in the model.

std::unordered_map< std::string, Tensor >	available_inputs_
	Available inputs in the model.

std::unordered_map< Expression, Variable >	equal_vars_
	Variables created to summarize linear constraints.

Static Private Attributes
static const std::map< std::string, std::function< void(OnnxDriver &, const ::onnx::NodeProto &)> >	node_handlers
	Map between node op_type and the corresponding handler..

Additional Inherited Members
Static Public Member Functions inherited from dlinear::Driver
static void	Error (const std::string &m)
	General error handling.

Protected Attributes inherited from dlinear::Driver
std::string	stream_name_
	The name of the stream being parsed.

Context &	context_
	The context filled during parsing of the expressions.

bool	debug_scanning_ {false}
	Enable debug output in the flex scanner.

bool	debug_parsing_ {false}
	Enable debug output in the bison parser.

Stats	stats_
	Statistics for the driver.

Timer *	timer_
	Pointer to the timer for the driver. Used to Pause the timer when checking sat.

Detailed Description

The OnnxDriver class reads the onnx file.

The information collected is used to update the context by running all the nodes, from the input to the output of the graph.

Definition at line 37 of file Driver.h.

Constructor & Destructor Documentation

◆ OnnxDriver()

dlinear::onnx::OnnxDriver::OnnxDriver ( Context & context )

explicit

Construct a new parser driver context.

Parameters

context context filled during parsing

Definition at line 113 of file Driver.cpp.

Member Function Documentation

◆ AddFormula()

void dlinear::onnx::OnnxDriver::AddFormula ( const std::string & output )

private

Add the formulas to the Context.

Parameters

output name of the output

Definition at line 174 of file Driver.cpp.

◆ AddInitializer()

void dlinear::onnx::OnnxDriver::AddInitializer ( const ::onnx::TensorProto & tensor )

private

Add an initializer to the available_inputs_.

Parameters

tensor tensor to add

Definition at line 167 of file Driver.cpp.

◆ AddNode() [1/2]

bool dlinear::onnx::OnnxDriver::AddNode ( const ::onnx::NodeProto & node )

private

Go through a specific node and add the corresponding assertions.

If any of the inputs required by the node is missing, the node is not added. If the node is successfully added, the outputs are made available in the available_inputs_.

Parameters

node	node to add

Returns: true if the node was added; false if the node was not added (e.g. some of the inputs are not yet available)

Definition at line 718 of file Driver.cpp.

◆ AddNode() [2/2]

template<NodeOpType T>

void dlinear::onnx::OnnxDriver::AddNode ( const ::onnx::NodeProto & node )

private

Add a node to the context.

Template Parameters

T	type of the node

Parameters

node	node to add

◆ AddNodes()

void dlinear::onnx::OnnxDriver::AddNodes ( )

private

Go through all the nodes in the graph and construct the final assertions.

For a queue with all the nodes in the graph. The queue is iterated until it is empty, or until no other node can be added. After a node has been successfully added, the corresponding node is removed from the queue and its outputs are made available in the available_inputs_.

Definition at line 744 of file Driver.cpp.

◆ AddValueInfo()

void dlinear::onnx::OnnxDriver::AddValueInfo	(	const ::onnx::ValueInfoProto &	value_info,
		bool	is_input = false )

private

Add the input and output to the Context.

Parameters

value_info	value_info to add
is_input	true if the value_info is an input

Definition at line 767 of file Driver.cpp.

◆ AddValueInfoTensor()

void dlinear::onnx::OnnxDriver::AddValueInfoTensor	(	const ::onnx::ValueInfoProto &	value_info,
		bool	is_input = false )

private

Add the input and output to the Context.

Parameters

value_info	value_info to add
is_input	true if the value_info is an input

Definition at line 783 of file Driver.cpp.

◆ available_inputs()

const std::unordered_map< std::string, Tensor > & dlinear::onnx::OnnxDriver::available_inputs ( ) const

inlinenodiscard

Get read-only access to the available_inputs of the Driver.

Returns: available_inputs of the Driver

Definition at line 51 of file Driver.h.

◆ GetAttribute()

template<IsAnyOf< bool, float, std::int64_t, std::string, std::vector< float >, std::vector< std::int64_t >, std::vector< std::string >, const ::onnx::TensorProto * > T>

templateconst::onnx::TensorProto * dlinear::onnx::OnnxDriver::GetAttribute	(	const ::onnx::NodeProto &	node,
		const std::string &	name,
		const std::optional< T > &	default_value = {} ) const

private

Get the attribute name from the node.

If the attribute is not found, the default_value is returned. If no default_value is provided, an exception is thrown.

Template Parameters

T	type of the attribute to get. Limited to bool float int64_t string vector<float>, vector<int64_t> vector<string> const onnx::TensorProto*.

Parameters

node	node to get the attribute from
name	name of the attribute
default_value	optional default value. If the attribute is not found, this value is returned.

Returns: attribute value

Exceptions

std::runtime_error if the attribute is not found and no default value is provided

Definition at line 153 of file Driver.cpp.

◆ graph()

const ::onnx::GraphProto & dlinear::onnx::OnnxDriver::graph ( ) const

inlinenodiscard

Get read-only access to the graph of the Driver.

Returns: graph of the Driver

Definition at line 55 of file Driver.h.

◆ model()

const ::onnx::ModelProto & dlinear::onnx::OnnxDriver::model ( ) const

inlinenodiscard

Get read-only access to the model of the Driver.

Returns: model of the Driver

Definition at line 53 of file Driver.h.

◆ ParseFile()

bool dlinear::onnx::OnnxDriver::ParseFile ( const std::string & filename )

overridevirtual

Invoke the scanner and parser on a file.

Use parse_stream with a std::ifstream if detection of file reading errors is required.

Parameters

filename input file name

Returns: true if successfully parsed; false if an error occurred

Reimplemented from dlinear::Driver.

Definition at line 125 of file Driver.cpp.

◆ ParseStreamCore()

bool dlinear::onnx::OnnxDriver::ParseStreamCore ( std::istream & in )

overridevirtual

Parse the stream.

Parameters

in	input stream

Returns: true if successfully parsed; false if an error occurred

Implements dlinear::Driver.

Definition at line 115 of file Driver.cpp.

◆ ToEqualVar()

const Variable & dlinear::onnx::OnnxDriver::ToEqualVar ( const Expression & expression )

private

Associate to a linear expression a fresh variable.

The variable is created and added to the equal_vars_. If the same expression is passed again, the same variable is returned.

Parameters

expression expression to associate with a variable

Returns: corresponding variable

Definition at line 794 of file Driver.cpp.

◆ variables()

const std::unordered_map< std::string, Tensor > & dlinear::onnx::OnnxDriver::variables ( ) const

inlinenodiscard

Get read-only access to the variables of the Driver.

Returns: variables of the Driver

Definition at line 49 of file Driver.h.

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

dlinear/parser/onnx/Driver.h
dlinear/parser/onnx/Driver.cpp

Public Member Functions

Private Member Functions

Private Attributes

Static Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ OnnxDriver()

Member Function Documentation

◆ AddFormula()

◆ AddInitializer()

◆ AddNode() [1/2]

◆ AddNode() [2/2]

◆ AddNodes()

◆ AddValueInfo()

◆ AddValueInfoTensor()

◆ available_inputs()

◆ GetAttribute()

◆ graph()

◆ model()

◆ ParseFile()

◆ ParseStreamCore()

◆ ToEqualVar()

◆ variables()