Z3
src
api
java
Pattern.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
24
public
class
Pattern
extends
AST
25
{
29
public
int
getNumTerms
()
30
{
31
return
Native.getPatternNumTerms(getContext().nCtx(), getNativeObject());
32
}
33
39
public
Expr<?>
[]
getTerms
()
40
{
41
42
int
n =
getNumTerms
();
43
Expr<?>
[] res =
new
Expr
[n];
44
for
(
int
i = 0; i < n; i++)
45
res[i] =
Expr
.create(getContext(),
46
Native.getPattern(getContext().nCtx(), getNativeObject(), i));
47
return
res;
48
}
49
53
@Override
54
public
String
toString
()
55
{
56
return
Native.patternToString(getContext().nCtx(), getNativeObject());
57
}
58
59
Pattern
(
Context
ctx,
long
obj)
60
{
61
super(ctx, obj);
62
}
63
}
com.microsoft.z3.AST
Definition:
AST.java:26
com.microsoft.z3.Context
Definition:
Context.java:36
com.microsoft.z3.Expr
Definition:
Expr.java:35
com.microsoft.z3.Pattern
Definition:
Pattern.java:25
com.microsoft.z3.Pattern.getNumTerms
int getNumTerms()
Definition:
Pattern.java:29
com.microsoft.z3.Pattern.toString
String toString()
Definition:
Pattern.java:54
com.microsoft.z3.Pattern.getTerms
Expr<?>[] getTerms()
Definition:
Pattern.java:39
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:10693
Generated on Sat Jun 4 2022 07:10:05 for Z3 by
1.9.3