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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
|
/******************************************************************************
* 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;
import java.util.HashMap;
import java.util.Map;
public class Result extends AbstractPointer
{
// region construction and destruction
Result(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
public enum UnknownExplanation {
REQUIRES_FULL_CHECK(0),
INCOMPLETE(1),
TIMEOUT(2),
RESOURCEOUT(3),
MEMOUT(4),
INTERRUPTED(5),
NO_STATUS(6),
UNSUPPORTED(7),
OTHER(8),
UNKNOWN_REASON(9);
/* the int value of the UnknownExplanation */
private int value;
private static Map<Integer, UnknownExplanation> explanationMap = new HashMap<>();
private UnknownExplanation(int value)
{
this.value = value;
}
static
{
for (UnknownExplanation explanation : UnknownExplanation.values())
{
explanationMap.put(explanation.getValue(), explanation);
}
}
public static UnknownExplanation fromInt(int value) throws CVC5ApiException
{
if (value < REQUIRES_FULL_CHECK.value || value > UNKNOWN_REASON.value)
{
throw new CVC5ApiException("UnknownExplanation value " + value
+ " is outside the valid range [" + REQUIRES_FULL_CHECK.value + ","
+ UNKNOWN_REASON.value + "]");
}
return explanationMap.get(value);
}
public int getValue()
{
return value;
}
}
/**
* Return true if Result is empty, i.e., a nullary Result, and not an actual
* result returned from a checkSat() (and friends) query.
*/
public boolean isNull()
{
return isNull(pointer);
}
private native boolean isNull(long pointer);
/**
* Return true if query was a satisfiable checkSat() or checkSatAssuming()
* query.
*/
public boolean isSat()
{
return isSat(pointer);
}
private native boolean isSat(long pointer);
/**
* Return true if query was an unsatisfiable checkSat() or
* checkSatAssuming() query.
*/
public boolean isUnsat()
{
return isUnsat(pointer);
}
private native boolean isUnsat(long pointer);
/**
* Return true if query was a checkSat() or checkSatAssuming() query and
* cvc5 was not able to determine (un)satisfiability.
*/
public boolean isSatUnknown()
{
return isSatUnknown(pointer);
}
private native boolean isSatUnknown(long pointer);
/**
* Return true if corresponding query was an entailed checkEntailed() query.
*/
public boolean isEntailed()
{
return isEntailed(pointer);
}
private native boolean isEntailed(long pointer);
/**
* Return true if corresponding query was a checkEntailed() query that is
* not entailed.
*/
public boolean isNotEntailed()
{
return isNotEntailed(pointer);
}
private native boolean isNotEntailed(long pointer);
/**
* Return true if query was a checkEntailed() query and cvc5 was not able to
* determine if it is entailed.
*/
public boolean isEntailmentUnknown()
{
return isEntailmentUnknown(pointer);
}
private native boolean isEntailmentUnknown(long pointer);
/**
* Operator overloading for equality of two results.
* @param r the result to compare to for equality
* @return true if the results are equal
*/
@Override public boolean equals(Object r)
{
if (this == r)
return true;
if (r == null || getClass() != r.getClass())
return false;
Result result = (Result) r;
if (this.pointer == result.pointer)
{
return true;
}
return equals(pointer, result.getPointer());
}
private native boolean equals(long pointer1, long pointer2);
/**
* @return an explanation for an unknown query result.
*/
public UnknownExplanation getUnknownExplanation()
{
try
{
int explanation = getUnknownExplanation(pointer);
return UnknownExplanation.fromInt(explanation);
}
catch (CVC5ApiException e)
{
e.printStackTrace();
throw new RuntimeException(e.getMessage());
}
}
private native int getUnknownExplanation(long pointer);
/**
* @return a string representation of this result.
*/
protected native String toString(long pointer);
}
|
