fix some build dependencies in options-building; should fix a strange bug Andy saw...

diff --git a/src/options/Makefile.am b/src/options/Makefile.am
index e1cd721f3767cb1160f8c919fcca955d24fbb863..088c972b3f585b62ea2388446adf0b77763ad1c3 100644 (file)
--- a/src/options/Makefile.am
+++ b/src/options/Makefile.am
@@ -1,23 +1,45 @@
+OPTIONS_FILES_SRCS = \
+       base_options.cpp \
+       base_options.h \
+       ../expr/options.cpp \
+       ../expr/options.h \
+       ../theory/booleans/options.cpp \
+       ../theory/booleans/options.h \
+       ../theory/options.cpp \
+       ../theory/options.h \
+       ../theory/bv/options.cpp \
+       ../theory/bv/options.h \
+       ../theory/datatypes/options.cpp \
+       ../theory/datatypes/options.h \
+       ../theory/builtin/options.cpp \
+       ../theory/builtin/options.h \
+       ../theory/arith/options.cpp \
+       ../theory/arith/options.h \
+       ../theory/uf/options.cpp \
+       ../theory/uf/options.h \
+       ../theory/arrays/options.cpp \
+       ../theory/arrays/options.h \
+       ../theory/quantifiers/options.cpp \
+       ../theory/quantifiers/options.h \
+       ../theory/rewriterules/options.cpp \
+       ../theory/rewriterules/options.h \
+       ../prop/options.cpp \
+       ../prop/options.h \
+       ../proof/options.cpp \
+       ../proof/options.h \
+       ../printer/options.cpp \
+       ../printer/options.h \
+       ../smt/options.cpp \
+       ../smt/options.h \
+       ../decision/options.cpp \
+       ../decision/options.h \
+       ../main/options.cpp \
+       ../main/options.h \
+       ../parser/options.cpp \
+       ../parser/options.h
+
 OPTIONS_FILES = \
-       options/base_options \
-       expr/options \
-       theory/booleans/options \
-       theory/options \
-       theory/bv/options \
-       theory/datatypes/options \
-       theory/builtin/options \
-       theory/arith/options \
-       theory/uf/options \
-       theory/arrays/options \
-       theory/quantifiers/options \
-       theory/rewriterules/options \
-       prop/options \
-       proof/options \
-       printer/options \
-       smt/options \
-       decision/options \
-       main/options \
-       parser/options
+       $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
 
 AM_CPPFLAGS = \
        -D__BUILDING_CVC4LIB \
@@ -32,37 +54,67 @@ liboptions_la_SOURCES = \
        option_exception.h
 
 nodist_liboptions_la_SOURCES = \
-       options.cpp \
-       options_holder.h \
-       $(OPTIONS_FILES:%=../%.cpp) \
-       $(OPTIONS_FILES:%=../%.h)
-nodist_liboptions_la_OBJECTS = \
-       $(patsubst %.cpp,%.lo,$(filter %.cpp,$(nodist_liboptions_la_SOURCES)))
-
-BUILT_SOURCES = \
        options.cpp \
        options_holder.h \
        base_options.cpp \
        base_options.h \
+       ../expr/options.cpp \
+       ../expr/options.h \
+       ../theory/booleans/options.cpp \
+       ../theory/booleans/options.h \
+       ../theory/options.cpp \
+       ../theory/options.h \
+       ../theory/bv/options.cpp \
+       ../theory/bv/options.h \
+       ../theory/datatypes/options.cpp \
+       ../theory/datatypes/options.h \
+       ../theory/builtin/options.cpp \
+       ../theory/builtin/options.h \
+       ../theory/arith/options.cpp \
+       ../theory/arith/options.h \
+       ../theory/uf/options.cpp \
+       ../theory/uf/options.h \
+       ../theory/arrays/options.cpp \
+       ../theory/arrays/options.h \
+       ../theory/quantifiers/options.cpp \
+       ../theory/quantifiers/options.h \
+       ../theory/rewriterules/options.cpp \
+       ../theory/rewriterules/options.h \
+       ../prop/options.cpp \
+       ../prop/options.h \
+       ../proof/options.cpp \
+       ../proof/options.h \
+       ../printer/options.cpp \
+       ../printer/options.h \
+       ../smt/options.cpp \
+       ../smt/options.h \
+       ../decision/options.cpp \
+       ../decision/options.h \
+       ../main/options.cpp \
+       ../main/options.h \
+       ../parser/options.cpp \
+       ../parser/options.h
+
+BUILT_SOURCES = \
+       exprs-builts \
        ../smt/smt_options.cpp \
