The Driver is the base class for all the parsers. More...

#include <Driver.h>

Inheritance diagram for dlinear::Driver:

Public Member Functions
	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.

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

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.

Static Public Member Functions
static void	Error (const std::string &m)
	General error handling.

Protected Member Functions
virtual bool	ParseStreamCore (std::istream &in)=0
	Parse the stream.

Protected Attributes
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 Driver is the base class for all the parsers.

It contains the common logic to allow the parsed data to be saved in the context. It coordinates the communication between the parser (bison) and the scanner (flex).

Definition at line 26 of file Driver.h.

Member Function Documentation

◆ context()

const Context & dlinear::Driver::context ( ) const

inlinenodiscard

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

Returns: enabled of the Driver

Definition at line 143 of file Driver.h.

◆ Exit()

void dlinear::Driver::Exit ( )

inline

Callback for the command exit.

Terminate the parsing

Definition at line 136 of file Driver.h.

◆ GetAssertions()

void dlinear::Driver::GetAssertions ( ) const

Callback for the command get-assertions.

Print all the assertions currently in the context. If the mode is set to silent, it does not print anything.

Definition at line 76 of file Driver.cpp.

◆ GetInfo()

void dlinear::Driver::GetInfo ( const std::string & key ) const

Callback for the command get-info.

Print information about the solver or the current context.

Parameters

key	key of the information to print

Definition at line 93 of file Driver.cpp.

◆ GetOption()

void dlinear::Driver::GetOption ( const std::string & key ) const

Callback for the command get-option.

Print the value of and option or an empty string if the option is not set.

Parameters

key	key of the option

Definition at line 88 of file Driver.cpp.

◆ m_stream_name()

std::string & dlinear::Driver::m_stream_name ( )

inline

Get read-write access to the stream name of the input being parsed.

Returns: stream name of the input being parsed

Definition at line 147 of file Driver.h.

◆ Maximize()

void dlinear::Driver::Maximize ( const Expression & f )

Maximize the objective function f.

The objective function is added to the context as a constraint.

Parameters

f	expression to maximize}

Definition at line 98 of file Driver.cpp.

◆ Minimize()

void dlinear::Driver::Minimize ( const Expression & f )

Minimize the objective function f.

The objective function is added to the context as a constraint.

Parameters

f	expression to minimize

Definition at line 106 of file Driver.cpp.

◆ ParseFile()

bool dlinear::Driver::ParseFile ( const std::string & filename )

virtual

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 in dlinear::onnx::OnnxDriver.

Definition at line 54 of file Driver.cpp.

◆ ParseStream()

bool dlinear::Driver::ParseStream	(	std::istream &	in,
		const std::string &	sname = "stream input" )

Invoke the scanner and parser for a stream.

Parameters

in	input stream
sname	stream name for error messages

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

Definition at line 30 of file Driver.cpp.

◆ ParseStreamCore()

virtual bool dlinear::Driver::ParseStreamCore ( std::istream & in )

protectedpure virtual

Parse the stream.

Parameters

in	input stream

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

Implemented in dlinear::mps::MpsDriver, dlinear::onnx::OnnxDriver, dlinear::smt2::Smt2Driver, and dlinear::vnnlib::VnnlibDriver.

◆ ParseString()

bool dlinear::Driver::ParseString	(	const std::string &	input,
		const std::string &	sname = "string stream" )

Invoke the scanner and parser on an input string.

Parameters

input	input string
sname	stream name for error messages

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

Definition at line 49 of file Driver.cpp.

◆ Pop()

void dlinear::Driver::Pop ( int n )

inline

Restore a previously pushed context from the stack.

The current state of the context can be stored by calling Push.

Parameters

n	number of stacks to pop

Definition at line 76 of file Driver.h.

◆ Push()

void dlinear::Driver::Push ( int n )

inline

Push the current context to the stack.

The current state of the context can be restored by calling Pop.

Parameters

n	number of stacks to push

Definition at line 69 of file Driver.h.

◆ SetInfo()

void dlinear::Driver::SetInfo	(	const std::string &	key,
		const std::string &	value )

inline

Callback for the command set-info.

Set the value of the information identified by key.

Parameters

key	key of the information to set
value	value of the information

Definition at line 108 of file Driver.h.

◆ SetLogic()

void dlinear::Driver::SetLogic ( const Logic logic )

inline

Callback for the command set-logic.

Set the logic used through the input.

Parameters

logic smt-lib logic

Definition at line 119 of file Driver.h.

◆ SetOption()

void dlinear::Driver::SetOption	(	const std::string &	key,
		const std::string &	value )

inline

Callback for the command set-option.

Set the value of the option identified by key.

Parameters

key	key of the option to set
value	value of the option

Definition at line 114 of file Driver.h.

◆ stats()

const Stats & dlinear::Driver::stats ( ) const

inlinenodiscard

Statistics for the driver.

Returns: statistics for the driver

Definition at line 153 of file Driver.h.

◆ stream_name()

const std::string & dlinear::Driver::stream_name ( ) const

inlinenodiscard

Get read-only access to the stream name of the input being parsed.

Returns: stream name of the input being parsed

Definition at line 145 of file Driver.h.

◆ trace_parsing()

bool dlinear::Driver::trace_parsing ( ) const

inlinenodiscard

Check whether the trace debugger is enabled.

Returns: true if the trace debugger is enabled; false if the trace debugger is not enabled

Definition at line 141 of file Driver.h.

◆ trace_scanning()

bool dlinear::Driver::trace_scanning ( ) const

inlinenodiscard

Check whether the scanner debugger is enabled.

Returns: true if the scanner debugger is enabled; false if the scanner debugger is not enabled

Definition at line 139 of file Driver.h.

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

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

Public Member Functions

Static Public Member Functions

Protected Member Functions

Protected Attributes

Detailed Description

Member Function Documentation

◆ context()

◆ Exit()

◆ GetAssertions()

◆ GetInfo()

◆ GetOption()

◆ m_stream_name()

◆ Maximize()

◆ Minimize()

◆ ParseFile()

◆ ParseStream()

◆ ParseStreamCore()

◆ ParseString()

◆ Pop()

◆ Push()

◆ SetInfo()

◆ SetLogic()

◆ SetOption()

◆ stats()

◆ stream_name()

◆ trace_parsing()

◆ trace_scanning()