Refactoring Options Handler & Library Cycle Breaking

What to Know As a User:
A number of files have moved. Users that include files in the public API in more refined ways than using #include <cvc4.h> should consult which files have moved. Note though that some files may move again after being cleaned up. A number of small tweaks have been made to the swig interfaces that may cause issues. Please file bug reports for any problems.

The Problem:
The build order of CVC4 used to be [roughly] specified as:
  options < expr < util < libcvc4 < parsers < main
Each of these had their own directories and their own Makefile.am files. With the exception of the util/ directory, each of the subdirectories built exactly one convenience library. The util/ directory additionally built a statistics library. While the order above was partially correct, the build order was more complicated as options/Makefile.am executed building the sources for expr/Makefile.am as part of its BUILT_SOURCES phase. This options/Makefile.am also build the options/h and options.cpp files in other directories. There were cyclical library dependencies between the first four above libraries. All of these aspects combined to make options extremely brittle and hard to develop. Maintaining these between clang versus gcc, and bazel versus autotools has become increasing unpredictable.

The Solution:
To address these cyclic build problems, I am simplifying the build process. Here are the main things that have to happen:
1. util/ will be split into 3 separate directories: base, util, and smt_util. Each will have their own library and Makefile.am file.
2. Dependencies for options/ will be moved into options/. If a type appears as an option, this file will be moved into options.
3. All of the old options_handlers.h files have been refactored.
4. Some files have moved from util into expr/ to resolve cycles. Some of these moves are temporary.
5. I am removing the libstatistics library.

The constraints that the CVC4 build system will eventually satisfy are:
- The include order for both the .h and .cpp files for a directory must respect the order libraries are built. For example, a file in options/ cannot include from the expr/ directory. This includes built source files such as those coming from */kinds files and */options files.
- The types definitions must also respect the build order. Forward type declarations will be allowed in exceptional, justified cases.
- The Makefile.am for a directory cannot generate a file outside of the directory it controls. (Or call another Makefile.am except through subdirectory calls.)
- One library per Makefile.am.
- No extra copies of libraries will be built for the purpose of distinguishing between external and internal visibility in libraries for building parser/ or main/ libraries and binaries. Any function used by parser/ and main/ will be labeled with CVC4_PUBLIC and be in a public API. (AFAICT, libstatistics was being built exactly to skirt this.)

The build order of CVC4 can now be [roughly] specified as
  base < options < util < expr < smt_util < libcvc4 < parsers < main
The distinction between "base < options < util < expr" are currently clean. The relationship between expr and the subsequent directories/libraries are not yet clean.

More details about the directories:

base/
The new directory base/ contains the shared utilities that are absolutely crucial to starting cvc4. The list currently includes just: cvc4_assert.{h,cpp}, output.{h,cpp}, exception.{h,cpp}, and tls.{h, h.in, cpp}. These are things that are required everywhere.

options/
The options/ directory is self contained.
- It contains all of the enums that appear as options. This includes things like theory/bv/bitblast_mode.h .
- There are exactly 4 classes that handled currently using forward declarations currently to this: LogicInfo, LemmaInputChannel, LemmaOutputChannel, and CommandSequence. These will all be removed from options.
- Functionality of the options_handlers.h files has been moved into smt/smt_options_handler.h. The options library itself only uses an interface class defined in options/options_handler_interface.h. We are now using virtual dispatch to avoid using inlined functions as was previously done.
- The */options_handlers.h files have been removed.
- The generated smt/smt_options.cpp file has been be replaced by pushing the functionality that was generated into: options/options_handler_{get,set}_option_template.cpp . The non-generated functionality was moved into smt_engine.cpp.
- All of the options files have been moved from their directories into options/. This means includes like theory/arith/options.h have changed to change to options/arith_options.h .

util/
The util/ directory continues to contain core utility classes that may be used [almost] everywhere. The exception is that these are not used by options/ or base/. This includes things like rational and integer. These may not use anything in expr/ or libcvc4. A number of files have been moved out of this directory as they have cyclic dependencies graph with exprs and types. The build process up to this directory is currently clean.

expr/
The expr/ directory continues to be the home of expressions. The major change is files moving from util/ moving into expr/. The reason for this is that these files form a cycle with files in expr/.
- An example is datatype.h. This includes "expr/expr.h", "expr/type.h" while "expr/command.h" includes datatype.h.
- Another example is predicate.h. This uses expr.h and is also declared in a kinds file and thus appears in kinds.h.
- The rule of thumb is if expr/ pulls it in it needs to be independent of expr/, in which case it is in util/, or it is not, in which case it is pulled into expr/.
- Some files do not have a strong justification currently. Result, ResourceManager and SExpr can be moved back into util/ once the iostream manipulation routines are refactored out of the Node and Expr classes.
- Note the kinds files are expected to remain in the theory/ directories. These are only read in order to build sources.
- This directory is not yet clean. It contains forward references into libcvc4 such as the printer. It also makes some classes used by main/ and parser CVC4_PUBLIC.

smt_util/
The smt_util/ directory contains those utility classes which require exprs, but expr/ does not require them. These are mostly utilities for working with expressions and nodes. Examples include ite_removal.h, LemmaInputChannel and LemmaOutputChannel.

What is up next:
- A number of new #warning "TODO: ..." items have been scattered throughout the code as reminders to myself. Help with these issues is welcomed.
- The expr/ directory needs to be cleaned up in a similar to options/. Before this happens statistics needs to be cleaned up.

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
-