diff options
Diffstat (limited to 'test/unit/api/java')
-rw-r--r-- | test/unit/api/java/DatatypeTest.java | 5 | ||||
-rw-r--r-- | test/unit/api/java/GrammarTest.java | 5 | ||||
-rw-r--r-- | test/unit/api/java/OpTest.java | 5 | ||||
-rw-r--r-- | test/unit/api/java/ResultTest.java | 5 | ||||
-rw-r--r-- | test/unit/api/java/SolverTest.java | 77 | ||||
-rw-r--r-- | test/unit/api/java/SortTest.java | 5 | ||||
-rw-r--r-- | test/unit/api/java/TermTest.java | 5 |
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"); |