ilang  0.9.1
ILAng: A Modeling and Verification Platform for SoCs
Public Types | Public Member Functions | Static Public Member Functions | Friends | List of all members
ilang::Func Class Reference

The class for uninterpreted function. More...

#include <func.h>

Inheritance diagram for ilang::Func:
ilang::Ast ilang::Object

Public Types

typedef std::shared_ptr< FuncFuncPtr
 Pointer type for normal use of Func.
 
- Public Types inherited from ilang::Ast
typedef std::shared_ptr< InstrLvlAbsInstrLvlAbsPtr
 Type for forward declaration of ILA.
 
- Public Types inherited from ilang::Object
typedef std::shared_ptr< ObjectObjPtr
 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 (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 Symbolname () 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.
 

Detailed Description

The class for uninterpreted function.


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