summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CMakeLists.txt4
-rw-r--r--cmake/CVC4Config.cmake.in10
-rwxr-xr-xconfigure.sh4
-rw-r--r--examples/CMakeLists.txt4
-rw-r--r--src/api/java/CMakeLists.txt28
-rw-r--r--src/api/java/genkinds.py113
-rw-r--r--src/api/parsekinds.py158
-rw-r--r--src/api/python/genkinds.py187
8 files changed, 345 insertions, 163 deletions
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 843fc16c1..1bbe6d288 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -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()
#-----------------------------------------------------------------------------#
diff --git a/cmake/CVC4Config.cmake.in b/cmake/CVC4Config.cmake.in
index 38cd4ba8d..ac6bccb20 100644
--- a/cmake/CVC4Config.cmake.in
+++ b/cmake/CVC4Config.cmake.in
@@ -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()
+
diff --git a/configure.sh b/configure.sh
index ed84a7270..d57bcd5d5 100755
--- a/configure.sh
+++ b/configure.sh
@@ -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;;
diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 7022aa674..4f7f1332f 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -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
index 000000000..9c25e7393
--- /dev/null
+++ b/src/api/java/CMakeLists.txt
@@ -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
index 000000000..955e47bae
--- /dev/null
+++ b/src/api/java/genkinds.py
@@ -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
index 000000000..0b86d8cec
--- /dev/null
+++ b/src/api/parsekinds.py
@@ -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()
+
diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py
index c19364559..30ee18708 100644
--- a/src/api/python/genkinds.py
+++ b/src/api/python/genkinds.py
@@ -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")
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback