Generate cvc/Kind.java for the java API (#6143)
authormudathirmahgoub <mudathirmahgoub@gmail.com>
Sat, 20 Mar 2021 10:23:44 +0000 (05:23 -0500)
committerGitHub <noreply@github.com>
Sat, 20 Mar 2021 10:23:44 +0000 (05:23 -0500)
PR changes:

Refactor python/genkinds.py by separating parsing from file generation.
Add java/genkinds.py to generate file Kind.java.
Enable java API in ./configure.sh with "under development" warning.

CMakeLists.txt
cmake/CVC4Config.cmake.in
configure.sh
examples/CMakeLists.txt
src/api/java/CMakeLists.txt [new file with mode: 0644]
src/api/java/genkinds.py [new file with mode: 0644]
src/api/parsekinds.py [new file with mode: 0644]
src/api/python/genkinds.py

index 843fc16c17d6ef89a34006af3e184f7f70e8c141..1bbe6d28803518f464fee0308b43bc1c0da8ca4b 100644 (file)
@@ -565,8 +565,8 @@ if(BUILD_BINDINGS_PYTHON)
 endif()
 
 if(BUILD_BINDINGS_JAVA)
-  message(FATAL_ERROR
-    "Java bindings for the new API are not implemented yet.")
+  add_subdirectory(src/api/java)
+  message(WARNING "Java API is currently under development.")
 endif()
 
 #-----------------------------------------------------------------------------#
index 38cd4ba8d434e3d99254cdd67fe4cf17591f7806..ac6bccb20fdcc1e9c32a79235f4883eac5814010 100644 (file)
@@ -18,7 +18,9 @@ if(NOT TARGET CVC4::cvc4)
   include(${CMAKE_CURRENT_LIST_DIR}/CVC4Targets.cmake)
 endif()
 
-if(CVC4_BINDINGS_JAVA AND NOT TARGET CVC4::cvc4jar)
-  set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@")
-  include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake)
-endif()
+# TODO(project wishue #83): enable these lines
+# if(CVC4_BINDINGS_JAVA AND NOT TARGET CVC4::cvc4jar)
+#  set_and_check(CVC4_JNI_PATH "@PACKAGE_LIBRARY_INSTALL_DIR@")
+# include(${CMAKE_CURRENT_LIST_DIR}/CVC4JavaTargets.cmake)
+# endif()
+
index ed84a7270dd16be18b001e355b8702f70c729654..d57bcd5d500053fb45024c62833c4cda78574ec6 100755 (executable)
@@ -295,7 +295,9 @@ do
     --java-bindings) java_bindings=ON;;
     --no-java-bindings) java_bindings=OFF;;
 
-    --all-bindings) python_bindings=ON;;
+    --all-bindings)
+      python_bindings=ON
+      java_bindings=ON;;
 
     --valgrind) valgrind=ON;;
     --no-valgrind) valgrind=OFF;;
index 7022aa6746728382fb873a92cf54847b71684d74..4f7f1332f2f56708a7aeada8370023d9a2dd7b95 100644 (file)
@@ -96,8 +96,8 @@ if(TARGET CVC4::cvc4jar)
   #       -Djava.library.path=${CVC4_JNI_PATH}
   #       SimpleVC
   # )
