Z3 |

Constructor.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
23 public class Constructor<R> extends Z3Object {
24 private final int n;
25
26 Constructor(Context ctx, int n, long nativeObj) {
27 super(ctx, nativeObj);
28 this.n = n;
29 }
30
37 public int getNumFields()
38 {
39 return n;
40 }
41
47 public FuncDecl<DatatypeSort<R>> ConstructorDecl()
48 {
49 Native.LongPtr constructor = new Native.LongPtr();
50 Native.LongPtr tester = new Native.LongPtr();
51 long[] accessors = new long[n];
52 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
53 return new FuncDecl<>(getContext(), constructor.value);
54 }
55
61 public FuncDecl<BoolSort> getTesterDecl()
62 {
63 Native.LongPtr constructor = new Native.LongPtr();
64 Native.LongPtr tester = new Native.LongPtr();
65 long[] accessors = new long[n];
66 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
67 return new FuncDecl<>(getContext(), tester.value);
68 }
69
75 public FuncDecl<?>[] getAccessorDecls()
76 {
77 Native.LongPtr constructor = new Native.LongPtr();
78 Native.LongPtr tester = new Native.LongPtr();
79 long[] accessors = new long[n];
80 Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
81 FuncDecl<?>[] t = new FuncDecl[n];
82 for (int i = 0; i < n; i++)
83 t[i] = new FuncDecl<>(getContext(), accessors[i]);
84 return t;
85 }
86
87 @Override
88 void incRef() {
89 // Datatype constructors are not reference counted.
90 }
91
92 @Override
93 void addToReferenceQueue() {
94 getContext().getConstructorDRQ().storeReference(getContext(), this);
95 }
96
97 static <R> Constructor<R> of(Context ctx, Symbol name, Symbol recognizer,
98 Symbol[] fieldNames, Sort[] sorts, int[] sortRefs) {
99 int n = AST.arrayLength(fieldNames);
100
101 if (n != AST.arrayLength(sorts))
102 throw new Z3Exception(
103 "Number of field names does not match number of sorts");
104 if (sortRefs != null && sortRefs.length != n)
105 throw new Z3Exception(
106 "Number of field names does not match number of sort refs");
107
108 if (sortRefs == null)
109 sortRefs = new int[n];
110
111 long nativeObj = Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
112 recognizer.getNativeObject(), n, Symbol.arrayToNative(fieldNames),
113 Sort.arrayToNative(sorts), sortRefs);
114 return new Constructor<>(ctx, n, nativeObj);
115
116 }
117}
com.microsoft.z3.Constructor
Definition: Constructor.java:23
com.microsoft.z3.Constructor.getAccessorDecls
FuncDecl<?>[] getAccessorDecls()
Definition: Constructor.java:75
com.microsoft.z3.Constructor.ConstructorDecl
FuncDecl< DatatypeSort< R > > ConstructorDecl()
Definition: Constructor.java:47
com.microsoft.z3.Constructor.getTesterDecl
FuncDecl< BoolSort > getTesterDecl()
Definition: Constructor.java:61
com.microsoft.z3.Constructor.getNumFields
int getNumFields()
Definition: Constructor.java:37
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.getConstructorDRQ
IDecRefQueue< Constructor<?> > getConstructorDRQ()
Definition: Context.java:4062
com.microsoft.z3.FuncDecl
Definition: FuncDecl.java:28
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24