Improvements to header installation on user machines. Internally, we can

still write, for example:

#include "expr/node.h"

but public CVC4 headers, upon installation to /usr/include/cvc4 (or wherever),
have such #includes rewritten automatically to:

#include <cvc4/expr/node.h>

22 files changed, 86 insertions, 55 deletions

diff --git a/contrib/cut-release b/contrib/cut-release
index 5ca8d5a9b..8f707dcc3 100755
--- a/contrib/cut-release
+++ b/contrib/cut-release
@@ -31,7 +31,7 @@ if [ $# -lt 1 ]; then
 fi
 
 if ! [ -e src/expr/node.h -a -e .svn ]; then
-  echo "$(basename "$0"): ERROR: you should run this from the top-level of a CVC4 subversion working directory" >&2
+  echo "$(basename "$0"): ERROR: You should run this from the top-level of a CVC4 subversion working directory" >&2
   exit 1
 fi
 
@@ -39,7 +39,7 @@ version="$1"
 shift
 
 if echo "$version" | grep '[^a-zA-Z0-9_.+(){}^%#-]' &>/dev/null; then
-  echo "$(basename "$0"): ERROR: version designation \`$version' contains illegal characters" >&2
+  echo "$(basename "$0"): ERROR: Version designation \`$version' contains illegal characters" >&2
   exit 1
 fi
 
@@ -63,14 +63,16 @@ echo "Version: $version"
 echo
 isthatright
 
+echo "Checking whether release \`$version' already exists..."
 if ! svn ls "https://subversive.cims.nyu.edu/cvc4/cvc4/tags/releases/$version" 2>&1 >/dev/null | grep non-existent >/dev/null; then
-  echo "$(basename "$0"): ERROR: subversion repo already contains a release \`$version'" >&2
+  echo "$(basename "$0"): ERROR: Subversion repo already contains a release \`$version'" >&2
   $dryrun || exit 1
 fi
 
+echo "Checking working directory for local modifications..."
 if $dryrun; then
   if [ -n "$(svn status -q configure.ac)" ]; then
-    echo "$(basename "$0"): ERROR: in dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2
+    echo "$(basename "$0"): ERROR: In dry-run mode, cannot operate properly with local modifications to \"configure.ac\", sorry" >&2
     exit 1
   fi
 elif [ -n "$(svn status -q)" ]; then
@@ -80,20 +82,41 @@ fi
 
 root="$(svn info | grep "^Repository Root: https://subversive.cims.nyu.edu/.*" | cut -f3 -d' ')"
 if [ -z "$root" ]; then
-  echo "$(basename "$0"): ERROR: can't get repository root URL" 2>&1
+  echo "$(basename "$0"): ERROR: Can't get repository root URL" 2>&1
   $dryrun || exit 1
 fi
 
+echo "Checking repo for unmerged updates..."
 if [ `svn -uq status | wc -l` -ne 1 ]; then
-  echo "$(basename "$0"): ERROR: this working directory isn't up to date" 2>&1
+  echo "$(basename "$0"): ERROR: This working directory isn't up to date" 2>&1
   $dryrun || exit 1
 fi
 
+echo "Checking sources for broken public headers..."
+suspect_files="\
+$(grep -r --exclude-dir=.svn '^[ \t]*#[ \t]*include[ \t]*"[^/]*"' src |
+  grep -v '"cvc4parser_public\.h"' |
+  grep -v '"cvc4_public\.h"' |
+  grep -v '"cvc4_private\.h"' |
+  grep -v '"cvc4autoconfig\.h"' |
+  grep -v '"cvc4parser_private\.h"' |
+  cut -f1 -d: |
+  sort -u |
+  xargs grep -l '^[ \t]*#[ \t]*include[ \t]*"cvc4.*public\.h"' |
+  xargs echo)"
+if [ -n "$suspect_files" ]; then
+  echo "$(basename "$0"): ERROR: The following publicly-installed headers appear" 2>&1
+  echo "$(basename "$0"): ERROR:   to have relative #includes and may be broken up" 2>&1
+  echo "$(basename "$0"): ERROR:   on install: $suspect_files" 2>&1
+  $dryrun || exit 1
+fi
+
+echo "Adjusting version info lines in configure.ac..."
 if ! grep '^m4_define(_CVC4_MAJOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_MINOR,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_RELEASE,  *[0-9][0-9]* *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_EXTRAVERSION,  *\[.*\] *)' configure.ac &>/dev/null; then
