blob: bf908aff2e1f157170464dadddb43d4b87a93fe2 (
plain)
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
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
|
/******************************************************************************
* Top contributors (to current version):
* Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed, Mudathir Mohamed
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* The cvc5 java API.
*/
package cvc5;
public class Op extends AbstractPointer
{
// region construction and destruction
Op(Solver solver, long pointer)
{
super(solver, pointer);
}
protected static native void deletePointer(long pointer);
public long getPointer()
{
return pointer;
}
@Override public void finalize()
{
deletePointer(pointer);
}
// endregion
/**
* Syntactic equality operator.
* Return true if both operators are syntactically identical.
* Both operators must belong to the same solver object.
* @param t the operator to compare to for equality
* @return true if the operators are equal
*/
@Override public boolean equals(Object t)
{
if (this == t)
return true;
if (t == null || getClass() != t.getClass())
return false;
return equals(pointer, ((Op) t).getPointer());
}
private native boolean equals(long pointer1, long pointer2);
/**
* @return the kind of this operator
*/
public Kind getKind()
{
try
{
int value = getKind(pointer);
return Kind.fromInt(value);
}
catch (CVC5ApiException e)
{
e.printStackTrace();
throw new RuntimeException(e.getMessage());
}
}
private native int getKind(long pointer);
/**
* @return true if this operator is a null term
*/
public boolean isNull()
{
return isNull(pointer);
}
private native boolean isNull(long pointer);
/**
* @return true iff this operator is indexed
*/
public boolean isIndexed()
{
return isIndexed(pointer);
}
private native boolean isIndexed(long pointer);
/**
* @return the number of indices of this op
*/
public int getNumIndices()
{
return getNumIndices(pointer);
}
private native int getNumIndices(long pointer);
/**
* Get the indices used to create this Op.
* Check the Op Kind with getKind() to determine which argument to use.
*
* @return the indices used to create this Op
*/
public int[] getIntegerIndices()
{
return getIntegerIndices(pointer);
}
private native int[] getIntegerIndices(long pointer);
/**
* Get the indices used to create this Op.
* Check the Op Kind with getKind() to determine which argument to use.
*
* @return the indices used to create this Op
*/
public String[] getStringIndices()
{
return getStringIndices(pointer);
}
private native String[] getStringIndices(long pointer);
/**
* @return a string representation of this operator
*/
protected native String toString(long pointer);
}
|
