diff options
author | makaimann <makaim@stanford.edu> | 2020-02-19 13:54:17 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-19 15:54:17 -0600 |
commit | c82720479efcf922136f0919f6fc26a502b2515a (patch) | |
tree | f9007e124cfc07490e914ae1e1e05747e1e1ee11 /src/api/python/genkinds.py | |
parent | c6a9ab9da205df7cbf192edc142ee151404dcb1b (diff) |
Add Python bindings using Cython -- see below for more details (#2879)
Diffstat (limited to 'src/api/python/genkinds.py')
-rwxr-xr-x | src/api/python/genkinds.py | 255 |
1 files changed, 255 insertions, 0 deletions
diff --git a/src/api/python/genkinds.py b/src/api/python/genkinds.py new file mode 100755 index 000000000..1e22875e7 --- /dev/null +++ b/src/api/python/genkinds.py @@ -0,0 +1,255 @@ +#!/usr/bin/env python +""" +This script reads CVC4/src/api/cvc4cppkind.h and generates +.pxd and .pxi files which declare all the CVC4 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 +from collections import OrderedDict + +#################### Default Filenames ################ +DEFAULT_HEADER = 'cvc4cppkind.h' +DEFAULT_PREFIX = 'kinds' + +##################### Useful Constants ################ +OCB = '{' +CCB = '}' +SC = ';' +EQ = '=' +C = ',' +US = '_' +NL = '\n' + +#################### Enum Declarations ################ +ENUM_START = 'enum CVC4_PUBLIC Kind' +ENUM_END = CCB+SC + +################ 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 " + +KINDS_PXD_TOP = \ +r"""cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api": + cdef cppclass Kind: + pass + + +# Kind declarations: See cvc4cppkind.h for additional information +cdef extern from "api/cvc4cppkind.h" namespace "CVC4::api::Kind": +""" + +KINDS_PXI_TOP = \ +r"""# distutils: language = c++ +# distutils: extra_compile_args = -std=c++11 + +from cvc4kinds cimport * +import sys +from types import ModuleType + +cdef class kind: + cdef Kind k + cdef str name + def __cinit__(self, str name): + self.name = name + + def __eq__(self, kind other): + return (<int> self.k) == (<int> other.k) + + def __ne__(self, kind other): + return (<int> self.k) != (<int> other.k) + + def __hash__(self): + return hash((<int> self.k, self.name)) + + def __str__(self): + return self.name + + def __repr__(self): + return self.name + + def as_int(self): + return <int> self.k + +# create a kinds submodule +kinds = ModuleType('kinds') +# fake a submodule for dotted imports, e.g. from pycvc4.kinds import * +sys.modules['%s.%s'%(__name__, kinds.__name__)] = kinds +kinds.__file__ = kinds.__name__ + ".py" +""" + +KINDS_ATTR_TEMPLATE = \ +r""" +cdef kind {name} = kind("{name}") +{name}.k = {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() + + +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='<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 .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) + + kp.gen_pxd(kinds_file_prefix + ".pxd") + kp.gen_pxi(kinds_file_prefix + ".pxi") |