-  echo "$(basename "$0"): ERROR: cannot locate the version info lines of configure.ac" >&2
+  echo "$(basename "$0"): ERROR: Cannot locate the version info lines of configure.ac" >&2
   $dryrun || exit 1
 fi
 perl -pi -e 's/^m4_define\(_CVC4_MAJOR, ( *)[0-9]+( *)\)/m4_define(_CVC4_MAJOR, ${1}'"$major"'$2)/;
@@ -114,7 +137,7 @@ if ! grep '^m4_define(_CVC4_MAJOR,  *'"$major"' *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_MINOR,  *'"$minor"' *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_RELEASE,  *'"$release"' *)' configure.ac &>/dev/null ||
    ! grep '^m4_define(_CVC4_EXTRAVERSION,  *\['"$extra"'\] *)' configure.ac &>/dev/null; then
-  echo "$(basename "$0"): INTERNAL ERROR: cannot find the modified version info lines in configure.ac, bailing..." >&2
+  echo "$(basename "$0"): INTERNAL ERROR: Cannot find the modified version info lines in configure.ac, bailing..." >&2
   exit 1
 fi
 if [ -z "$(svn status -q configure.ac)" ]; then
@@ -122,6 +145,7 @@ if [ -z "$(svn status -q configure.ac)" ]; then
   exit 1
 fi
 
+echo "Building and checking distribution \`cvc4-$version'..."
 if ! $SHELL -c '\
 	version="'$version'"; \
 	set -ex; \
@@ -140,11 +164,11 @@ if ! $SHELL -c '\
 fi
 
 if ! [ -e release-$version/cvc4-$version.tar.gz ]; then
-  echo "$(basename "$0"): INTERNAL ERROR: cannot find the distribution tarball I just built" >&2
+  echo "$(basename "$0"): INTERNAL ERROR: Cannot find the distribution tarball I just built" >&2
   exit 1
 fi
 if ! [ -e release-$version/src/main/cvc4 ]; then
-  echo "$(basename "$0"): INTERNAL ERROR: cannot find the binary I just built" >&2
+  echo "$(basename "$0"): INTERNAL ERROR: Cannot find the binary I just built" >&2
   exit 1
 fi
 
diff --git a/src/Makefile.am b/src/Makefile.am
index 906a64a65..627a89a67 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -99,6 +99,7 @@ svninfo.tmp:
 install-data-local:
 	(echo include/cvc4.h; \
 	 echo include/cvc4_public.h; \
+	 echo include/cvc4parser_public.h; \
 	 find * -name '*.h' | \
 		xargs grep -l '^# *include  *"cvc4.*_public\.h"'; \
 	(cd "$(srcdir)" && find * -name '*.h' | \
@@ -111,16 +112,21 @@ install-data-local:
 		$(mkinstalldirs) "$$(dirname "$(DESTDIR)$(includedir)/cvc4/$$d")"; \
 		if [ -e "$$f" ]; then \
 			path="$$f"; \
+			fixpath="$$f.fix"; \
 		else \
 			path="$(srcdir)/$$f"; \
+			fixpath="$(builddir)/$$f.fix"; \
+			$(MKDIR_P) "`dirname "$$fixpath"`"; \
 		fi; \
-		echo $(INSTALL_DATA) "$$path" "$(DESTDIR)$(includedir)/cvc4/$$d"; \
-		$(INSTALL_DATA) "$$path" "$(DESTDIR)$(includedir)/cvc4/$$d"; \
+		sed 's,^\([ \t]*#[ \t]*include[ \t*]\)"\(.*\)"\([ \t]*\)$$,\1<cvc4/\2>\3,' "$$path" > "$$fixpath" || exit 1; \
+		echo $(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d"; \
+		$(INSTALL_DATA) "$$fixpath" "$(DESTDIR)$(includedir)/cvc4/$$d" || exit 1; \
 	done
 
 uninstall-local:
 	-(echo include/cvc4.h; \
 	  echo include/cvc4_public.h; \
+	  echo include/cvc4parser_public.h; \
 	  find * -name '*.h' | \
 		xargs grep -l '^# *include  *"cvc4.*_public\.h"'; \
 	(cd "$(srcdir)" && find * -name '*.h' | \
diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp
index 58fb70dcb..6a8a98547 100644
--- a/src/bindings/compat/c/c_interface.cpp
+++ b/src/bindings/compat/c/c_interface.cpp
@@ -21,7 +21,7 @@
 
 
 #include <strings.h>
-#include "c_interface_defs.h"
+#include "bindings/compat/c/c_interface_defs.h"
 #include "compat/cvc3_compat.h"
 //#include "vc.h"
 //#include "command_line_flags.h"
diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h
index ce372be70..14fea7478 100644
--- a/src/bindings/compat/c/c_interface.h
+++ b/src/bindings/compat/c/c_interface.h
@@ -24,7 +24,7 @@
 #ifndef _cvc3__include__c_interface_h_
 #define _cvc3__include__c_interface_h_
 
-#include "c_interface_defs.h"
+#include "bindings/compat/c/c_interface_defs.h"
 
 //! Flags can be NULL
 VC vc_createValidityChecker(Flags flags);
diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h
index 3ce1e9224..c6bcc04f8 100644
--- a/src/bindings/compat/java/include/cvc3/JniUtils.h
+++ b/src/bindings/compat/java/include/cvc3/JniUtils.h
@@ -5,9 +5,10 @@
 #include <string>
 #include <jni.h>
 #include <typeinfo>
-#include "vcl.h"
-#include "hash_map.h"
-#include "exception.h"
+#include "compat/cvc3_compat.h"
+//#include "vcl.h"
+//#include "hash_map.h"
+//#include "exception.h"
 
 namespace Java_cvc3_JniUtils {
 
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 1914bb736..ded7ad8fe 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -151,8 +151,8 @@
 #include "cvc4_private.h"
 
 /* strong dependency; make sure node is included first */
-#include "node.h"
-#include "type_node.h"
+#include "expr/node.h"
+#include "expr/type_node.h"
 
 #ifndef __CVC4__NODE_BUILDER_H
 #define __CVC4__NODE_BUILDER_H
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index ef576839c..f2d6f1714 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -27,7 +27,7 @@
 
 #include "cvc4autoconfig.h"
 
-#include "interactive_shell.h"
+#include "main/interactive_shell.h"
 
 #include "expr/command.h"
 #include "parser/input.h"
@@ -61,15 +61,15 @@ using __gnu_cxx::stdio_filebuf;
 char* commandGenerator(const char* text, int state);
 
 static const char* const cvc_commands[] = {
-#include "cvc_tokens.h"
+#include "main/cvc_tokens.h"
 };/* cvc_commands */
 
 static const char* const smt_commands[] = {
-#include "smt_tokens.h"
+#include "main/smt_tokens.h"
 };/* smt_commands */
 
 static const char* const smt2_commands[] = {
-#include "smt2_tokens.h"
+#include "main/smt2_tokens.h"
 };/* smt2_commands */
 
 static const char* const* commandsBegin;
diff --git a/src/main/main.cpp b/src/main/main.cpp
index ef19e1604..ec0a00ff8 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -26,8 +26,8 @@
 #include <unistd.h>
 
 #include "cvc4autoconfig.h"
-#include "main.h"
-#include "interactive_shell.h"
+#include "main/main.h"
+#include "main/interactive_shell.h"
 #include "parser/parser.h"
 #include "parser/parser_builder.h"
 #include "parser/parser_exception.h"
diff --git a/src/main/util.cpp b/src/main/util.cpp
index 255d84205..89aa5c6aa 100644
--- a/src/main/util.cpp
+++ b/src/main/util.cpp
@@ -30,7 +30,7 @@
 #include "util/stats.h"
 
 #include "cvc4autoconfig.h"
-#include "main.h"
+#include "main/main.h"
 
 using CVC4::Exception;
 using namespace std;
diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp
index ec3b7077e..e52145d4e 100644
--- a/src/parser/antlr_input.cpp
+++ b/src/parser/antlr_input.cpp
@@ -20,13 +20,13 @@
 #include <antlr3.h>
 #include <stdint.h>
 
-#include "antlr_input.h"
-#include "input.h"
-#include "bounded_token_buffer.h"
-#include "bounded_token_factory.h"
-#include "memory_mapped_input_buffer.h"
-#include "parser_exception.h"
-#include "parser.h"
+#include "parser/antlr_input.h"
+#include "parser/input.h"
+#include "parser/bounded_token_buffer.h"
+#include "parser/bounded_token_factory.h"
+#include "parser/memory_mapped_input_buffer.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
 
 #include "expr/command.h"
 #include "expr/type.h"
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 913dd8013..dca26ab75 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -28,9 +28,9 @@
 #include <string>
 #include <vector>
 
-#include "bounded_token_buffer.h"
-#include "parser_exception.h"
-#include "input.h"
+#include "parser/bounded_token_buffer.h"
+#include "parser/parser_exception.h"
+#include "parser/input.h"
 
 #include "util/Assert.h"
 #include "util/bitvector.h"
diff --git a/src/parser/antlr_input_imports.cpp b/src/parser/antlr_input_imports.cpp
index 2805d518a..870edb928 100644
--- a/src/parser/antlr_input_imports.cpp
+++ b/src/parser/antlr_input_imports.cpp
@@ -54,9 +54,9 @@
 #include <antlr3.h>
 #include <sstream>
 
-#include "antlr_input.h"
-#include "parser.h"
-#include "parser_exception.h"
+#include "parser/antlr_input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
 #include "util/Assert.h"
 
 using namespace std;
diff --git a/src/parser/bounded_token_factory.cpp b/src/parser/bounded_token_factory.cpp
index 71b8849e5..f05c9007a 100644
--- a/src/parser/bounded_token_factory.cpp
+++ b/src/parser/bounded_token_factory.cpp
@@ -19,7 +19,7 @@
 #include <antlr3input.h>
 #include <antlr3commontoken.h>
 #include <antlr3interfaces.h>
-#include "bounded_token_factory.h"
+#include "parser/bounded_token_factory.h"
 
 namespace CVC4 {
 namespace parser {
diff --git a/src/parser/input.cpp b/src/parser/input.cpp
index 27b207342..70c887371 100644
--- a/src/parser/input.cpp
+++ b/src/parser/input.cpp
@@ -16,9 +16,9 @@
  ** A super-class for input language parsers
  **/
 
-#include "input.h"
-#include "parser_exception.h"
-#include "parser.h"
+#include "parser/input.h"
+#include "parser/parser_exception.h"
+#include "parser/parser.h"
 
 #include "expr/command.h"
 #include "expr/type.h"
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 3f2ec107a..f1ad4b330 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -21,9 +21,9 @@
 #include <iterator>
 #include <stdint.h>
 
-#include "input.h"
-#include "parser.h"
-#include "parser_exception.h"
+#include "parser/input.h"
+#include "parser/parser.h"
+#include "parser/parser_exception.h"
 #include "expr/command.h"
 #include "expr/expr.h"
 #include "expr/kind.h"
diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp
index d4725c4bc..5c755b5f6 100644
--- a/src/parser/parser_builder.cpp
+++ b/src/parser/parser_builder.cpp
@@ -18,9 +18,9 @@
 
 #include <string>
 
-#include "parser_builder.h"
-#include "input.h"
-#include "parser.h"
+#include "parser/parser_builder.h"
+#include "parser/input.h"
+#include "parser/parser.h"
 #include "smt/smt.h"
 #include "smt2/smt2.h"
 
diff --git a/src/parser/smt/smt_input.cpp b/src/parser/smt/smt_input.cpp
index d368339f5..85a117dd0 100644
--- a/src/parser/smt/smt_input.cpp
+++ b/src/parser/smt/smt_input.cpp
@@ -18,7 +18,7 @@
 
 #include <antlr3.h>
 
-#include "smt_input.h"
+#include "parser/smt/smt_input.h"
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/parser/smt2/smt2_input.cpp b/src/parser/smt2/smt2_input.cpp
index acd0e17f6..8f43b0acf 100644
--- a/src/parser/smt2/smt2_input.cpp
+++ b/src/parser/smt2/smt2_input.cpp
@@ -18,7 +18,7 @@
 
 #include <antlr3.h>
 
-#include "smt2_input.h"
+#include "parser/smt2/smt2_input.h"
 #include "expr/expr_manager.h"
 #include "parser/input.h"
 #include "parser/parser.h"
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index a8dc39765..5e5d55f63 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -17,7 +17,7 @@
  ** \todo document this file
  **/
 
-#include "cnf_proof.h"
+#include "proof/cnf_proof.h"
 using namespace CVC4::prop;
 
 namespace CVC4 {
diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 1e06621b4..50ded8758 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -17,7 +17,7 @@
  **
  **/
 
-#include "array_info.h"
+#include "theory/arrays/array_info.h"
 
 namespace CVC4 {
 namespace theory {
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 7fa215bfc..366c2d3f7 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -24,7 +24,7 @@
 #include "theory/theory.h"
 #include "theory/arrays/union_find.h"
 #include "util/congruence_closure.h"
-#include "array_info.h"
+#include "theory/arrays/array_info.h"
 #include "util/hash.h"
 #include "util/ntuple.h"
 #include "util/stats.h"
diff --git a/src/theory/bv/equality_engine.cpp b/src/theory/bv/equality_engine.cpp
index ee4e9903c..a4d2e6329 100644
--- a/src/theory/bv/equality_engine.cpp
+++ b/src/theory/bv/equality_engine.cpp
@@ -17,7 +17,7 @@
  ** \todo document this file
  **/
 
-#include "equality_engine.h"
+#include "theory/bv/equality_engine.h"
 
 using namespace CVC4::theory::bv;