From c56a361253836f38e275651165a957664c7e126a Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 30 Mar 2022 16:58:08 -0500 Subject: [PATCH] Patch cross reference in Kind.java documentation (#8458) This PR patches cross reference links in Kind.java comments for now until a proper way is implemented that handles documentation for cpp, python and Java API. --- .clang-format | 2 +- src/api/cpp/cvc5_kind.h | 6 +- src/api/java/genenums.py.in | 38 +- .../io/github/cvc5/api/AbstractPointer.java | 3 +- src/api/java/io/github/cvc5/api/Datatype.java | 9 +- .../github/cvc5/api/DatatypeConstructor.java | 9 +- src/api/java/io/github/cvc5/api/Op.java | 3 +- src/api/java/io/github/cvc5/api/Pair.java | 3 +- src/api/java/io/github/cvc5/api/Result.java | 3 +- src/api/java/io/github/cvc5/api/Solver.java | 11 +- src/api/java/io/github/cvc5/api/Sort.java | 6 +- .../java/io/github/cvc5/api/Statistics.java | 9 +- src/api/java/io/github/cvc5/api/Term.java | 15 +- src/api/java/io/github/cvc5/api/Triplet.java | 3 +- test/unit/api/java/DatatypeTest.java | 30 +- test/unit/api/java/GrammarTest.java | 18 +- test/unit/api/java/OpTest.java | 24 +- test/unit/api/java/ResultTest.java | 21 +- test/unit/api/java/SolverTest.java | 462 ++++++++++++------ test/unit/api/java/SortTest.java | 153 ++++-- test/unit/api/java/SynthResultTest.java | 18 +- test/unit/api/java/TermTest.java | 111 +++-- 22 files changed, 645 insertions(+), 312 deletions(-) diff --git a/.clang-format b/.clang-format index b240da02a..7e4ae214e 100644 --- a/.clang-format +++ b/.clang-format @@ -24,7 +24,7 @@ AllowShortCaseLabelsOnASingleLine: true BinPackArguments: false BinPackParameters: false BreakBeforeBinaryOperators: NonAssignment -BreakAfterJavaFieldAnnotations: false +BreakAfterJavaFieldAnnotations: true BraceWrapping: AfterCaseLabel: true AfterObjCDeclaration: true diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 161241466..8f3d65744 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -1514,7 +1514,7 @@ enum Kind : int32_t * RoundingMode constant. * * - Create Term of this Kind with: - * - Solver::mkRoundingMode(RoundingMode rm) const + * - Solver::mkRoundingMode(RoundingMode) const */ CONST_ROUNDINGMODE, /** @@ -2797,8 +2797,8 @@ enum Kind : int32_t * - 1..2: Terms of bag sort (Bag E), [1] an element of sort E * * Create with: - * - Solver::mkTerm(Kind kind, const Term& child1, const Term& child2) const - * - Solver::mkTerm(Kind kind, const std::vector& children) const + * - Solver::mkTerm(Kind, const Term&, const Term&) const + * - Solver::mkTerm(Kind, const std::vector&) const */ BAG_COUNT, /** diff --git a/src/api/java/genenums.py.in b/src/api/java/genenums.py.in index 74e1c4e3f..b9d4a3026 100644 --- a/src/api/java/genenums.py.in +++ b/src/api/java/genenums.py.in @@ -103,8 +103,22 @@ CPP_JAVA_MAPPING = \ r"\buint64_t\b": "long", r"\bunsigned char\b": "byte", r"cvc5::": "cvc5.", - r"Term::Term\(\)": "Solver.getNullTerm()", - r"Solver::": "Solver.", + r"Term::Term\(\)": "{@link Solver#getNullTerm()", + r"Term::": "{@link Term#", + r"Solver::": "{@link Solver#", + r"Datatype::": "{@link Datatype#", + r"DatatypeConstructor::": "{@link DatatypeConstructor#", + r"DatatypeConstructorDecl::": "{@link DatatypeConstructorDecl#", + r"DatatypeDecl::": "{@link DatatypeDecl#", + r"DatatypeSelector::": "{@link DatatypeSelector#", + r"Grammar::": "{@link Grammar#", + r"Op::": "{@link Op#", + r"OptionInfo::": "{@link OptionInfo#", + r"Result::": "{@link Result#", + r"Sort::": "{@link Sort#", + r"Stat::": "{@link Stat#", + r"Statistics::": "{@link Statistics#", + r"SynthResult::": "{@link SynthResult#", r"std::vector": "int[]", r"std::vector": "Term[]", r"std::string": "String", @@ -122,7 +136,25 @@ CPP_JAVA_MAPPING = \ def format_comment(comment): for pattern, replacement in CPP_JAVA_MAPPING.items(): comment = re.sub(pattern, replacement, comment) - return """ /**\n{}\n */""".format(textwrap.indent(comment, ' * ')) + comment = """ /**\n{}\n */""".format(textwrap.indent(comment, ' * ')) + + # e.g. {@link Solver#mkBitVector(int, long) becomes {@link Solver#mkBitVector(int,long)} + def close_link(match): + link = match.group() + link = link.replace(" ", "") + link = link.replace("@link", "@link ") + if "}" in link: + return link + return "{0}}} ".format(link) + + # e.g. {@link Solver#mkBitVector(int, long) + function_pattern = re.compile(r"{@link (.*?\))") + comment = re.sub(function_pattern, close_link, comment) + # e.g. {@link BigInteger#Ten + field_pattern = re.compile(r"{@link [a-zA-Z.#]*\s") + comment = re.sub(field_pattern, close_link, comment) + comment = comment.replace("- {@link Solver#mkString(std.wstring)}", "") + return comment # Files generation diff --git a/src/api/java/io/github/cvc5/api/AbstractPointer.java b/src/api/java/io/github/cvc5/api/AbstractPointer.java index c627dcf84..11c00e7fb 100644 --- a/src/api/java/io/github/cvc5/api/AbstractPointer.java +++ b/src/api/java/io/github/cvc5/api/AbstractPointer.java @@ -41,7 +41,8 @@ abstract class AbstractPointer implements IPointer return solver; } - @Override public String toString() + @Override + public String toString() { return toString(pointer); } diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index 6fdaaac37..bb6c32ea9 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -213,12 +213,14 @@ public class Datatype extends AbstractPointer implements Iterable= size - 1) { @@ -230,7 +232,8 @@ public class Datatype extends AbstractPointer implements Iterable iterator() + @Override + public Iterator iterator() { return new ConstIterator(); } diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java index bd8b7d163..e84a63ef1 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java @@ -174,12 +174,14 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable= size - 1) { @@ -191,7 +193,8 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable iterator() + @Override + public Iterator iterator() { return new ConstIterator(); } diff --git a/src/api/java/io/github/cvc5/api/Op.java b/src/api/java/io/github/cvc5/api/Op.java index 87d85c963..1dc894251 100644 --- a/src/api/java/io/github/cvc5/api/Op.java +++ b/src/api/java/io/github/cvc5/api/Op.java @@ -39,7 +39,8 @@ public class Op extends AbstractPointer * @param t the operator to compare to for equality * @return true if the operators are equal */ - @Override public boolean equals(Object t) + @Override + public boolean equals(Object t) { if (this == t) return true; diff --git a/src/api/java/io/github/cvc5/api/Pair.java b/src/api/java/io/github/cvc5/api/Pair.java index 307273e5e..948bf92ec 100644 --- a/src/api/java/io/github/cvc5/api/Pair.java +++ b/src/api/java/io/github/cvc5/api/Pair.java @@ -25,7 +25,8 @@ public class Pair this.second = second; } - @Override public boolean equals(Object pair) + @Override + public boolean equals(Object pair) { if (this == pair) return true; diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java index d9361e51c..1dea116ac 100644 --- a/src/api/java/io/github/cvc5/api/Result.java +++ b/src/api/java/io/github/cvc5/api/Result.java @@ -84,7 +84,8 @@ public class Result extends AbstractPointer * @param r the result to compare to for equality * @return true if the results are equal */ - @Override public boolean equals(Object r) + @Override + public boolean equals(Object r) { if (this == r) return true; diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index b959cd0da..acfd0cd99 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -43,7 +43,8 @@ public class Solver implements IPointer, AutoCloseable // store pointers for terms, sorts, etc List abstractPointers = new ArrayList<>(); - @Override public void close() + @Override + public void close() { // delete heap memory for terms, sorts, etc for (int i = abstractPointers.size() - 1; i >= 0; i--) @@ -712,7 +713,7 @@ public class Solver implements IPointer, AutoCloseable * Create operator of kind: * - RECORD_UPDATE * - DIVISIBLE (to support arbitrary precision integers) - * See enum Kind for a description of the parameters. + * See enum {@link Kind} for a description of the parameters. * @param kind the kind of the operator * @param arg the string argument to this operator */ @@ -738,7 +739,7 @@ public class Solver implements IPointer, AutoCloseable * - FLOATINGPOINT_TO_SBV * - FLOATINGPOINT_TO_SBV_TOTAL * - TUPLE_UPDATE - * See enum Kind for a description of the parameters. + * See enum {@link Kind} for a description of the parameters. * @param kind the kind of the operator * @param arg the unsigned int argument to this operator * @throws CVC5ApiException @@ -760,7 +761,7 @@ public class Solver implements IPointer, AutoCloseable * - FLOATINGPOINT_TO_FP_FROM_REAL * - FLOATINGPOINT_TO_FP_FROM_SBV * - FLOATINGPOINT_TO_FP_FROM_UBV - * See enum Kind for a description of the parameters. + * See enum {@link Kind} for a description of the parameters. * @param kind the kind of the operator * @param arg1 the first unsigned int argument to this operator * @param arg2 the second unsigned int argument to this operator @@ -779,7 +780,7 @@ public class Solver implements IPointer, AutoCloseable /** * Create operator of Kind: * - TUPLE_PROJECT - * See enum Kind for a description of the parameters. + * See enum {@link Kind} for a description of the parameters. * @param kind the kind of the operator * @param args the arguments (indices) of the operator * @throws CVC5ApiException diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 9f4cd1c9e..51c90116a 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -39,7 +39,8 @@ public class Sort extends AbstractPointer implements Comparable * @param s the sort to compare to * @return true if the sorts are equal */ - @Override public boolean equals(Object s) + @Override + public boolean equals(Object s) { if (this == s) return true; @@ -62,7 +63,8 @@ public class Sort extends AbstractPointer implements Comparable * @return a negative integer, zero, or a positive integer as this sort * is less than, equal to, or greater than the specified sort. */ - @Override public int compareTo(Sort s) + @Override + public int compareTo(Sort s) { return this.compareTo(pointer, s.getPointer()); } diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java index cf8a2c704..5810480de 100644 --- a/src/api/java/io/github/cvc5/api/Statistics.java +++ b/src/api/java/io/github/cvc5/api/Statistics.java @@ -90,12 +90,14 @@ public class Statistics extends AbstractPointer implements Iterable next() + @Override + public Map.Entry next() { try { @@ -115,7 +117,8 @@ public class Statistics extends AbstractPointer implements Iterable, Iterable< * @param t the term to compare to for equality * @return true if the terms are equal */ - @Override public boolean equals(Object t) + @Override + public boolean equals(Object t) { if (this == t) return true; @@ -71,7 +72,8 @@ public class Term extends AbstractPointer implements Comparable, Iterable< * @return a negative integer, zero, or a positive integer as this term * is less than, equal to, or greater than the specified term. */ - @Override public int compareTo(Term t) + @Override + public int compareTo(Term t) { return this.compareTo(pointer, t.getPointer()); } @@ -716,12 +718,14 @@ public class Term extends AbstractPointer implements Comparable, Iterable< size = getNumChildren(); } - @Override public boolean hasNext() + @Override + public boolean hasNext() { return currentIndex < size - 1; } - @Override public Term next() + @Override + public Term next() { if (currentIndex >= size - 1) { @@ -740,7 +744,8 @@ public class Term extends AbstractPointer implements Comparable, Iterable< } } - @Override public Iterator iterator() + @Override + public Iterator iterator() { return new ConstIterator(); } diff --git a/src/api/java/io/github/cvc5/api/Triplet.java b/src/api/java/io/github/cvc5/api/Triplet.java index 1b98ac416..170d81cfb 100644 --- a/src/api/java/io/github/cvc5/api/Triplet.java +++ b/src/api/java/io/github/cvc5/api/Triplet.java @@ -27,7 +27,8 @@ public class Triplet this.third = third; } - @Override public boolean equals(Object object) + @Override + public boolean equals(Object object) { if (this == object) return true; diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index aeea03d56..ad179fb9f 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -28,17 +28,20 @@ class DatatypeTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void mkDatatypeSort() throws CVC5ApiException + @Test + void mkDatatypeSort() throws CVC5ApiException { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); @@ -55,7 +58,8 @@ class DatatypeTest assertDoesNotThrow(() -> nilConstr.getConstructorTerm()); } - @Test void mkDatatypeSorts() throws CVC5ApiException + @Test + void mkDatatypeSorts() throws CVC5ApiException { /* Create two mutual datatypes corresponding to this definition * block: @@ -122,7 +126,8 @@ class DatatypeTest assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(dtdeclsBad)); } - @Test void datatypeStructs() throws CVC5ApiException + @Test + void datatypeStructs() throws CVC5ApiException { Sort intSort = d_solver.getIntegerSort(); Sort boolSort = d_solver.getBooleanSort(); @@ -194,7 +199,8 @@ class DatatypeTest assertTrue(dtRecord.isWellFounded()); } - @Test void datatypeNames() throws CVC5ApiException + @Test + void datatypeNames() throws CVC5ApiException { Sort intSort = d_solver.getIntegerSort(); @@ -231,7 +237,8 @@ class DatatypeTest assertThrows(CVC5ApiException.class, () -> d_solver.getNullDatatypeDecl().getName()); } - @Test void parametricDatatype() throws CVC5ApiException + @Test + void parametricDatatype() throws CVC5ApiException { List v = new ArrayList<>(); Sort t1 = d_solver.mkParamSort("T1"); @@ -276,7 +283,8 @@ class DatatypeTest assertNotEquals(pairIntReal, pairRealInt); } - @Test void datatypeIsFinite() throws CVC5ApiException + @Test + void datatypeIsFinite() throws CVC5ApiException { List v = new ArrayList<>(); DatatypeDecl dtypedecl = d_solver.mkDatatypeDecl("dt", v); @@ -296,7 +304,8 @@ class DatatypeTest assertThrows(CVC5ApiException.class, () -> pdtype.getDatatype().isFinite()); } - @Test void datatypeSimplyRec() throws CVC5ApiException + @Test + void datatypeSimplyRec() throws CVC5ApiException { /* Create mutual datatypes corresponding to this definition block: * @@ -495,7 +504,8 @@ class DatatypeTest assertTrue(dtsorts.get(0).getDatatype().isWellFounded()); } - @Test void datatypeSpecializedCons() throws CVC5ApiException + @Test + void datatypeSpecializedCons() throws CVC5ApiException { /* Create mutual datatypes corresponding to this definition block: * DATATYPE diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java index 15d978692..65c1d56c9 100644 --- a/test/unit/api/java/GrammarTest.java +++ b/test/unit/api/java/GrammarTest.java @@ -27,17 +27,20 @@ class GrammarTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void addRule() + @Test + void addRule() { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); @@ -62,7 +65,8 @@ class GrammarTest assertThrows(CVC5ApiException.class, () -> g.addRule(start, d_solver.mkBoolean(false))); } - @Test void addRules() + @Test + void addRules() { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); @@ -91,7 +95,8 @@ class GrammarTest CVC5ApiException.class, () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)})); } - @Test void addAnyConstant() + @Test + void addAnyConstant() { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); @@ -113,7 +118,8 @@ class GrammarTest assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start)); } - @Test void addAnyVariable() + @Test + void addAnyVariable() { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 4cca6e711..367b00864 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -30,24 +30,28 @@ class OpTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void getKind() throws CVC5ApiException + @Test + void getKind() throws CVC5ApiException { Op x; x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1); assertDoesNotThrow(() -> x.getKind()); } - @Test void isNull() throws CVC5ApiException + @Test + void isNull() throws CVC5ApiException { Op x = d_solver.getNullOp(); assertTrue(x.isNull()); @@ -55,13 +59,15 @@ class OpTest assertFalse(x.isNull()); } - @Test void opFromKind() + @Test + void opFromKind() { assertDoesNotThrow(() -> d_solver.mkOp(ADD)); assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT)); } - @Test void getNumIndices() throws CVC5ApiException + @Test + void getNumIndices() throws CVC5ApiException { // Operators with 0 indices Op plus = d_solver.mkOp(ADD); @@ -114,7 +120,8 @@ class OpTest assertEquals(6, tupleProject.getNumIndices()); } - @Test void opSubscriptOperator() throws CVC5ApiException + @Test + void opSubscriptOperator() throws CVC5ApiException { // Operators with 0 indices Op plus = d_solver.mkOp(ADD); @@ -177,7 +184,8 @@ class OpTest } } - @Test void opScopingToString() throws CVC5ApiException + @Test + void opScopingToString() throws CVC5ApiException { Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5); String op_repr = bitvector_repeat_ot.toString(); diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index ffe1ee412..4ac75bcfa 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -26,17 +26,20 @@ class ResultTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void isNull() + @Test + void isNull() { Result res_null = d_solver.getNullResult(); assertTrue(res_null.isNull()); @@ -50,7 +53,8 @@ class ResultTest assertFalse(res.isNull()); } - @Test void eq() + @Test + void eq() { Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(u_sort, "x"); @@ -63,7 +67,8 @@ class ResultTest assertEquals(res3, res2); } - @Test void isSat() + @Test + void isSat() { Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(u_sort, "x"); @@ -73,7 +78,8 @@ class ResultTest assertFalse(res.isUnknown()); } - @Test void isUnsat() + @Test + void isUnsat() { Sort u_sort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkConst(u_sort, "x"); @@ -83,7 +89,8 @@ class ResultTest assertFalse(res.isUnknown()); } - @Test void isUnknown() throws CVC5ApiException + @Test + void isUnknown() throws CVC5ApiException { d_solver.setLogic("QF_NIA"); d_solver.setOption("incremental", "false"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 213979e62..7bcbb1af8 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -30,17 +30,20 @@ class SolverTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void recoverableException() throws CVC5ApiException + @Test + void recoverableException() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); @@ -48,47 +51,56 @@ class SolverTest assertThrows(CVC5ApiRecoverableException.class, () -> d_solver.getValue(x)); } - @Test void supportsFloatingPoint() throws CVC5ApiException + @Test + void supportsFloatingPoint() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN)); } - @Test void getBooleanSort() throws CVC5ApiException + @Test + void getBooleanSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getBooleanSort()); } - @Test void getIntegerSort() + @Test + void getIntegerSort() { assertDoesNotThrow(() -> d_solver.getIntegerSort()); } - @Test void getNullSort() throws CVC5ApiException + @Test + void getNullSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getNullSort()); } - @Test void getRealSort() throws CVC5ApiException + @Test + void getRealSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getRealSort()); } - @Test void getRegExpSort() throws CVC5ApiException + @Test + void getRegExpSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getRegExpSort()); } - @Test void getStringSort() throws CVC5ApiException + @Test + void getStringSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getStringSort()); } - @Test void getRoundingModeSort() throws CVC5ApiException + @Test + void getRoundingModeSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.getRoundingModeSort()); } - @Test void mkArraySort() throws CVC5ApiException + @Test + void mkArraySort() throws CVC5ApiException { Sort boolSort = d_solver.getBooleanSort(); Sort intSort = d_solver.getIntegerSort(); @@ -110,20 +122,23 @@ class SolverTest slv.close(); } - @Test void mkBitVectorSort() throws CVC5ApiException + @Test + void mkBitVectorSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkBitVectorSort(32)); assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVectorSort(0)); } - @Test void mkFloatingPointSort() throws CVC5ApiException + @Test + void mkFloatingPointSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkFloatingPointSort(4, 8)); assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPointSort(0, 8)); assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPointSort(4, 0)); } - @Test void mkDatatypeSort() throws CVC5ApiException + @Test + void mkDatatypeSort() throws CVC5ApiException { DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons"); @@ -141,7 +156,8 @@ class SolverTest slv.close(); } - @Test void mkDatatypeSorts() throws CVC5ApiException + @Test + void mkDatatypeSorts() throws CVC5ApiException { Solver slv = new Solver(); @@ -209,7 +225,8 @@ class SolverTest /* Note: More tests are in datatype_api_black. */ } - @Test void mkFunctionSort() throws CVC5ApiException + @Test + void mkFunctionSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkFunctionSort( @@ -260,13 +277,15 @@ class SolverTest slv.close(); } - @Test void mkParamSort() throws CVC5ApiException + @Test + void mkParamSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkParamSort("T")); assertDoesNotThrow(() -> d_solver.mkParamSort("")); } - @Test void mkPredicateSort() + @Test + void mkPredicateSort() { assertDoesNotThrow(() -> d_solver.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()})); assertThrows(CVC5ApiException.class, () -> d_solver.mkPredicateSort(new Sort[] {})); @@ -282,7 +301,8 @@ class SolverTest slv.close(); } - @Test void mkRecordSort() throws CVC5ApiException + @Test + void mkRecordSort() throws CVC5ApiException { Pair[] fields = new Pair[] {new Pair<>("b", d_solver.getBooleanSort()), new Pair<>("bv", d_solver.mkBitVectorSort(8)), @@ -298,7 +318,8 @@ class SolverTest slv.close(); } - @Test void mkSetSort() throws CVC5ApiException + @Test + void mkSetSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getBooleanSort())); assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getIntegerSort())); @@ -308,7 +329,8 @@ class SolverTest slv.close(); } - @Test void mkBagSort() throws CVC5ApiException + @Test + void mkBagSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getBooleanSort())); assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getIntegerSort())); @@ -318,7 +340,8 @@ class SolverTest slv.close(); } - @Test void mkSequenceSort() throws CVC5ApiException + @Test + void mkSequenceSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkSequenceSort(d_solver.getBooleanSort())); assertDoesNotThrow( @@ -328,13 +351,15 @@ class SolverTest slv.close(); } - @Test void mkUninterpretedSort() throws CVC5ApiException + @Test + void mkUninterpretedSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("u")); assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("")); } - @Test void mkUnresolvedSort() throws CVC5ApiException + @Test + void mkUnresolvedSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u")); assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("u", 1)); @@ -342,14 +367,16 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkUnresolvedSort("", 1)); } - @Test void mkUninterpretedSortConstructorSort() throws CVC5ApiException + @Test + void mkUninterpretedSortConstructorSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("s", 2)); assertDoesNotThrow(() -> d_solver.mkUninterpretedSortConstructorSort("", 2)); assertThrows(CVC5ApiException.class, () -> d_solver.mkUninterpretedSortConstructorSort("", 0)); } - @Test void mkTupleSort() throws CVC5ApiException + @Test + void mkTupleSort() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort()})); Sort funSort = @@ -363,7 +390,8 @@ class SolverTest slv.close(); } - @Test void mkBitVector() throws CVC5ApiException + @Test + void mkBitVector() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkBitVector(8, 2)); assertDoesNotThrow(() -> d_solver.mkBitVector(32, 2)); @@ -406,7 +434,8 @@ class SolverTest assertEquals(d_solver.mkBitVector(8, "-1", 10), d_solver.mkBitVector(8, "FF", 16)); } - @Test void mkVar() throws CVC5ApiException + @Test + void mkVar() throws CVC5ApiException { Sort boolSort = d_solver.getBooleanSort(); Sort intSort = d_solver.getIntegerSort(); @@ -422,13 +451,15 @@ class SolverTest slv.close(); } - @Test void mkBoolean() throws CVC5ApiException + @Test + void mkBoolean() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkBoolean(true)); assertDoesNotThrow(() -> d_solver.mkBoolean(false)); } - @Test void mkRoundingMode() throws CVC5ApiException + @Test + void mkRoundingMode() throws CVC5ApiException { assertEquals(d_solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN).toString(), "roundNearestTiesToEven"); @@ -442,7 +473,8 @@ class SolverTest "roundNearestTiesToAway"); } - @Test void mkFloatingPoint() throws CVC5ApiException + @Test + void mkFloatingPoint() throws CVC5ApiException { Term t1 = d_solver.mkBitVector(8); Term t2 = d_solver.mkBitVector(4); @@ -461,7 +493,8 @@ class SolverTest slv.close(); } - @Test void mkCardinalityConstraint() throws CVC5ApiException + @Test + void mkCardinalityConstraint() throws CVC5ApiException { Sort su = d_solver.mkUninterpretedSort("u"); Sort si = d_solver.getIntegerSort(); @@ -473,7 +506,8 @@ class SolverTest slv.close(); } - @Test void mkEmptySet() throws CVC5ApiException + @Test + void mkEmptySet() throws CVC5ApiException { Solver slv = new Solver(); Sort s = d_solver.mkSetSort(d_solver.getBooleanSort()); @@ -484,7 +518,8 @@ class SolverTest slv.close(); } - @Test void mkEmptyBag() throws CVC5ApiException + @Test + void mkEmptyBag() throws CVC5ApiException { Solver slv = new Solver(); Sort s = d_solver.mkBagSort(d_solver.getBooleanSort()); @@ -496,7 +531,8 @@ class SolverTest slv.close(); } - @Test void mkEmptySequence() throws CVC5ApiException + @Test + void mkEmptySequence() throws CVC5ApiException { Solver slv = new Solver(); Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort()); @@ -506,38 +542,45 @@ class SolverTest slv.close(); } - @Test void mkFalse() throws CVC5ApiException + @Test + void mkFalse() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkFalse()); assertDoesNotThrow(() -> d_solver.mkFalse()); } - @Test void mkFloatingPointNaN() throws CVC5ApiException + @Test + void mkFloatingPointNaN() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkFloatingPointNaN(3, 5)); } - @Test void mkFloatingPointNegZero() throws CVC5ApiException + @Test + void mkFloatingPointNegZero() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.mkFloatingPointNegZero(3, 5)); } - @Test void mkFloatingPointNegInf() + @Test + void mkFloatingPointNegInf() { assertDoesNotThrow(() -> d_solver.mkFloatingPointNegInf(3, 5)); } - @Test void mkFloatingPointPosInf() + @Test + void mkFloatingPointPosInf() { assertDoesNotThrow(() -> d_solver.mkFloatingPointPosInf(3, 5)); } - @Test void mkFloatingPointPosZero() + @Test + void mkFloatingPointPosZero() { assertDoesNotThrow(() -> d_solver.mkFloatingPointPosZero(3, 5)); } - @Test void mkOp() + @Test + void mkOp() { // Unlike c++, mkOp(Kind kind, Kind k) is a type error in java // assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL)); @@ -561,12 +604,14 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkOp(TUPLE_PROJECT, args)); } - @Test void mkPi() + @Test + void mkPi() { assertDoesNotThrow(() -> d_solver.mkPi()); } - @Test void mkInteger() + @Test + void mkInteger() { assertDoesNotThrow(() -> d_solver.mkInteger("123")); assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("1.23")); @@ -607,7 +652,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkInteger(val4)); } - @Test void mkReal() + @Test + void mkReal() { assertDoesNotThrow(() -> d_solver.mkReal("123")); assertDoesNotThrow(() -> d_solver.mkReal("1.23")); @@ -652,33 +698,38 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkReal(val4, val4)); } - @Test void mkRegexpNone() + @Test + void mkRegexpNone() { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone())); } - @Test void mkRegexpAll() + @Test + void mkRegexpAll() { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll())); } - @Test void mkRegexpAllchar() + @Test + void mkRegexpAllchar() { Sort strSort = d_solver.getStringSort(); Term s = d_solver.mkConst(strSort, "s"); assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAllchar())); } - @Test void mkSepEmp() + @Test + void mkSepEmp() { assertDoesNotThrow(() -> d_solver.mkSepEmp()); } - @Test void mkSepNil() + @Test + void mkSepNil() { assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort())); @@ -687,7 +738,8 @@ class SolverTest slv.close(); } - @Test void mkString() + @Test + void mkString() { assertDoesNotThrow(() -> d_solver.mkString("")); assertDoesNotThrow(() -> d_solver.mkString("asdfasdf")); @@ -695,7 +747,8 @@ class SolverTest assertEquals(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\""); } - @Test void mkTerm() throws CVC5ApiException + @Test + void mkTerm() throws CVC5ApiException { Sort bv32 = d_solver.mkBitVectorSort(32); Term a = d_solver.mkConst(bv32, "a"); @@ -753,7 +806,8 @@ class SolverTest slv.close(); } - @Test void mkTermFromOp() throws CVC5ApiException + @Test + void mkTermFromOp() throws CVC5ApiException { Sort bv32 = d_solver.mkBitVectorSort(32); Term a = d_solver.mkConst(bv32, "a"); @@ -854,13 +908,15 @@ class SolverTest slv.close(); } - @Test void mkTrue() + @Test + void mkTrue() { assertDoesNotThrow(() -> d_solver.mkTrue()); assertDoesNotThrow(() -> d_solver.mkTrue()); } - @Test void mkTuple() + @Test + void mkTuple() { assertDoesNotThrow(() -> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)}, @@ -895,7 +951,8 @@ class SolverTest slv.close(); } - @Test void mkUniverseSet() + @Test + void mkUniverseSet() { assertDoesNotThrow(() -> d_solver.mkUniverseSet(d_solver.getBooleanSort())); assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort())); @@ -904,7 +961,8 @@ class SolverTest slv.close(); } - @Test void mkConst() + @Test + void mkConst() { Sort boolSort = d_solver.getBooleanSort(); Sort intSort = d_solver.getIntegerSort(); @@ -923,7 +981,8 @@ class SolverTest slv.close(); } - @Test void mkConstArray() + @Test + void mkConstArray() { Sort intSort = d_solver.getIntegerSort(); Sort arrSort = d_solver.mkArraySort(intSort, intSort); @@ -946,7 +1005,8 @@ class SolverTest slv.close(); } - @Test void declareDatatype() + @Test + void declareDatatype() { DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil"); DatatypeConstructorDecl[] ctors1 = new DatatypeConstructorDecl[] {nil}; @@ -969,7 +1029,8 @@ class SolverTest slv.close(); } - @Test void declareFun() throws CVC5ApiException + @Test + void declareFun() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); Sort funSort = @@ -988,14 +1049,16 @@ class SolverTest slv.close(); } - @Test void declareSort() + @Test + void declareSort() { assertDoesNotThrow(() -> d_solver.declareSort("s", 0)); assertDoesNotThrow(() -> d_solver.declareSort("s", 2)); assertDoesNotThrow(() -> d_solver.declareSort("", 2)); } - @Test void defineSort() + @Test + void defineSort() { Sort sortVar0 = d_solver.mkParamSort("T0"); Sort sortVar1 = d_solver.mkParamSort("T1"); @@ -1010,7 +1073,8 @@ class SolverTest new Sort[] {sortVar0, sortVar1}, new Sort[] {intSort, realSort})); } - @Test void defineFun() throws CVC5ApiException + @Test + void defineFun() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); Sort funSort = @@ -1051,7 +1115,8 @@ class SolverTest slv.close(); } - @Test void defineFunGlobal() + @Test + void defineFunGlobal() { Sort bSort = d_solver.getBooleanSort(); @@ -1073,7 +1138,8 @@ class SolverTest assertTrue(d_solver.checkSat().isUnsat()); } - @Test void defineFunRec() throws CVC5ApiException + @Test + void defineFunRec() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort); @@ -1132,7 +1198,8 @@ class SolverTest slv.close(); } - @Test void defineFunRecWrongLogic() throws CVC5ApiException + @Test + void defineFunRecWrongLogic() throws CVC5ApiException { d_solver.setLogic("QF_BV"); Sort bvSort = d_solver.mkBitVectorSort(32); @@ -1145,7 +1212,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f, new Term[] {b, b}, v)); } - @Test void defineFunRecGlobal() throws CVC5ApiException + @Test + void defineFunRecGlobal() throws CVC5ApiException { Sort bSort = d_solver.getBooleanSort(); Sort fSort = d_solver.mkFunctionSort(bSort, bSort); @@ -1170,7 +1238,8 @@ class SolverTest assertTrue(d_solver.checkSat().isUnsat()); } - @Test void defineFunsRec() throws CVC5ApiException + @Test + void defineFunsRec() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); Sort bvSort = d_solver.mkBitVectorSort(32); @@ -1260,7 +1329,8 @@ class SolverTest slv.close(); } - @Test void defineFunsRecWrongLogic() throws CVC5ApiException + @Test + void defineFunsRecWrongLogic() throws CVC5ApiException { d_solver.setLogic("QF_BV"); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -1279,7 +1349,8 @@ class SolverTest new Term[] {f1, f2}, new Term[][] {{b, b}, {u}}, new Term[] {v1, v2})); } - @Test void defineFunsRecGlobal() throws CVC5ApiException + @Test + void defineFunsRecGlobal() throws CVC5ApiException { Sort bSort = d_solver.getBooleanSort(); Sort fSort = d_solver.mkFunctionSort(bSort, bSort); @@ -1300,7 +1371,8 @@ class SolverTest assertTrue(d_solver.checkSat().isUnsat()); } - @Test void uFIteration() + @Test + void uFIteration() { Sort intSort = d_solver.getIntegerSort(); Sort funSort = d_solver.mkFunctionSort(new Sort[] {intSort, intSort}, intSort); @@ -1319,13 +1391,15 @@ class SolverTest } } - @Test void getInfo() + @Test + void getInfo() { assertDoesNotThrow(() -> d_solver.getInfo("name")); assertThrows(CVC5ApiException.class, () -> d_solver.getInfo("asdf")); } - @Test void getAbduct() throws CVC5ApiException + @Test + void getAbduct() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); d_solver.setOption("produce-abducts", "true"); @@ -1360,7 +1434,8 @@ class SolverTest assertEquals(output2, truen); } - @Test void getAbduct2() throws CVC5ApiException + @Test + void getAbduct2() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); d_solver.setOption("incremental", "false"); @@ -1377,7 +1452,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getAbduct(conj)); } - @Test void getAbductNext() throws CVC5ApiException + @Test + void getAbductNext() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); d_solver.setOption("produce-abducts", "true"); @@ -1399,7 +1475,8 @@ class SolverTest assertNotEquals(output, output2); } - @Test void getInterpolant() throws CVC5ApiException + @Test + void getInterpolant() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); d_solver.setOption("produce-interpolants", "true"); @@ -1424,7 +1501,8 @@ class SolverTest assertTrue(output.getSort().isBoolean()); } - @Test void getInterpolantNext() throws CVC5ApiException + @Test + void getInterpolantNext() throws CVC5ApiException { d_solver.setLogic("QF_LIA"); d_solver.setOption("produce-interpolants", "true"); @@ -1447,7 +1525,8 @@ class SolverTest assertNotEquals(output, output2); } - @Test void getOp() throws CVC5ApiException + @Test + void getOp() throws CVC5ApiException { Sort bv32 = d_solver.mkBitVectorSort(32); Term a = d_solver.mkConst(bv32, "a"); @@ -1483,13 +1562,15 @@ class SolverTest assertTrue(listhead.hasOp()); } - @Test void getOption() + @Test + void getOption() { assertDoesNotThrow(() -> d_solver.getOption("incremental")); assertThrows(CVC5ApiException.class, () -> d_solver.getOption("asdf")); } - @Test void getOptionNames() + @Test + void getOptionNames() { String[] names = d_solver.getOptionNames(); assertTrue(names.length > 100); @@ -1497,7 +1578,8 @@ class SolverTest assertFalse(Arrays.asList(names).contains("foobar")); } - @Test void getOptionInfo() + @Test + void getOptionInfo() { List assertions = new ArrayList<>(); { @@ -1606,7 +1688,8 @@ class SolverTest assertAll(assertions); } - @Test void getStatistics() + @Test + void getStatistics() { // do some array reasoning to make sure we have a double statistics { @@ -1655,14 +1738,16 @@ class SolverTest } } - @Test void getUnsatAssumptions1() + @Test + void getUnsatAssumptions1() { d_solver.setOption("incremental", "false"); d_solver.checkSatAssuming(d_solver.mkFalse()); assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions()); } - @Test void getUnsatAssumptions2() + @Test + void getUnsatAssumptions2() { d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-assumptions", "false"); @@ -1670,7 +1755,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions()); } - @Test void getUnsatAssumptions3() + @Test + void getUnsatAssumptions3() { d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-assumptions", "true"); @@ -1680,7 +1766,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions()); } - @Test void getUnsatCore1() + @Test + void getUnsatCore1() { d_solver.setOption("incremental", "false"); d_solver.assertFormula(d_solver.mkFalse()); @@ -1688,7 +1775,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore()); } - @Test void getUnsatCore2() + @Test + void getUnsatCore2() { d_solver.setOption("incremental", "false"); d_solver.setOption("produce-unsat-cores", "false"); @@ -1697,7 +1785,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore()); } - @Test void getUnsatCoreAndProof() + @Test + void getUnsatCoreAndProof() { d_solver.setOption("incremental", "true"); d_solver.setOption("produce-unsat-cores", "true"); @@ -1741,7 +1830,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getProof()); } - @Test void getDifficulty() + @Test + void getDifficulty() { d_solver.setOption("produce-difficulty", "true"); // cannot ask before a check sat @@ -1750,14 +1840,16 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getDifficulty()); } - @Test void getDifficulty2() + @Test + void getDifficulty2() { d_solver.checkSat(); // option is not set assertThrows(CVC5ApiException.class, () -> d_solver.getDifficulty()); } - @Test void getDifficulty3() throws CVC5ApiException + @Test + void getDifficulty3() throws CVC5ApiException { d_solver.setOption("produce-difficulty", "true"); Sort intSort = d_solver.getIntegerSort(); @@ -1778,7 +1870,8 @@ class SolverTest } } - @Test void getLearnedLiterals() + @Test + void getLearnedLiterals() { d_solver.setOption("produce-learned-literals", "true"); // cannot ask before a check sat @@ -1787,7 +1880,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getLearnedLiterals()); } - @Test void getLearnedLiterals2() + @Test + void getLearnedLiterals2() { d_solver.setOption("produce-learned-literals", "true"); Sort intSort = d_solver.getIntegerSort(); @@ -1803,7 +1897,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getLearnedLiterals()); } - @Test void getValue1() + @Test + void getValue1() { d_solver.setOption("produce-models", "false"); Term t = d_solver.mkTrue(); @@ -1812,7 +1907,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t)); } - @Test void getValue2() + @Test + void getValue2() { d_solver.setOption("produce-models", "true"); Term t = d_solver.mkFalse(); @@ -1821,7 +1917,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t)); } - @Test void getValue3() + @Test + void getValue3() { d_solver.setOption("produce-models", "true"); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -1861,7 +1958,8 @@ class SolverTest slv.close(); } - @Test void getModelDomainElements() + @Test + void getModelDomainElements() { d_solver.setOption("produce-models", "true"); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -1877,7 +1975,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getModelDomainElements(intSort)); } - @Test void getModelDomainElements2() + @Test + void getModelDomainElements2() { d_solver.setOption("produce-models", "true"); d_solver.setOption("finite-model-find", "true"); @@ -1894,7 +1993,8 @@ class SolverTest assertTrue(d_solver.getModelDomainElements(uSort).length == 1); } - @Test void isModelCoreSymbol() + @Test + void isModelCoreSymbol() { d_solver.setOption("produce-models", "true"); d_solver.setOption("model-cores", "simple"); @@ -1912,7 +2012,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.isModelCoreSymbol(zero)); } - @Test void getModel() + @Test + void getModel() { d_solver.setOption("produce-models", "true"); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -1930,7 +2031,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms2)); } - @Test void getModel2() + @Test + void getModel2() { d_solver.setOption("produce-models", "true"); Sort[] sorts = new Sort[] {}; @@ -1938,7 +2040,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts, terms)); } - @Test void getModel3() + @Test + void getModel3() { d_solver.setOption("produce-models", "true"); Sort[] sorts = new Sort[] {}; @@ -1950,7 +2053,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getModel(sorts2, terms)); } - @Test void getQuantifierElimination() + @Test + void getQuantifierElimination() { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm( @@ -1965,7 +2069,8 @@ class SolverTest slv.close(); } - @Test void getQuantifierEliminationDisjunct() + @Test + void getQuantifierEliminationDisjunct() { Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x"); Term forall = d_solver.mkTerm( @@ -1981,7 +2086,8 @@ class SolverTest slv.close(); } - @Test void declareSepHeap() throws CVC5ApiException + @Test + void declareSepHeap() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2010,7 +2116,8 @@ class SolverTest solver.checkSat(); } - @Test void getValueSepHeap1() throws CVC5ApiException + @Test + void getValueSepHeap1() throws CVC5ApiException { d_solver.setLogic("QF_BV"); d_solver.setOption("incremental", "false"); @@ -2020,7 +2127,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap()); } - @Test void getValueSepHeap2() throws CVC5ApiException + @Test + void getValueSepHeap2() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2029,7 +2137,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap()); } - @Test void getValueSepHeap3() throws CVC5ApiException + @Test + void getValueSepHeap3() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2040,7 +2149,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap()); } - @Test void getValueSepHeap4() throws CVC5ApiException + @Test + void getValueSepHeap4() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2051,7 +2161,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepHeap()); } - @Test void getValueSepHeap5() throws CVC5ApiException + @Test + void getValueSepHeap5() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2060,7 +2171,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getValueSepHeap()); } - @Test void getValueSepNil1() throws CVC5ApiException + @Test + void getValueSepNil1() throws CVC5ApiException { d_solver.setLogic("QF_BV"); d_solver.setOption("incremental", "false"); @@ -2070,7 +2182,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil()); } - @Test void getValueSepNil2() throws CVC5ApiException + @Test + void getValueSepNil2() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2079,7 +2192,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil()); } - @Test void getValueSepNil3() throws CVC5ApiException + @Test + void getValueSepNil3() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2090,7 +2204,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil()); } - @Test void getValueSepNil4() throws CVC5ApiException + @Test + void getValueSepNil4() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2101,7 +2216,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.getValueSepNil()); } - @Test void getValueSepNil5() throws CVC5ApiException + @Test + void getValueSepNil5() throws CVC5ApiException { d_solver.setLogic("ALL"); d_solver.setOption("incremental", "false"); @@ -2110,7 +2226,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getValueSepNil()); } - @Test void push1() + @Test + void push1() { d_solver.setOption("incremental", "true"); assertDoesNotThrow(() -> d_solver.push(1)); @@ -2118,25 +2235,29 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "true")); } - @Test void push2() + @Test + void push2() { d_solver.setOption("incremental", "false"); assertThrows(CVC5ApiException.class, () -> d_solver.push(1)); } - @Test void pop1() + @Test + void pop1() { d_solver.setOption("incremental", "false"); assertThrows(CVC5ApiException.class, () -> d_solver.pop(1)); } - @Test void pop2() + @Test + void pop2() { d_solver.setOption("incremental", "true"); assertThrows(CVC5ApiException.class, () -> d_solver.pop(1)); } - @Test void pop3() + @Test + void pop3() { d_solver.setOption("incremental", "true"); assertDoesNotThrow(() -> d_solver.push(1)); @@ -2144,7 +2265,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.pop(1)); } - @Test void blockModel1() + @Test + void blockModel1() { d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); @@ -2153,7 +2275,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); } - @Test void blockModel2() throws CVC5ApiException + @Test + void blockModel2() throws CVC5ApiException { d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); @@ -2162,7 +2285,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); } - @Test void blockModel3() throws CVC5ApiException + @Test + void blockModel3() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); d_solver.setOption("block-models", "literals"); @@ -2171,7 +2295,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModel()); } - @Test void blockModel4() throws CVC5ApiException + @Test + void blockModel4() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); d_solver.setOption("block-models", "literals"); @@ -2181,7 +2306,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.blockModel()); } - @Test void blockModelValues1() throws CVC5ApiException + @Test + void blockModelValues1() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); d_solver.setOption("block-models", "literals"); @@ -2197,7 +2323,8 @@ class SolverTest slv.close(); } - @Test void blockModelValues2() throws CVC5ApiException + @Test + void blockModelValues2() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); @@ -2206,7 +2333,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x})); } - @Test void blockModelValues3() throws CVC5ApiException + @Test + void blockModelValues3() throws CVC5ApiException { d_solver.setOption("block-models", "literals"); Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x"); @@ -2215,7 +2343,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x})); } - @Test void blockModelValues4() throws CVC5ApiException + @Test + void blockModelValues4() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); d_solver.setOption("block-models", "literals"); @@ -2224,7 +2353,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x})); } - @Test void blockModelValues5() throws CVC5ApiException + @Test + void blockModelValues5() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); d_solver.setOption("block-models", "literals"); @@ -2234,7 +2364,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x})); } - @Test void setInfo() throws CVC5ApiException + @Test + void setInfo() throws CVC5ApiException { assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc4-lagic", "QF_BV")); assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc2-logic", "QF_BV")); @@ -2260,7 +2391,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("status", "asdf")); } - @Test void simplify() throws CVC5ApiException + @Test + void simplify() throws CVC5ApiException { assertThrows(CVC5ApiException.class, () -> d_solver.simplify(d_solver.getNullTerm())); @@ -2335,7 +2467,8 @@ class SolverTest slv.close(); } - @Test void assertFormula() + @Test + void assertFormula() { assertDoesNotThrow(() -> d_solver.assertFormula(d_solver.mkTrue())); assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm())); @@ -2344,14 +2477,16 @@ class SolverTest slv.close(); } - @Test void checkSat() throws CVC5ApiException + @Test + void checkSat() throws CVC5ApiException { d_solver.setOption("incremental", "false"); assertDoesNotThrow(() -> d_solver.checkSat()); assertThrows(CVC5ApiException.class, () -> d_solver.checkSat()); } - @Test void checkSatAssuming() throws CVC5ApiException + @Test + void checkSatAssuming() throws CVC5ApiException { d_solver.setOption("incremental", "false"); assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue())); @@ -2361,7 +2496,8 @@ class SolverTest slv.close(); } - @Test void checkSatAssuming1() throws CVC5ApiException + @Test + void checkSatAssuming1() throws CVC5ApiException { Sort boolSort = d_solver.getBooleanSort(); Term x = d_solver.mkConst(boolSort, "x"); @@ -2377,7 +2513,8 @@ class SolverTest slv.close(); } - @Test void checkSatAssuming2() throws CVC5ApiException + @Test + void checkSatAssuming2() throws CVC5ApiException { d_solver.setOption("incremental", "true"); @@ -2428,7 +2565,8 @@ class SolverTest slv.close(); } - @Test void setLogic() throws CVC5ApiException + @Test + void setLogic() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA")); assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV")); @@ -2436,7 +2574,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AUFLIRA")); } - @Test void setOption() throws CVC5ApiException + @Test + void setOption() throws CVC5ApiException { assertDoesNotThrow(() -> d_solver.setOption("bv-sat-solver", "minisat")); assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "1")); @@ -2444,7 +2583,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "minisat")); } - @Test void resetAssertions() throws CVC5ApiException + @Test + void resetAssertions() throws CVC5ApiException { d_solver.setOption("incremental", "true"); @@ -2459,7 +2599,8 @@ class SolverTest d_solver.checkSatAssuming(new Term[] {slt, ule}); } - @Test void declareSygusVar() throws CVC5ApiException + @Test + void declareSygusVar() throws CVC5ApiException { d_solver.setOption("sygus", "true"); Sort boolSort = d_solver.getBooleanSort(); @@ -2481,7 +2622,8 @@ class SolverTest slv.close(); } - @Test void mkSygusGrammar() throws CVC5ApiException + @Test + void mkSygusGrammar() throws CVC5ApiException { Term nullTerm = d_solver.getNullTerm(); Term boolTerm = d_solver.mkBoolean(true); @@ -2513,7 +2655,8 @@ class SolverTest slv.close(); } - @Test void synthFun() throws CVC5ApiException + @Test + void synthFun() throws CVC5ApiException { d_solver.setOption("sygus", "true"); Sort nullSort = d_solver.getNullSort(); @@ -2553,7 +2696,8 @@ class SolverTest slv.close(); } - @Test void synthInv() throws CVC5ApiException + @Test + void synthInv() throws CVC5ApiException { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); @@ -2579,7 +2723,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i4", new Term[] {x}, g2)); } - @Test void addSygusConstraint() throws CVC5ApiException + @Test + void addSygusConstraint() throws CVC5ApiException { d_solver.setOption("sygus", "true"); Term nullTerm = d_solver.getNullTerm(); @@ -2596,7 +2741,8 @@ class SolverTest slv.close(); } - @Test void addSygusAssume() + @Test + void addSygusAssume() { d_solver.setOption("sygus", "true"); Term nullTerm = d_solver.getNullTerm(); @@ -2613,7 +2759,8 @@ class SolverTest slv.close(); } - @Test void addSygusInvConstraint() throws CVC5ApiException + @Test + void addSygusInvConstraint() throws CVC5ApiException { d_solver.setOption("sygus", "true"); Sort bool = d_solver.getBooleanSort(); @@ -2680,14 +2827,16 @@ class SolverTest slv.close(); } - @Test void checkSynth() throws CVC5ApiException + @Test + void checkSynth() throws CVC5ApiException { assertThrows(CVC5ApiException.class, () -> d_solver.checkSynth()); d_solver.setOption("sygus", "true"); assertDoesNotThrow(() -> d_solver.checkSynth()); } - @Test void getSynthSolution() throws CVC5ApiException + @Test + void getSynthSolution() throws CVC5ApiException { d_solver.setOption("sygus", "true"); d_solver.setOption("incremental", "false"); @@ -2712,7 +2861,8 @@ class SolverTest slv.close(); } - @Test void getSynthSolutions() throws CVC5ApiException + @Test + void getSynthSolutions() throws CVC5ApiException { d_solver.setOption("sygus", "true"); d_solver.setOption("incremental", "false"); @@ -2737,7 +2887,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x})); slv.close(); } - @Test void checkSynthNext() throws CVC5ApiException + @Test + void checkSynthNext() throws CVC5ApiException { d_solver.setOption("sygus", "true"); d_solver.setOption("incremental", "true"); @@ -2751,7 +2902,8 @@ class SolverTest assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f})); } - @Test void checkSynthNext2() throws CVC5ApiException + @Test + void checkSynthNext2() throws CVC5ApiException { d_solver.setOption("sygus", "true"); d_solver.setOption("incremental", "false"); @@ -2761,7 +2913,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext()); } - @Test void checkSynthNext3() throws CVC5ApiException + @Test + void checkSynthNext3() throws CVC5ApiException { d_solver.setOption("sygus", "true"); d_solver.setOption("incremental", "true"); @@ -2770,7 +2923,8 @@ class SolverTest assertThrows(CVC5ApiException.class, () -> d_solver.checkSynthNext()); } - @Test void tupleProject() throws CVC5ApiException + @Test + void tupleProject() throws CVC5ApiException { Sort[] sorts = new Sort[] {d_solver.getBooleanSort(), d_solver.getIntegerSort(), diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index b8071b77c..d527439b4 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -31,12 +31,14 @@ class SortTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } @@ -65,14 +67,16 @@ class SortTest return d_solver.mkDatatypeSort(paramDtypeSpec); } - @Test void operators_comparison() + @Test + void operators_comparison() { assertDoesNotThrow(() -> d_solver.getIntegerSort() == d_solver.getNullSort()); assertDoesNotThrow(() -> d_solver.getIntegerSort() != d_solver.getNullSort()); assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort())); } - @Test void hasGetSymbol() throws CVC5ApiException + @Test + void hasGetSymbol() throws CVC5ApiException { Sort n = d_solver.getNullSort(); Sort b = d_solver.getBooleanSort(); @@ -90,64 +94,74 @@ class SortTest assertEquals(s1.getSymbol(), "|s1\\|"); } - @Test void isBoolean() + @Test + void isBoolean() { assertTrue(d_solver.getBooleanSort().isBoolean()); assertDoesNotThrow(() -> d_solver.getNullSort().isBoolean()); } - @Test void isInteger() + @Test + void isInteger() { assertTrue(d_solver.getIntegerSort().isInteger()); assertTrue(!d_solver.getRealSort().isInteger()); assertDoesNotThrow(() -> d_solver.getNullSort().isInteger()); } - @Test void isReal() + @Test + void isReal() { assertTrue(d_solver.getRealSort().isReal()); assertTrue(!d_solver.getIntegerSort().isReal()); assertDoesNotThrow(() -> d_solver.getNullSort().isReal()); } - @Test void isString() + @Test + void isString() { assertTrue(d_solver.getStringSort().isString()); assertDoesNotThrow(() -> d_solver.getNullSort().isString()); } - @Test void isRegExp() + @Test + void isRegExp() { assertTrue(d_solver.getRegExpSort().isRegExp()); assertDoesNotThrow(() -> d_solver.getNullSort().isRegExp()); } - @Test void isRoundingMode() throws CVC5ApiException + @Test + void isRoundingMode() throws CVC5ApiException { assertTrue(d_solver.getRoundingModeSort().isRoundingMode()); assertDoesNotThrow(() -> d_solver.getNullSort().isRoundingMode()); } - @Test void isBitVector() throws CVC5ApiException + @Test + void isBitVector() throws CVC5ApiException { assertTrue(d_solver.mkBitVectorSort(8).isBitVector()); assertDoesNotThrow(() -> d_solver.getNullSort().isBitVector()); } - @Test void isFloatingPoint() throws CVC5ApiException + @Test + void isFloatingPoint() throws CVC5ApiException { assertTrue(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint()); assertDoesNotThrow(() -> d_solver.getNullSort().isFloatingPoint()); } - @Test void isDatatype() throws CVC5ApiException + @Test + void isDatatype() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); assertTrue(dt_sort.isDatatype()); assertDoesNotThrow(() -> d_solver.getNullSort().isDatatype()); } - @Test void isConstructor() throws CVC5ApiException + @Test + void isConstructor() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); @@ -156,7 +170,8 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isConstructor()); } - @Test void isSelector() throws CVC5ApiException + @Test + void isSelector() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); @@ -165,7 +180,8 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isSelector()); } - @Test void isTester() throws CVC5ApiException + @Test + void isTester() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); @@ -174,28 +190,32 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isTester()); } - @Test void isFunction() + @Test + void isFunction() { Sort fun_sort = d_solver.mkFunctionSort(d_solver.getRealSort(), d_solver.getIntegerSort()); assertTrue(fun_sort.isFunction()); assertDoesNotThrow(() -> d_solver.getNullSort().isFunction()); } - @Test void isPredicate() + @Test + void isPredicate() { Sort pred_sort = d_solver.mkPredicateSort(new Sort[] {d_solver.getRealSort()}); assertTrue(pred_sort.isPredicate()); assertDoesNotThrow(() -> d_solver.getNullSort().isPredicate()); } - @Test void isTuple() + @Test + void isTuple() { Sort tup_sort = d_solver.mkTupleSort(new Sort[] {d_solver.getRealSort()}); assertTrue(tup_sort.isTuple()); assertDoesNotThrow(() -> d_solver.getNullSort().isTuple()); } - @Test void isRecord() + @Test + void isRecord() { Sort rec_sort = d_solver.mkRecordSort(new Pair[] {new Pair("asdf", d_solver.getRealSort())}); @@ -203,49 +223,56 @@ class SortTest assertDoesNotThrow(() -> d_solver.getNullSort().isRecord()); } - @Test void isArray() + @Test + void isArray() { Sort arr_sort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getIntegerSort()); assertTrue(arr_sort.isArray()); assertDoesNotThrow(() -> d_solver.getNullSort().isArray()); } - @Test void isSet() + @Test + void isSet() { Sort set_sort = d_solver.mkSetSort(d_solver.getRealSort()); assertTrue(set_sort.isSet()); assertDoesNotThrow(() -> d_solver.getNullSort().isSet()); } - @Test void isBag() + @Test + void isBag() { Sort bag_sort = d_solver.mkBagSort(d_solver.getRealSort()); assertTrue(bag_sort.isBag()); assertDoesNotThrow(() -> d_solver.getNullSort().isBag()); } - @Test void isSequence() + @Test + void isSequence() { Sort seq_sort = d_solver.mkSequenceSort(d_solver.getRealSort()); assertTrue(seq_sort.isSequence()); assertDoesNotThrow(() -> d_solver.getNullSort().isSequence()); } - @Test void isUninterpreted() + @Test + void isUninterpreted() { Sort un_sort = d_solver.mkUninterpretedSort("asdf"); assertTrue(un_sort.isUninterpretedSort()); assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSort()); } - @Test void isUninterpretedSortSortConstructor() throws CVC5ApiException + @Test + void isUninterpretedSortSortConstructor() throws CVC5ApiException { Sort sc_sort = d_solver.mkUninterpretedSortConstructorSort("asdf", 1); assertTrue(sc_sort.isUninterpretedSortConstructor()); assertDoesNotThrow(() -> d_solver.getNullSort().isUninterpretedSortConstructor()); } - @Test void getDatatype() throws CVC5ApiException + @Test + void getDatatype() throws CVC5ApiException { Sort dtypeSort = create_datatype_sort(); assertDoesNotThrow(() -> dtypeSort.getDatatype()); @@ -254,7 +281,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getDatatype()); } - @Test void datatypeSorts() throws CVC5ApiException + @Test + void datatypeSorts() throws CVC5ApiException { Sort intSort = d_solver.getIntegerSort(); Sort dtypeSort = create_datatype_sort(); @@ -296,7 +324,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorCodomainSort()); } - @Test void instantiate() throws CVC5ApiException + @Test + void instantiate() throws CVC5ApiException { // instantiate parametric datatype, check should not fail Sort paramDtypeSort = create_param_datatype_sort(); @@ -316,7 +345,8 @@ class SortTest assertDoesNotThrow(() -> sortConsSort.instantiate(new Sort[] {d_solver.getIntegerSort()})); } - @Test void isInstantiated() throws CVC5ApiException + @Test + void isInstantiated() throws CVC5ApiException { Sort paramDtypeSort = create_param_datatype_sort(); assertFalse(paramDtypeSort.isInstantiated()); @@ -332,7 +362,8 @@ class SortTest assertFalse(d_solver.mkBitVectorSort(32).isInstantiated()); } - @Test void getInstantiatedParameters() throws CVC5ApiException + @Test + void getInstantiatedParameters() throws CVC5ApiException { Sort intSort = d_solver.getIntegerSort(); Sort realSort = d_solver.getRealSort(); @@ -379,7 +410,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getInstantiatedParameters()); } - @Test void getUninterpretedSortConstructor() throws CVC5ApiException + @Test + void getUninterpretedSortConstructor() throws CVC5ApiException { Sort intSort = d_solver.getIntegerSort(); Sort realSort = d_solver.getRealSort(); @@ -392,7 +424,8 @@ class SortTest assertEquals(sortConsSort, instSortConsSort.getUninterpretedSortConstructor()); } - @Test void getFunctionArity() throws CVC5ApiException + @Test + void getFunctionArity() throws CVC5ApiException { Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); @@ -401,7 +434,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionArity()); } - @Test void getFunctionDomainSorts() throws CVC5ApiException + @Test + void getFunctionDomainSorts() throws CVC5ApiException { Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); @@ -410,7 +444,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionDomainSorts()); } - @Test void getFunctionCodomainSort() throws CVC5ApiException + @Test + void getFunctionCodomainSort() throws CVC5ApiException { Sort funSort = d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()); @@ -419,7 +454,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getFunctionCodomainSort()); } - @Test void getArrayIndexSort() throws CVC5ApiException + @Test + void getArrayIndexSort() throws CVC5ApiException { Sort elementSort = d_solver.mkBitVectorSort(32); Sort indexSort = d_solver.mkBitVectorSort(32); @@ -428,7 +464,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> indexSort.getArrayIndexSort()); } - @Test void getArrayElementSort() throws CVC5ApiException + @Test + void getArrayElementSort() throws CVC5ApiException { Sort elementSort = d_solver.mkBitVectorSort(32); Sort indexSort = d_solver.mkBitVectorSort(32); @@ -437,7 +474,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> indexSort.getArrayElementSort()); } - @Test void getSetElementSort() throws CVC5ApiException + @Test + void getSetElementSort() throws CVC5ApiException { Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort()); assertDoesNotThrow(() -> setSort.getSetElementSort()); @@ -447,7 +485,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSetElementSort()); } - @Test void getBagElementSort() throws CVC5ApiException + @Test + void getBagElementSort() throws CVC5ApiException { Sort bagSort = d_solver.mkBagSort(d_solver.getIntegerSort()); assertDoesNotThrow(() -> bagSort.getBagElementSort()); @@ -457,7 +496,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getBagElementSort()); } - @Test void getSequenceElementSort() throws CVC5ApiException + @Test + void getSequenceElementSort() throws CVC5ApiException { Sort seqSort = d_solver.mkSequenceSort(d_solver.getIntegerSort()); assertTrue(seqSort.isSequence()); @@ -467,7 +507,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSequenceElementSort()); } - @Test void getSymbol() throws CVC5ApiException + @Test + void getSymbol() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); assertDoesNotThrow(() -> uSort.getSymbol()); @@ -475,7 +516,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } - @Test void getUninterpretedSortConstructorName() throws CVC5ApiException + @Test + void getUninterpretedSortConstructorName() throws CVC5ApiException { Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); assertDoesNotThrow(() -> sSort.getSymbol()); @@ -483,7 +525,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getSymbol()); } - @Test void getUninterpretedSortConstructorArity() throws CVC5ApiException + @Test + void getUninterpretedSortConstructorArity() throws CVC5ApiException { Sort sSort = d_solver.mkUninterpretedSortConstructorSort("s", 2); assertDoesNotThrow(() -> sSort.getUninterpretedSortConstructorArity()); @@ -491,7 +534,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getUninterpretedSortConstructorArity()); } - @Test void getBitVectorSize() throws CVC5ApiException + @Test + void getBitVectorSize() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(32); assertDoesNotThrow(() -> bvSort.getBitVectorSize()); @@ -499,7 +543,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> setSort.getBitVectorSize()); } - @Test void getFloatingPointExponentSize() throws CVC5ApiException + @Test + void getFloatingPointExponentSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); assertDoesNotThrow(() -> fpSort.getFloatingPointExponentSize()); @@ -507,7 +552,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointExponentSize()); } - @Test void getFloatingPointSignificandSize() throws CVC5ApiException + @Test + void getFloatingPointSignificandSize() throws CVC5ApiException { Sort fpSort = d_solver.mkFloatingPointSort(4, 8); assertDoesNotThrow(() -> fpSort.getFloatingPointSignificandSize()); @@ -515,7 +561,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> setSort.getFloatingPointSignificandSize()); } - @Test void getDatatypeArity() throws CVC5ApiException + @Test + void getDatatypeArity() throws CVC5ApiException { // create datatype sort, check should not fail DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list"); @@ -531,7 +578,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getDatatypeArity()); } - @Test void getTupleLength() throws CVC5ApiException + @Test + void getTupleLength() throws CVC5ApiException { Sort tupleSort = d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); @@ -540,7 +588,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getTupleLength()); } - @Test void getTupleSorts() throws CVC5ApiException + @Test + void getTupleSorts() throws CVC5ApiException { Sort tupleSort = d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), d_solver.getIntegerSort()}); @@ -549,7 +598,8 @@ class SortTest assertThrows(CVC5ApiException.class, () -> bvSort.getTupleSorts()); } - @Test void sortCompare() throws CVC5ApiException + @Test + void sortCompare() throws CVC5ApiException { Sort boolSort = d_solver.getBooleanSort(); Sort intSort = d_solver.getIntegerSort(); @@ -562,7 +612,8 @@ class SortTest == (intSort.compareTo(bvSort) >= 0)); } - @Test void sortScopedToString() throws CVC5ApiException + @Test + void sortScopedToString() throws CVC5ApiException { String name = "uninterp-sort"; Sort bvsort8 = d_solver.mkBitVectorSort(8); diff --git a/test/unit/api/java/SynthResultTest.java b/test/unit/api/java/SynthResultTest.java index efc82a816..c47363948 100644 --- a/test/unit/api/java/SynthResultTest.java +++ b/test/unit/api/java/SynthResultTest.java @@ -26,17 +26,20 @@ class SynthResultTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void isNull() + @Test + void isNull() { SynthResult res_null = d_solver.getNullSynthResult(); assertTrue(res_null.isNull()); @@ -45,7 +48,8 @@ class SynthResultTest assertFalse(res_null.isUnknown()); } - @Test void hasSolution() + @Test + void hasSolution() { d_solver.setOption("sygus", "true"); Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort()); @@ -58,13 +62,15 @@ class SynthResultTest assertFalse(res.isUnknown()); } - @Test void hasNoSolution() + @Test + void hasNoSolution() { SynthResult res_null = d_solver.getNullSynthResult(); assertFalse(res_null.hasSolution()); } - @Test void isUnknown() + @Test + void isUnknown() { d_solver.setOption("sygus", "true"); Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort()); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index ee5d1429d..2bd4cb08b 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -34,17 +34,20 @@ class TermTest { private Solver d_solver; - @BeforeEach void setUp() + @BeforeEach + void setUp() { d_solver = new Solver(); } - @AfterEach void tearDown() + @AfterEach + void tearDown() { d_solver.close(); } - @Test void eq() + @Test + void eq() { Sort uSort = d_solver.mkUninterpretedSort("u"); Term x = d_solver.mkVar(uSort, "x"); @@ -59,7 +62,8 @@ class TermTest assertTrue(x != z); } - @Test void getId() + @Test + void getId() { Term n = d_solver.getNullTerm(); assertThrows(CVC5ApiException.class, () -> n.getId()); @@ -72,7 +76,8 @@ class TermTest assertNotEquals(x.getId(), z.getId()); } - @Test void getKind() throws CVC5ApiException + @Test + void getKind() throws CVC5ApiException { Sort uSort = d_solver.mkUninterpretedSort("u"); Sort intSort = d_solver.getIntegerSort(); @@ -114,7 +119,8 @@ class TermTest assertEquals(ss.getKind(), SEQ_CONCAT); } - @Test void getSort() throws CVC5ApiException + @Test + void getSort() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -159,7 +165,8 @@ class TermTest assertEquals(p_f_y.getSort(), boolSort); } - @Test void getOp() throws CVC5ApiException + @Test + void getOp() throws CVC5ApiException { Sort intsort = d_solver.getIntegerSort(); Sort bvsort = d_solver.mkBitVectorSort(8); @@ -219,7 +226,8 @@ class TermTest Term nilOpTerm = list.getConstructorTerm("nil"); } - @Test void hasGetSymbol() throws CVC5ApiException + @Test + void hasGetSymbol() throws CVC5ApiException { Term n = d_solver.getNullTerm(); Term t = d_solver.mkBoolean(true); @@ -234,7 +242,8 @@ class TermTest assertEquals(c.getSymbol(), "|\\|"); } - @Test void isNull() throws CVC5ApiException + @Test + void isNull() throws CVC5ApiException { Term x = d_solver.getNullTerm(); assertTrue(x.isNull()); @@ -242,7 +251,8 @@ class TermTest assertFalse(x.isNull()); } - @Test void notTerm() throws CVC5ApiException + @Test + void notTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -271,7 +281,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.notTerm()); } - @Test void andTerm() throws CVC5ApiException + @Test + void andTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -337,7 +348,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x)); } - @Test void orTerm() throws CVC5ApiException + @Test + void orTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -403,7 +415,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x)); } - @Test void xorTerm() throws CVC5ApiException + @Test + void xorTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -469,7 +482,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x)); } - @Test void eqTerm() throws CVC5ApiException + @Test + void eqTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -535,7 +549,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x)); } - @Test void impTerm() throws CVC5ApiException + @Test + void impTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -601,7 +616,8 @@ class TermTest assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x)); } - @Test void iteTerm() throws CVC5ApiException + @Test + void iteTerm() throws CVC5ApiException { Sort bvSort = d_solver.mkBitVectorSort(8); Sort intSort = d_solver.getIntegerSort(); @@ -645,7 +661,8 @@ class TermTest assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b)); } - @Test void termAssignment() + @Test + void termAssignment() { Term t1 = d_solver.mkInteger(1); Term t2 = t1; @@ -653,7 +670,8 @@ class TermTest assertEquals(t1, d_solver.mkInteger(1)); } - @Test void termCompare() + @Test + void termCompare() { Term t1 = d_solver.mkInteger(1); Term t2 = d_solver.mkTerm(ADD, d_solver.mkInteger(2), d_solver.mkInteger(2)); @@ -664,7 +682,8 @@ class TermTest assertTrue((t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0)); } - @Test void termChildren() throws CVC5ApiException + @Test + void termChildren() throws CVC5ApiException { // simple term 2+3 Term two = d_solver.mkInteger(2); @@ -686,7 +705,8 @@ class TermTest assertThrows(CVC5ApiException.class, () -> tnull.getChild(0)); } - @Test void getIntegerValue() throws CVC5ApiException + @Test + void getIntegerValue() throws CVC5ApiException { Term int1 = d_solver.mkInteger("-18446744073709551616"); Term int2 = d_solver.mkInteger("-18446744073709551615"); @@ -749,14 +769,16 @@ class TermTest assertEquals(int11.getIntegerValue().toString(), "18446744073709551616"); } - @Test void getString() + @Test + void getString() { Term s1 = d_solver.mkString("abcde"); assertTrue(s1.isStringValue()); assertEquals(s1.getStringValue(), "abcde"); } - @Test void getReal() throws CVC5ApiException + @Test + void getReal() throws CVC5ApiException { Term real1 = d_solver.mkReal("0"); Term real2 = d_solver.mkReal(".0"); @@ -792,7 +814,8 @@ class TermTest assertEquals("23432343/10000", Utils.getRational(real10.getRealValue())); } - @Test void getConstArrayBase() + @Test + void getConstArrayBase() { Sort intsort = d_solver.getIntegerSort(); Sort arrsort = d_solver.mkArraySort(intsort, intsort); @@ -803,7 +826,8 @@ class TermTest assertEquals(one, constarr.getConstArrayBase()); } - @Test void getBoolean() + @Test + void getBoolean() { Term b1 = d_solver.mkBoolean(true); Term b2 = d_solver.mkBoolean(false); @@ -814,7 +838,8 @@ class TermTest assertFalse(b2.getBooleanValue()); } - @Test void getBitVector() throws CVC5ApiException + @Test + void getBitVector() throws CVC5ApiException { Term b1 = d_solver.mkBitVector(8, 15); Term b2 = d_solver.mkBitVector(8, "00001111", 2); @@ -855,7 +880,8 @@ class TermTest assertEquals("f", b7.getBitVectorValue(16)); } - @Test void getUninterpretedSortValue() throws CVC5ApiException + @Test + void getUninterpretedSortValue() throws CVC5ApiException { d_solver.setOption("produce-models", "true"); Sort uSort = d_solver.mkUninterpretedSort("u"); @@ -870,7 +896,8 @@ class TermTest assertDoesNotThrow(() -> vy.getUninterpretedSortValue()); } - @Test void isRoundingModeValue() throws CVC5ApiException + @Test + void isRoundingModeValue() throws CVC5ApiException { assertFalse(d_solver.mkInteger(15).isRoundingModeValue()); assertTrue( @@ -878,7 +905,8 @@ class TermTest assertFalse(d_solver.mkConst(d_solver.getRoundingModeSort()).isRoundingModeValue()); } - @Test void getRoundingModeValue() throws CVC5ApiException + @Test + void getRoundingModeValue() throws CVC5ApiException { assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(15).getRoundingModeValue()); assertEquals( @@ -895,7 +923,8 @@ class TermTest RoundingMode.ROUND_NEAREST_TIES_TO_AWAY); } - @Test void getTuple() + @Test + void getTuple() { Sort s1 = d_solver.getIntegerSort(); Sort s2 = d_solver.getRealSort(); @@ -911,7 +940,8 @@ class TermTest assertEquals(Arrays.asList((new Term[] {t1, t2, t3})), Arrays.asList(tup.getTupleValue())); } - @Test void getFloatingPoint() throws CVC5ApiException + @Test + void getFloatingPoint() throws CVC5ApiException { Term bvval = d_solver.mkBitVector(16, "0000110000000011", 2); Term fp = d_solver.mkFloatingPoint(5, 11, bvval); @@ -931,7 +961,8 @@ class TermTest assertTrue(d_solver.mkFloatingPointNaN(5, 11).isFloatingPointNaN()); } - @Test void getSet() + @Test + void getSet() { Sort s = d_solver.mkSetSort(d_solver.getIntegerSort()); @@ -966,7 +997,8 @@ class TermTest assertEquals(a, b); } - @Test void getSequence() + @Test + void getSequence() { Sort s = d_solver.mkSequenceSort(d_solver.getIntegerSort()); @@ -997,7 +1029,8 @@ class TermTest assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue())); } - @Test void getCardinalityConstraint() throws CVC5ApiException + @Test + void getCardinalityConstraint() throws CVC5ApiException { Sort su = d_solver.mkUninterpretedSort("u"); Term t = d_solver.mkCardinalityConstraint(su, 3); @@ -1012,7 +1045,8 @@ class TermTest assertThrows(CVC5ApiException.class, () -> nullt.isCardinalityConstraint()); } - @Test void substitute() + @Test + void substitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); Term one = d_solver.mkInteger(1); @@ -1063,7 +1097,8 @@ class TermTest assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs)); } - @Test void constArray() throws CVC5ApiException + @Test + void constArray() throws CVC5ApiException { Sort intsort = d_solver.getIntegerSort(); Sort arrsort = d_solver.mkArraySort(intsort, intsort); @@ -1082,7 +1117,8 @@ class TermTest stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5)); } - @Test void getSequenceValue() throws CVC5ApiException + @Test + void getSequenceValue() throws CVC5ApiException { Sort realsort = d_solver.getRealSort(); Sort seqsort = d_solver.mkSequenceSort(realsort); @@ -1099,7 +1135,8 @@ class TermTest assertThrows(CVC5ApiException.class, () -> su.getSequenceValue()); } - @Test void termScopedToString() + @Test + void termScopedToString() { Sort intsort = d_solver.getIntegerSort(); Term x = d_solver.mkConst(intsort, "x"); -- 2.30.2