-
-  add_subdirectory(api/java)
+  # TODO(project wishue #83): enable java examples
+  add_subdirectory(api/java)
 endif()
 
 if(CVC4_BINDINGS_PYTHON)
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
new file mode 100644 (file)
index 0000000..9c25e73
--- /dev/null
@@ -0,0 +1,28 @@
+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+##   Mudathir Mohamed
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+
+# create a directory for the cvc package
+file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/cvc")
+
+# Generate cvc/Kind.java
+add_custom_target(
+  gen-java-kinds
+  ALL
+  COMMAND
+    "${PYTHON_EXECUTABLE}"
+    "${CMAKE_CURRENT_LIST_DIR}/genkinds.py"
+    --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cvc4cppkind.h"
+    --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc/Kind"
+  DEPENDS
+    genkinds.py
+  COMMENT
+    "Generate Kind.java"
+)
diff --git a/src/api/java/genkinds.py b/src/api/java/genkinds.py
new file mode 100644 (file)
index 0000000..955e47b
--- /dev/null
@@ -0,0 +1,113 @@
+#!/usr/bin/env python
+#
+# genkinds.py
+# Top contributors (to current version):
+#   Mudathir Mohamed
+# This file is part of the CVC4 project.
+# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+# in the top-level source directory and their institutional affiliations.
+# All rights reserved.  See the file COPYING in the top-level source
+# directory for licensing information.
+#
+
+"""
+This script reads CVC4/src/api/cvc4cppkind.h and generates
+cvc/Kind.java file which declare all the CVC4 kinds.
+"""
+
+import argparse
+import os
+import sys
+
+# the following command in CVC4/build/src/api/java/CMakeFiles/gen-java-kinds.dir/build.make
+# cd CVC4/build/src/api/java && /usr/bin/python3 CVC4/src/api/java/genkinds.py ...
+# indicates we are in directory CVC4/build/src/api/java
+# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py
+sys.path.insert(0, os.path.abspath('../../../../src/api'))
+
+from parsekinds import *
+
+# Default Filenames
+DEFAULT_PREFIX = 'Kind'
+
+# Code Blocks
+
+KINDS_JAVA_TOP = \
+    r"""package cvc;
+
+import java.util.HashMap;
+import java.util.Map;
+
+public enum Kind 
+{
+"""
+
+KINDS_JAVA_BOTTOM = \
+    r""";
+
+  /* the int value of the kind */
+  private int value;
+  private static Map<Integer, Kind> kindMap = new HashMap<>();
+  private Kind(int value)
+  {
+    this.value = value;
+  }
+
+  static
+  {
+    for (Kind kind : Kind.values())
+    {
+      kindMap.put(kind.getValue(), kind);
+    }
+  }
+
+  public static Kind fromInt(int value) throws CVCApiException
+  {
+    if (value < INTERNAL_KIND.value || value > LAST_KIND.value)
+    {
+      throw new CVCApiException("Kind value " + value + " is outside the valid range ["
+          + INTERNAL_KIND.value + "," + LAST_KIND.value + "]");
+    }
+    return kindMap.get(value);
+  }
+
+  public int getValue()
+  {
+    return value;
+  }
+}
+"""
+
+
+# Files generation
+
+def gen_java(parser: KindsParser, filename):
+    f = open(filename, "w")
+    code = KINDS_JAVA_TOP
+    enum_value = -2  # initial enum value
+    for kind, name in parser.kinds.items():
+        code += "  {name}({enum_value}),\n".format(name=kind, enum_value=enum_value)
+        enum_value = enum_value + 1
+    code += KINDS_JAVA_BOTTOM
+    f.write(code)
+    f.close()
+
+
+if __name__ == "__main__":
+    parser = argparse.ArgumentParser('Read a kinds header file and generate a '
+                                     'corresponding java file')
+    parser.add_argument('--kinds-header', metavar='<KINDS_HEADER>',
+                        help='The header file to read kinds from',
+                        default=DEFAULT_HEADER)
+    parser.add_argument('--kinds-file-prefix', metavar='<KIND_FILE_PREFIX>',
+                        help='The prefix for the generated .java file',
+                        default=DEFAULT_PREFIX)
+
+    args = parser.parse_args()
+    kinds_header = args.kinds_header
+    kinds_file_prefix = args.kinds_file_prefix
+
+    kp = KindsParser()
+    kp.parse(kinds_header)
+
+    gen_java(kp, kinds_file_prefix + ".java")
diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py
new file mode 100644 (file)
index 0000000..0b86d8c
--- /dev/null
@@ -0,0 +1,158 @@
+#!/usr/bin/env python
+#####################
+## genkinds.py
+## Top contributors (to current version):
+##   Makai Mann
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved.  See the file COPYING in the top-level source
+## directory for licensing information.
+##
+
+"""
+This script implements KindsParser which
+parses the header file CVC4/src/api/cvc4cppkind.h
+
+The script is aware of the '#if 0' pattern and will ignore
+kinds declared between '#if 0' and '#endif'. It can also
+handle nested '#if 0' pairs.
+"""
+
+from collections import OrderedDict
+
+#################### Default Filenames ################
+DEFAULT_HEADER = 'cvc4cppkind.h'
+
+##################### Useful Constants ################
+OCB = '{'
+CCB = '}'
+SC = ';'
+EQ = '='
+C = ','
+US = '_'
+NL = '\n'
+
+# Enum Declarations
+ENUM_START = 'enum CVC4_EXPORT Kind'
+ENUM_END = CCB + SC
+
+# Comments and Macro Tokens
+COMMENT = '//'
+BLOCK_COMMENT_BEGIN = '/*'
+BLOCK_COMMENT_END = '*/'
+MACRO_BLOCK_BEGIN = '#if 0'
+MACRO_BLOCK_END = '#endif'
+
+# Format Kind Names
+# special cases for format_name
+_IS = '_IS'
+# replacements after some preprocessing
+replacements = {
+    'Bitvector': 'BV',
+    'Floatingpoint': 'FP'
+}
+
+
+class KindsParser:
+    tokenmap = {
+        BLOCK_COMMENT_BEGIN: BLOCK_COMMENT_END,
+        MACRO_BLOCK_BEGIN: MACRO_BLOCK_END
+    }
+
+    def __init__(self):
+        self.kinds = OrderedDict()
+        self.endtoken = None
+        self.endtoken_stack = []
+        self.in_kinds = False
+
+    def format_name(self, name):
+        '''
+        In the Python API, each Kind name is reformatted for easier use
+
+        The naming scheme is:
+           1. capitalize the first letter of each word (delimited by underscores)
+           2. make the rest of the letters lowercase
+           3. replace Floatingpoint with FP
+           4. replace Bitvector with BV
+
+        There is one exception:
+           FLOATINGPOINT_ISNAN  --> FPIsNan
+
+        For every "_IS" in the name, there's an underscore added before step 1,
+           so that the word after "Is" is capitalized
+
+        Examples:
+           BITVECTOR_PLUS      -->  BVPlus
+           APPLY_SELECTOR      -->  ApplySelector
+           FLOATINGPOINT_ISNAN -->  FPIsNan
+           SETMINUS            -->  Setminus
+
+        See the generated .pxi file for an explicit mapping
+        '''
+        name = name.replace(_IS, _IS + US)
+        words = [w.capitalize() for w in name.lower().split(US)]
+        name = "".join(words)
+
+        for og, new in replacements.items():
+            name = name.replace(og, new)
+
+        return name
+
+    def ignore_block(self, line):
+        '''
+        Returns a boolean telling self.parse whether to ignore a line or not.
+        It also updates all the necessary state to track comments and macro
+        blocks
+        '''
+
+        # check if entering block comment or macro block
+        for token in self.tokenmap:
+            if token in line:
+                if self.tokenmap[token] not in line:
+                    if self.endtoken is not None:
+                        self.endtoken_stack.append(self.endtoken)
+                    self.endtoken = self.tokenmap[token]
+                return True
+
+        # check if currently in block comment or macro block
+        if self.endtoken is not None:
+            # check if reached the end of block comment or macro block
+            if self.endtoken in line:
+                if self.endtoken_stack:
+                    self.endtoken = self.endtoken_stack.pop()
+                else:
+                    self.endtoken = None
+            return True
+
+        return False
+
+    def parse(self, filename):
+        f = open(filename, "r")
+
+        for line in f.read().split(NL):
+            line = line.strip()
+            if COMMENT in line:
+                line = line[:line.find(COMMENT)]
+            if not line:
+                continue
+
+            if self.ignore_block(line):
+                continue
+
+            if ENUM_END in line:
+                self.in_kinds = False
+                break
+            elif self.in_kinds:
+                if line == OCB:
+                    continue
+                if EQ in line:
+                    line = line[:line.find(EQ)].strip()
+                elif C in line:
+                    line = line[:line.find(C)].strip()
+                self.kinds[line] = self.format_name(line)
+            elif ENUM_START in line:
+                self.in_kinds = True
+                continue
+        f.close()
+
index c193645597d3474c4a5363f83be73b75002ed806..30ee187080fa810aba764034bf4648ffb2667548 100644 (file)
@@ -22,41 +22,22 @@ handle nested '#if 0' pairs.
 """
 
 import argparse
-from collections import OrderedDict
+import os
+import sys
 
-#################### Default Filenames ################
-DEFAULT_HEADER      = 'cvc4cppkind.h'
-DEFAULT_PREFIX      = 'kinds'
+# the following command in CVC4/build/src/api/python/CMakeFiles/gen-pycvc4-kinds.dir/build.make
+# cd CVC4/build/src/api/python && /usr/bin/python3 CVC4/src/api/python/genkinds.py ...
+# indicates we are in directory CVC4/build/src/api/python
+# so we use ../../../../src/api to access CVC4/src/api/parsekinds.py
+sys.path.insert(0, os.path.abspath('../../../../src/api'))
 
-##################### Useful Constants ################
-OCB                 = '{'
-CCB                 = '}'
-SC                  = ';'
-EQ                  = '='
-C                   = ','
-US                  = '_'
-NL                  = '\n'
+from parsekinds import *
 
-#################### Enum Declarations ################
-ENUM_START          = 'enum CVC4_EXPORT Kind'
-ENUM_END            = CCB+SC
+#################### Default Filenames ################
+DEFAULT_PREFIX = 'kinds'
 
 ################ Comments and Macro Tokens ############
 PYCOMMENT           = '#'
-COMMENT             = '//'
-BLOCK_COMMENT_BEGIN = '/*'
-BLOCK_COMMENT_END   = '*/'
-MACRO_BLOCK_BEGIN   = '#if 0'
-MACRO_BLOCK_END     = '#endif'
-
-#################### Format Kind Names ################
-# special cases for format_name
-_IS                 = '_IS'
-# replacements after some preprocessing
-replacements        = {
-    'Bitvector'    : 'BV',
-    'Floatingpoint': 'FP'
-}
 
 ####################### Code Blocks ###################
 CDEF_KIND = "    cdef Kind "
@@ -126,130 +107,28 @@ cdef kind {name} = kind(<int> {kind})
 setattr(kinds, "{name}", {name})
 """
 
