The MpsDriver class brings together all components. More...

#include <Driver.h>

Inheritance diagram for dlinear::mps::MpsDriver:

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

void	ObjectiveSense (bool is_min)
	Set the objective sense of the problem after having encountered the OBJSENSE section.

void	ObjectiveName (const std::string &row)
	Set the name of the objective row after having encountered the OBJNAME section.

void	AddRow (Sense sense, const std::string &row)
	Add a row to the problem.

void	AddColumn (const std::string &column, const std::string &row, mpq_class value)
	Add a column to the problem.

void	AddRhs (const std::string &rhs, const std::string &row, mpq_class value)
	Add the right hand side of the row.

void	AddRange (const std::string &rhs, const std::string &row, mpq_class value)
	Add a new row contraint based on the range.

void	AddBound (BoundType type, const std::string &bound, const std::string &column, mpq_class value)
	Add a bound to a variable (column).

void	AddBound (BoundType type, const std::string &bound, const std::string &column)
	Add a binary bound to a variable (column).

void	End ()
	Called when the parser has reached the ENDATA section.

const std::string &	problem_name () const
	Get read-only access to the problem_name of the MpsDriver.

std::string &	m_problem_name ()
	Get read-write access to the problem_name of the MpsDriver.

bool	strict_mps () const
	Check whether the strict mps is enabled.

void	set_strict_mps (bool b)
	Set the strict mps mode.

std::size_t	n_assertions () const
	Get read-only access to the number of assertions of the MpsDriver.

bool	is_min () const
	Check whether the minimization is enabled.

const std::string &	obj_row () const
	Get read-only access to the objective row name of the MpsDriver.

MpsScanner *	scanner ()
	Get read-only access to the scanner of the MpsDriver.

void	ToSmt2 (std::ostream &os) const
	Print the problem in the smt2 format.

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.

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 location &l, const std::string &m)
	Error handling with associated line number.

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

Private Member Functions
bool	VerifyStrictRhs (const std::string &rhs)
	If strict_mps_ is true, keeps track of the name of the first rhs found.

bool	VerifyStrictBound (const std::string &bound)
	If strict_mps_ is true, keeps track of the name of the first bound found.

Private Attributes
std::string	problem_name_
	The name of the problem. Used to name the context.

bool	is_min_ {true}
	True if the problem is a minimization problem.

std::string	obj_row_
	The name of the objective row.

MpsScanner *	scanner_ {nullptr}
	The scanner producing the tokens for the parser.

bool	strict_mps_ {false}
	If true, the parser will check that all rhs, ranges and bounds have the same name.

std::unordered_map< std::string, std::map< Expression, mpq_class > >	rows_
	The rows of the problem.

std::unordered_map< std::string, Sense >	row_senses_
	The sense of each row.

std::unordered_map< std::string, Variable >	columns_
	The columns of the problem. Contains the variables.

std::unordered_map< std::string, bool >	skip_lower_bound_
	True if there is no need to manually add the lb 0 <= V.

std::unordered_map< std::string, mpq_class >	rhs_values_
	The values of the hand side of the problem.

std::map< std::string, Formula >	rhs_
	Assertions built by combining the rows and the rhs.

std::map< std::string, Formula >	bounds_
	Assertions built by combining the columns and the bounds.

std::string	rhs_name_
	The name of the first rhs found. Used if strict_mps_ is true.

std::string	bound_name_
	The name of the first bound found. Used if strict_mps_ is true.

Additional Inherited Members
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 MpsDriver class brings together all components.

It creates an instance of the Parser and Scanner classes and connects them. Then the input stream is fed into the scanner object and the parser gets it's token sequence. Furthermore the driver object is available in the grammar rules as a parameter. Therefore the driver class contains a reference to the structure into which the parsed data is saved.

Definition at line 37 of file Driver.h.

Member Function Documentation

◆ AddBound() [1/2]

void dlinear::mps::MpsDriver::AddBound	(	BoundType	type,
		const std::string &	bound,
		const std::string &	column )

Add a binary bound to a variable (column).

The value is not present, for it is inferred from the bound type. If strict_mps_ is true and multiple bounds are found, only the first one is considered, the others are skipped. In the mps file, a bound line is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
Bound Type	Bound	Column

Parameters

type	bound type. Must be either BV, FR, MI or PL.
bound	identifier of the bound. Used if strict_mps_ is true.
column	identifier of the variable (column)

