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 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 
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.TupleSort.mkDecl
FuncDecl mkDecl()
Definition: TupleSort.java:29
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.Sort
Definition: Sort.java:27
com.microsoft.z3.TupleSort.getNumFields
int getNumFields()
Definition: TupleSort.java:39
com.microsoft.z3.Native.getTupleSortFieldDecl
static long getTupleSortFieldDecl(long a0, long a1, int a2)
Definition: Native.java:2758
com.microsoft.z3.Native.LongPtr
Definition: Native.java:6
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.TupleSort
Definition: TupleSort.java:24
com.microsoft.z3.Native.getTupleSortMkDecl
static long getTupleSortMkDecl(long a0, long a1)
Definition: Native.java:2740
com.microsoft.z3.Context.nCtx
long nCtx()
Definition: Context.java:3966
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.AST
Definition: AST.java:26
com.microsoft.z3.Native.mkTupleSort
static long mkTupleSort(long a0, long a1, int a2, long[] a3, long[] a4, LongPtr a5, long[] a6)
Definition: Native.java:1017
com.microsoft.z3.Native.getTupleSortNumFields
static int getTupleSortNumFields(long a0, long a1)
Definition: Native.java:2749
com.microsoft.z3.TupleSort.getFieldDecls
FuncDecl[] getFieldDecls()
Definition: TupleSort.java:48
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Z3Object.arrayToNative
static long[] arrayToNative(Z3Object[] a)
Definition: Z3Object.java:73