Z3
Data Structures | Public Member Functions | Properties
FuncInterp.Entry Class Reference

An Entry object represents an element in the finite map used to encode a function interpretation. More...

+ Inheritance diagram for FuncInterp.Entry:

Data Structures

class  DecRefQueue
 

Public Member Functions

override string ToString ()
 A string representation of the function entry. More...
 
- Public Member Functions inherited from Z3Object
void Dispose ()
 Disposes of the underlying native Z3 object. More...
 

Properties

Expr Value [get]
 Return the (symbolic) value of this entry. More...
 
uint NumArgs [get]
 The number of arguments of the entry. More...
 
Expr[] Args [get]
 The arguments of the function entry. More...
 

Detailed Description

An Entry object represents an element in the finite map used to encode a function interpretation.

Definition at line 35 of file FuncInterp.cs.

Member Function Documentation

◆ ToString()

override string ToString ( )
inline

A string representation of the function entry.

Definition at line 75 of file FuncInterp.cs.

76 {
77 uint n = NumArgs;
78 string res = "[";
79 Expr[] args = Args;
80 for (uint i = 0; i < n; i++)
81 res += args[i] + ", ";
82 return res + Value + "]";
83 }
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:52
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:41
Expr[] Args
The arguments of the function entry.
Definition: FuncInterp.cs:60

Property Documentation

◆ Args

Expr [] Args
get

The arguments of the function entry.

Definition at line 59 of file FuncInterp.cs.

60 {
61 get
62 {
63
64 uint n = NumArgs;
65 Expr[] res = new Expr[n];
66 for (uint i = 0; i < n; i++)
67 res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
68 return res;
69 }
70 }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().

◆ NumArgs

uint NumArgs
get

The number of arguments of the entry.

Definition at line 51 of file FuncInterp.cs.

52 {
53 get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
54 }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().

◆ Value

Expr Value
get

Return the (symbolic) value of this entry.

Definition at line 40 of file FuncInterp.cs.

41 {
42 get
43 {
44 return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
45 }
46 }

Referenced by FuncInterp.Entry.ToString(), and FuncInterp.ToString().