dlinear::smt2 Namespace Reference

Namespace for the SMT2 parser of the dlinear library. More...

Classes
class	FunctionDefinition
	A new function defined by the user in the SMT2 language using the define-fun command. More...
class	Smt2Driver
	The Smt2Driver class brings together all components. More...
class	Smt2Scanner
	Smt2Scanner is a derived class to add some extra function to the scanner class. More...
class	Term
	Generic term that can be either an expression or a formula. More...

Enumerations
enum class	Sort { Binary , Bool , Int , Real }
	Sort of a term. More...

Functions
Sort	ParseSort (const std::string &s)
	Parse a string to a sort.
Variable::Type	SortToType (Sort sort)
	Convert a sort to a variable type.

Detailed Description

Namespace for the SMT2 parser of the dlinear library.

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear

Licence:

BSD 3-Clause License

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear @copyrignt 2017 Toyota Research Institute (dreal4)

Licence:

BSD 3-Clause License Driver form the parsing and execution of smt2 files.

The driver puts in communication the parser and the scanner. In the end, it produces a context that can be used to solve the problem.

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear @copyrignt 2017 Toyota Research Institute (dreal4)

Licence:

BSD 3-Clause License Function definition class

In the SMT2 language, a function definition is a way to define a function in terms of its parameters and body. A function defined in this way can be called with the operator() method by providing the required arguments.

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear

Licence:

BSD 3-Clause License SMT2 parser for the dlinear library.

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear @copyrignt 2017 Toyota Research Institute (dreal4)

Licence:

BSD 3-Clause License Sort enum.

Author

Ernesto Casablanca (casab.nosp@m.lanc.nosp@m.aerne.nosp@m.sto@.nosp@m.gmail.nosp@m..com)

Copyright

2024 dlinear @copyrignt 2017 Toyota Research Institute (dreal4)

Licence:

BSD 3-Clause License Term class.

Terms are the building blocks of a smt problem. They can take many forms, such as:

• variables
• constants
• functions

Enumeration Type Documentation

Sort

enum class dlinear::smt2::Sort

strong

Sort of a term.

Enumerator
Binary	Binary sort.
Bool	Boolean sort.
Int	Integer sort.
Real	Real sort.

Definition at line 18 of file Sort.h.

Function Documentation

ParseSort()

Sort dlinear::smt2::ParseSort

(

const std::string &

s

)

Parse a string to a sort.

Parameters

s	string to parse

Returns

sort parsed from s

Definition at line 12 of file Sort.cpp.

SortToType()

Variable::Type dlinear::smt2::SortToType

(

Sort

sort

)

Convert a sort to a variable type.

The conversion is as follows:

• Binary -> BINARY
• Bool -> BOOLEAN
• Int -> INTEGER
• Real -> CONTINUOUS

  Parameters

  sort	sort to convert

  Returns

  variable type corresponding to sort

Definition at line 43 of file Sort.cpp.