The class for uninterpreted function. More...

#include <func.h>

Inheritance diagram for ilang::Func:

Public Types
typedef std::shared_ptr< Func >	FuncPtr
	Pointer type for normal use of Func.

Public Types inherited from ilang::Object
typedef std::shared_ptr< Object >	ObjPtr
	Pointer type for normal use of Object.

Public Member Functions
	Func (const std::string &name, const SortPtr out, const std::vector< SortPtr > &args)
	Constructor for multiple-argument function.

	~Func ()
	Default destructor.

const SortPtr	out () const
	Return the output sort.

size_t	arg_num () const
	Return the number of arguments.

const SortPtr	arg (const int &i) const
	Return the sort of the i-th argument.

bool	CheckSort (const std::vector< std::shared_ptr< Expr >> &args) const
	Check if the input arguments match the specified sort.

z3::func_decl	GetZ3FuncDecl (z3::context &ctx) const
	Return the z3 func_decl.

std::ostream &	Print (std::ostream &out) const
	Output to stream.

Public Member Functions inherited from ilang::Ast
	Ast ()
	Default constructor.

	Ast (const std::string &name)
	Constructor with name.

virtual	~Ast ()
	Default destructor.

bool	is_ast () const
	Is type Ast.

virtual bool	is_expr () const
	Is type Ast::Expr.

virtual bool	is_func () const
	Is type Ast::Func.

InstrLvlAbsPtr	host () const
	Return the hosting ILA.

void	set_host (const InstrLvlAbsPtr &host)
	Set the hosting ILA.

Public Member Functions inherited from ilang::Object
	Object ()
	Default constructor.

	Object (const std::string &name)
	Constructor with string name.

virtual	~Object ()
	Default destructor.

const Symbol &	name () const
	Get the symbol (name).

virtual bool	is_instr_lvl_abs () const
	Is type InstrLvlAbs.

virtual bool	is_instr () const
	Is type Instr.

Static Public Member Functions
static FuncPtr	New (const std::string &name, const SortPtr out=Sort::MakeBoolSort())
	Create an uninterpreted function (Func) with no input (nondet).

static FuncPtr	New (const std::string &name, const SortPtr out, const SortPtr arg0)
	Create an uninterpreted function (Func) with one input.

static FuncPtr	New (const std::string &name, const SortPtr out, const SortPtr arg0, const SortPtr arg1)
	Create an uninterpreted function (Func) with two inputs.

static FuncPtr	New (const std::string &name, const SortPtr out, const std::vector< SortPtr > &args)
	Create an uninterpreted function (Func) with multiple inputs.

Friends
std::ostream &	operator<< (std::ostream &out, const FuncPtr &f)
	Overload output stream.

Additional Inherited Members
Protected Types inherited from ilang::Ast
typedef std::shared_ptr < InstrLvlAbs >	InstrLvlAbsPtr
	Type for forward declaration of ILA.

Detailed Description

The class for uninterpreted function.

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

Public Types