00001 00018 package com.microsoft.z3; 00019 00024 public class Pattern extends AST 00025 { 00029 public int getNumTerms() throws Z3Exception 00030 { 00031 return Native.getPatternNumTerms(getContext().nCtx(), getNativeObject()); 00032 } 00033 00039 public Expr[] getTerms() throws Z3Exception 00040 { 00041 00042 int n = getNumTerms(); 00043 Expr[] res = new Expr[n]; 00044 for (int i = 0; i < n; i++) 00045 res[i] = Expr.create(getContext(), 00046 Native.getPattern(getContext().nCtx(), getNativeObject(), i)); 00047 return res; 00048 } 00049 00053 public String toString() 00054 { 00055 try 00056 { 00057 return Native.patternToString(getContext().nCtx(), getNativeObject()); 00058 } catch (Z3Exception e) 00059 { 00060 return "Z3Exception: " + e.getMessage(); 00061 } 00062 } 00063 00064 Pattern(Context ctx, long obj) throws Z3Exception 00065 { 00066 super(ctx, obj); 00067 } 00068 }