From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 29 Sep 2011 06:40:27 +0000 (+0000)
Subject: build system fixes
X-Git-Tag: cvc5-1.0.0~8447
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42f89e550bb15d401c335ded7912a871b2b45af3;p=cvc5.git

build system fixes
---

diff --git a/src/Makefile.am b/src/Makefile.am
index 4244bd053..5b245d303 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -53,6 +53,11 @@ libcvc4_noinst_la_LIBADD = \
 	@builddir@/theory/libtheory.la \
 	@builddir@/lib/libreplacements.la
 
+CLEANFILES = \
+	subversion_versioninfo.cpp \
+	svninfo.tmp \
+	svninfo
+
 EXTRA_DIST = \
 	include/cvc4parser_private.h \
 	include/cvc4parser_public.h \
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 52fb4a21e..2552e39d6 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -39,6 +39,7 @@ endif
 #	cvc4bindings_tcl.so
 
 nodist_libcvc4bindings_java_la_SOURCES = java.cpp
+libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
 nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp
 nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp
 nodist_libcvc4bindings_php_la_SOURCES = php.cpp
@@ -47,7 +48,7 @@ nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp
 nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp
 nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp
 
-BUILT_SOURCES = \
+CLEANFILES = \
 	java.cpp \
 	csharp.cpp \
 	perl.cpp \
@@ -59,8 +60,7 @@ BUILT_SOURCES = \
 
 EXTRA_DIST = swig.h
 
-CLEANFILES = \
-	$(BUILT_SOURCES) \
+MOSTLYCLEANFILES = \
         .swig_deps \
 	$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
 	cvc4.jar
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index aa18c1119..25765f0f0 100644
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -147,4 +147,4 @@ cvc4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class)
 
 clean-local:
 	rm -fr classes cvc3
-CLEANFILES = .cvc3dir .classes .headers cvc4compat.jar
+MOSTLYCLEANFILES = .cvc3dir .classes .headers cvc4compat.jar $(JNI_CPP_FILES)
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 14fee33c9..6a070a88a 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -80,6 +80,7 @@ CLEANFILES = \
 	expr_manager.h \
 	expr_manager.cpp \
 	type_checker.cpp \
+	type_properties.h \
 	$(top_builddir)/src/theory/.subdirs
 
 include @top_srcdir@/src/theory/Makefile.subdirs
diff --git a/src/lib/Makefile.am b/src/lib/Makefile.am
index ba0ebdd20..7867a1d4e 100644
--- a/src/lib/Makefile.am
+++ b/src/lib/Makefile.am
@@ -15,5 +15,7 @@ EXTRA_DIST = \
 	clock_gettime.c \
 	clock_gettime.h
 
+CLEANFILES = empty.c
+
 # empty.c hack -- need *some* source file so that library make rules are built
 empty.c:; touch empty.c
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 93df4fe38..689ca4cdd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -275,13 +275,13 @@ bool TheoryEngine::properConflict(TNode conflict) const {
 
 bool TheoryEngine::properPropagation(TNode lit) const {
   Assert(!lit.isNull());
-#warning fixme
+#warning implement TheoryEngine::properPropagation()
   return true;
 }
 
 bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
   Assert(!node.isNull() && !expl.isNull());
-#warning fixme
+#warning implement TheoryEngine::properExplanation()
   return true;
 }
 
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index e909e1705..e915fe483 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -161,3 +161,19 @@ EXTRA_DIST = \
 	rational.i \
 	pseudoboolean.i \
 	hash.i
+
+MOSTLYCLEANFILES = \
+	Debug_tags \
+	Trace_tags \
+	Debug_tags.tmp \
+	Trace_tags.tmp \
+	Debug_tags.h \
+	Trace_tags.h
+
+DISTCLEANFILES = \
+	integer.h.tmp \
+	rational.h.tmp \
+	tls.h.tmp \
+	integer.h \
+	rational.h \
+	tls.h