diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Makefile.am | 10 | ||||
-rw-r--r-- | src/bindings/compat/c/c_interface.cpp | 2 | ||||
-rw-r--r-- | src/bindings/compat/c/c_interface.h | 2 | ||||
-rw-r--r-- | src/bindings/compat/java/include/cvc3/JniUtils.h | 7 | ||||
-rw-r--r-- | src/expr/node_builder.h | 4 | ||||
-rw-r--r-- | src/main/interactive_shell.cpp | 8 | ||||
-rw-r--r-- | src/main/main.cpp | 4 | ||||
-rw-r--r-- | src/main/util.cpp | 2 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 14 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 6 | ||||
-rw-r--r-- | src/parser/antlr_input_imports.cpp | 6 | ||||
-rw-r--r-- | src/parser/bounded_token_factory.cpp | 2 | ||||
-rw-r--r-- | src/parser/input.cpp | 6 | ||||
-rw-r--r-- | src/parser/parser.cpp | 6 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 6 | ||||
-rw-r--r-- | src/parser/smt/smt_input.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/smt2_input.cpp | 2 | ||||
-rw-r--r-- | src/proof/cnf_proof.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/array_info.cpp | 2 | ||||
-rw-r--r-- | src/theory/arrays/theory_arrays.h | 2 | ||||
-rw-r--r-- | src/theory/bv/equality_engine.cpp | 2 |
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; |