6 files changed, 34 insertions, 65 deletions
diff --git a/contrib/alttheoryskel/Makefile b/contrib/alttheoryskel/Makefile
deleted file mode 100644
index 2aeda0cf8..000000000
--- a/contrib/alttheoryskel/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/$dir
-
-include $(topdir)/Makefile.subdir
diff --git a/contrib/alttheoryskel/Makefile.am b/contrib/alttheoryskel/Makefile.am
deleted file mode 100644
index 2f36e8fc1..000000000
--- a/contrib/alttheoryskel/Makefile.am
+++ /dev/null
@@ -1,14 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = lib$dir.la
-
-lib$dir_la_SOURCES = \
-	theory_$dir.h \
-	theory_$dir.cpp
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/contrib/new-theory b/contrib/new-theory
index 4649e5943..c1478a980 100755
--- a/contrib/new-theory
+++ b/contrib/new-theory
@@ -5,6 +5,11 @@
 
 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
@@ -126,34 +131,36 @@ else
 fi
 
 echo
-echo "Adding $dir to SUBDIRS to 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"
+echo "Adding $dir to THEORIES to src/Makefile.am..."
+if grep -q '^THEORIES = .*[^a-zA-Z0-9_]'"$dir"'\([^a-zA-Z0-9_]\|$\)' src/Makefile.am &>/dev/null; then
+  echo "NOTE: src/Makefile.am already lists theory $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
+  awk '/^THEORIES = / {print $0,"'"$dir"'"} !/^THEORIES = / {print$0}' src/Makefile.am > src/Makefile.am.new-theory
+  if ! cp -f src/Makefile.am src/Makefile.am~; then
+    echo "ERROR: cannot copy src/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
+  if ! mv -f src/Makefile.am.new-theory src/Makefile.am; then
+    echo "ERROR: cannot replace src/Makefile.am !" >&2
     exit 1
   fi
 fi
 
-echo "Adding lib$dir.la to LIBADD to 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$dir.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
+echo "Adding sources to src/Makefile.am..."
+
+perl -e '
+  while(<>) { print; last if /^libcvc4_la_SOURCES = /; }
+  if('$alternate') {
+    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\ttheory/'"$dir"'/options_handlers.h\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 ../theory/$dir/options.cpp to OPTIONS_FILES_SRCS"
diff --git a/contrib/theoryskel/Makefile b/contrib/theoryskel/Makefile
deleted file mode 100644
index 2aeda0cf8..000000000
--- a/contrib/theoryskel/Makefile
+++ /dev/null
@@ -1,4 +0,0 @@
-topdir = ../../..
-srcdir = src/theory/$dir
-
-include $(topdir)/Makefile.subdir
diff --git a/contrib/theoryskel/Makefile.am b/contrib/theoryskel/Makefile.am
deleted file mode 100644
index 000544d98..000000000
--- a/contrib/theoryskel/Makefile.am
+++ /dev/null
@@ -1,16 +0,0 @@
-AM_CPPFLAGS = \
-	-D__BUILDING_CVC4LIB \
-	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
-
-noinst_LTLIBRARIES = lib$dir.la
-
-lib$dir_la_SOURCES = \
-	theory_$dir.h \
-	theory_$dir.cpp \
-	theory_$dir_rewriter.h \
-	theory_$dir_type_rules.h
-
-EXTRA_DIST = \
-	kinds \
-	options_handlers.h
diff --git a/src/Makefile.am b/src/Makefile.am
index a056c1d84..1858d4d32 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -14,8 +14,8 @@ LIBCVC4_VERSION = @CVC4_LIBRARY_VERSION@
 
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4LIB \
-        -D __STDC_LIMIT_MACROS \
-        -D __STDC_FORMAT_MACROS \
+	-D __STDC_LIMIT_MACROS \
+	-D __STDC_FORMAT_MACROS \
 	-I@builddir@ -I@srcdir@/include -I@srcdir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
 
@@ -449,10 +449,10 @@ EXTRA_DIST = \
 	theory/rewriterules/kinds \
 	theory/arith/kinds \
 	theory/booleans/kinds \
-        theory/example/ecdata.h \
-        theory/example/ecdata.cpp \
-        theory/example/theory_uf_tim.h \
-        theory/example/theory_uf_tim.cpp
+	theory/example/ecdata.h \
+	theory/example/ecdata.cpp \
+	theory/example/theory_uf_tim.h \
+	theory/example/theory_uf_tim.cpp
 
 svn_versioninfo.cpp: svninfo
 	$(AM_V_GEN)( \