1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
#!/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
# 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 cvc5;
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"::": "."
}
# 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)
java_comment = "\n /**"
for line in comment.split("\n"):
java_comment += "\n * " + line
java_comment = " " + java_comment.strip() + "/"
return java_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, name in parser.kinds.items():
comment = parser.get_comment(kind)
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")
|
