-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
+# 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 = \
+ 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_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_get_option_template.cpp \
+ options_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_get_option_template.cpp.sed \
+ options_set_option_template.cpp.sed
+
+
+DOCUMENTATION_FILES = \
+ ../../doc/cvc4.1 \
+ ../../doc/libcvc4.3 \
+ ../../doc/SmtEngine.3cvc \
+ ../../doc/options.3cvc
+
+DOCUMENTATION_TEMPLATE_FILES = \
+ ../../doc/cvc4.1_template \
+ ../../doc/libcvc4.3_template \
+ ../../doc/SmtEngine.3cvc_template \
+ ../../doc/options.3cvc_template
+
+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 \
- -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
+ -I@builddir@/.. -I@srcdir@/../include -I@srcdir@/..
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 \
+ argument_extender.cpp \
+ argument_extender.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 \
+ open_ostream.cpp \
+ open_ostream.h \
+ option_exception.h \
options.h \
- base_options_handlers.h
+ options_handler.cpp \
+ options_handler.h \
+ options_public_functions.cpp \
+ printer_modes.cpp \
+ printer_modes.h \
+ quantifiers_modes.cpp \
+ quantifiers_modes.h \
+ set_language.cpp \
+ set_language.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:%=../%.cpp) \
- $(OPTIONS_FILES:%=../%.h)
-nodist_liboptions_la_OBJECTS = \
- $(patsubst %.cpp,%.lo,$(filter %.cpp,$(nodist_liboptions_la_SOURCES)))
+ $(OPTIONS_HEADS) \
+ $(OPTIONS_CPPS) \
+ options_get_option.cpp \
+ options_set_option.cpp
+
BUILT_SOURCES = \
+ $(CPP_TEMPLATE_SEDS) \
+ $(DOCUMENTATION_FILES) \
+ $(DOCUMENTATION_TEMPLATE_SEDS) \
+ $(OPTIONS_CPPS) \
+ $(OPTIONS_HEADS) \
+ $(OPTIONS_OPTIONS_FILES) \
+ $(OPTIONS_SEDS) \
options.cpp \
+ options_get_option.cpp \
+ options_set_option.cpp \
options_holder.h \
- base_options.cpp \
- base_options.h \
- ../smt/smt_options.cpp \
- $(OPTIONS_FILES:%=../%.cpp) \
- $(OPTIONS_FILES:%=../%.h) \
- exprs-builts
+ summary.sed
-DISTCLEANFILES = \
+
+CLEANFILES = \
$(BUILT_SOURCES) \
- options-stamp
+ $(DOCUMENTATION_FILES) \
+ $(OPTIONS_TEMPS)
EXTRA_DIST = \
- mkoptions \
- base_options \
- base_options_template.h \
+ $(DOCUMENTATION_FILES) \
+ $(OPTIONS_CPPS) \
+ $(OPTIONS_HEADS) \
+ $(OPTIONS_SRC_FILES) \
base_options_template.cpp \
- options_template.cpp \
- options_holder_template.h \
+ base_options_template.h \
+ language.i \
+ mkoptions \
+ option_exception.i \
options.i \
- $(OPTIONS_FILES:%=../%)
-
-if CVC4_DEBUG
-# listing Debug_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
-endif
-if CVC4_TRACING
-# listing 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 += \
- Trace_tags.h \
- Trace_tags
-endif
-%_tags.h: %_tags
- $(AM_V_GEN)( \
- echo 'static char const* const $^[] = {'; \
- for tag in `cat $^`; do \
- echo "\"$$tag\","; \
- done; \
- echo 'NULL'; \
- echo '};' \
- ) >"$@"
-
-# This .tmp business is to keep from having to re-compile options.cpp
-# (and then re-link the libraries) if nothing has changed.
-%_tags: %_tags.tmp
+ options_get_option_template.cpp \
+ options_holder_template.h \
+ options_set_option_template.cpp \
+ options_template.cpp
+
+
+
+
+
+# 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_get_option_template.cpp options_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:;
+
+
+# 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
-# .PHONY ensures the .tmp version is always rebuilt (to check for any changes)
-.PHONY: Debug_tags.tmp Trace_tags.tmp
-# The "sed" invocation below is particularly obnoxious, but it works around
-# inconsistencies in REs on different platforms, using only a basic regular
-# expression (no |, no \<, ...).
-Debug_tags.tmp Trace_tags.tmp:
- $(AM_V_GEN)\
- grep '\<$(@:_tags.tmp=) *( *\".*\" *)' \
- `find @srcdir@/../ -name "*.cpp" -or -name "*.h" -or -name "*.cc" -or -name "*.g"` | \
- sed 's/^$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/;s/.*[^a-zA-Z0-9_]$(@:_tags.tmp=) *( *\"\([^"]*\)\".*/\1/' | sort | uniq >"$@"
-
-MOSTLYCLEANFILES = \
- Debug_tags \
- Trace_tags \
- Debug_tags.tmp \
- Trace_tags.tmp \
- 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:%=../%)
+
+
+# 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 "$<" ) > "$@"
+
+$(DOCUMENTATION_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.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_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+ @srcdir@/base_options_template.h \
+ base_options_template.h.sed \
+ "$<" \
+ ) > "$@"
+
+summary.sed : mkoptions $(OPTIONS_OPTIONS_FILES)
+ $(AM_V_at)chmod +x @srcdir@/mkoptions
+ $(AM_V_GEN)(@srcdir@/mkoptions summary-sed \
+ $(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 $(OPTIONS_HEADS)
+ $(AM_V_at)chmod +x @srcdir@/mkoptions
+ $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+ @srcdir@/options_holder_template.h \
+ @builddir@/options_holder_template.h.sed \
+ summary.sed \
+ ) > "$@"
+
+# 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_GEN)(@srcdir@/mkoptions \
- @srcdir@/options_holder_template.h @srcdir@/options_holder.h \
- @srcdir@/options_template.cpp @srcdir@/options.cpp \
- @srcdir@/../smt/smt_options_template.cpp @srcdir@/../smt/smt_options.cpp \
- @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 $(srcdir)/../$(o))") \
- )
- touch "$@"
-
-base_options $(OPTIONS_FILES:%=../%):;
-
-.PHONY: exprs-builts
-exprs-builts:; $(AM_V_at)[ "$(FROM_EXPR)" != 1 ] && $(MAKE) -C ../expr builts || true
+ $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+ @srcdir@/base_options_template.cpp \
+ base_options_template.cpp.sed \
+ "$<" \
+ ) > "$@"
+
+
+
+
+# mkoptions apply-sed-to-template sed-file template-file
+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 \
+ @builddir@/options_template.cpp.sed \
+ summary.sed \
+ ) > "$@"
+
+
+# mkoptions apply-sed-to-template sed-file template-file
+options_get_option.cpp : options_get_option_template.cpp options_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@/options_get_option_template.cpp \
+ @builddir@/options_get_option_template.cpp.sed \
+ summary.sed \
+ ) > "$@"
+
+options_set_option.cpp : options_set_option_template.cpp options_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_set_option_template.cpp \
+ @builddir@/options_set_option_template.cpp.sed \
+ summary.sed \
+ ) > "$@"
+
+
+
+$(DOCUMENTATION_FILES) : % : %_template %_template.sed mkoptions summary.sed
+# echo "$<"
+# echo "$@"
+ $(AM_V_at)chmod +x @srcdir@/mkoptions
+ $(AM_V_GEN)(@srcdir@/mkoptions apply-sed-files-to-template \
+ "$<" \
+ "$<".sed \
+ @builddir@/summary.sed \
+ ) > "$@"
+
+
+
+#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
+# includes are available during distclean, even though they come from
+# directories that are cleaned first. Without this rule, "distclean"
+# fails.
+%.Plo:; $(MKDIR_P) "$(dir $@)" && : > "$@"
+
projects / cvc5.git / blobdiff