-       $(OPTIONS_FILES:%=../%.cpp) \
-       $(OPTIONS_FILES:%=../%.h) \
-       exprs-builts
+       options.cpp \
+       options_holder.h
 
 DISTCLEANFILES = \
+       $(OPTIONS_FILES_SRCS) \
        $(BUILT_SOURCES) \
        options-stamp
 
 EXTRA_DIST = \
        mkoptions \
-       base_options \
        base_options_template.h \
        base_options_template.cpp \
        options_template.cpp \
        options_holder_template.h \
        options.i \
        option_exception.i \
-       $(OPTIONS_FILES:%=../%)
+       $(OPTIONS_FILES)
 
 if CVC4_DEBUG
 # listing Debug_tags too ensures that make doesn't auto-remove it
@@ -116,8 +168,8 @@ MOSTLYCLEANFILES = \
        Debug_tags.h \
        Trace_tags.h
 
-options_holder.h options.cpp ../smt/smt_options.cpp base_options.cpp base_options.h $(OPTIONS_FILES:%=../%.cpp) $(OPTIONS_FILES:%=../%.h): options-stamp
-options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES:%=../%)
+options_holder.h options.cpp ../smt/smt_options.cpp $(OPTIONS_FILES_SRCS): options-stamp
+options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILES)
        $(AM_V_at)chmod +x @srcdir@/mkoptions
        $(AM_V_GEN)(@srcdir@/mkoptions \
                @srcdir@/options_holder_template.h @builddir@/options_holder.h \
@@ -126,11 +178,11 @@ options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options
                @top_builddir@/doc/cvc4.1_template @top_builddir@/doc/cvc4.1 \
                -t \
                @srcdir@/base_options_template.h @srcdir@/base_options_template.cpp \
-               $(foreach o,$(OPTIONS_FILES),"$(srcdir)/../$(o)" "$(dir $(builddir)/../$(o))") \
+               $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)" "$(dir $(builddir)/$(o))") \
        )
        touch "$@"
 
-base_options $(OPTIONS_FILES:%=../%):;
+$(OPTIONS_FILES):;
 
 .PHONY: exprs-builts
 exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true

diff --git a/src/options/mkoptions b/src/options/mkoptions
index a551d5bd970380ceea35a72341585b0de356c5a9..540e2b77ad363a851661cc924005bd7504e6a0d5 100755 (executable)
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -2,7 +2,7 @@
 #
 # mkoptions
 # Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2011  The CVC4 Project
+# Copyright (c) 2011-2012  The CVC4 Project
 #
 # The purpose of this script is to create options.{h,cpp}
 # from template files and a list of options.
@@ -12,7 +12,7 @@
 #   mkoptions (template-file output-file)+ -t options.h-template options.cpp-template (options-file output-dir)+
 #
 
-copyright=2011
+copyright=2011-2012
 
 me=$(basename "$0")
 
@@ -1103,14 +1103,18 @@ EOF
 
   ) >"$output.tmp"
 
-  diff -q "$output" "$output.tmp" &>/dev/null || (mv -f "$output.tmp" "$output" && echo "regenerated $output")
-  rm -f "$output.tmp"
+  if diff -q "$output" "$output.tmp" &>/dev/null; then
+    rm -f "$output.tmp"
+  else
+    mv -f "$output.tmp" "$output"
+    echo "regenerated $output"
+  fi
 }
 
 while [ $# -gt 0 ]; do
   kf="$1"; shift
   if [ $# -eq 0 ]; then
-    echo "$me: error: mismatched number of templates and output files (before -t)" >&2
+    echo "$me: error: mismatched number of templates and output files (after -t)" >&2
     usage
     exit 1
   fi