Z3
src/api/java/RelationSort.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines