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

#include </home/soonhokong/work/dreal4/dreal/smt2/driver.h>

Public Member Functions
	Smt2Driver ()=default
	construct a new parser driver context

	Smt2Driver (Context context)

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

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

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

void	CheckSat ()
	Calls context_.CheckSat() and print proper output messages to cout.

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

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]`. More...

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. More...

void	DefineFun (const std::string &name, const std::vector< Variable > &parameters, Sort return_type, const Term &body)
	Handles define-fun.

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

void	GetValue (const std::vector< Term > &term_list) const
	`GetValue([t1, t2, ..., tn])` returns a list of values [v1, v2, ..., vn] where v_i is equivalent to t_i in the current model. More...

void	GetOption (const std::string &key) const
	Handles `(get-option key)`.

const Variable &	lookup_variable (const std::string &name)
	Returns a variable associated with a name `name`. More...

void	PushScope ()

void	PopScope ()

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

std::string	MakeUniqueName (const std::string &name)

bool	trace_scanning () const

void	set_trace_scanning (bool b)

bool	trace_parsing () const

void	set_trace_parsing (bool b)

Context &	mutable_context ()

std::string &	mutable_streamname ()

Static Public Member Functions
static void	error (const location &l, const std::string &m)
	Error handling with associated line number. More...

static void	error (const std::string &m)
	General error handling. More...

static Variable	ParseVariableSort (const std::string &name, Sort s)

static Formula	EliminateBooleanVariables (const Variables &vars, const Formula &f)
	Eliminate Boolean variables in `vars`, `[b_1, ... More...

Public Attributes
Smt2Scanner *	scanner {nullptr}
	Pointer to the current scanenr instance, this is used to connect the parser to the scanner. More...

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.

Member Function Documentation

◆ DeclareLocalVariable()

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.

◆ DeclareVariable()

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].

◆ EliminateBooleanVariables()

Formula EliminateBooleanVariables	(	const Variables &	vars,
		const Formula &	f
	)

static

Eliminate Boolean variables in vars, `[b_1, ...

b_n], from @p f by constructingf[b ↦ true] ∧ f[b ↦ false]. This is used in handlingforall` terms.

◆ error() [1/2]

void 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.

◆ error() [2/2]

void error ( const std::string & m )

static

General error handling.

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

◆ GetModel()

void GetModel ( ) const

Returns a representation of a model computed by the solver in response to an invocation of the check-sat.

◆ GetValue()

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

GetValue([t1, t2, ..., tn]) returns a list of values [v1, v2, ..., vn] where v_i is equivalent to t_i in the current model.

◆ lookup_variable()

const Variable & lookup_variable ( const std::string & name )

Returns a variable associated with a name name.

Exceptions

if	no variable is associated with `name`.

◆ parse_file()

bool parse_file ( const std::string & filename )

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

◆ parse_stream()

bool parse_stream	(	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

◆ parse_string()

bool parse_string	(	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

◆ RegisterVariable()

Variable 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.

Member Data Documentation

◆ scanner

Smt2Scanner* scanner {nullptr}

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

It is used in the yylex macro.

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

/home/soonhokong/work/dreal4/dreal/smt2/driver.h
/home/soonhokong/work/dreal4/dreal/smt2/driver.cc

Public Member Functions

Static Public Member Functions

Public Attributes

Detailed Description

Member Function Documentation

◆ DeclareLocalVariable()

◆ DeclareVariable()

◆ EliminateBooleanVariables()

◆ error() [1/2]

◆ error() [2/2]

◆ GetModel()

◆ GetValue()

◆ lookup_variable()

◆ parse_file()

◆ parse_stream()

◆ parse_string()

◆ RegisterVariable()

Member Data Documentation

◆ scanner