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.Native.getPattern
static long getPattern(long a0, long a1, int a2)
Definition:
Native.java:3316
com.microsoft.z3.Pattern.getNumTerms
int getNumTerms()
Definition:
Pattern.java:29
com.microsoft.z3.Pattern
Definition:
Pattern.java:24
com.microsoft.z3.Native.getPatternNumTerms
static int getPatternNumTerms(long a0, long a1)
Definition:
Native.java:3307
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.Expr
Definition:
Expr.java:30
com.microsoft.z3.AST
Definition:
AST.java:25
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.Native.patternToString
static String patternToString(long a0, long a1)
Definition:
Native.java:3831
com.microsoft.z3.Pattern.getTerms
Expr[] getTerms()
Definition:
Pattern.java:39
com.microsoft.z3.Pattern.toString
String toString()
Definition:
Pattern.java:54
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:10111
Generated on Sat May 9 2020 00:00:00 for Z3 by
1.8.17