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 36 of file FuncInterp.cs.

Member Function Documentation

◆ ToString()

override string ToString ( )
inline

A string representation of the function entry.

Definition at line 79 of file FuncInterp.cs.

80  {
81  uint n = NumArgs;
82  string res = "[";
83  Expr[] args = Args;
84  for (uint i = 0; i < n; i++)
85  res += args[i] + ", ";
86  return res + Value + "]";
87  }
Expr Value
Return the (symbolic) value of this entry.
Definition: FuncInterp.cs:42
Expr [] Args
The arguments of the function entry.
Definition: FuncInterp.cs:62
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:54

Property Documentation

◆ Args

Expr [] Args
get

The arguments of the function entry.

Definition at line 62 of file FuncInterp.cs.

Referenced by FuncInterp.ToString().

62  {
63  get
64  {
65  Contract.Ensures(Contract.Result<Expr[]>() != null);
66  Contract.Ensures(Contract.Result<Expr[]>().Length == this.NumArgs);
67 
68  uint n = NumArgs;
69  Expr[] res = new Expr[n];
70  for (uint i = 0; i < n; i++)
71  res[i] = Expr.Create(Context, Native.Z3_func_entry_get_arg(Context.nCtx, NativeObject, i));
72  return res;
73  }
74  }
uint NumArgs
The number of arguments of the entry.
Definition: FuncInterp.cs:54

◆ NumArgs

uint NumArgs
get

The number of arguments of the entry.

Definition at line 54 of file FuncInterp.cs.

Referenced by FuncInterp.ToString().

54  {
55  get { return Native.Z3_func_entry_get_num_args(Context.nCtx, NativeObject); }
56  }

◆ Value

Expr Value
get

Return the (symbolic) value of this entry.

Definition at line 42 of file FuncInterp.cs.

Referenced by FuncInterp.ToString().

42  {
43  get
44  {
45  Contract.Ensures(Contract.Result<Expr>() != null);
46  return Expr.Create(Context, Native.Z3_func_entry_get_value(Context.nCtx, NativeObject));
47  }
48  }