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>

21 files changed, 52 insertions, 45 deletions

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;