From: Andres Noetzli Date: Fri, 25 Mar 2022 20:28:12 +0000 (-0700) Subject: Generate `enum` bindings for Python and Java (#8393) X-Git-Tag: cvc5-1.0.0~170 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fb54473f59d21a3125f67dc1f8f834431bc207f5;p=cvc5.git 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). --- 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/genenums.py.in b/src/api/java/genenums.py.in new file mode 100644 index 000000000..5ecd5bd40 --- /dev/null +++ b/src/api/java/genenums.py.in @@ -0,0 +1,155 @@ +#!/usr/bin/env python +############################################################################### +# Top contributors (to current version): +# Mudathir Mohamed, Makai Mann, Mathias Preiner +# +# 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 +cvc5/Kind.java file which declares all cvc5 kinds. +""" + +import argparse +import os +import sys +import re +import textwrap + +# 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 = 'Kind' + +# Code Blocks + +ENUM_JAVA_TOP = \ + r"""package io.github.cvc5.{namespace}; + +import java.util.HashMap; +import java.util.Map; + +public enum {name} +{{ +""" + +ENUM_JAVA_BOTTOM = \ + r"""; + + /* the int value of the kind */ + private int value; + private static Map 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 CVC5ApiException + { + if (value < INTERNAL_KIND.value || value > LAST_KIND.value) + { + throw new CVC5ApiException("Kind value " + value + " is outside the valid range [" + + INTERNAL_KIND.value + "," + LAST_KIND.value + "]"); + } + return kindMap.get(value); + } + + public int getValue() + { + return value; + } +} +""" + +# mapping from c++ patterns to java +CPP_JAVA_MAPPING = \ + { + r"\bbool\b": "boolean", + r"\bconst\b\s?": "", + r"\bint32_t\b": "int", + r"\bint64_t\b": "long", + r"\buint32_t\b": "int", + r"\buint64_t\b": "long", + r"\bunsigned char\b": "byte", + r"cvc5::api::": "cvc5.", + r"Term::Term\(\)": "Solver.getNullTerm()", + r"Solver::": "Solver.", + r"std::vector": "int[]", + r"std::vector": "Term[]", + r"std::string": "String", + r"&": "", + r"::": ".", + r">": ">", + r"<": "<", + r"@f\[": "", + r"@f\]": "", + r"@note": "", + } + + +# convert from c++ doc to java doc +def format_comment(comment): + for pattern, replacement in CPP_JAVA_MAPPING.items(): + comment = re.sub(pattern, replacement, comment) + return """ /**\n{}\n */""".format(textwrap.indent(comment, ' * ')) + + +# Files generation +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 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() + enums_header = args.enums_header + java_api_path = args.java_api_path + + ep = EnumParser() + ep.parse(enums_header) + + gen_java(ep, java_api_path) diff --git a/src/api/java/genkinds.py.in b/src/api/java/genkinds.py.in deleted file mode 100644 index 41f02d221..000000000 --- a/src/api/java/genkinds.py.in +++ /dev/null @@ -1,147 +0,0 @@ -#!/usr/bin/env python -############################################################################### -# Top contributors (to current version): -# Mudathir Mohamed, Makai Mann, Mathias Preiner -# -# 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 -cvc5/Kind.java file which declares all cvc5 kinds. -""" - -import argparse -import os -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')) - -from parsekinds import * - -# Default Filenames -DEFAULT_PREFIX = 'Kind' - -# Code Blocks - -KINDS_JAVA_TOP = \ - r"""package io.github.cvc5.api; - -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 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 CVC5ApiException - { - if (value < INTERNAL_KIND.value || value > LAST_KIND.value) - { - throw new CVC5ApiException("Kind value " + value + " is outside the valid range [" - + INTERNAL_KIND.value + "," + LAST_KIND.value + "]"); - } - return kindMap.get(value); - } - - public int getValue() - { - return value; - } -} -""" - -# mapping from c++ patterns to java -CPP_JAVA_MAPPING = \ - { - r"\bbool\b": "boolean", - r"\bconst\b\s?": "", - r"\bint32_t\b": "int", - r"\bint64_t\b": "long", - r"\buint32_t\b": "int", - r"\buint64_t\b": "long", - r"\bunsigned char\b": "byte", - r"cvc5::api::": "cvc5.", - r"Term::Term\(\)": "Solver.getNullTerm()", - r"Solver::": "Solver.", - r"std::vector": "int[]", - r"std::vector": "Term[]", - r"std::string": "String", - r"&": "", - r"::": ".", - r">": ">", - r"<": "<", - r"@f\[": "", - r"@f\]": "", - r"@note": "", - } - - -# convert from c++ doc to java doc -def format_comment(comment): - for pattern, replacement in CPP_JAVA_MAPPING.items(): - comment = re.sub(pattern, replacement, comment) - return """ /**\n{}\n */""".format(textwrap.indent(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() - - -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='', - 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/parseenums.py b/src/api/parseenums.py new file mode 100644 index 000000000..172d46089 --- /dev/null +++ b/src/api/parseenums.py @@ -0,0 +1,201 @@ +#!/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 implements EnumParser which parses a header file that defines +enums. + +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 +import textwrap + +##################### Useful Constants ################ +OCB = '{' +CCB = '}' +SC = ';' +EQ = '=' +C = ',' +US = '_' +NL = '\n' + +NAMESPACE_START = 'namespace' + +# Expected C++ Enum Declarations +ENUM_START = 'enum' +ENUM_END = CCB + SC + +# Comments and Macro Tokens +COMMENT = '//' +BLOCK_COMMENT_BEGIN = '/*' +BLOCK_COMMENT_END = '*/' +MACRO_BLOCK_BEGIN = '#if 0' +MACRO_BLOCK_END = '#endif' + + +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): + # 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 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_current_enum(self): + ''' + Returns the enum that is currently being parsed + ''' + return self.get_current_namespace().enums[-1] + + def format_comment(self, comment): + ''' + Removes the C++ syntax for block comments and returns just the text. + ''' + assert comment[:2] == '/*', \ + "Expecting to start with /* but got \"{}\"".format(comment[:2]) + assert comment[-2:] == '*/', \ + "Expecting to end with */ but got \"{}\"".format(comment[-2:]) + comment = comment[2:-2].strip('*\n') # /** ... */ -> ... + comment = textwrap.dedent(comment) # remove indentation + comment = comment.replace('\n*', '\n') # remove leading "*"" + comment = textwrap.dedent(comment) # remove indentation + comment = comment.replace('\\rst', '').replace('\\endrst', '') + comment = comment.strip() # remove leading and trailing spaces + return comment + + 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 entering block comment, override previous block comment + if token == BLOCK_COMMENT_BEGIN: + self.latest_block_comment = 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: + # if in block comment, record the line + if self.endtoken == BLOCK_COMMENT_END: + self.latest_block_comment += "\n" + line + # 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): + 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 + elif line.startswith(NAMESPACE_START): + tokens = line.split() + name = tokens[1] + self.namespaces.append(CppNamespace(name)) diff --git a/src/api/parsekinds.py b/src/api/parsekinds.py deleted file mode 100644 index 6eee76693..000000000 --- a/src/api/parsekinds.py +++ /dev/null @@ -1,151 +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 implements KindsParser which -parses the header file cvc5/src/api/cpp/cvc5_kind.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 -import textwrap - -##################### Useful Constants ################ -OCB = '{' -CCB = '}' -SC = ';' -EQ = '=' -C = ',' -US = '_' -NL = '\n' - -# Expected C++ Enum Declarations -ENUM_START = 'enum 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' - - -class KindsParser: - 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 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 - self.latest_block_comment = "" - - def get_comment(self, kind_name): - ''' - Look up a documentation comment for a Kind by C++ name - ''' - return self.kinds_doc[kind_name] - - def format_comment(self, comment): - ''' - Removes the C++ syntax for block comments and returns just the text. - ''' - assert comment[:2] == '/*', \ - "Expecting to start with /* but got \"{}\"".format(comment[:2]) - assert comment[-2:] == '*/', \ - "Expecting to end with */ but got \"{}\"".format(comment[-2:]) - comment = comment[2:-2].strip('*\n') # /** ... */ -> ... - comment = textwrap.dedent(comment) # remove indentation - comment = comment.replace('\n*', '\n') # remove leading "*"" - comment = textwrap.dedent(comment) # remove indentation - comment = comment.replace('\\rst', '').replace('\\endrst', '') - comment = comment.strip() # remove leading and trailing spaces - return comment - - 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 entering block comment, override previous block comment - if token == BLOCK_COMMENT_BEGIN: - self.latest_block_comment = 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: - # if in block comment, record the line - if self.endtoken == BLOCK_COMMENT_END: - self.latest_block_comment += "\n" + line - # 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 - 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() 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")