build system fixes

diff --git a/src/Makefile.am b/src/Makefile.am
index 4244bd0532c3f84d688349d76f18f8e6d944e66c..5b245d303724bc442ee08a3e7d27c52c1e53ac3a 100644 (file)
--- 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 52fb4a21e11e5d95ad03839e942838a638b96bd2..2552e39d6a2d8b76fd39abcaa60ba908a3bb2054 100644 (file)
--- 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 aa18c11191af463c198b7f6909633de43428cad9..25765f0f028b084643dd0307d5b01405b78a03d3 100644 (file)
--- 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 14fee33c9ba70269ec99dc4a06a3da2f462f964d..6a070a88a046c0e35e8496a55b1f5baf2fdbae93 100644 (file)
--- 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 ba0ebdd2043c913573462cef75a241cc308b3498..7867a1d4efc6a480c8449a5015dd631e96ccd1d7 100644 (file)
--- 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 93df4fe38062975411f612dfc9e11f9eec0bab8b..689ca4cddce5b2d583483a81c83d520417bf8b7e 100644 (file)
--- 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 e909e1705965c3f20541d4a227ac7805247968de..e915fe48306dbb84e6bae8661b1e5391474e141f 100644 (file)
--- 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