Fix Java target and Relations example (#4583)

Currently, our CVC4Config file is never including the CVC4 Java targets
because of a typo in `cmake/CVC4Config.cmake.in`. For this reason, our
build system for the examples would never actually build the examples.
Fixing this issue brought up another issue in our Relations Java example
that was using an outdated `System.loadLibrary()` call. This commit
fixes the typo and the example.

Note: Most changes in `Relations.java` were caused by ClangFormat.

diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index f60e99736bcca22364d0ab9683f5bde41a8de18f..0047cc0ecb6257b865db8ae9476a7488eb902c72 100644 (file)
--- a/cmake/CVC4Config.cmake.in
+++ b/cmake/CVC4Config.cmake.in
@@ -1,6 +1,6 @@
 @PACKAGE_INIT@
 
-set(CVC4_BINDINGS_JAVA @BUILD_BINDINGS_JAVA@)
+set(CVC4_BINDINGS_JAVA @BUILD_SWIG_BINDINGS_JAVA@)
 
 if(NOT TARGET CVC4::cvc4)
   include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)

diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index 86a39406206b2ce4f8685e0a7a5e2cd913e56065..ea26ebce314fd77c7ea494b5607a09ae6fdfa45e 100644 (file)
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -64,13 +64,9 @@ This file uses the API to make a sat call equivalent to the following benchmark:
 (get-model)
  */
 
-public
-class Relations
-{
- public
-  static void main(String[] args)
-  {
-    System.load("/usr/local/lib/libcvc4jni.so");
+public class Relations {
+  public static void main(String[] args) {
+    System.loadLibrary("cvc4jni");
 
     ExprManager manager = new ExprManager();
     SmtEngine smtEngine = new SmtEngine(manager);
@@ -134,9 +130,12 @@ class Relations
     // (assert (not (= females (as emptyset (Set (Tuple Person))))))
     Expr femaleSetIsNotEmpty = manager.mkExpr(Kind.NOT, isEmpty2);
 
-    // (assert (= (intersection males females) (as emptyset (Set (Tuple Person)))))
-    Expr malesFemalesIntersection = manager.mkExpr(Kind.INTERSECTION, males, females);
-    Expr malesAndFemalesAreDisjoint = manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr);
+    // (assert (= (intersection males females) (as emptyset (Set (Tuple
+    // Person)))))
+    Expr malesFemalesIntersection =
+        manager.mkExpr(Kind.INTERSECTION, males, females);
+    Expr malesAndFemalesAreDisjoint =
+        manager.mkExpr(Kind.EQUAL, malesFemalesIntersection, emptySetExpr);
 
     // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
     // (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
@@ -157,11 +156,13 @@ class Relations
 
     // (assert (= parent (union father mother)))
     Expr unionFatherMother = manager.mkExpr(Kind.UNION, father, mother);
-    Expr parentIsFatherOrMother = manager.mkExpr(Kind.EQUAL, parent, unionFatherMother);
+    Expr parentIsFatherOrMother =
+        manager.mkExpr(Kind.EQUAL, parent, unionFatherMother);
 
     // (assert (= parent (union father mother)))
     Expr transitiveClosure = manager.mkExpr(Kind.TCLOSURE, parent);
-    Expr descendantFormula = manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure);
+    Expr descendantFormula =
+        manager.mkExpr(Kind.EQUAL, descendant, transitiveClosure);
 
     // (assert (= parent (union father mother)))
     Expr transpose = manager.mkExpr(Kind.TRANSPOSE, descendant);
@@ -176,28 +177,29 @@ class Relations
     vectorExpr vectorExpr = new vectorExpr();
     vectorExpr.add(x);
     Expr quantifiedVariables = manager.mkExpr(Kind.BOUND_VAR_LIST, x);
-    Expr noSelfAncestor = manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember);
+    Expr noSelfAncestor =
+        manager.mkExpr(Kind.FORALL, quantifiedVariables, notMember);
 
     // formulas
     Expr formula1 = manager.mkExpr(Kind.AND,
-                                             peopleAreTheUniverse,
-                                             maleSetIsNotEmpty,
-                                             femaleSetIsNotEmpty,
-                                             malesAndFemalesAreDisjoint);
+        peopleAreTheUniverse,
+        maleSetIsNotEmpty,
+        femaleSetIsNotEmpty,
+        malesAndFemalesAreDisjoint);
 
     Expr formula2 = manager.mkExpr(Kind.AND,
-                                             formula1,
-                                             fatherIsNotEmpty,
-                                             motherIsNotEmpty,
-                                             fathersAreMales,
-                                             mothersAreFemales);
+        formula1,
+        fatherIsNotEmpty,
+        motherIsNotEmpty,
+        fathersAreMales,
+        mothersAreFemales);
 
     Expr formula3 = manager.mkExpr(Kind.AND,
-                                             formula2,
-                                             parentIsFatherOrMother,
-                                             descendantFormula,
-                                             ancestorFormula,
-                                             noSelfAncestor);
+        formula2,
+        parentIsFatherOrMother,
+        descendantFormula,
+        ancestorFormula,
+        noSelfAncestor);
 
     // check sat
     Result result = smtEngine.checkSat(formula3);