Definition at line 176 of file Driver.cpp.

◆ AddBound() [2/2]

void dlinear::mps::MpsDriver::AddBound	(	BoundType	type,
		const std::string &	bound,
		const std::string &	column,
		mpq_class	value )

Add a bound to a variable (column).

If strict_mps_ is true and multiple bounds are found, only the first one is considered, the others are skipped. In the mps file, a bound line is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
Bound Type	Bound	Column	Value

Parameters

type	bound type
bound	identifier of the bound. Used if strict_mps_ is true.
column	identifier of the variable (column)
value	bound value

Definition at line 147 of file Driver.cpp.

◆ AddColumn()

void dlinear::mps::MpsDriver::AddColumn	(	const std::string &	column,
		const std::string &	row,
		mpq_class	value )

Add a column to the problem.

It creates a the variable (column), if not already present, and adds its coefficient (value) to the row. In the mps file, a row is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
	Column	Row1	Value(Row1)	Row2	Value(Row2)

The last two fields are optional.

Parameters

column	identifier of the column (variable)
row	identifier of the row
value	coefficient of the column in the row

Definition at line 75 of file Driver.cpp.

◆ AddRange()

void dlinear::mps::MpsDriver::AddRange	(	const std::string &	rhs,
		const std::string &	row,
		mpq_class	value )

Add a new row contraint based on the range.

If strict_mps_ is true and multiple ranges are found, only the first one is considered, the others are skipped. In the mps file, a range line is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
	Rhs	Row1	Value (Row1)	Row2	Value (Row2)

The last two fields are optional. The behaviour depends on the sense of the row:

| Row type | Range sign | Lower rhs | Upper rhs | |-------—|---------—|--------—|--------—| | G | +/- | rhs | rhs + |r| | | L | +/- | rhs - |r| | rhs | | E | + | rhs | rhs + r | | E | - | rhs + r | rhs |

Parameters

rhs	identifier of the rhs. Used if strict_mps_ is true.
row	identifier of the row
value	range value

Definition at line 117 of file Driver.cpp.

◆ AddRhs()

void dlinear::mps::MpsDriver::AddRhs	(	const std::string &	rhs,
		const std::string &	row,
		mpq_class	value )

Add the right hand side of the row.

It creates a formula that combines the row and the rhs using the sense of the row. If strict_mps_ is true and multiple rhs are found, only the first one is considered, the others are skipped. In the mps file, an RHS line is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
	RHS	Row1	Value (Row1)	Row2	Value (Row2)

The last two fields are optional.

Parameters

rhs	identifier of the rhs. Used if strict_mps_ is true.
row	identifier of the row
value	rhs value

Definition at line 89 of file Driver.cpp.

◆ AddRow()

void dlinear::mps::MpsDriver::AddRow	(	Sense	sense,
		const std::string &	row )

Add a row to the problem.

It creates a record for the row and stores the sense. In the mps file, a row is defined by:

Field1	Field2	Field3	Field4	Field5	Field6
Sense	Row

Parameters

sense	relation between the row and the rhs
row	identifier of the row

Definition at line 66 of file Driver.cpp.

◆ End()

void dlinear::mps::MpsDriver::End ( )

Called when the parser has reached the ENDATA section.

It finalizes the assertions, adding the default lower bound if needed, and launches the solver.

Definition at line 202 of file Driver.cpp.

◆ error()

void dlinear::mps::MpsDriver::error	(	const location &	l,
		const std::string &	m )

static

Error handling with associated line number.

This can be modified to output the error e.g. to a dialog box.

Definition at line 54 of file Driver.cpp.

◆ is_min()

bool dlinear::mps::MpsDriver::is_min ( ) const

inlinenodiscard

Check whether the minimization is enabled.

Returns: true if the minimization is enabled; false if the minimization is not enabled

Definition at line 204 of file Driver.h.

◆ m_problem_name()

std::string & dlinear::mps::MpsDriver::m_problem_name ( )

inline

Get read-write access to the problem_name of the MpsDriver.

Returns: problem_name of the MpsDriver

Definition at line 193 of file Driver.h.

◆ n_assertions()

std::size_t dlinear::mps::MpsDriver::n_assertions ( ) const

inlinenodiscard

Get read-only access to the number of assertions of the MpsDriver.

