fixes to new-theory script; resolves bug #307

diff --git a/contrib/new-theory b/contrib/new-theory
index 7ada1de6cd0d2c996c65f9ae58ed873ef192704e..4aedd7c0f7f161093b0503bc7b11d76c6d122291 100755 (executable)
--- 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 e860c5373d07405169a8df77851d0af5d0abd5b2..6e090b984d5a543409057238ddc16b0b7cfa0331 100644 (file)
--- 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 4d24f3e167a07c72e17d7c296abd27c15a1920d1..e885cb9c7cddb7d95fbb0e19830de31de8189f18 100644 (file)
--- 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) {