From fb54473f59d21a3125f67dc1f8f834431bc207f5 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 25 Mar 2022 13:28:12 -0700 Subject: [PATCH] Generate `enum` bindings for Python and Java (#8393) This commit generalizes the generation of bindings for enums to include enums in cvc5_types.h. The commit only generates the bindings, but does not use them yet (e.g., do add an argument to Solver::blockModels()). The generated Java bindings already respect the C++ namespace whereas the Python bindings require a minor restructuring to make the namespaces work (i.e., instead of cvc5kinds, we should have cvc5.api.kinds). --- src/CMakeLists.txt | 2 + src/api/cpp/cvc5.h | 1 + src/api/cpp/cvc5_kind.h | 6 +- src/api/cpp/cvc5_types.h | 33 ++++ src/api/java/CMakeLists.txt | 36 +++- .../java/{genkinds.py.in => genenums.py.in} | 74 ++++---- src/api/{parsekinds.py => parseenums.py} | 136 +++++++++----- src/api/python/CMakeLists.txt | 39 +++- src/api/python/genenums.py.in | 174 ++++++++++++++++++ src/api/python/genkinds.py.in | 166 ----------------- 10 files changed, 401 insertions(+), 266 deletions(-) create mode 100644 src/api/cpp/cvc5_types.h rename src/api/java/{genkinds.py.in => genenums.py.in} (59%) rename src/api/{parsekinds.py => parseenums.py} (53%) create mode 100644 src/api/python/genenums.py.in delete mode 100644 src/api/python/genkinds.py.in diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 063930fa6..f263bdc72 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -19,6 +19,7 @@ libcvc5_add_sources( api/cpp/cvc5.h api/cpp/cvc5_checks.h api/cpp/cvc5_kind.h + api/cpp/cvc5_types.h decision/assertion_list.cpp decision/assertion_list.h decision/decision_engine.cpp @@ -1404,6 +1405,7 @@ add_subdirectory(main) install(FILES api/cpp/cvc5.h api/cpp/cvc5_kind.h + api/cpp/cvc5_types.h DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/cvc5/) install(FILES diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 026a7365b..16552edb7 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -30,6 +30,7 @@ #include #include "api/cpp/cvc5_kind.h" +#include "api/cpp/cvc5_types.h" namespace cvc5 { diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 4e9bedab5..57e8133b3 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -20,8 +20,7 @@ #include -namespace cvc5 { -namespace api { +namespace cvc5::api { /* -------------------------------------------------------------------------- */ /* Kind */ @@ -4113,8 +4112,7 @@ std::string kindToString(Kind k) CVC5_EXPORT; */ std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT; -} // namespace api -} // namespace cvc5 +} // namespace cvc5::api namespace std { diff --git a/src/api/cpp/cvc5_types.h b/src/api/cpp/cvc5_types.h new file mode 100644 index 000000000..3ce20688b --- /dev/null +++ b/src/api/cpp/cvc5_types.h @@ -0,0 +1,33 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andres Noetzli + * + * This file is part of the cvc5 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. + * **************************************************************************** + * + * Common cvc5 types. + */ + +#include "cvc5_export.h" + +#ifndef CVC5__API__CVC5_TYPES_H +#define CVC5__API__CVC5_TYPES_H + +namespace cvc5::modes { + +enum BlockModelsMode +{ + /** Block models based on the SAT skeleton. */ + LITERALS, + /** Block models based on the concrete model values for the free variables. */ + VALUES +}; + +} + +#endif diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt index 342a37394..da4fa60c4 100644 --- a/src/api/java/CMakeLists.txt +++ b/src/api/java/CMakeLists.txt @@ -18,29 +18,45 @@ file(MAKE_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api") set(JNI_DIR "${CMAKE_CURRENT_BINARY_DIR}/jni") file(MAKE_DIRECTORY ${JNI_DIR}) -# Generate Kind.java -configure_file(genkinds.py.in genkinds.py) +configure_file(genenums.py.in genenums.py) +# Generate Kind.java set(JAVA_KIND_FILE "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/Kind.java" ) - add_custom_command( OUTPUT ${JAVA_KIND_FILE} COMMAND "${PYTHON_EXECUTABLE}" - "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/Kind" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" + --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/" DEPENDS - "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - "${PROJECT_SOURCE_DIR}/src/api/parsekinds.py" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" ) - add_custom_target(generate-java-kinds DEPENDS ${JAVA_KIND_FILE}) +set(JAVA_TYPES_FILES + "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/api/BlockModelsMode.java" +) +add_custom_command( + OUTPUT + ${JAVA_TYPES_FILES} + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_types.h" + --java-api-path "${CMAKE_CURRENT_BINARY_DIR}/io/github/cvc5/" + DEPENDS + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" + "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_types.h" +) +add_custom_target(generate-java-types DEPENDS ${JAVA_TYPES_FILES}) + # find java find_package(Java COMPONENTS Development REQUIRED) include(UseJava) @@ -93,7 +109,7 @@ add_custom_command( ) add_custom_target(generate-jni-headers DEPENDS ${JNI_HEADERS}) -add_dependencies(generate-jni-headers generate-java-kinds) +add_dependencies(generate-jni-headers generate-java-kinds generate-java-types) # find jni package find_package(JNI REQUIRED) diff --git a/src/api/java/genkinds.py.in b/src/api/java/genenums.py.in similarity index 59% rename from src/api/java/genkinds.py.in rename to src/api/java/genenums.py.in index 41f02d221..5ecd5bd40 100644 --- a/src/api/java/genkinds.py.in +++ b/src/api/java/genenums.py.in @@ -22,27 +22,28 @@ import sys import re import textwrap -# get access to cvc5/src/api/parsekinds.py -sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api')) +# get access to cvc5/src/api/parseenums.py +SOURCE_DIR = '${CMAKE_SOURCE_DIR}/src' +sys.path.insert(0, os.path.abspath(f'{SOURCE_DIR}/api')) -from parsekinds import * +from parseenums import * -# Default Filenames +#################### Default Filenames ################ DEFAULT_PREFIX = 'Kind' # Code Blocks -KINDS_JAVA_TOP = \ - r"""package io.github.cvc5.api; +ENUM_JAVA_TOP = \ + r"""package io.github.cvc5.{namespace}; import java.util.HashMap; import java.util.Map; -public enum Kind -{ +public enum {name} +{{ """ -KINDS_JAVA_BOTTOM = \ +ENUM_JAVA_BOTTOM = \ r"""; /* the int value of the kind */ @@ -112,36 +113,43 @@ def format_comment(comment): # Files generation -def gen_java(parser: KindsParser, filename): - f = open(filename, "w") - code = KINDS_JAVA_TOP - enum_value = -2 # initial enum value - for kind, comment in parser.kinds_doc.items(): - comment = format_comment(comment) - code += "{comment}\n {name}({enum_value}),\n".format( - comment=comment, name=kind, enum_value=enum_value) - enum_value = enum_value + 1 - code += KINDS_JAVA_BOTTOM - f.write(code) - f.close() +def gen_java(parser: EnumParser, path): + for namespace in parser.namespaces: + for enum in namespace.enums: + subnamespace = namespace.name.split('::')[1] + filedir = os.path.join(path, subnamespace) + if not os.path.exists(filedir): + os.mkdir(filedir) + filename = os.path.join(filedir, enum.name + ".java") + with open(filename, "w") as f: + code = ENUM_JAVA_TOP.format(name=enum.name, + namespace=subnamespace) + for name, value in enum.enumerators.items(): + comment = enum.enumerators_doc.get(name, '') + comment = format_comment(comment) + code += "{comment}\n {name}({enum_value}),\n".format( + comment=comment, name=name, enum_value=value) + code += ENUM_JAVA_BOTTOM + f.write(code) if __name__ == "__main__": - parser = argparse.ArgumentParser('Read a kinds header file and generate a ' - 'corresponding java file') - parser.add_argument('--kinds-header', - metavar='', - help='The header file to read kinds from') - parser.add_argument('--kinds-file-prefix', - metavar='', + parser = argparse.ArgumentParser( + 'Read an enums header file and generate a ' + 'corresponding java file') + parser.add_argument('--enums-header', + metavar='', + help='The header file to read enums from') + parser.add_argument('--java-api-path', + metavar='', 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 + enums_header = args.enums_header + java_api_path = args.java_api_path - kp = KindsParser() - kp.parse(kinds_header) + ep = EnumParser() + ep.parse(enums_header) - gen_java(kp, kinds_file_prefix + ".java") + gen_java(ep, java_api_path) diff --git a/src/api/parsekinds.py b/src/api/parseenums.py similarity index 53% rename from src/api/parsekinds.py rename to src/api/parseenums.py index 6eee76693..172d46089 100644 --- a/src/api/parsekinds.py +++ b/src/api/parseenums.py @@ -12,12 +12,11 @@ # ############################################################################# ## """ -This script implements KindsParser which -parses the header file cvc5/src/api/cpp/cvc5_kind.h +This script implements EnumParser which parses a header file that defines +enums. -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. +The script is aware of the '#if 0' pattern and will ignore enum values declared +between '#if 0' and '#endif'. It can also handle nested '#if 0' pairs. """ from collections import OrderedDict @@ -32,8 +31,10 @@ C = ',' US = '_' NL = '\n' +NAMESPACE_START = 'namespace' + # Expected C++ Enum Declarations -ENUM_START = 'enum Kind' +ENUM_START = 'enum' ENUM_END = CCB + SC # Comments and Macro Tokens @@ -44,30 +45,58 @@ MACRO_BLOCK_BEGIN = '#if 0' MACRO_BLOCK_END = '#endif' -class KindsParser: +class CppNamespace: + + def __init__(self, name): + # The name of the namespace + self.name = name + # The enums in this namespace + self.enums = [] + + +class CppEnum: + + def __init__(self, name): + # The name of the enum + self.name = name + # dictionary from C++ value name to shortened name + self.enumerators = OrderedDict() + # dictionary from shortened name to documentation comment + self.enumerators_doc = OrderedDict() + + +class EnumParser: tokenmap = { BLOCK_COMMENT_BEGIN: BLOCK_COMMENT_END, MACRO_BLOCK_BEGIN: MACRO_BLOCK_END } def __init__(self): - # dictionary from shortened name to documentation comment - self.kinds_doc = OrderedDict() + # the namespaces that have been parsed + self.namespaces = [] # the end token for the current type of block # none if not in a block comment or macro self.endtoken = None # stack of end tokens self.endtoken_stack = [] - # boolean that is true when in the kinds enum - self.in_kinds = False - # latest block comment - used for kinds documentation + # boolean that is true when in an enum + self.in_enum = False + # latest block comment - used for enums documentation self.latest_block_comment = "" + # The value of the last enumerator + self.last_value = -1 + + def get_current_namespace(self): + ''' + Returns the namespace that is currently being parsed + ''' + return self.namespaces[-1] - def get_comment(self, kind_name): + def get_current_enum(self): ''' - Look up a documentation comment for a Kind by C++ name + Returns the enum that is currently being parsed ''' - return self.kinds_doc[kind_name] + return self.get_current_namespace().enums[-1] def format_comment(self, comment): ''' @@ -120,32 +149,53 @@ class KindsParser: 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: + with open(filename, "r") as f: + for line in f: + 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_enum = False + break + elif self.in_enum: + if line == OCB: + continue + name = None + value = None + if EQ in line: + (name, remainder) = line.split(EQ) + name = name.strip() + if C in remainder: + value = int(remainder[:remainder.find(C)].strip()) + else: + value = int(remainder) + elif C in line: + name = line[:line.find(C)].strip() + else: + name = line + + if not value: + value = self.last_value + 1 + self.last_value = value + + enum = self.get_current_enum() + enum.enumerators[name] = value + fmt_comment = self.format_comment( + self.latest_block_comment) + enum.enumerators_doc[name] = fmt_comment + elif ENUM_START in line: + self.in_enum = True + tokens = line.split() + name = tokens[1] + self.get_current_namespace().enums.append(CppEnum(name)) continue - name = line - if EQ in line: - name = line[:line.find(EQ)].strip() - elif C in line: - name = line[:line.find(C)].strip() - fmt_comment = self.format_comment(self.latest_block_comment) - self.kinds_doc[name] = fmt_comment - elif ENUM_START in line: - self.in_kinds = True - continue - f.close() + elif line.startswith(NAMESPACE_START): + tokens = line.split() + name = tokens[1] + self.namespaces.append(CppNamespace(name)) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 99f7ee49b..60c1e0d93 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -48,27 +48,46 @@ find_package(Cython 0.29 REQUIRED) set(CYTHON_FLAGS "-X embedsignature=True") +configure_file(genenums.py.in genenums.py) + # Generate cvc5kinds.{pxd,pyx} -configure_file(genkinds.py.in genkinds.py) -set(GENERATED_FILES +set(GENERATED_KINDS_FILES "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxd" "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds.pxi" ) add_custom_command( OUTPUT - ${GENERATED_FILES} + ${GENERATED_KINDS_FILES} COMMAND "${PYTHON_EXECUTABLE}" - "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - --kinds-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" - --kinds-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" + --enums-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5kinds" DEPENDS - "${CMAKE_CURRENT_BINARY_DIR}/genkinds.py" - "${PROJECT_SOURCE_DIR}/src/api/parsekinds.py" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_kind.h" ) +add_custom_target(cvc5kinds DEPENDS ${GENERATED_KINDS_FILES}) -add_custom_target(cvc5kinds DEPENDS ${GENERATED_FILES}) +set(GENERATED_TYPES_FILES + "${CMAKE_CURRENT_BINARY_DIR}/cvc5types.pxd" + "${CMAKE_CURRENT_BINARY_DIR}/cvc5types.pxi" +) +add_custom_command( + OUTPUT + ${GENERATED_TYPES_FILES} + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + --enums-header "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_types.h" + --enums-file-prefix "${CMAKE_CURRENT_BINARY_DIR}/cvc5types" + DEPENDS + "${CMAKE_CURRENT_BINARY_DIR}/genenums.py" + "${PROJECT_SOURCE_DIR}/src/api/parseenums.py" + "${PROJECT_SOURCE_DIR}/src/api/cpp/cvc5_types.h" +) +add_custom_target(cvc5types DEPENDS ${GENERATED_TYPES_FILES}) include_directories(${CMAKE_CURRENT_BINARY_DIR}) # for cvc5kinds.pxi add_cython_target(cvc5_python_base CXX) @@ -76,7 +95,7 @@ add_cython_target(cvc5_python_base CXX) add_library(cvc5_python_base MODULE cvc5_python_base) -add_dependencies(cvc5_python_base cvc5kinds) +add_dependencies(cvc5_python_base cvc5kinds cvc5types) target_include_directories(cvc5_python_base PRIVATE diff --git a/src/api/python/genenums.py.in b/src/api/python/genenums.py.in new file mode 100644 index 000000000..abfce6a25 --- /dev/null +++ b/src/api/python/genenums.py.in @@ -0,0 +1,174 @@ +#!/usr/bin/env python +############################################################################### +# Top contributors (to current version): +# Makai Mann, Mudathir Mohamed, Aina Niemetz +# +# This file is part of the cvc5 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 a file that defines enums and generates .pxd and .pxi files +which declare all the enum values and implement a Python wrapper for values, +respectively. The default names are kinds.pxd / kinds.pxi, but the name is +configurable from the command line with --enums-file-prefix. + +The script is aware of the '#if 0' pattern and will ignore values declared +between '#if 0' and '#endif'. It can also handle nested '#if 0' pairs. +""" + +import argparse +import os +import re +import sys + +# get access to cvc5/src/api/parseenums.py +SOURCE_DIR = '${CMAKE_SOURCE_DIR}/src' +sys.path.insert(0, os.path.abspath(f'{SOURCE_DIR}/api')) + +from parseenums import * + +#################### Default Filenames ################ +DEFAULT_PREFIX = 'kinds' + +################ Comments and Macro Tokens ############ +PYCOMMENT = '#' + +ENUMS_PXD_TOP_TEMPLATE = \ +r"""cdef extern from "{header}" namespace "{namespace}": + cdef enum {enum}: +""" + +ENUMS_PXI_TOP = \ +r'''# distutils: language = c++ +# distutils: extra_compile_args = -std=c++11 + +from {basename} cimport {enum} as c_{enum} +from enum import Enum + +class {enum}(Enum): + """The {enum} enum""" + def __new__(cls, value, doc): + self = object.__new__(cls) + self._value_ = value + self.__doc__ = doc + return self +''' + +ENUMS_ATTR_TEMPLATE = r''' {name}=c_{enum}.{cpp_name}, """{doc}""" +''' + +# Format Kind Names +# special cases for format_name +_IS = '_IS' +# replacements after some preprocessing +replacements = {'Bitvector': 'BV', 'Floatingpoint': 'FP'} + + +def format_name(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_IS_NAN --> 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_ADD --> BVAdd + APPLY_SELECTOR --> ApplySelector + FLOATINGPOINT_IS_NAN --> FPIsNan + SET_MINUS --> 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 + + +comment_repls = { + '`Solver::([a-zA-Z]+)\(([^)]*)\)[^`]*`': ':py:meth:`pycvc5.Solver.\\1`', +} + + +def reformat_comment(comment): + for pat, repl in comment_repls.items(): + comment = re.sub(pat, repl, comment) + return comment + + +def gen_pxd(parser: EnumParser, file_prefix, header): + with open(file_prefix + ".pxd", "w") as f: + for namespace in parser.namespaces: + for enum in namespace.enums: + # include the format_name docstring in the generated file + # could be helpful for users to see the formatting rules + for line in format_name.__doc__.split(NL): + f.write(PYCOMMENT) + if not line.isspace(): + f.write(line) + f.write(NL) + f.write( + ENUMS_PXD_TOP_TEMPLATE.format(header=header[len(SOURCE_DIR) + + 1:], + enum=enum.name, + namespace=namespace.name)) + for enumerator in enum.enumerators: + f.write(" {},\n".format(enumerator)) + + +def gen_pxi(parser: EnumParser, file_prefix): + basename = file_prefix[file_prefix.rfind("/") + 1:] + with open(file_prefix + ".pxi", "w") as f: + for namespace in parser.namespaces: + for enum in namespace.enums: + f.write(ENUMS_PXI_TOP.format(basename=basename, + enum=enum.name)) + for name, value in enum.enumerators.items(): + doc = reformat_comment(enum.enumerators_doc.get(name, '')) + f.write( + ENUMS_ATTR_TEMPLATE.format(name=format_name(name), + enum=enum.name, + cpp_name=name, + doc=doc)) + + +if __name__ == "__main__": + parser = argparse.ArgumentParser( + 'Read a header with enums and generate a ' + 'corresponding pxd file, with simplified enum names.') + parser.add_argument('--enums-header', + metavar='', + help='The header file to read enums from') + parser.add_argument('--enums-file-prefix', + metavar='', + help='The prefix for the .pxd and .pxi files to write ' + 'the Cython declarations to.', + default=DEFAULT_PREFIX) + + args = parser.parse_args() + enums_header = args.enums_header + enums_file_prefix = args.enums_file_prefix + + kp = EnumParser() + kp.parse(enums_header) + + gen_pxd(kp, enums_file_prefix, enums_header) + gen_pxi(kp, enums_file_prefix) diff --git a/src/api/python/genkinds.py.in b/src/api/python/genkinds.py.in deleted file mode 100644 index 5af6e79a5..000000000 --- a/src/api/python/genkinds.py.in +++ /dev/null @@ -1,166 +0,0 @@ -#!/usr/bin/env python -############################################################################### -# Top contributors (to current version): -# Makai Mann, Mudathir Mohamed, Aina Niemetz -# -# This file is part of the cvc5 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 cvc5/src/api/cpp/cvc5_kind.h and generates -.pxd and .pxi files which declare all the cvc5 kinds and -implement a Python wrapper for kinds, respectively. The -default names are kinds.pxd / kinds.pxi, but the name is -configurable from the command line with --kinds-file-prefix. - -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. -""" - -import argparse -import os -import re -import sys - -# get access to cvc5/src/api/parsekinds.py -sys.path.insert(0, os.path.abspath('${CMAKE_SOURCE_DIR}/src/api')) - -from parsekinds import * - -#################### Default Filenames ################ -DEFAULT_PREFIX = 'kinds' - -################ Comments and Macro Tokens ############ -PYCOMMENT = '#' - -KINDS_PXD_TOP = \ -r"""cdef extern from "api/cpp/cvc5_kind.h" namespace "cvc5::api": - enum Kind: -""" - -KINDS_PXI_TOP = \ -r'''# distutils: language = c++ -# distutils: extra_compile_args = -std=c++11 - -from cvc5kinds cimport Kind as c_Kind -from enum import Enum - -class Kind(Enum): - """The Kinds enum""" - def __new__(cls, value, doc): - self = object.__new__(cls) - self._value_ = value - self.__doc__ = doc - return self -''' - -KINDS_ATTR_TEMPLATE = r''' {name}=c_Kind.{kind}, """{doc}""" -''' - -# Format Kind Names -# special cases for format_name -_IS = '_IS' -# replacements after some preprocessing -replacements = {'Bitvector': 'BV', 'Floatingpoint': 'FP'} - - -def format_name(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_IS_NAN --> 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_ADD --> BVAdd - APPLY_SELECTOR --> ApplySelector - FLOATINGPOINT_IS_NAN --> FPIsNan - SET_MINUS --> 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 gen_pxd(parser: KindsParser, filename): - with open(filename, "w") as f: - # include the format_name docstring in the generated file - # could be helpful for users to see the formatting rules - for line in format_name.__doc__.split(NL): - f.write(PYCOMMENT) - if not line.isspace(): - f.write(line) - f.write(NL) - f.write(KINDS_PXD_TOP) - for name, _ in parser.kinds_doc.items(): - f.write(' {},\n'.format(name)) - - -def gen_pxi(parser: KindsParser, filename): - with open(filename, "w") as f: - f.write(KINDS_PXI_TOP) - for name, doc in parser.kinds_doc.items(): - f.write( - KINDS_ATTR_TEMPLATE.format(name=format_name(name), - kind=name, - doc=doc)) - - -comment_repls = { - '`Solver::([a-zA-Z]+)\(([^)]*)\)[^`]*`': ':py:meth:`pycvc5.Solver.\\1`', -} - - -def reformat_comment(comment): - for pat, repl in comment_repls.items(): - comment = re.sub(pat, repl, comment) - return comment - - -if __name__ == "__main__": - parser = argparse.ArgumentParser( - 'Read a kinds header file and generate a ' - 'corresponding pxd file, with simplified kind names.') - parser.add_argument('--kinds-header', - metavar='', - help='The header file to read kinds from') - parser.add_argument('--kinds-file-prefix', - metavar='', - help='The prefix for the .pxd and .pxi files to write ' - 'the Cython declarations to.', - 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) - - for name in kp.kinds_doc: - kp.kinds_doc[name] = reformat_comment(kp.kinds_doc[name]) - - gen_pxd(kp, kinds_file_prefix + ".pxd") - gen_pxi(kp, kinds_file_prefix + ".pxi") -- 2.30.2