Finish the Java Api (#6396)

This commit finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.

1 files changed, 34 insertions, 49 deletions

diff --git a/test/unit/api/java/cvc5/OpTest.java b/test/unit/api/java/cvc5/OpTest.java
index afe728b88..f4dd181f4 100644
--- a/test/unit/api/java/cvc5/OpTest.java
+++ b/test/unit/api/java/cvc5/OpTest.java
@@ -23,38 +23,38 @@ import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-class OpTest {
+class OpTest
+{
   private Solver d_solver;
 
-  @BeforeEach
-  void setUp() {
+  @BeforeEach void setUp()
+  {
     d_solver = new Solver();
   }
 
-  @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());
     x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
     assertFalse(x.isNull());
   }
 
-  @Test
-  void opFromKind() {
+  @Test void opFromKind()
+  {
     assertDoesNotThrow(() -> d_solver.mkOp(PLUS));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
   }
 
-  @Test
-  void getIndicesString() throws CVC5ApiException {
+  @Test void getIndicesString() throws CVC5ApiException
+  {
     Op x = d_solver.getNullOp();
     assertThrows(CVC5ApiException.class, () -> x.getStringIndices());
 
@@ -64,8 +64,8 @@ class OpTest {
     assertEquals(divisible_idx, "4");
   }
 
-  @Test
-  void getIndicesUint() throws CVC5ApiException {
+  @Test void getIndicesUint() throws CVC5ApiException
+  {
     Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
     assertTrue(bitvector_repeat_ot.isIndexed());
     int bitvector_repeat_idx = bitvector_repeat_ot.getIntegerIndices()[0];
@@ -77,23 +77,19 @@ class OpTest {
     //              () -> bitvector_repeat_ot.getIntegerIndices());
 
     Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
-    int bitvector_zero_extend_idx =
-        bitvector_zero_extend_ot.getIntegerIndices()[0];
+    int bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIntegerIndices()[0];
     assertEquals(bitvector_zero_extend_idx, 6);
 
     Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
-    int bitvector_sign_extend_idx =
-        bitvector_sign_extend_ot.getIntegerIndices()[0];
+    int bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIntegerIndices()[0];
     assertEquals(bitvector_sign_extend_idx, 7);
 
     Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
-    int bitvector_rotate_left_idx =
-        bitvector_rotate_left_ot.getIntegerIndices()[0];
+    int bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIntegerIndices()[0];
     assertEquals(bitvector_rotate_left_idx, 8);
 
     Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
-    int bitvector_rotate_right_idx =
-        bitvector_rotate_right_ot.getIntegerIndices()[0];
+    int bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIntegerIndices()[0];
     assertEquals(bitvector_rotate_right_idx, 9);
 
     Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
@@ -101,18 +97,16 @@ class OpTest {
     assertEquals(int_to_bitvector_idx, 10);
 
     Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
-    int floatingpoint_to_ubv_idx =
-        floatingpoint_to_ubv_ot.getIntegerIndices()[0];
+    int floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIntegerIndices()[0];
     assertEquals(floatingpoint_to_ubv_idx, 11);
 
     Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
-    int floatingpoint_to_sbv_idx =
-        floatingpoint_to_sbv_ot.getIntegerIndices()[0];
+    int floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIntegerIndices()[0];
     assertEquals(floatingpoint_to_sbv_idx, 13);
   }
 
-  @Test
-  void getIndicesPairUint() throws CVC5ApiException {
+  @Test void getIndicesPairUint() throws CVC5ApiException
+  {
     Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
     assertTrue(bitvector_extract_ot.isIndexed());
     int[] bitvector_extract_indices = bitvector_extract_ot.getIntegerIndices();
@@ -122,47 +116,38 @@ class OpTest {
         d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_ieee_bitvector_indices =
         floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_floatingpoint_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
     int[] floatingpoint_to_fp_floatingpoint_indices =
         floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_real_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
-    int[] floatingpoint_to_fp_real_indices =
-        floatingpoint_to_fp_real_ot.getIntegerIndices();
+    Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
+    int[] floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_signed_bitvector_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_signed_bitvector_indices =
         floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_unsigned_bitvector_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_unsigned_bitvector_indices =
         floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_generic_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
-    int[] floatingpoint_to_fp_generic_indices =
-        floatingpoint_to_fp_generic_ot.getIntegerIndices();
+    Op floatingpoint_to_fp_generic_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
+    int[] floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_generic_indices, new int[] {4, 25});
-    assertThrows(CVC5ApiException.class,
-        () -> floatingpoint_to_fp_generic_ot.getStringIndices());
+    assertThrows(CVC5ApiException.class, () -> floatingpoint_to_fp_generic_ot.getStringIndices());
   }
 
-  @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();