Z3 |

RelationSort.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public class RelationSort extends Sort
24{
28 public int getArity()
29 {
30 return Native.getRelationArity(getContext().nCtx(), getNativeObject());
31 }
32
37 public Sort[] getColumnSorts()
38 {
39
40 if (m_columnSorts != null)
41 return m_columnSorts;
42
43 int n = getArity();
44 Sort[] res = new Sort[n];
45 for (int i = 0; i < n; i++)
46 res[i] = Sort.create(getContext(), Native.getRelationColumn(getContext()
47 .nCtx(), getNativeObject(), i));
48 return res;
49 }
50
51 private Sort[] m_columnSorts = null;
52
53 RelationSort(Context ctx, long obj)
54 {
55 super(ctx, obj);
56 }
57}
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.RelationSort
Definition: RelationSort.java:24
com.microsoft.z3.RelationSort.getColumnSorts
Sort[] getColumnSorts()
Definition: RelationSort.java:37
com.microsoft.z3.RelationSort.getArity
int getArity()
Definition: RelationSort.java:28
com.microsoft.z3.Sort
Definition: Sort.java:27