-class KindsParser:
-    tokenmap = {
-        BLOCK_COMMENT_BEGIN : BLOCK_COMMENT_END,
-        MACRO_BLOCK_BEGIN   : MACRO_BLOCK_END
-    }
-
-    def __init__(self):
-        self.kinds = OrderedDict()
-        self.endtoken = None
-        self.endtoken_stack = []
-        self.in_kinds = False
-
-    def format_name(self, name):
-        '''
-        In the Python API, each Kind name is reformatted for easier use
-
-        The naming scheme is:
-           1. capitalize the first letter of each word (delimited by underscores)
-           2. make the rest of the letters lowercase
-           3. replace Floatingpoint with FP
-           4. replace Bitvector with BV
-
-        There is one exception:
-           FLOATINGPOINT_ISNAN  --> FPIsNan
-
-        For every "_IS" in the name, there's an underscore added before step 1,
-           so that the word after "Is" is capitalized
-
-        Examples:
-           BITVECTOR_PLUS      -->  BVPlus
-           APPLY_SELECTOR      -->  ApplySelector
-           FLOATINGPOINT_ISNAN -->  FPIsNan
-           SETMINUS            -->  Setminus
-
-        See the generated .pxi file for an explicit mapping
-        '''
-        name = name.replace(_IS, _IS+US)
-        words = [w.capitalize() for w in name.lower().split(US)]
-        name = "".join(words)
-
-        for og, new in replacements.items():
-            name = name.replace(og, new)
-
-        return name
-
-    def ignore_block(self, line):
-        '''
-        Returns a boolean telling self.parse whether to ignore a line or not.
-        It also updates all the necessary state to track comments and macro
-        blocks
-        '''
-
-        # check if entering block comment or macro block
-        for token in self.tokenmap:
-            if token in line:
-                if self.tokenmap[token] not in line:
-                    if self.endtoken is not None:
-                        self.endtoken_stack.append(self.endtoken)
-                    self.endtoken = self.tokenmap[token]
-                return True
-
-        # check if currently in block comment or macro block
-        if self.endtoken is not None:
-            # check if reached the end of block comment or macro block
-            if self.endtoken in line:
-                if self.endtoken_stack:
-                    self.endtoken = self.endtoken_stack.pop()
-                else:
-                    self.endtoken =None
-            return True
-
-        return False
-
-    def parse(self, filename):
-        f = open(filename, "r")
-
-        for line in f.read().split(NL):
-            line = line.strip()
-            if COMMENT in line:
-                line = line[:line.find(COMMENT)]
-            if not line:
-                continue
-
-            if self.ignore_block(line):
-                continue
-
-            if ENUM_END in line:
-                self.in_kinds = False
-                break
-            elif self.in_kinds:
-                if line == OCB:
-                    continue
-                if EQ in line:
-                    line = line[:line.find(EQ)].strip()
-                elif C in line:
-                    line = line[:line.find(C)].strip()
-                self.kinds[line] = self.format_name(line)
-            elif ENUM_START in line:
-                self.in_kinds = True
-                continue
-
-        f.close()
-
-    def gen_pxd(self, filename):
-        f = open(filename, "w")
-        f.write(KINDS_PXD_TOP)
-        # include the format_name docstring in the generated file
-        # could be helpful for users to see the formatting rules
-        for line in self.format_name.__doc__.split(NL):
-            f.write(PYCOMMENT)
-            if not line.isspace():
-                f.write(line)
-            f.write(NL)
-        for kind in self.kinds:
-            f.write(CDEF_KIND + kind + NL)
-        f.close()
 
