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>

diff --git a/contrib/cut-release b/contrib/cut-release
index 5ca8d5a9b144f89d7c470fc6ea7ed0c184c70b01..8f707dcc321109e7bcd88ef9defedd041f26b034 100755 (executable)
--- 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 906a64a652acccc1d42deb5b1a90b5cbb62ed721..627a89a67e9ab3c3734a1e14515bc15d2f118afa 100644 (file)
--- 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 58fb70dcb9950bb33f3012e25f2a49b9c07ee006..6a8a98547d614ae2d07b0b1e3376cfb1414e840a 100644 (file)
--- 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 ce372be702023d4c1698577bf9acc482798a74b0..14fea74787709774365c12ed9e3572f5645b5f5b 100644 (file)
--- 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 3ce1e922481aa79dd2f7a583d97f727c43ab76ce..c6bcc04f854833cbeb3dd213d5c67a4e945ecc2e 100644 (file)
--- 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 1914bb736f8fb57fe5fd7d5f5fcd2abd3665e182..ded7ad8fe52cc586b17b3b804119045915e21113 100644 (file)
--- 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 ef576839c9c8b5960aaa7058a275d11942cbb39f..f2d6f1714fe157324d0e27028f771cb803aff2e6 100644 (file)
--- 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 ef19e1604b90c1c8e24051f7769ad24a6d9ebb47..ec0a00ff888929c36902ff887841ce6365b5e03e 100644 (file)
--- 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 255d84205e6b295e1d56ae5df05dd5cb4c346f9a..89aa5c6aa7c3c1e3905221302750f69c6baae2cb 100644 (file)
--- 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 ec3b7077ee8701f05189e89d9676249656e62421..e52145d4e751ac0251834f7c33118b2c28bb26cd 100644 (file)
--- 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 913dd80132587c149be59620eed57777e0c8ddb6..dca26ab753196897589e60a6c14116fb074c04d5 100644 (file)
--- 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 2805d518a4f6e06602331a202e110b9700139ae5..870edb92825d1646aa2ff56cfdd14d0177321472 100644 (file)
--- 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 71b8849e54c05127e842973b03bd8522688776e2..f05c9007a09f4955d834f7e5ffac4bdc66d89169 100644 (file)
--- 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 27b20734248d71bd257b9e09d6ea8e5263764123..70c887371a3f3dd48f764c46a550e5f67e679e42 100644 (file)
--- 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 3f2ec107a3b6fd80237080ef426dfe7cbd1483b5..f1ad4b330172a60f6bd491683a0228fb947fa533 100644 (file)
--- 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 d4725c4bc0d6aa6495e7383d8beb2b0ef9d99f2a..5c755b5f68390271aee0047fcee4da50835a269f 100644 (file)
--- 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 d368339f55d513feefa6ae2f49550510cc7bad7d..85a117dd05fe26171d033d63ef5d0c47cc6539ea 100644 (file)
--- 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 acd0e17f60aeeeceaba977f7b50ea75a953e4a9b..8f43b0acfb1a3584fd0cc11a11da5818e8c7b69e 100644 (file)
--- 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 a8dc397659f15db8234432dc6ae1c0ae4244449e..5e5d55f638cc5b62fd326b567f615cadb5bee0cf 100644 (file)
--- 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 1e06621b4c7b8d6b1ab020873c29e84f8be855c2..50ded875859a8e15b9de40336d5474c07049aa3a 100644 (file)
--- 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 7fa215bfcf5c00012a7002b5fa27f757df2a11c5..366c2d3f703120d5e70700ada92545bcadef6da9 100644 (file)
--- 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 ee4e9903c659aa02d8bd57d2967f2afda76a151f..a4d2e6329af664bdf89bf19e58ee79cbaf8c2fc5 100644 (file)
--- 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;