#include <list>
#include <solvers/smt/smt_solver.h>
#include <string>
#include <unistd.h>
#include <irep2/irep2.h>

Include dependency graph for smtlib_conv.h:

This graph shows which files directly or indirectly include this file:

Classes
struct	sexpr
class	smtlib_smt_sort
class	smtlib_smt_ast
class	smtlib_convt
struct	smtlib_convt::process_emitter
struct	smtlib_convt::file_emitter
struct	smtlib_convt::symbol_table_rec
struct	smtlib_convt::external_process_died
	Thrown when the external solver process can no longer provide a usable answer: a write hit EPIPE (the process died) or its response could not be parsed (typically EOF from a dead process). More...

Enumerations
enum	smt_func_kind { SMT_FUNC_INT , SMT_FUNC_BOOL , SMT_FUNC_BVINT , SMT_FUNC_REAL , SMT_FUNC_SYMBOL , SMT_FUNC_ADD , SMT_FUNC_BVADD , SMT_FUNC_SUB , SMT_FUNC_BVSUB , SMT_FUNC_MUL , SMT_FUNC_BVMUL , SMT_FUNC_DIV , SMT_FUNC_BVUDIV , SMT_FUNC_BVSDIV , SMT_FUNC_MOD , SMT_FUNC_BVSMOD , SMT_FUNC_BVUMOD , SMT_FUNC_SHL , SMT_FUNC_BVSHL , SMT_FUNC_BVASHR , SMT_FUNC_NEG , SMT_FUNC_BVNEG , SMT_FUNC_BVLSHR , SMT_FUNC_BVNOT , SMT_FUNC_BVXOR , SMT_FUNC_BVOR , SMT_FUNC_BVAND , SMT_FUNC_IMPLIES , SMT_FUNC_XOR , SMT_FUNC_OR , SMT_FUNC_AND , SMT_FUNC_NOT , SMT_FUNC_LT , SMT_FUNC_BVSLT , SMT_FUNC_BVULT , SMT_FUNC_GT , SMT_FUNC_BVSGT , SMT_FUNC_BVUGT , SMT_FUNC_LTE , SMT_FUNC_BVSLTE , SMT_FUNC_BVULTE , SMT_FUNC_GTE , SMT_FUNC_BVSGTE , SMT_FUNC_BVUGTE , SMT_FUNC_EQ , SMT_FUNC_NOTEQ , SMT_FUNC_ITE , SMT_FUNC_STORE , SMT_FUNC_SELECT , SMT_FUNC_CONCAT , SMT_FUNC_EXTRACT , SMT_FUNC_INT2REAL , SMT_FUNC_REAL2INT , SMT_FUNC_IS_INT , SMT_FUNC_FNEG , SMT_FUNC_FABS , SMT_FUNC_ISZERO , SMT_FUNC_ISNAN , SMT_FUNC_ISINF , SMT_FUNC_ISNORMAL , SMT_FUNC_ISNEG , SMT_FUNC_ISPOS , SMT_FUNC_IEEE_EQ , SMT_FUNC_IEEE_ADD , SMT_FUNC_IEEE_SUB , SMT_FUNC_IEEE_MUL , SMT_FUNC_IEEE_DIV , SMT_FUNC_IEEE_FMA , SMT_FUNC_IEEE_SQRT , SMT_FUNC_IEEE_RM_NE , SMT_FUNC_IEEE_RM_ZR , SMT_FUNC_IEEE_RM_PI , SMT_FUNC_IEEE_RM_MI , SMT_FUNC_BV2FLOAT , SMT_FUNC_FLOAT2BV , SMT_FUNC_UF }
	Identifiers for SMT functions. More...

Enumeration Type Documentation

◆ smt_func_kind

enum smt_func_kind

Identifiers for SMT functions.

Each SMT function gets a unique identifier, representing its interpretation when applied to some arguments. This can be used to describe a function application when joined with some arguments. Initial values such as terminal functions (i.e. bool, int, symbol literals) shouldn't normally be encountered and instead converted to an smt_ast before use. The 'HACKS' function represents some kind of special case, according to where it is encountered; the same for 'INVALID'.

See also: smt_solver_baset::convert_terminal; smt_solver_baset::convert_ast

Enumerator
SMT_FUNC_INT
SMT_FUNC_BOOL
SMT_FUNC_BVINT
SMT_FUNC_REAL
SMT_FUNC_SYMBOL
SMT_FUNC_ADD
SMT_FUNC_BVADD
SMT_FUNC_SUB
SMT_FUNC_BVSUB
SMT_FUNC_MUL
SMT_FUNC_BVMUL
SMT_FUNC_DIV
SMT_FUNC_BVUDIV
SMT_FUNC_BVSDIV
SMT_FUNC_MOD
SMT_FUNC_BVSMOD
SMT_FUNC_BVUMOD
SMT_FUNC_SHL
SMT_FUNC_BVSHL
SMT_FUNC_BVASHR
SMT_FUNC_NEG
SMT_FUNC_BVNEG
SMT_FUNC_BVLSHR
SMT_FUNC_BVNOT
SMT_FUNC_BVXOR
SMT_FUNC_BVOR
SMT_FUNC_BVAND
SMT_FUNC_IMPLIES
SMT_FUNC_XOR
SMT_FUNC_OR
SMT_FUNC_AND
SMT_FUNC_NOT
SMT_FUNC_LT
SMT_FUNC_BVSLT
SMT_FUNC_BVULT
SMT_FUNC_GT
SMT_FUNC_BVSGT
SMT_FUNC_BVUGT
SMT_FUNC_LTE
SMT_FUNC_BVSLTE
SMT_FUNC_BVULTE
SMT_FUNC_GTE
SMT_FUNC_BVSGTE
SMT_FUNC_BVUGTE
SMT_FUNC_EQ
SMT_FUNC_NOTEQ
SMT_FUNC_ITE
SMT_FUNC_STORE
SMT_FUNC_SELECT
SMT_FUNC_CONCAT
SMT_FUNC_EXTRACT
SMT_FUNC_INT2REAL
SMT_FUNC_REAL2INT
SMT_FUNC_IS_INT
SMT_FUNC_FNEG
SMT_FUNC_FABS
SMT_FUNC_ISZERO
SMT_FUNC_ISNAN
SMT_FUNC_ISINF
SMT_FUNC_ISNORMAL
SMT_FUNC_ISNEG
SMT_FUNC_ISPOS
SMT_FUNC_IEEE_EQ
SMT_FUNC_IEEE_ADD
SMT_FUNC_IEEE_SUB
SMT_FUNC_IEEE_MUL
SMT_FUNC_IEEE_DIV
SMT_FUNC_IEEE_FMA
SMT_FUNC_IEEE_SQRT
SMT_FUNC_IEEE_RM_NE
SMT_FUNC_IEEE_RM_ZR
SMT_FUNC_IEEE_RM_PI
SMT_FUNC_IEEE_RM_MI
SMT_FUNC_BV2FLOAT
SMT_FUNC_FLOAT2BV
SMT_FUNC_UF

Classes

Enumerations

Enumeration Type Documentation

◆ smt_func_kind