summaryrefslogtreecommitdiff
path: root/test/unit/api/java
diff options
context:
space:
mode:
Diffstat (limited to 'test/unit/api/java')
-rw-r--r--test/unit/api/java/DatatypeTest.java5
-rw-r--r--test/unit/api/java/GrammarTest.java5
-rw-r--r--test/unit/api/java/OpTest.java5
-rw-r--r--test/unit/api/java/ResultTest.java5
-rw-r--r--test/unit/api/java/SolverTest.java77
-rw-r--r--test/unit/api/java/SortTest.java5
-rw-r--r--test/unit/api/java/TermTest.java5
7 files changed, 95 insertions, 12 deletions
diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index cd9d7ee73..fb23ea515 100644
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -33,6 +33,11 @@ class DatatypeTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void mkDatatypeSort() throws CVC5ApiException
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java
index e9b0d730c..37e1b5206 100644
--- a/test/unit/api/java/GrammarTest.java
+++ b/test/unit/api/java/GrammarTest.java
@@ -32,6 +32,11 @@ class GrammarTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void addRule()
{
Sort bool = d_solver.getBooleanSort();
diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index c63157155..9b4999211 100644
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -32,6 +32,11 @@ class OpTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void getKind() throws CVC5ApiException
{
Op x;
diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index 38e981888..59bd752ca 100644
--- a/test/unit/api/java/ResultTest.java
+++ b/test/unit/api/java/ResultTest.java
@@ -31,6 +31,11 @@ class ResultTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void isNull()
{
Result res_null = d_solver.getNullResult();
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 58b8d03aa..e61022e99 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -35,6 +35,11 @@ class SolverTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void recoverableException() throws CVC5ApiException
{
d_solver.setOption("produce-models", "true");
@@ -102,6 +107,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort));
+ slv.close();
}
@Test void mkBitVectorSort() throws CVC5ApiException
@@ -132,6 +138,7 @@ class SolverTest
DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSort(throwsDtypeSpec));
+ slv.close();
}
@Test void mkDatatypeSorts() throws CVC5ApiException
@@ -175,6 +182,7 @@ class SolverTest
assertThrows(
CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+ slv.close();
/* Note: More tests are in datatype_api_black. */
}
@@ -227,6 +235,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, slv.getIntegerSort()));
assertThrows(
CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
+ slv.close();
}
@Test void mkParamSort() throws CVC5ApiException
@@ -248,6 +257,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(
CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
+ slv.close();
}
@Test void mkRecordSort() throws CVC5ApiException
@@ -263,6 +273,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields));
+ slv.close();
}
@Test void mkSetSort() throws CVC5ApiException
@@ -272,6 +283,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkSetSort(d_solver.mkBitVectorSort(4)));
+ slv.close();
}
@Test void mkBagSort() throws CVC5ApiException
@@ -281,6 +293,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkBagSort(d_solver.mkBitVectorSort(4)));
+ slv.close();
}
@Test void mkSequenceSort() throws CVC5ApiException
@@ -290,6 +303,7 @@ class SolverTest
() -> d_solver.mkSequenceSort(d_solver.mkSequenceSort(d_solver.getIntegerSort())));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkSequenceSort(d_solver.getIntegerSort()));
+ slv.close();
}
@Test void mkUninterpretedSort() throws CVC5ApiException
@@ -316,6 +330,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(
CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
+ slv.close();
}
@Test void mkBitVector() throws CVC5ApiException
@@ -374,6 +389,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkVar(d_solver.getNullSort(), "a"));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkVar(boolSort, "x"));
+ slv.close();
}
@Test void mkBoolean() throws CVC5ApiException
@@ -422,6 +438,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
+ slv.close();
}
@Test void mkCardinalityConstraint() throws CVC5ApiException
@@ -429,13 +446,11 @@ class SolverTest
Sort su = d_solver.mkUninterpretedSort("u");
Sort si = d_solver.getIntegerSort();
assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3));
- assertThrows(
- CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
- assertThrows(
- CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
+ assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
+ assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
Solver slv = new Solver();
- assertThrows(
- CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+ assertThrows(CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+ slv.close();
}
@Test void mkEmptySet() throws CVC5ApiException
@@ -446,6 +461,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.mkEmptySet(s));
assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptySet(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> slv.mkEmptySet(s));
+ slv.close();
}
@Test void mkEmptyBag() throws CVC5ApiException
@@ -457,6 +473,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptyBag(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s));
+ slv.close();
}
@Test void mkEmptySequence() throws CVC5ApiException
@@ -466,6 +483,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.mkEmptySequence(s));
assertDoesNotThrow(() -> d_solver.mkEmptySequence(d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class, () -> slv.mkEmptySequence(s));
+ slv.close();
}
@Test void mkFalse() throws CVC5ApiException
@@ -639,6 +657,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort()));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkSepNil(d_solver.getIntegerSort()));
+ slv.close();
}
@Test void mkString()
@@ -704,6 +723,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v2));
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v3));
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(DISTINCT, v6));
+ slv.close();
}
@Test void mkTermFromOp() throws CVC5ApiException
@@ -804,6 +824,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v2));
assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v3));
assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm2, v4));
+ slv.close();
}
@Test void mkTrue()
@@ -844,6 +865,7 @@ class SolverTest
()
-> slv.mkTuple(new Sort[] {slv.mkBitVectorSort(3)},
new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+ slv.close();
}
@Test void mkUniverseSet()
@@ -852,6 +874,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort()));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkUniverseSet(d_solver.getBooleanSort()));
+ slv.close();
}
@Test void mkConst()
@@ -870,6 +893,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort));
+ slv.close();
}
@Test void mkConstArray()
@@ -892,6 +916,7 @@ class SolverTest
Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort2, zero));
assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort, zero2));
+ slv.close();
}
@Test void declareDatatype()
@@ -914,6 +939,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1));
+ slv.close();
}
@Test void declareFun() throws CVC5ApiException
@@ -932,6 +958,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort));
+ slv.close();
}
@Test void declareSort()
@@ -974,7 +1001,7 @@ class SolverTest
assertThrows(
CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v2));
assertThrows(
- CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v2));
+ CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort, v2));
// b3 has function sort, which is allowed as an argument
assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1));
@@ -994,6 +1021,7 @@ class SolverTest
CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort, v12));
assertThrows(
CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort2, v1));
+ slv.close();
}
@Test void defineFunGlobal()
@@ -1074,6 +1102,7 @@ class SolverTest
assertThrows(
CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1));
+ slv.close();
}
@Test void defineFunRecWrongLogic() throws CVC5ApiException
@@ -1201,6 +1230,7 @@ class SolverTest
()
-> slv.defineFunsRec(
new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2}));
+ slv.close();
}
@Test void defineFunsRecWrongLogic() throws CVC5ApiException
@@ -1581,6 +1611,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
+ slv.close();
}
@Test void getModelDomainElements()
@@ -1680,10 +1711,12 @@ class SolverTest
d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
assertThrows(
CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm()));
- assertThrows(CVC5ApiException.class,
- () -> d_solver.getQuantifierElimination(new Solver().mkBoolean(false)));
+ Solver slv = new Solver();
+ assertThrows(
+ CVC5ApiException.class, () -> d_solver.getQuantifierElimination(slv.mkBoolean(false)));
assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall));
+ slv.close();
}
@Test void getQuantifierEliminationDisjunct()
@@ -1695,10 +1728,12 @@ class SolverTest
assertThrows(CVC5ApiException.class,
() -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));
+ Solver slv = new Solver();
assertThrows(CVC5ApiException.class,
- () -> d_solver.getQuantifierEliminationDisjunct(new Solver().mkBoolean(false)));
+ () -> d_solver.getQuantifierEliminationDisjunct(slv.mkBoolean(false)));
assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall));
+ slv.close();
}
@Test void declareSeparationHeap() throws CVC5ApiException
@@ -1910,8 +1945,10 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {}));
assertThrows(CVC5ApiException.class,
() -> d_solver.blockModelValues(new Term[] {d_solver.getNullTerm()}));
- assertThrows(CVC5ApiException.class,
- () -> d_solver.blockModelValues(new Term[] {new Solver().mkBoolean(false)}));
+ Solver slv = new Solver();
+ assertThrows(
+ CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {slv.mkBoolean(false)}));
+ slv.close();
}
@Test void blockModelValues2() throws CVC5ApiException
@@ -2049,6 +2086,7 @@ class SolverTest
d_solver.defineFunsRec(new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b3}}, new Term[] {v1, v2});
assertDoesNotThrow(() -> d_solver.simplify(f1));
assertDoesNotThrow(() -> d_solver.simplify(f2));
+ slv.close();
}
@Test void assertFormula()
@@ -2057,6 +2095,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm()));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.assertFormula(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkEntailed()
@@ -2066,6 +2105,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue()));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkEntailed1()
@@ -2081,6 +2121,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.checkEntailed(z));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkEntailed2()
@@ -2131,6 +2172,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkSat() throws CVC5ApiException
@@ -2147,6 +2189,7 @@ class SolverTest
assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.mkTrue()));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkSatAssuming1() throws CVC5ApiException
@@ -2162,6 +2205,7 @@ class SolverTest
assertDoesNotThrow(() -> d_solver.checkSatAssuming(z));
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+ slv.close();
}
@Test void checkSatAssuming2() throws CVC5ApiException
@@ -2212,6 +2256,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+ slv.close();
}
@Test void setLogic() throws CVC5ApiException
@@ -2261,6 +2306,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort));
+ slv.close();
}
@Test void mkSygusGrammar() throws CVC5ApiException
@@ -2291,6 +2337,7 @@ class SolverTest
() -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
assertThrows(CVC5ApiException.class,
() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
+ slv.close();
}
@Test void synthFun() throws CVC5ApiException
@@ -2328,6 +2375,7 @@ class SolverTest
CVC5ApiException.class, () -> slv.synthFun("", new Term[] {}, d_solver.getBooleanSort()));
assertThrows(CVC5ApiException.class,
() -> slv.synthFun("f1", new Term[] {x}, d_solver.getBooleanSort()));
+ slv.close();
}
@Test void synthInv() throws CVC5ApiException
@@ -2367,6 +2415,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
+ slv.close();
}
@Test void addSygusAssume()
@@ -2381,6 +2430,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm));
+ slv.close();
}
@Test void addSygusInvConstraint() throws CVC5ApiException
@@ -2445,6 +2495,7 @@ class SolverTest
CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22));
assertThrows(
CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post));
+ slv.close();
}
@Test void getSynthSolution() throws CVC5ApiException
@@ -2468,6 +2519,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f));
+ slv.close();
}
@Test void getSynthSolutions() throws CVC5ApiException
@@ -2493,6 +2545,7 @@ class SolverTest
Solver slv = new Solver();
assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
+ slv.close();
}
@Test void tupleProject() throws CVC5ApiException
diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 6649e5de0..977ba483e 100644
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -36,6 +36,11 @@ class SortTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
Sort create_datatype_sort() throws CVC5ApiException
{
DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index cb59849e0..94f35e97f 100644
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -39,6 +39,11 @@ class TermTest
d_solver = new Solver();
}
+ @AfterEach void tearDown()
+ {
+ d_solver.close();
+ }
+
@Test void eq()
{
Sort uSort = d_solver.mkUninterpretedSort("u");
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback