3 # usage: new-theory [--alternate existing-theory] new-theory-dir-name
8 if ! perl
-v &>/dev
/null
; then
9 echo "ERROR: perl is required to run this script." >&2
13 if [ ! -e src
/theory
/theory_engine.h
]; then
14 echo "ERROR: This script doesn't appear to be the contrib/ subdirectory" >&2
15 echo "ERROR: of the CVC4 source tree." >&2
19 # Trailing whitespaces in src/Makefile.am mess with the regexps (and are
20 # generally undesirable, so we throw an error instead of ignoring them).
21 if grep -q '[[:blank:]]$' src
/Makefile.am
; then
22 echo "ERROR: trailing whitespaces in src/Makefile.am" >&2
26 if [ $# -ge 1 -a "$1" = --alternate ]; then
36 echo "usage: new-theory [--alternate existing-theory] new-theory-dir-name" >&2
37 echo "e.g.: new-theory arrays" >&2
38 echo "e.g.: new-theory sets" >&2
39 echo "e.g.: new-theory rewrite_rules" >&2
40 echo "e.g.: new-theory --alternate arith difference-logic" >&2
42 echo "This tool will create a new src/theory/<new-theory-dir-name>" >&2
43 echo "directory and fill in some infrastructural files in that directory." >&2
44 echo "It also will incorporate that directory into the build process." >&2
45 echo "Please refer to the file README.WHATS-NEXT file created in that" >&2
46 echo "directory for tips on what to do next." >&2
48 echo "Theories with multiple words (e.g. \"rewrite_rules\") should have" >&2
49 echo "directories and namespaces separated by an underscore (_). The" >&2
50 echo "resulting class names created by this script will be in CamelCase" >&2
51 echo "(e.g. RewriteRules) if that convention is followed." >&2
53 echo "With --alternate, create a new theory directory that is declared as" >&2
54 echo "an alternate implementation of an existing host theory. Such" >&2
55 echo "\"alternates\" share preprocessing, typechecking, rewriting (i.e.," >&2
56 echo "normal form), and expression kinds with their host theories, but" >&2
57 echo "differ in decision procedure implementation. They are selectable" >&2
58 echo "at runtime with --use-theory." >&2
64 if [ -e "src/theory/$dir" ]; then
65 echo "ERROR: Theory \"$dir\" already exists." >&2
66 echo "ERROR: Please choose a new directory name (or move that one aside)." >&2
67 echo "ERROR: Or, if you'd like to create an alternate implementation of" >&2
68 echo "ERROR: $dir, use this program this way:" >&2
69 echo "ERROR: new-theory --alternate $dir new-implementation-name" >&2
73 if ! expr "$dir" : '[a-zA-Z][a-zA-Z0-9_]*$' &>/dev
/null ||
74 expr "$dir" : '_$' &>/dev
/null
; then
75 echo "ERROR: \"$dir\" is not a valid theory name." >&2
77 echo "ERROR: Theory names must start with a letter and be composed of" >&2
78 echo "ERROR: letters, numbers, and the underscore (_) character; an" >&2
79 echo "ERROR: underscore cannot be the final character." >&2
84 if ! [ -d "src/theory/$alttheory" -a -f "src/theory/$alttheory/kinds" ]; then
85 echo "ERROR: Theory \"$alttheory\" doesn't exist, or cannot read its kinds file." >&2
89 function theory() { echo $1 | sed 's,^THEORY_,,'; exit; }
90 source "src
/theory
/$alttheory/kinds
"
94 id
="`echo "$dir" | tr a-z A-Z`"
95 # convoluted, but should be relatively portable and give a CamelCase
96 # representation for a string. (e.g. "foo_bar" becomes "FooBar")
97 camel
="`echo "$dir" | awk 'BEGIN { RS="_
";ORS="";OFS="" } // {print toupper(substr($1,1,1)),substr($1,2,length($1))} END {print "\n"}'`"
99 if ! mkdir
"src/theory/$dir"; then
100 echo "ERROR: encountered an error creating directory src/theory/$dir" >&2
104 echo "Theory of $dir"
105 echo "Theory directory: src/theory/$dir"
106 echo "Theory id: THEORY_$id"
107 $alternate && echo "Alternate for theory id: THEORY_$alt_id"
108 echo "Theory class: CVC4::theory::$dir::Theory$camel"
113 dest
="`echo "$src" | sed "s
/DIR
/$dir/g
"`"
114 echo "Creating src/theory/$dir/$dest..."
115 sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g" \
116 contrib
/theoryskel
/$src \
117 > "src/theory/$dir/$dest"
120 function copyaltskel
{
122 dest
="`echo "$src" | sed "s
/DIR
/$dir/g
"`"
123 echo "Creating src/theory/$dir/$dest..."
124 sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
125 contrib
/alttheoryskel
/$src \
126 > "src/theory/$dir/$dest"
129 function copyoptions
{
131 dest
="`echo "$src" | sed "s
/DIR
/$dir/g
"`"
132 echo "Creating src/options/$dest..."
133 sed "s/\$dir/$dir/g;s/\$camel/$camel/g;s/\$id/$id/g;s/\$alt_id/$alt_id/g" \
134 contrib
/optionsskel
/$src \
135 > "src/options/$dest"
138 # copy files from the skeleton, with proper replacements
141 for file in `ls contrib/alttheoryskel`; do
146 for file in `ls contrib/theoryskel`; do
150 # Copy the options file independently
151 for file in `ls contrib/optionsskel`; do
157 echo "Adding $dir to THEORIES to src/Makefile.theories..."
158 if grep -q '^THEORIES = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src
/Makefile.theories
&>/dev
/null
; then
159 echo "NOTE: src/Makefile.theories already lists theory $dir"
161 awk '/^THEORIES = / {print $0,"'"$dir"'"} !/^THEORIES = / {print$0}' src
/Makefile.theories
> src
/Makefile.theories.new-theory
162 if ! cp -f src
/Makefile.theories src
/Makefile.theories~
; then
163 echo "ERROR: cannot copy src/Makefile.theories !" >&2
166 if ! mv -f src
/Makefile.theories.new-theory src
/Makefile.theories
; then
167 echo "ERROR: cannot replace src/Makefile.theories !" >&2
172 echo "Adding sources to src/Makefile.am..."
175 while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
177 while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/theory_'"$dir"'.h \\\n\ttheory/'"$dir"'/theory_'"$dir"'.cpp\n"; last; } else { print; } }
179 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; } }
181 while(<>) { print; last if /^EXTRA_DIST = /; }
182 while(<>) { if(!/\\$/) { chomp; print "$_ \\\n\ttheory/'"$dir"'/kinds\n"; last; } else { print; } }
183 while(<>) { print; }' src
/Makefile.am
> src
/Makefile.am.new-theory
184 if ! mv -f src
/Makefile.am.new-theory src
/Makefile.am
; then
185 echo "ERROR: cannot replace src/Makefile.am !" >&2
189 echo "Adding ${dir}_options.toml to src/options/Makefile.am..."
190 if grep -q '^ ${dir}_options.toml' src
/options
/Makefile.am
&>/dev
/null
; then
191 echo "NOTE: src/options/Makefile.am already seems to link to $dir option files"
193 awk -v name
="$dir" -f contrib
/new-theory.
awk src
/options
/Makefile.am
> src
/options
/Makefile.am.new-theory
194 if ! cp -f src
/options
/Makefile.am src
/options
/Makefile.am~
; then
195 echo "ERROR: cannot copy src/options/Makefile.am !" >&2
198 if ! mv -f src
/options
/Makefile.am.new-theory src
/options
/Makefile.am
; then
199 echo "ERROR: cannot replace src/options/Makefile.am !" >&2
205 echo "Rerunning autogen.sh..."