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  public String toString()
54  {
55  try
56  {
57  return Native.patternToString(getContext().nCtx(), getNativeObject());
58  } catch (Z3Exception e)
59  {
60  return "Z3Exception: " + e.getMessage();
61  }
62  }
63 
64  Pattern(Context ctx, long obj)
65  {
66  super(ctx, obj);
67  }
68 }
static long getPattern(long a0, long a1, int a2)
Definition: Native.java:2675
static String patternToString(long a0, long a1)
Definition: Native.java:3121
static int getPatternNumTerms(long a0, long a1)
Definition: Native.java:2666