00001 00018 package com.microsoft.z3; 00019 00023 public class RelationSort extends Sort 00024 { 00028 public int getArity() throws Z3Exception 00029 { 00030 return Native.getRelationArity(getContext().nCtx(), getNativeObject()); 00031 } 00032 00037 public Sort[] getColumnSorts() throws Z3Exception 00038 { 00039 00040 if (m_columnSorts != null) 00041 return m_columnSorts; 00042 00043 int n = getArity(); 00044 Sort[] res = new Sort[n]; 00045 for (int i = 0; i < n; i++) 00046 res[i] = Sort.create(getContext(), Native.getRelationColumn(getContext() 00047 .nCtx(), getNativeObject(), i)); 00048 return res; 00049 } 00050 00051 private Sort[] m_columnSorts = null; 00052 00053 RelationSort(Context ctx, long obj) throws Z3Exception 00054 { 00055 super(ctx, obj); 00056 } 00057 }