diff options
Diffstat (limited to 'src/options/Makefile.am')
| -rw-r--r-- | src/options/Makefile.am | 495 |
1 files changed, 297 insertions, 198 deletions
diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 0d4b970d8..d871bfb0a 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -1,65 +1,177 @@ -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/strings/options.cpp \ - ../theory/strings/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 \ - ../theory/idl/options.cpp \ - ../theory/idl/options.h \ - ../theory/sets/options.cpp \ - ../theory/sets/options.h \ - ../theory/fp/options.cpp \ - ../theory/fp/options.h - -OPTIONS_FILES = \ - $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) - -OPTIONS_CPPS = \ - $(filter %.cpp,$(OPTIONS_FILES_SRCS)) - -OPTIONS_HEADS = \ - $(filter %.h,$(OPTIONS_FILES_SRCS)) +# How options are built: +# Step 1: Copy the X_options source file into builddir as X_options.tmp. +# X_options.tmp is a .PHONY rule to force this step to always be done. +# Step 2: Compare X_options.tmp to X_options.options. +# If they are different, overwrite "X_options.options". +# This is the file that we use to generate options from. +# This is always up to dat with X_options. The change in name is just +# to keep Makefile stage more explicit. +# Step 3: Generate X_options.sed from X_options.options using mkoptions. +# Step 4: Generate X_options.h from X_options.sed +# Step 5: Generate X_options.cpp from X_options.sed. +# This stage also waits for X_options.h as otherwise it cannot compile. +# + +OPTIONS_SRC_FILES = \ + arith_options \ + arrays_options \ + base_options \ + booleans_options \ + builtin_options \ + bv_options \ + datatypes_options \ + decision_options \ + expr_options \ + fp_options \ + idl_options \ + main_options \ + parser_options \ + printer_options \ + proof_options \ + prop_options \ + quantifiers_options \ + sets_options \ + smt_options \ + strings_options \ + theory_options \ + uf_options + +OPTIONS_TEMPS = \ + arith_options.tmp \ + arrays_options.tmp \ + base_options.tmp \ + booleans_options.tmp \ + builtin_options.tmp \ + bv_options.tmp \ + datatypes_options.tmp \ + decision_options.tmp \ + expr_options.tmp \ + fp_options.tmp \ + idl_options.tmp \ + main_options.tmp \ + parser_options.tmp \ + printer_options.tmp \ + proof_options.tmp \ + prop_options.tmp \ + quantifiers_options.tmp \ + sets_options.tmp \ + smt_options.tmp \ + strings_options.tmp \ + theory_options.tmp \ + uf_options.tmp + +OPTIONS_OPTIONS_FILES = \ + arith_options.options \ + arrays_options.options \ + base_options.options \ + booleans_options.options \ + builtin_options.options \ + bv_options.options \ + datatypes_options.options \ + decision_options.options \ + expr_options.options \ + fp_options.options \ + idl_options.options \ + main_options.options \ + parser_options.options \ + printer_options.options \ + proof_options.options \ + prop_options.options \ + quantifiers_options.options \ + sets_options.options \ + smt_options.options \ + strings_options.options \ + theory_options.options \ + uf_options.options OPTIONS_SEDS = \ - $(patsubst %,%.sed,$(OPTIONS_FILES)) + arith_options.sed \ + arrays_options.sed \ + base_options.sed \ + booleans_options.sed \ + builtin_options.sed \ + bv_options.sed \ + datatypes_options.sed \ + decision_options.sed \ + expr_options.sed \ + fp_options.sed \ + idl_options.sed \ + main_options.sed \ + parser_options.sed \ + printer_options.sed \ + proof_options.sed \ + prop_options.sed \ + quantifiers_options.sed \ + sets_options.sed \ + smt_options.sed \ + strings_options.sed \ + theory_options.sed \ + uf_options.sed -OPTIONS_OBJ = \ - $(patsubst %.cpp,%.$(OBJEXT),$(OPTIONS_CPP)) +OPTIONS_HEADS = \ + arith_options.h \ + arrays_options.h \ + base_options.h \ + booleans_options.h \ + builtin_options.h \ + bv_options.h \ + datatypes_options.h \ + decision_options.h \ + expr_options.h \ + fp_options.h \ + idl_options.h \ + main_options.h \ + parser_options.h \ + printer_options.h \ + proof_options.h \ + prop_options.h \ + quantifiers_options.h \ + sets_options.h \ + smt_options.h \ + strings_options.h \ + theory_options.h \ + uf_options.h +OPTIONS_CPPS = \ + arith_options.cpp \ + arrays_options.cpp \ + base_options.cpp \ + booleans_options.cpp \ + builtin_options.cpp \ + bv_options.cpp \ + datatypes_options.cpp \ + decision_options.cpp \ + expr_options.cpp \ + fp_options.cpp \ + idl_options.cpp \ + main_options.cpp \ + parser_options.cpp \ + printer_options.cpp \ + proof_options.cpp \ + prop_options.cpp \ + quantifiers_options.cpp \ + sets_options.cpp \ + smt_options.cpp \ + strings_options.cpp \ + theory_options.cpp \ + uf_options.cpp + + +CPP_TEMPLATE_FILES = \ + base_options_template.h \ + base_options_template.cpp \ + options_holder_template.h \ + options_template.cpp \ + options_handler_get_option_template.cpp \ + options_handler_set_option_template.cpp +CPP_TEMPLATE_SEDS = \ + base_options_template.h.sed \ + base_options_template.cpp.sed \ + options_holder_template.h.sed \ + options_template.cpp.sed \ + options_handler_get_option_template.cpp.sed \ + options_handler_set_option_template.cpp.sed DOCUMENTATION_FILES = \ @@ -68,19 +180,17 @@ DOCUMENTATION_FILES = \ ../../doc/SmtEngine.3cvc \ ../../doc/options.3cvc -TEMPLATE_FILES = \ - base_options_template.h \ - base_options_template.cpp \ - options_holder_template.h \ - options_template.cpp \ - ../smt/smt_options_template.cpp \ +DOCUMENTATION_TEMPLATE_FILES = \ ../../doc/cvc4.1_template \ ../../doc/libcvc4.3_template \ ../../doc/SmtEngine.3cvc_template \ ../../doc/options.3cvc_template -TEMPLATE_SEDS = \ - $(patsubst %,%.sed,$(TEMPLATE_FILES)) +DOCUMENTATION_TEMPLATE_SEDS = \ + ../../doc/cvc4.1_template.sed \ + ../../doc/libcvc4.3_template.sed \ + ../../doc/SmtEngine.3cvc_template.sed \ + ../../doc/options.3cvc_template.sed AM_CPPFLAGS = \ -D__BUILDING_CVC4LIB \ @@ -90,63 +200,98 @@ AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN) noinst_LTLIBRARIES = liboptions.la liboptions_la_SOURCES = \ + arith_heuristic_pivot_rule.cpp \ + arith_heuristic_pivot_rule.h \ + arith_propagation_mode.cpp \ + arith_propagation_mode.h \ + arith_unate_lemma_mode.cpp \ + arith_unate_lemma_mode.h \ + base_handlers.h \ + boolean_term_conversion_mode.cpp \ + boolean_term_conversion_mode.h \ + bv_bitblast_mode.cpp \ + bv_bitblast_mode.h \ + decision_mode.cpp \ + decision_mode.h \ + decision_weight.h \ + didyoumean.cpp \ + didyoumean.h \ + language.cpp \ + language.h \ + logic_info_forward.h \ + option_exception.h \ options.h \ - base_options_handlers.h \ - option_exception.h + options_handler_interface.cpp \ + options_handler_interface.h \ + printer_modes.cpp \ + printer_modes.h \ + quantifiers_modes.cpp \ + quantifiers_modes.h \ + simplification_mode.cpp \ + simplification_mode.h \ + theoryof_mode.cpp \ + theoryof_mode.h \ + ufss_mode.h + nodist_liboptions_la_SOURCES = \ options.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) + $(OPTIONS_HEADS) \ + $(OPTIONS_CPPS) \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp BUILT_SOURCES = \ - exprs-builts \ - ../smt/smt_options.cpp \ + $(CPP_TEMPLATE_SEDS) \ + $(DOCUMENTATION_FILES) \ + $(DOCUMENTATION_TEMPLATE_SEDS) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_OPTIONS_FILES) \ + $(OPTIONS_SEDS) \ options.cpp \ + options_handler_get_option.cpp \ + options_handler_set_option.cpp \ options_holder.h \ - $(OPTIONS_FILES_SRCS) \ - $(OPTIONS_SEDS) \ - summary.sed \ - $(TEMPLATE_SEDS) - + summary.sed -# The documentation files are added to BUILT_SOURCES to get the files to -# be built. Alternative suggestions for building these files would be -# appreciated. +# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it +# after building (if it does, we don't get the "cached" effect with +# the .tmp files below, and we have to re-compile and re-link each +# time, even when there are no changes). BUILT_SOURCES += \ - $(DOCUMENTATION_FILES) - + Debug_tags.h \ + Debug_tags \ + Trace_tags.h \ + Trace_tags CLEANFILES = \ - $(OPTIONS_FILES_SRCS) \ $(BUILT_SOURCES) \ - $(DOCUMENTATION_FILES) + $(DOCUMENTATION_FILES) \ + $(OPTIONS_TEMPS) EXTRA_DIST = \ - mkoptions \ - base_options_template.h \ + $(DOCUMENTATION_FILES) \ + $(OPTIONS_CPPS) \ + $(OPTIONS_HEADS) \ + $(OPTIONS_SRC_FILES) \ base_options_template.cpp \ - options_template.cpp \ - options_holder_template.h \ - options.i \ - option_exception.i \ - $(OPTIONS_FILES) \ + base_options_template.h \ + language.i \ + mkoptions \ mktagheaders \ mktags \ - $(DOCUMENTATION_FILES) + option_exception.i \ + options.i \ + options_handler_get_option_template.cpp \ + options_handler_interface.i \ + options_handler_set_option_template.cpp \ + options_holder_template.h \ + options_template.cpp -# listing {Debug,Trace}_tags too ensures that make doesn't auto-remove it -# after building (if it does, we don't get the "cached" effect with -# the .tmp files below, and we have to re-compile and re-link each -# time, even when there are no changes). -BUILT_SOURCES += \ - Debug_tags.h \ - Debug_tags \ - Trace_tags.h \ - Trace_tags - %_tags.h: %_tags mktagheaders $(AM_V_at)chmod +x @srcdir@/mktagheaders $(AM_V_GEN)( @srcdir@/mktagheaders "$<" "$<" ) >"$@" @@ -175,52 +320,72 @@ MOSTLYCLEANFILES = \ Debug_tags.h \ Trace_tags.h -# mkoptions template-sed template-file (options-file)* -# mkoptions apply-sed-files-to-template sed-file template-file filename +# Make sure the implicit rules never mistake a _template.cpp or _template.h file for source file. +options_holder_template.h options_template.cpp options_handler_get_option_template.cpp options_handler_set_option_template.cpp base_options_template.h base_options_template.cpp :; + +# Make sure the implicit rules never mistake X_options for the -o file for a +# CPP file. +arith_options arrays_options base_options booleans_options builtin_options bv_options datatypes_options decision_options expr_options fp_options idl_options main_options parser_options printer_options proof_options prop_options quantifiers_options sets_options smt_options strings_options theory_options uf_options:; -$(OPTIONS_FILES):; -options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp :; +# These are phony to force them to be made everytime. +.PHONY: arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp + +# Make is happier being listed explictly. Not sure why. +arith_options.tmp arrays_options.tmp base_options.tmp booleans_options.tmp builtin_options.tmp bv_options.tmp datatypes_options.tmp decision_options.tmp expr_options.tmp fp_options.tmp idl_options.tmp main_options.tmp parser_options.tmp printer_options.tmp proof_options.tmp prop_options.tmp quantifiers_options.tmp sets_options.tmp smt_options.tmp strings_options.tmp theory_options.tmp uf_options.tmp: + echo "$@" "$(@:.tmp=)" + $(AM_V_GEN)(cp "@srcdir@/$(@:.tmp=)" "$@" || true) +#TIM: +#The (... || true) here is to make distcheck not fail. + +%_options.options: %_options.tmp + $(AM_V_GEN)\ + diff -q "$^" "$@" &>/dev/null || mv "$^" "$@" || true -$(TEMPLATE_SEDS) : %.sed : % mkoptions + +# This bit is kinda tricky. +# We use the updating of %_options.options to signal that the options file updated. +# However, we use the original file in src to generate the file. +%_options.sed: %_options.options mkoptions + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions module-sed "@srcdir@/$(@:.sed=)" ) > "$@" + + +$(CPP_TEMPLATE_SEDS): %.sed : % mkoptions # echo "template seds" # echo "$@" # echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" - -$(OPTIONS_SEDS) : %.sed : % mkoptions -# echo "sedheads" +$(DOCUMENTATION_TEMPLATE_SEDS): %.sed : % mkoptions +# echo "template seds" # echo "$@" -# echo $(OPTIONS_SEDS) +# echo $(TEMPLATE_SEDS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` - $(AM_V_GEN)(@srcdir@/mkoptions module-sed "$<" ) > "$@" + $(AM_V_GEN)(@srcdir@/mkoptions template-sed "$<" ) > "$@" -$(OPTIONS_HEADS) : %.h : %.sed mkoptions base_options_template.h base_options_template.h.sed +%_options.h : %_options.sed mkoptions base_options_template.h base_options_template.h.sed # echo heads # echo "$@" # echo $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.h \ base_options_template.h.sed \ "$<" \ ) > "$@" -summary.sed : mkoptions $(OPTIONS_FILES) +summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions summary-sed \ - $(foreach o,$(OPTIONS_FILES),"$(srcdir)/$(o)") \ + $(OPTIONS_OPTIONS_FILES) \ ) > summary.sed # mkoptions apply-sed-to-template sed-file template-file -options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions -# echo "$(OPTIONS_FILES)" +options_holder.h : options_holder_template.h options_holder_template.h.sed summary.sed mkoptions $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_holder_template.h \ @@ -228,19 +393,9 @@ options_holder.h : options_holder_template.h options_holder_template.h.sed summa summary.sed \ ) > "$@" -gen-heads-stamp : $(OPTIONS_HEADS) options_holder.h -.PHONY : gen-heads-stamp - - -# Bit of a hack here. The .h file needs to always be built before the .cpp file is compiled. -$(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options_template.cpp.sed gen-heads-stamp -# echo "cpps" -# echo "$@" -# echo "$<" -# echo $(OPTIONS_CPPS) -# echo $(OPTIONS_FILES_SRCS) +# Make sure not to match with "options.cpp" too. +%_options.cpp: %_options.sed %_options.h mkoptions options_holder.h base_options_template.cpp base_options_template.cpp.sed $(AM_V_at)chmod +x @srcdir@/mkoptions - $(AM_V_at)mkdir -p `dirname "$@"` $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/base_options_template.cpp \ base_options_template.cpp.sed \ @@ -249,9 +404,9 @@ $(OPTIONS_CPPS) : %.cpp : %.sed mkoptions base_options_template.cpp base_options + # mkoptions apply-sed-to-template sed-file template-file -options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) options_holder.h $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ @srcdir@/options_template.cpp \ @@ -261,15 +416,21 @@ options.cpp : options_template.cpp options_template.cpp.sed mkoptions summary.se # mkoptions apply-sed-to-template sed-file template-file -../smt/smt_options.cpp : ../smt/smt_options_template.cpp ../smt/smt_options_template.cpp.sed mkoptions summary.sed gen-heads-stamp -# echo "$(OPTIONS_FILES)" +options_handler_get_option.cpp : options_handler_get_option_template.cpp options_handler_get_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) $(AM_V_at)chmod +x @srcdir@/mkoptions $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ - @srcdir@/../smt/smt_options_template.cpp \ - @builddir@/../smt/smt_options_template.cpp.sed \ + @srcdir@/options_handler_get_option_template.cpp \ + @builddir@/options_handler_get_option_template.cpp.sed \ summary.sed \ ) > "$@" +options_handler_set_option.cpp : options_handler_set_option_template.cpp options_handler_set_option_template.cpp.sed mkoptions summary.sed $(OPTIONS_HEADS) + $(AM_V_at)chmod +x @srcdir@/mkoptions + $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \ + @srcdir@/options_handler_set_option_template.cpp \ + @builddir@/options_handler_set_option_template.cpp.sed \ + summary.sed \ + ) > "$@" @@ -285,7 +446,7 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed -#options-stamp: options_holder_template.h options_template.cpp ../smt/smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) +#options-stamp: options_holder_template.h options_template.cpp smt_options_template.cpp base_options_template.h base_options_template.cpp mkoptions $(OPTIONS_FILE_SRCS) # This rule is ugly. It's needed to ensure that automake's dependence @@ -294,65 +455,3 @@ $(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed # fails. %.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@" -# Tim: -# This is insanely ugly and brittle! -# *Any* proposal to clean this up is welcomed! -# We are overloading automake's default distclean here. We have to overload -# distclean because otherwise it deletes the dependency directory -# "src/expr/.deps", then when running make distclean in src/expr it attempts to -# include .Plo files "defined in src/expr/.deps". -# An example from src/expr/Makefile.ina : -# @AMDEP_TRUE@@am__include@ @am__quote@./$(DEPDIR)/attribute.Plo@am__quote@ -# The include must fail because this make file deleted that directory and -# distclean cannot proceed. So we override distclean to only remove -# "-rm -rf ./$(DEPDIR)". We then do manual massaging to finish up removing the -# extra files. To reproduce this, you can comment out the distclean below, run -# a distcheck and repeat this process. -# Why was this not a problem before? I do not know. -MANUAL_RM = \ - $(CLEANFILES) \ - ../main/.dirstamp \ - ../expr/.dirstamp \ - ../options/options.lo \ - ../options/base_options.lo \ - ../options/.libs/options.o \ - ../options/.libs/base_options.o \ - ../options/.libs/liboptions.a \ - ../options/Trace_tags.tmp \ - ../options/Debug_tags.tmp \ - ../options/liboptions.la \ - ../parser/.dirstamp \ - ../expr/.deps/options.Plo \ - ../main/.deps/options.Plo \ - ../parser/.deps/options.Plo \ - ../prop/options.lo \ - ../decision/options.lo \ - ../printer/options.lo \ - ../proof/options.lo \ - ../smt/options.lo \ - ../theory/arith/options.lo \ - ../theory/arrays/options.lo \ - ../theory/booleans/options.lo \ - ../theory/builtin/options.lo \ - ../theory/bv/options.lo \ - ../theory/datatypes/options.lo \ - ../theory/fp/options.lo \ - ../theory/idl/options.lo \ - ../theory/quantifiers/options.lo \ - ../theory/sets/options.lo \ - ../theory/strings/options.lo \ - ../theory/test_newalttheory/options.lo \ - ../theory/test_newtheory/options.lo \ - ../theory/uf/options.lo \ - ../theory/options.lo - - - -distclean: - -rm -rf ./$(DEPDIR) - -rm -f Makefile - -rm -f $(MANUAL_RM) - -.PHONY: exprs-builts -exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true - |