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
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
|
#!/bin/bash
#
# usage: new-theory [--alternate existing-theory] new-theory-dir-name
#
cd "`dirname "$0"`/.."
if ! perl -v &>/dev/null; then
echo "ERROR: perl is required to run this script." >&2
exit 1
fi
if [ ! -e src/theory/theory_engine.h ]; then
echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2
echo "ERROR: of the CVC4 source tree." >&2
exit 1
fi
if [ $# -ge 1 -a "$1" = --alternate ]; then
shift
alternate=true
alttheory="$1"
shift
else
alternate=false
fi
if [ $# -ne 1 ]; then
echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
echo "e.g.: new-theory arrays" >&2
echo "e.g.: new-theory sets" >&2
echo "e.g.: new-theory rewrite_rules" >&2
echo "e.g.: new-theory --alternate arith difference-logic" >&2
echo >&2
echo "This tool will create a new src/theory/<new-theory-dir-name>" >&2
echo "directory and fill in some infrastructural files in that directory." >&2
echo "It also will incorporate that directory into the build process." >&2
echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
echo "directory for tips on what to do next." >&2
echo >&2
echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
echo "directories and namespaces separated by an underscore (_). The" >&2
echo "resulting class names created by this script will be in CamelCase" >&2
echo "(e.g. RewriteRules) if that convention is followed." >&2
echo >&2
echo "With --alternate, create a new theory directory that is declared as" >&2
echo "an alternate implementation of an existing host theory. Such" >&2
echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
echo "normal form), and expression kinds with their host theories, but" >&2
echo "differ in decision procedure implementation. They are selectable" >&2
echo "at runtime with --use-theory." >&2
exit 1
fi
dir="$1"
if [ -e "src/theory/$dir" ]; then
echo "ERROR: Theory \"$dir\" already exists." >&2
echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
echo "ERROR: $dir, use this program this way:" >&2
echo "ERROR: new-theory --alternate $dir new-implementation-name" >&2
exit 1
fi
if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev/null ||
expr "$dir" : '_$' &>/dev/null; then
echo "ERROR: \"$dir\" is not a valid theory name." >&2
echo "ERROR:" >&2
echo "ERROR: Theory names must start with a letter and be composed of" >&2
echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2
echo "ERROR: underscore cannot be the final character." >&2
exit 1
fi
if $alternate; then
if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
exit 1
fi
alt_id="$(
function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
source "src/theory/$alttheory/kinds"
)"
fi
id="`echo "$dir" | tr a-z A-Z`"
# convoluted, but should be relatively portable and give a CamelCase
# representation for a string. (e.g. "foo_bar" becomes "FooBar")
camel="`echo "$dir" | awk 'BEGIN { RS="_";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
if ! mkdir "src/theory/$dir"; then
echo "ERROR: encountered an error creating directory src/theory/$dir" >&2
exit 1
fi
echo "Theory of $dir"
echo "Theory directory: src/theory/$dir"
echo "Theory id: THEORY_$id"
$alternate && echo "Alternate for theory id: THEORY_$alt_id"
echo "Theory class: CVC4::theory::$dir::Theory$camel"
echo
function copyskel {
src="$1"
dest="`echo "$src" | sed "s/DIR/$dir/g"`"
echo "Creating src/theory/$dir/$dest..."
sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
contrib/theoryskel/$src \
> "src/theory/$dir/$dest"
}
function copyaltskel {
src="$1"
dest="`echo "$src" | sed "s/DIR/$dir/g"`"
echo "Creating src/theory/$dir/$dest..."
sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
contrib/alttheoryskel/$src \
> "src/theory/$dir/$dest"
}
function copyoptions {
src="$1"
dest="`echo "$src" | sed "s/DIR/$dir/g"`"
echo "Creating src/options/$dest..."
sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
contrib/optionsskel/$src \
> "src/options/$dest"
}
# copy files from the skeleton, with proper replacements
if $alternate; then
alternate01=1
for file in `ls contrib/alttheoryskel`; do
copyaltskel "$file"
done
else
alternate01=0
for file in `ls contrib/theoryskel`; do
copyskel "$file"
done
fi
# Copy the options file independently
for file in `ls contrib/optionsskel`; do
copyoptions "$file"
done
echo
echo "Adding $dir to THEORIES to src/Makefile.theories..."
if grep -q '^THEORIES = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/Makefile.theories &>/dev/null; then
echo "NOTE: src/Makefile.theories already lists theory $dir"
else
awk '/^THEORIES = / {print $0,"'"$dir"'"} !/^THEORIES = / {print$0}' src/Makefile.theories > src/Makefile.theories.new-theory
if ! cp -f src/Makefile.theories src/Makefile.theories~; then
echo "ERROR: cannot copy src/Makefile.theories !" >&2
exit 1
fi
if ! mv -f src/Makefile.theories.new-theory src/Makefile.theories; then
echo "ERROR: cannot replace src/Makefile.theories !" >&2
exit 1
fi
fi
echo "Adding sources to src/Makefile.am..."
perl -e '
while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
if('$alternate01') {
while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp\n"; last; } else { print; } }
} else {
while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp \\\n\ttheory/'"$dir"'/theory_'"$dir"'_rewriter.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'_type_rules.h\n"; last; } else { print; } }
}
while(<>) { print; last if /^EXTRA_DIST = /; }
while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } }
while(<>) { print; }' src/Makefile.am > src/Makefile.am.new-theory
if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
echo "ERROR: cannot replace src/Makefile.am !" >&2
exit 1
fi
echo "Adding ${dir}_options to src/options/Makefile.am..."
if grep -q '^ ${dir}_options' src/options/Makefile.am &>/dev/null; then
echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
else
awk -v name="$dir" -f contrib/new-theory.awk src/options/Makefile.am > src/options/Makefile.am.new-theory
if ! cp -f src/options/Makefile.am src/options/Makefile.am~; then
echo "ERROR: cannot copy src/options/Makefile.am !" >&2
exit 1
fi
if ! mv -f src/options/Makefile.am.new-theory src/options/Makefile.am; then
echo "ERROR: cannot replace src/options/Makefile.am !" >&2
exit 1
fi
fi
echo
echo "Rerunning autogen.sh..."
./autogen.sh
|
