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
install(FILES
api/cpp/cvc5.h
api/cpp/cvc5_kind.h
+ api/cpp/cvc5_types.h
DESTINATION
${CMAKE_INSTALL_INCLUDEDIR}/cvc5/)
install(FILES
#include <vector>
#include "api/cpp/cvc5_kind.h"
+#include "api/cpp/cvc5_types.h"
namespace cvc5 {
#include <ostream>
-namespace cvc5 {
-namespace api {
+namespace cvc5::api {
/* -------------------------------------------------------------------------- */
/* Kind */
*/
std::ostream& operator<<(std::ostream& out, Kind k) CVC5_EXPORT;
-} // namespace api
-} // namespace cvc5
+} // namespace cvc5::api
namespace std {
--- /dev/null
+/******************************************************************************
+ * 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
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)
)
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)
--- /dev/null
+#!/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<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 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>": "int[]",
+ r"std::vector<Term>": "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='<ENUMS_HEADER>',
+ help='The header file to read enums from')
+ parser.add_argument('--java-api-path',
+ metavar='<ENUMS_FILE_PREFIX>',
+ 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)
+++ /dev/null
-#!/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<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 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>": "int[]",
- r"std::vector<Term>": "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='<KINDS_HEADER>',
- help='The header file to read kinds from')
- 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")
--- /dev/null
+#!/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))
+++ /dev/null
-#!/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()
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)
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
--- /dev/null
+#!/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='<ENUMS_HEADER>',
+ help='The header file to read enums from')
+ parser.add_argument('--enums-file-prefix',
+ metavar='<ENUMS_FILE_PREFIX>',
+ 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)
+++ /dev/null
-#!/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='<KINDS_HEADER>',
- help='The header file to read kinds from')
- 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)
-
- 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")
projects / cvc5.git / commitdiff