Returns: number of assertions of the MpsDriver

Definition at line 202 of file Driver.h.

◆ obj_row()

const std::string & dlinear::mps::MpsDriver::obj_row ( ) const

inlinenodiscard

Get read-only access to the objective row name of the MpsDriver.

Returns: objective row name of the MpsDriver

Definition at line 206 of file Driver.h.

◆ ObjectiveName()

void dlinear::mps::MpsDriver::ObjectiveName ( const std::string & row )

Set the name of the objective row after having encountered the OBJNAME section.

In the mps file, the objective name is defined by:

OBJNAME name

Parameters

row	name of the objective row

Definition at line 61 of file Driver.cpp.

◆ ObjectiveSense()

void dlinear::mps::MpsDriver::ObjectiveSense ( bool is_min )

Set the objective sense of the problem after having encountered the OBJSENSE section.

In the mps file, the objective sense is defined by:

OBJSENSE MAX or MIN

Parameters

is_min whether the problem is a minimization problem. It is true by default.

Definition at line 56 of file Driver.cpp.

◆ ParseStreamCore()

bool dlinear::mps::MpsDriver::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 18 of file Driver.cpp.

◆ problem_name()

const std::string & dlinear::mps::MpsDriver::problem_name ( ) const

inlinenodiscard

Get read-only access to the problem_name of the MpsDriver.

Returns: problem_name of the MpsDriver

Definition at line 191 of file Driver.h.

◆ scanner()

MpsScanner * dlinear::mps::MpsDriver::scanner ( )

inlinenodiscard

Get read-only access to the scanner of the MpsDriver.

Returns: scanner of the MpsDriver

Definition at line 208 of file Driver.h.

◆ set_strict_mps()

void dlinear::mps::MpsDriver::set_strict_mps ( bool b )

inline

Set the strict mps mode.

Parameters

b	new value of the strict mps mode

Definition at line 200 of file Driver.h.

◆ strict_mps()

bool dlinear::mps::MpsDriver::strict_mps ( ) const

inlinenodiscard

Check whether the strict mps is enabled.

Returns: true if the strict mps is enabled; false if the strict mps is not enabled

Definition at line 195 of file Driver.h.

◆ ToSmt2()

void dlinear::mps::MpsDriver::ToSmt2 ( std::ostream & os ) const

Print the problem in the smt2 format.

Parameters

os	output stream

Definition at line 234 of file Driver.cpp.

◆ VerifyStrictBound()

bool dlinear::mps::MpsDriver::VerifyStrictBound ( const std::string & bound )

inlineprivate

If strict_mps_ is true, keeps track of the name of the first bound found.

All the other bound must have the same name, otherwise they are skipped.

Parameters

bound identifier of the bound

Returns: whether the bound should be considered

Definition at line 30 of file Driver.cpp.

◆ VerifyStrictRhs()

bool dlinear::mps::MpsDriver::VerifyStrictRhs ( const std::string & rhs )

inlineprivate

If strict_mps_ is true, keeps track of the name of the first rhs found.

All the other rhs must have the same name, otherwise they are skipped.

Parameters

rhs	identifier of the rhs

Returns: whether the rhs should be considered

Definition at line 42 of file Driver.cpp.

Member Data Documentation

◆ rows_

std::unordered_map<std::string, std::map<Expression, mpq_class> > dlinear::mps::MpsDriver::rows_

private

The rows of the problem.

Contains a map between each variable, stored as an expression, and the coefficient. It will be used to build the final row_expression using the ExpressionAddFactory class. The result is then combined with the rhs value and the correct row sense to build the Formula that makes up the assertion.

Definition at line 245 of file Driver.h.

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

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

Public Member Functions

Static Public Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ AddBound() [1/2]

◆ AddBound() [2/2]

◆ AddColumn()

◆ AddRange()

◆ AddRhs()

◆ AddRow()

◆ End()

◆ error()

◆ is_min()

◆ m_problem_name()

◆ n_assertions()

◆ obj_row()

◆ ObjectiveName()

◆ ObjectiveSense()

◆ ParseStreamCore()

◆ problem_name()

◆ scanner()

◆ set_strict_mps()

◆ strict_mps()

◆ ToSmt2()

◆ VerifyStrictBound()

◆ VerifyStrictRhs()

Member Data Documentation

◆ rows_