dash/program/src/main/java/com/microsoft/z3/Constructor.java at master · foens/dash · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
/**
 * This file was automatically generated from Constructor.cs
 * w/ further modifications by:
 * @author Christoph M. Wintersteiger (cwinter)
 **/

package com.microsoft.z3;

/**
 * Constructors are used for datatype sorts.
 **/
public class Constructor extends Z3Object
{
	/**
	 * The number of fields of the constructor.
	 * @throws Z3Exception
	 **/
	public int getNumFields() throws Z3Exception
	{
		return n;
	}

	/**
	 * The function declaration of the constructor.
	 * @throws Z3Exception
	 **/
	public FuncDecl ConstructorDecl() throws Z3Exception
	{
	    Native.LongPtr constructor = new Native.LongPtr();
	    Native.LongPtr tester = new Native.LongPtr();
	    long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        return new FuncDecl(getContext(), constructor.value);
	}

	/**
	 * The function declaration of the tester.
	 * @throws Z3Exception
	 **/
	public FuncDecl getTesterDecl() throws Z3Exception
	{
	    Native.LongPtr constructor = new Native.LongPtr();
        Native.LongPtr tester = new Native.LongPtr();
        long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        return new FuncDecl(getContext(), tester.value);
	}

	/**
	 * The function declarations of the accessors
	 * @throws Z3Exception
	 **/
	public FuncDecl[] getAccessorDecls() throws Z3Exception
	{
	    Native.LongPtr constructor = new Native.LongPtr();
        Native.LongPtr tester = new Native.LongPtr();
        long[] accessors = new long[n];
        Native.queryConstructor(getContext().nCtx(), getNativeObject(), n, constructor, tester, accessors);
        FuncDecl[] t = new FuncDecl[n];
        for (int i = 0; i < n; i++)
            t[i] = new FuncDecl(getContext(), accessors[i]);
        return t;
	}

	/**
	 * Destructor.
	 **/
	protected void finalize() throws Z3Exception
	{
		Native.delConstructor(getContext().nCtx(), getNativeObject());
	}

	private int n = 0;

	Constructor(Context ctx, Symbol name, Symbol recognizer,
			Symbol[] fieldNames, Sort[] sorts, int[] sortRefs)
			throws Z3Exception
	{
		super(ctx);

		n = arrayLength(fieldNames);

		if (n != arrayLength(sorts))
			throw new Z3Exception(
					"Number of field names does not match number of sorts");
		if (sortRefs != null && sortRefs.length != n)
			throw new Z3Exception(
					"Number of field names does not match number of sort refs");

		if (sortRefs == null)
			sortRefs = new int[n];

		setNativeObject(Native.mkConstructor(ctx.nCtx(), name.getNativeObject(),
				recognizer.getNativeObject(), n, arrayToNative(fieldNames),
				arrayToNative(sorts), sortRefs));

	}
}