Z3
src/api/java/Pattern.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines