blob: 4aedd7c0f7f161093b0503bc7b11d76c6d122291 (
plain)
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
|
#!/bin/bash
#
# usage: new-theory theory-directory-name
#
cd "`dirname "$0"`/.."
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 [ $# -ne 1 ]; then
echo "usage: new-theory theory-directory-name" >&2
echo "e.g.: new-theory arith" >&2
echo "e.g.: new-theory arrays" >&2
echo "e.g.: new-theory sets" >&2
echo "e.g.: new-theory rewrite_rules" >&2
echo >&2
echo "This tool will create a new src/theory/<theory-directory-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."
echo
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
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
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
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"
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"
}
# copy files from the skeleton, with proper replacements
for file in `ls contrib/theoryskel`; do
copyskel "$file"
done
echo
echo "Adding $dir to SUBDIRS in src/theory/Makefile.am..."
if grep -q '^SUBDIRS = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/theory/Makefile.am &>/dev/null; then
echo "NOTE: src/theory/Makefile.am already descends into dir $dir"
else
awk '/^SUBDIRS = / {print $0,"'"$dir"'"} !/^SUBDIRS = / {print$0}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
echo "ERROR: cannot copy src/theory/Makefile.am !" >&2
exit 1
fi
if ! mv -f src/theory/Makefile.am.new-theory src/theory/Makefile.am; then
echo "ERROR: cannot replace src/theory/Makefile.am !" >&2
exit 1
fi
fi
echo "Adding lib$theory.la to LIBADD in src/theory/Makefile.am..."
if grep -q '^ @builddir@/'"$dir"'/lib'"$dir"'\.la\>' src/theory/Makefile.am &>/dev/null; then
echo "NOTE: src/theory/Makefile.am already seems to include lib$theory.la"
else
awk '!/^libtheory_la_LIBADD = / {print$0} /^libtheory_la_LIBADD = / {while(/\\ *$/){print $0;getline} print $0,"\\";print "\t@builddir@/'"$dir"'/lib'"$dir"'.la"}' src/theory/Makefile.am > src/theory/Makefile.am.new-theory
if ! cp -f src/theory/Makefile.am src/theory/Makefile.am~; then
echo "ERROR: cannot copy src/theory/Makefile.am !" >&2
exit 1
fi
if ! mv -f src/theory/Makefile.am.new-theory src/theory/Makefile.am; then
echo "ERROR: cannot replace src/theory/Makefile.am !" >&2
exit 1
fi
fi
echo
echo "Rerunning autogen.sh..."
./autogen.sh
|