-    def gen_pxi(self, filename):
-        f = open(filename, "w")
-        pxi = KINDS_PXI_TOP
-        for kind, name in self.kinds.items():
-            pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind)
-        f.write(pxi)
-        f.close()
+def gen_pxd(parser: KindsParser, filename):
+    f = open(filename, "w")
+    f.write(KINDS_PXD_TOP)
+    # include the format_name docstring in the generated file
+    # could be helpful for users to see the formatting rules
+    for line in parser.format_name.__doc__.split(NL):
+        f.write(PYCOMMENT)
+        if not line.isspace():
+            f.write(line)
+        f.write(NL)
+    for kind in parser.kinds:
+        f.write(CDEF_KIND + kind + NL)
+    f.close()
+
+def gen_pxi(parser : KindsParser, filename):
+    f = open(filename, "w")
+    pxi = KINDS_PXI_TOP
+    for kind, name in parser.kinds.items():
+        pxi += KINDS_ATTR_TEMPLATE.format(name=name, kind=kind)
+    f.write(pxi)
+    f.close()
 
 
 if __name__ == "__main__":
@@ -270,5 +149,5 @@ if __name__ == "__main__":
     kp = KindsParser()
     kp.parse(kinds_header)
 
-    kp.gen_pxd(kinds_file_prefix + ".pxd")
-    kp.gen_pxi(kinds_file_prefix + ".pxi")
+    gen_pxd(kp, kinds_file_prefix + ".pxd")
+    gen_pxi(kp, kinds_file_prefix + ".pxi")