From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 9 Jun 2020 04:20:25 +0000 (-0700)
Subject: Fix Java target and Relations example (#4583)
X-Git-Tag: cvc5-1.0.0~3237
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=84c72e3c371dc916604e66f4af4f138833f7c11b;p=cvc5.git

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 f60e99736..0047cc0ec 100644
--- 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 86a394062..ea26ebce3 100644
--- 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);