Z3
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 }
static long getPattern(long a0, long a1, int a2)
Definition: Native.java:2942
static String patternToString(long a0, long a1)
Definition: Native.java:3388
static int getPatternNumTerms(long a0, long a1)
Definition: Native.java:2933
def String(name, ctx=None)
Definition: z3py.py:9443