Z3
Pattern.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
24public 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
55 {
56 return Native.patternToString(getContext().nCtx(), getNativeObject());
57 }
58
59 Pattern(Context ctx, long obj)
60 {
61 super(ctx, obj);
62 }
63}
static int getPatternNumTerms(long a0, long a1)
Definition: Native.java:3305
static long getPattern(long a0, long a1, int a2)
Definition: Native.java:3314
static String patternToString(long a0, long a1)
Definition: Native.java:3829
def String(name, ctx=None)
Definition: z3py.py:10085