diff options
| -rwxr-xr-x | contrib/new-theory | 23 | ||||
| -rw-r--r-- | contrib/theoryskel/README.WHATS-NEXT | 9 | ||||
| -rw-r--r-- | contrib/theoryskel/theory_DIR.cpp | 2 |
3 files changed, 32 insertions, 2 deletions
diff --git a/contrib/new-theory b/contrib/new-theory index 7ada1de6c..4aedd7c0f 100755 --- a/contrib/new-theory +++ b/contrib/new-theory @@ -16,12 +16,18 @@ if [ $# -ne 1 ]; then 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 @@ -74,7 +80,7 @@ for file in `ls contrib/theoryskel`; do done echo -echo "Adding $dir to src/theory/Makefile.am..." +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 @@ -89,6 +95,21 @@ else 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 diff --git a/contrib/theoryskel/README.WHATS-NEXT b/contrib/theoryskel/README.WHATS-NEXT index e860c5373..6e090b984 100644 --- a/contrib/theoryskel/README.WHATS-NEXT +++ b/contrib/theoryskel/README.WHATS-NEXT @@ -24,6 +24,15 @@ and finally: * to choose which work will be done at QUICK_CHECK, STANDARD or at FULL_EFFORT. +You'll probably find the Developer's wiki useful: + + http://church.cims.nyu.edu/wiki/CVC_Portal + +...and in particular the Deverloper's Guide: + + http://church.cims.nyu.edu/wiki/Developer%27s_Guide + +which contains coding guidelines for the CVC4 project. Good luck, and please contact cvc4-devel@cs.nyu.edu for assistance should you need it! diff --git a/contrib/theoryskel/theory_DIR.cpp b/contrib/theoryskel/theory_DIR.cpp index 4d24f3e16..e885cb9c7 100644 --- a/contrib/theoryskel/theory_DIR.cpp +++ b/contrib/theoryskel/theory_DIR.cpp @@ -11,7 +11,7 @@ Theory$camel::Theory$camel(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) : - Theory(THEORY_UF, c, u, out, valuation) { + Theory(THEORY_$id, c, u, out, valuation) { }/* Theory$camel::Theory$camel() */ void Theory$camel::check(Effort level) { |