summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/Makefile.am12
-rw-r--r--src/expr/Makefile.am82
-rw-r--r--src/expr/declaration_scope.h2
-rw-r--r--src/parser/cvc/Makefile.am6
-rw-r--r--src/parser/smt/Makefile.am6
-rw-r--r--src/parser/smt2/Makefile.am8
-rw-r--r--src/prop/Makefile.am3
-rw-r--r--src/theory/Makefile.am22
-rw-r--r--src/theory/Makefile.subdirs1
-rw-r--r--src/theory/arith/Makefile.am5
-rw-r--r--src/util/Makefile.am1
11 files changed, 83 insertions, 65 deletions
diff --git a/src/Makefile.am b/src/Makefile.am
index 97c66ac89..e436971fa 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -42,6 +42,12 @@ libcvc4_noinst_la_LIBADD = \
@builddir@/smt/libsmt.la \
@builddir@/theory/libtheory.la
+EXTRA_DIST = \
+ include/cvc4parser_private.h \
+ include/cvc4parser_public.h \
+ include/cvc4_private.h \
+ include/cvc4_public.h
+
# empty.cpp hack; see above
empty.cpp:; touch empty.cpp
@@ -55,3 +61,9 @@ install-data-local: $(publicheaders)
echo $(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
$(INSTALL_DATA) "$(srcdir)/$$f" "$(DESTDIR)/$(includedir)/cvc4"; \
done
+
+uninstall-local:
+ @for f in $(publicheaders); do \
+ rm -f "$(DESTDIR)/$(includedir)/cvc4/$$f"
+ done
+ rmdir "$(DESTDIR)/$(includedir)/cvc4"
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index db863440c..5f2453898 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -10,47 +10,63 @@ libexpr_la_SOURCES = \
node.cpp \
type_node.h \
type_node.cpp \
+ type_constant.h \
node_builder.h \
convenience_node_builders.h \
- @srcdir@/expr.h \
type.h \
type.cpp \
node_value.h \
node_manager.h \
- @srcdir@/expr_manager.h \
attribute.h \
+ attribute_internals.h \
attribute.cpp \
- @srcdir@/kind.h \
- @srcdir@/metakind.h \
node_manager.cpp \
- @srcdir@/expr_manager.cpp \
node_value.cpp \
- @srcdir@/expr.cpp \
command.h \
command.cpp \
declaration_scope.h \
declaration_scope.cpp \
expr_manager_scope.h
+nodist_libexpr_la_SOURCES = \
+ kind.h \
+ metakind.h \
+ expr.h \
+ expr.cpp \
+ expr_manager.h \
+ expr_manager.cpp
EXTRA_DIST = \
- @srcdir@/kind.h \
- @srcdir@/metakind.h \
- @srcdir@/expr_manager.h \
- @srcdir@/expr.h \
- @srcdir@/expr_manager.cpp \
- @srcdir@/expr.cpp \
- @srcdir@/type.h \
- @srcdir@/type.cpp \
kind_template.h \
metakind_template.h \
expr_manager_template.h \
expr_manager_template.cpp \
expr_template.h \
- expr_template.cpp
+ expr_template.cpp \
+ mkkind \
+ mkmetakind \
+ mkexpr
+
+BUILT_SOURCES = \
+ kind.h \
+ metakind.h \
+ expr.h \
+ expr.cpp \
+ expr_manager.h \
+ expr_manager.cpp \
+ $(top_builddir)/src/theory/.subdirs
+
+CLEANFILES = \
+ kind.h \
+ metakind.h \
+ expr.h \
+ expr.cpp \
+ expr_manager.h \
+ expr_manager.cpp \
+ $(top_builddir)/src/theory/.subdirs
include @top_srcdir@/src/theory/Makefile.subdirs
-@srcdir@/kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+kind.h: kind_template.h mkkind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkkind
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkkind \
@@ -58,7 +74,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-@srcdir@/metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+metakind.h: metakind_template.h mkmetakind @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkmetakind
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkmetakind \
@@ -66,7 +82,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-@srcdir@/expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.h: expr_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkexpr
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -74,7 +90,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-@srcdir@/expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr.cpp: expr_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkexpr
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -82,7 +98,7 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-@srcdir@/expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.h: expr_manager_template.h mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkexpr
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkexpr \
@@ -90,34 +106,10 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-@srcdir@/expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+expr_manager.cpp: expr_manager_template.cpp mkexpr @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mkexpr
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mkexpr \
$< \
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-
-BUILT_SOURCES = \
- @srcdir@/kind.h \
- @srcdir@/metakind.h \
- @srcdir@/expr.h \
- @srcdir@/expr.cpp \
- @srcdir@/expr_manager.h \
- @srcdir@/expr_manager.cpp
-
-dist-hook: \
- @srcdir@/kind.h \
- @srcdir@/metakind.h \
- @srcdir@/expr.h \
- @srcdir@/expr.cpp \
- @srcdir@/expr_manager.h \
- @srcdir@/expr_manager.cpp
-
-MAINTAINERCLEANFILES = \
- @srcdir@/kind.h \
- @srcdir@/metakind.h \
- @srcdir@/expr.h \
- @srcdir@/expr.cpp \
- @srcdir@/expr_manager.h \
- @srcdir@/expr_manager.cpp
diff --git a/src/expr/declaration_scope.h b/src/expr/declaration_scope.h
index 2318699e7..83462c355 100644
--- a/src/expr/declaration_scope.h
+++ b/src/expr/declaration_scope.h
@@ -19,7 +19,7 @@
#ifndef DECLARATION_SCOPE_H_
#define DECLARATION_SCOPE_H_
-#include "expr.h"
+#include "expr/expr.h"
#include "util/hash.h"
#include <ext/hash_map>
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index cfe983727..ea67ef356 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -28,8 +28,10 @@ libparsercvc_la_SOURCES = \
cvc_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/parser/smt/Makefile.am b/src/parser/smt/Makefile.am
index f5ea3aae3..19665b0f7 100644
--- a/src/parser/smt/Makefile.am
+++ b/src/parser/smt/Makefile.am
@@ -30,8 +30,10 @@ libparsersmt_la_SOURCES = \
smt_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index aabae5352..99ff0daba 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -25,13 +25,15 @@ ANTLR_STUFF = \
libparsersmt2_la_SOURCES = \
Smt2.g \
smt2.h \
- smt2.cpp \
+ smt2.cpp \
smt2_input.h \
smt2_input.cpp \
$(ANTLR_STUFF)
-BUILT_SOURCES = $(ANTLR_STUFF)
-dist-hook: $(ANTLR_STUFF)
+BUILT_SOURCES = $(ANTLR_STUFF) @srcdir@/stamp-generated
+
+EXTRA_DIST = @srcdir@/stamp-generated
+
MAINTAINERCLEANFILES = $(ANTLR_STUFF)
maintainer-clean-local:
-$(AM_V_at)rmdir @srcdir@/generated
diff --git a/src/prop/Makefile.am b/src/prop/Makefile.am
index 06504e73c..dbd32c062 100644
--- a/src/prop/Makefile.am
+++ b/src/prop/Makefile.am
@@ -11,7 +11,6 @@ libprop_la_SOURCES = \
sat.h \
sat.cpp \
cnf_stream.h \
- cnf_stream.cpp \
- cnf_conversion.h
+ cnf_stream.cpp
SUBDIRS = minisat
diff --git a/src/theory/Makefile.am b/src/theory/Makefile.am
index a2a206d40..ce15b86d4 100644
--- a/src/theory/Makefile.am
+++ b/src/theory/Makefile.am
@@ -6,12 +6,15 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
noinst_LTLIBRARIES = libtheory.la
libtheory_la_SOURCES = \
- @srcdir@/theoryof_table.h \
+ output_channel.h \
+ interrupted.h \
theory_engine.h \
theory_engine.cpp \
theory_test_utils.h \
theory.h \
theory.cpp
+nodist_libtheory_la_SOURCES = \
+ theoryof_table.h
libtheory_la_LIBADD = \
@builddir@/builtin/libbuiltin.la \
@@ -22,12 +25,19 @@ libtheory_la_LIBADD = \
@builddir@/bv/libbv.la
EXTRA_DIST = \
- @srcdir@/theoryof_table.h \
- theoryof_table_template.h
+ theoryof_table_template.h \
+ mktheoryof \
+ Makefile.subdirs
+
+BUILT_SOURCES = \
+ theoryof_table.h
+
+CLEANFILES = \
+ theoryof_table.h
include @top_srcdir@/src/theory/Makefile.subdirs
-@srcdir@/theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
+theoryof_table.h: theoryof_table_template.h mktheoryof @top_builddir@/src/theory/.subdirs @top_srcdir@/src/theory/*/kinds
$(AM_V_at)chmod +x @srcdir@/mktheoryof
$(AM_V_at)$(am__mv) $@ $@~ 2>/dev/null || true
$(AM_V_GEN)(@srcdir@/mktheoryof \
@@ -35,8 +45,4 @@ include @top_srcdir@/src/theory/Makefile.subdirs
`cat @top_builddir@/src/theory/.subdirs` \
> $@) || (rm -f $@ && exit 1)
-BUILT_SOURCES = @srcdir@/theoryof_table.h
-dist-hook: @srcdir@/theoryof_table.h
-MAINTAINERCLEANFILES = @srcdir@/theoryof_table.h
-
SUBDIRS = builtin booleans uf arith arrays bv
diff --git a/src/theory/Makefile.subdirs b/src/theory/Makefile.subdirs
index 0dfba2449..eafb350ae 100644
--- a/src/theory/Makefile.subdirs
+++ b/src/theory/Makefile.subdirs
@@ -4,3 +4,4 @@ $(top_builddir)/src/theory/.subdirs: $(top_srcdir)/src/theory/Makefile.am
echo " GEN " $@; \
$(am__mv) $(top_builddir)/src/theory/.subdirs.tmp $(top_builddir)/src/theory/.subdirs; \
fi
+
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index 4d299e8af..e500f5cf8 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -18,7 +18,6 @@ libarith_la_SOURCES = \
partial_model.cpp \
ordered_bounds_list.h \
basic.h \
- normal.h \
slack.h \
tableau.h \
arith_propagator.h \
@@ -26,4 +25,6 @@ libarith_la_SOURCES = \
theory_arith.h \
theory_arith.cpp
-EXTRA_DIST = kinds
+EXTRA_DIST = \
+ kinds \
+ normal_form_notes.txt
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b6ca5bcc6..a690f7432 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -16,6 +16,7 @@ libutil_la_SOURCES = \
decision_engine.h \
exception.h \
hash.h \
+ bool.h \
model.h \
options.h \
output.cpp \
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback