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

#include <Driver.h>

Inheritance diagram for dlinear::smt2::Smt2Driver:

Public Member Functions
	Smt2Driver (Context &context)
	construct a new parser driver context

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

void	DefineFun (const std::string &name, const std::vector< Variable > &parameters, Sort return_type, const Term &body)
	Called by the `define-fun` command in the SMT-2 file.

Variable	RegisterVariable (const std::string &name, Sort sort)
	Register a variable with name `name` and sort `s` in the scope.

Variable	DeclareVariable (const std::string &name, Sort sort)
	Declare a variable with name `name` and sort `sort`.

void	DeclareVariable (const std::string &name, Sort sort, const Term &lb, const Term &ub)
	Declare a variable with name `name` and sort `sort` which is bounded by an interval `[lb, ub]`

Variable	DeclareLocalVariable (const std::string &name, Sort sort)
	Declare a new variable with label `name` that is globally unique and cannot occur in an SMT-LIBv2 file.

void	DefineLocalConstant (const std::string &name, const Expression &value)
	Define a constant within the current scope.

void	GetValue (const std::vector< Term > &term_list) const
	Get the value of all the terms in `term_list`.

std::variant< const Expression , const Variable >	LookupDefinedName (const std::string &name) const
	Lookup a variable or constant expression associated with a name `name`.

const Expression &	LookupConstant (const std::string &name) const
	Lookup a constant expression associated with a name `name`.

const Variable &	LookupVariable (const std::string &name) const
	Lookup a variable associated with a name `name`.

Term	LookupFunction (const std::string &name, const std::vector< Term > &arguments) const
	Lookup a function with name `name` and run it with `arguments`, producing a new term.

Smt2Scanner *	scanner ()
	Pointer to the current scanner instance, this is used to connect the parser to the scanner.

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 Formula	EliminateBooleanVariables (const Variables &vars, const Formula &f)
	Eliminate Boolean variables \( [b_1, …, b_n] \in \) `vars` from `f`.

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

Private Attributes
Smt2Scanner *	scanner_ {nullptr}
	The scanner producing the tokens for the parser.

ScopedUnorderedMap< std::string, Expression >	scope_constants_
	Scoped map from a name to a constant.

ScopedUnorderedMap< std::string, Variable >	scope_variables_
	Scoped map from a name to a Variable.

ScopedUnorderedMap< std::string, FunctionDefinition >	scope_functions_
	Scoped map from a name to a Function.

int64_t	nextUniqueId_ {}
	Sequential value concatenated to names to make them unique.

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 Smt2Driver 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 38 of file Driver.h.

Member Function Documentation

◆ DefineFun()

void dlinear::smt2::Smt2Driver::DefineFun	(	const std::string &	name,
		const std::vector< Variable > &	parameters,
		Sort	return_type,
		const Term &	body )

Called by the define-fun command in the SMT-2 file.

It defines a function with name name, parameters parameters, return type return_type, and body body.

Parameters

name	name of the function
parameters	parameters the function takes
return_type	return type of the function
body	body of the function

Definition at line 45 of file Driver.cpp.

◆ EliminateBooleanVariables()

Formula dlinear::smt2::Smt2Driver::EliminateBooleanVariables	(	const Variables &	vars,
		const Formula &	f )

static

Eliminate Boolean variables \( [b_1, …, b_n] \in \) vars from f.

This is done by constructing \( f[b \to \text{true}] \land f[b \to \text{false}] \). Used in handling forall terms.

Parameters

vars	set of variables to eliminate
f	formula to eliminate the variables from

Returns: formula with the variables eliminated

Definition at line 35 of file Driver.cpp.

◆ error()

void dlinear::smt2::Smt2Driver::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 33 of file Driver.cpp.

◆ GetValue()

void dlinear::smt2::Smt2Driver::GetValue ( const std::vector< Term > & term_list ) const

Get the value of all the terms in term_list.

Maps each term \( t_i \in \) term_list to its value \( v_i \) in the current model.

Parameters

term_list list of terms to get the value of

Definition at line 82 of file Driver.cpp.

◆ LookupConstant()

const Expression & dlinear::smt2::Smt2Driver::LookupConstant ( const std::string & name ) const

Lookup a constant expression associated with a name name.

Parameters

name	name of the constant expression

Returns: the constant expression with name name

Exceptions

std::out_or_range std:: if no constant expression is associated with name

Definition at line 126 of file Driver.cpp.

◆ LookupDefinedName()

std::variant< const Expression *, const Variable * > dlinear::smt2::Smt2Driver::LookupDefinedName ( const std::string & name ) const

Lookup a variable or constant expression associated with a name name.

Parameters

name	name of the variable or constant expression

Returns: the variable or constant expression with name name

Exceptions

std::out_or_range std:: if no variable or constant expression is associated with name

Definition at line 118 of file Driver.cpp.

◆ LookupFunction()

Term dlinear::smt2::Smt2Driver::LookupFunction	(	const std::string &	name,
		const std::vector< Term > &	arguments ) const

Lookup a function with name name and run it with arguments, producing a new term.

Parameters

name	name of the function
arguments	arguments to pass to the function

Returns: output of the function name with arguments

Exceptions

std::out_or_range	if no function is associated with `name`
std::runtime_error	if the function is incompatible with the `arguments`

Definition at line 138 of file Driver.cpp.

◆ LookupVariable()

const Variable & dlinear::smt2::Smt2Driver::LookupVariable ( const std::string & name ) const

Lookup a variable associated with a name name.

Parameters

name	name of the variable

Returns: the variable with name name

Exceptions

std::out_or_range if no variable is associated with name

Definition at line 132 of file Driver.cpp.

◆ ParseStreamCore()

bool dlinear::smt2::Smt2Driver::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 21 of file Driver.cpp.

◆ RegisterVariable()

Variable dlinear::smt2::Smt2Driver::RegisterVariable	(	const std::string &	name,
		Sort	sort )

Register a variable with name name and sort s in the scope.

Note that it does not declare the variable in the context.

Definition at line 51 of file Driver.cpp.

◆ scanner()

Smt2Scanner * dlinear::smt2::Smt2Driver::scanner ( )

inline

Pointer to the current scanner instance, this is used to connect the parser to the scanner.

It is used in the yylex macro.

Definition at line 140 of file Driver.h.

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

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

Public Member Functions

Static Public Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Member Function Documentation

◆ DefineFun()

◆ EliminateBooleanVariables()

◆ error()

◆ GetValue()

◆ LookupConstant()

◆ LookupDefinedName()

◆ LookupFunction()

◆ LookupVariable()

◆ ParseStreamCore()

◆ RegisterVariable()

◆ scanner()