Z3
Data Structures | Public Member Functions
FuncInterp Class Reference
+ Inheritance diagram for FuncInterp:

Data Structures

class  Entry
 

Public Member Functions

int getNumEntries ()
 
Entry [] getEntries ()
 
Expr getElse ()
 
int getArity ()
 
String toString ()
 

Detailed Description

A function interpretation is represented as a finite map and an 'else' value. Each entry in the finite map represents the value of a function given a set of arguments.

Definition at line 25 of file FuncInterp.java.

Member Function Documentation

§ getArity()

int getArity ( )
inline

The arity of the function interpretation

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 143 of file FuncInterp.java.

144  {
145  return Native.funcInterpGetArity(getContext().nCtx(), getNativeObject());
146  }

§ getElse()

Expr getElse ( )
inline

The (symbolic) `else' value of the function interpretation.

Exceptions
Z3Exception
Z3Exceptionon error
Returns
an Expr

Definition at line 132 of file FuncInterp.java.

Referenced by FuncInterp.toString().

133  {
134  return Expr.create(getContext(),
135  Native.funcInterpGetElse(getContext().nCtx(), getNativeObject()));
136  }

§ getEntries()

Entry [] getEntries ( )
inline

The entries in the function interpretation

Exceptions
Z3Exception
Z3Exceptionon error

Definition at line 115 of file FuncInterp.java.

Referenced by FuncInterp.toString().

116  {
117  int n = getNumEntries();
118  Entry[] res = new Entry[n];
119  for (int i = 0; i < n; i++)
120  res[i] = new Entry(getContext(), Native.funcInterpGetEntry(getContext()
121  .nCtx(), getNativeObject(), i));
122  return res;
123  }

§ getNumEntries()

int getNumEntries ( )
inline

The number of entries in the function interpretation.

Exceptions
Z3Exceptionon error
Returns
an int

Definition at line 104 of file FuncInterp.java.

Referenced by FuncInterp.getEntries().

105  {
106  return Native.funcInterpGetNumEntries(getContext().nCtx(), getNativeObject());
107  }

§ toString()

String toString ( )
inline

A string representation of the function interpretation.

Definition at line 151 of file FuncInterp.java.

152  {
153  String res = "";
154  res += "[";
155  for (Entry e : getEntries())
156  {
157  int n = e.getNumArgs();
158  if (n > 1)
159  res += "[";
160  Expr[] args = e.getArgs();
161  for (int i = 0; i < n; i++)
162  {
163  if (i != 0)
164  res += ", ";
165  res += args[i];
166  }
167  if (n > 1)
168  res += "]";
169  res += " -> " + e.getValue() + ", ";
170  }
171  res += "else -> " + getElse();
172  res += "]";
173  return res;
174  }
def String(name, ctx=None)
Definition: z3py.py:9443