Z3 |

TupleSort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public class TupleSort extends Sort
24{
29 public FuncDecl<TupleSort> mkDecl()
30 {
31
32 return new FuncDecl<>(getContext(), Native.getTupleSortMkDecl(getContext()
33 .nCtx(), getNativeObject()));
34 }
35
39 public int getNumFields()
40 {
41 return Native.getTupleSortNumFields(getContext().nCtx(), getNativeObject());
42 }
43
48 public FuncDecl<?>[] getFieldDecls()
49 {
50
51 int n = getNumFields();
52 FuncDecl<?>[] res = new FuncDecl[n];
53 for (int i = 0; i < n; i++)
54 res[i] = new FuncDecl<>(getContext(), Native.getTupleSortFieldDecl(
55 getContext().nCtx(), getNativeObject(), i));
56 return res;
57 }
58
59 TupleSort(Context ctx, Symbol name, int numFields, Symbol[] fieldNames,
60 Sort[] fieldSorts)
61 {
62 super(ctx, Native.mkTupleSort(ctx.nCtx(), name.getNativeObject(),
63 numFields, Symbol.arrayToNative(fieldNames),
64 AST.arrayToNative(fieldSorts), new Native.LongPtr(),
65 new long[numFields]));
66 }
67};
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:4008
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.TupleSort
Definition: TupleSort.java:24
com.microsoft.z3.TupleSort.mkDecl
FuncDecl< TupleSort > mkDecl()
Definition: TupleSort.java:29
com.microsoft.z3.TupleSort.getNumFields
int getNumFields()
Definition: TupleSort.java:39
com.microsoft.z3.TupleSort.getFieldDecls
FuncDecl<?>[] getFieldDecls()
Definition: TupleSort.java:48
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73