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}
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Expr
Definition: Expr.java:35
com.microsoft.z3.Pattern
Definition: Pattern.java:25
com.microsoft.z3.Pattern.getNumTerms
int getNumTerms()
Definition: Pattern.java:29
com.microsoft.z3.Pattern.toString
String toString()
Definition: Pattern.java:54
com.microsoft.z3.Pattern.getTerms
Expr<?>[] getTerms()
Definition: Pattern.java:39
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693