smt_sort.h File Reference

#include <irep2/irep2_type.h>

Include dependency graph for smt_sort.h:

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

Go to the source code of this file.

Classes
class	smt_sort
class	solver_smt_sort< solver_sort >

Typedefs
typedef const smt_sort *	smt_sortt

Enumerations
enum	smt_sort_kind {   SMT_SORT_INT , SMT_SORT_REAL , SMT_SORT_BV , SMT_SORT_FIXEDBV ,   SMT_SORT_ARRAY , SMT_SORT_BOOL , SMT_SORT_STRUCT , SMT_SORT_BVFP ,   SMT_SORT_FPBV , SMT_SORT_BVFP_RM , SMT_SORT_FPBV_RM }
	Identifier for SMT sort kinds Each different kind of sort (i.e., arrays, bv's, bools, etc) gets its own identifier. More...

Functions
template<typename T>
const solver_smt_sort< T > *	to_solver_smt_sort (smt_sortt s)

Typedef Documentation

smt_sortt

typedef const smt_sort* smt_sortt

Enumeration Type Documentation

smt_sort_kind

enum smt_sort_kind

Identifier for SMT sort kinds Each different kind of sort (i.e., arrays, bv's, bools, etc) gets its own identifier.

To be able to describe multiple kinds at the same time, they take binary values, so that they can be used as bits in an integer.

Enumerator
SMT_SORT_INT
SMT_SORT_REAL
SMT_SORT_BV
SMT_SORT_FIXEDBV
SMT_SORT_ARRAY
SMT_SORT_BOOL
SMT_SORT_STRUCT
SMT_SORT_BVFP
SMT_SORT_FPBV
SMT_SORT_BVFP_RM
SMT_SORT_FPBV_RM

Function Documentation

to_solver_smt_sort()

template<typename T>

const solver_smt_sort< T > * to_solver_smt_sort

(

smt_sortt

s

)