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, 164 insertions, 0 deletions

diff --git a/src/options/smt_options b/src/options/smt_options
new file mode 100644
index 000000000..f658d929a
--- /dev/null
+++ b/src/options/smt_options
@@ -0,0 +1,164 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SMT "options/smt_options.h" SMT layer
+
+common-option - dump --dump=MODE argument :handler CVC4::options::dumpMode :handler-include "options/options_handler_interface.h"
+ dump preprocessed assertions, etc., see --dump=help
+common-option - dump-to --dump-to=FILE argument :handler CVC4::options::dumpToFile :handler-include "options/options_handler_interface.h"
+ all dumping goes to FILE (instead of stdout)
+
+expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo* :include "options/logic_info_forward.h" :handler CVC4::options::stringToLogicInfo :handler-include "options/options_handler_interface.h" :default NULL
+ set the logic, and override all further user attempts to change it
+
+option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::options::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" :handler-include "options/options_handler_interface.h"
+ choose simplification mode, see --simplification=help
+alias --no-simplification = --simplification=none
+ turn off all simplification (same as --simplification=none)
+
+option doStaticLearning static-learning --static-learning bool :default true
+ use static learning (on by default)
+
+option expandDefinitions expand-definitions bool :default false
+ always expand symbol definitions in output
+common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ support the get-value and get-model commands
+option checkModels check-models --check-models bool :link --produce-models --produce-assertions :link-smt produce-models :link-smt produce-assertions :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
+option dumpModels --dump-models bool :default false :link --produce-models
+ output models after every SAT/INVALID/UNKNOWN response
+option proof produce-proofs --proof bool :default false :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ turn on proof generation
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" :read-write
+ after UNSAT/VALID, machine-check the generated proof
+option dumpProofs --dump-proofs bool :default false :link --proof
+ output proofs after every UNSAT/VALID response
+option dumpInstantiations --dump-instantiations bool :default false
+ output instantiations of quantified formulas after every UNSAT/VALID response
+option dumpSynth --dump-synth bool :read-write :default false
+ output solution for synthesis conjectures after every UNSAT/VALID response
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ turn on unsat core generation
+option checkUnsatCores check-unsat-cores --check-unsat-cores bool :link --produce-unsat-cores :link-smt produce-unsat-cores :read-write
+ after UNSAT/VALID, produce and check an unsat core (expensive)
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ output unsat cores after every UNSAT/VALID response
+
+option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h"
+ support the get-assignment command
+
+undocumented-option interactiveMode interactive-mode bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write
+ deprecated name for produce-assertions
+common-option produceAssertions produce-assertions --produce-assertions bool :predicate CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write
+ keep an assertions list (enables get-assertions command)
+
+option doITESimp --ite-simp bool :read-write
+ turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
+
+option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
+ do the ite simplification pass again if repeating simplification
+
+option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
+ enables simplifyWithCare in ite simplificiation
+
+option compressItes --simp-ite-compress bool :default false :read-write
+ enables compressing ites after ite simplification
+
+option unconstrainedSimp --unconstrained-simp bool :default false :read-write
+ turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
+
+option repeatSimp --repeat-simp bool :read-write
+ make multiple passes with nonclausal simplifier
+
+option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
+ post ite compression enables zombie removal while the number of nodes is above this threshold
+
+option sortInference --sort-inference bool :read-write :default false
+ calculate sort inference of input problem, convert the input based on monotonic sorts
+
+common-option incrementalSolving incremental -i --incremental bool :default true
+ enable incremental solving
+
+option abstractValues abstract-values --abstract-values bool :default false
+ in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
+option modelUninterpDtEnum --model-u-dt-enum bool :default false
+ in models, output uninterpreted sorts as datatype enumerations
+
+option - regular-output-channel argument :handler CVC4::options::setRegularOutputChannel :handler-include "options/options_handler_interface.h"
+ set the regular output channel of the solver
+option - diagnostic-output-channel argument :handler CVC4::options::setDiagnosticOutputChannel :handler-include "options/options_handler_interface.h"
+ set the diagnostic output channel of the solver
+
+common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler CVC4::options::tlimitHandler :handler-include "options/options_handler_interface.h"
+ enable time limiting (give milliseconds)
+common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler CVC4::options::tlimitPerHandler :handler-include "options/options_handler_interface.h"
+ enable time limiting per query (give milliseconds)
+common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler CVC4::options::rlimitHandler :handler-include "options/options_handler_interface.h"
+ enable resource limiting (currently, roughly the number of SAT conflicts)
+common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler CVC4::options::rlimitPerHandler :handler-include "options/options_handler_interface.h"
+ enable resource limiting per query
+common-option hardLimit hard-limit --hard-limit bool :default false
+ the resource limit is hard potentially leaving the smtEngine in an unsafe state (should be destroyed and rebuild after resourcing out)
+common-option cpuTime cpu-time --cpu-time bool :default false
+ measures CPU time if set to true and wall time if false (default false)
+
+# Resource spending options for SPARK
+expert-option rewriteStep rewrite-step --rewrite-step unsigned :default 1
+ ammount of resources spent for each rewrite step
+
+expert-option theoryCheckStep theory-check-step --theory-check-step unsigned :default 1
+ ammount of resources spent for each theory check call
+
+expert-option decisionStep decision-step --decision-step unsigned :default 1
+ ammount of getNext decision calls in the decision engine
+ 
+expert-option bitblastStep bitblast-step --bitblast-step unsigned :default 1
+ ammount of resources spent for each bitblast step
+ 
+expert-option parseStep parse-step --parse-step unsigned :default 1
+ ammount of resources spent for each command/expression parsing
+ 
+expert-option lemmaStep lemma-step --lemma-step unsigned :default 1
+ ammount of resources spent when adding lemmas
+ 
+expert-option restartStep restart-step --restart-step unsigned :default 1
+ ammount of resources spent for each theory restart
+ 
+expert-option cnfStep cnf-step --cnf-step unsigned :default 1
+ ammount of resources spent for each call to cnf conversion
+ 
+expert-option preprocessStep preprocess-step --preprocess-step unsigned :default 1
+ ammount of resources spent for each preprocessing step in SmtEngine
+ 
+expert-option quantifierStep quantifier-step --quantifier-step unsigned :default 1
+ ammount of resources spent for quantifier instantiations
+ 
+expert-option satConflictStep sat-conflict-step --sat-conflict-step unsigned :default 1
+ ammount of resources spent for each sat conflict (main sat solver)
+ 
+expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsigned :default 1
+ ammount of resources spent for each sat conflict (bitvectors)
+ 
+ 
+expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
+ eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
+
+# --replay is currently broken; don't document it for 1.0
+undocumented-option replayFilename --replay=FILE std::string :handler CVC4::options::checkReplayFilename :handler-include "options/options_handler_interface.h"
+ replay decisions from file
+undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::options::checkReplayLogFilename :handler-include "options/options_handler_interface.h"
+ log decisions and propagations to file
+option replayStream ExprStream*
+
+# portfolio options
+option lemmaInputChannel LemmaInputChannel* :default NULL :include "base/lemma_input_channel_forward.h"
+ The input channel to receive notfication events for new lemmas
+option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "base/lemma_output_channel_forward.h"
+ The output channel to receive notfication events for new lemmas
+
+option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
+ Force no CPU limit when dumping models and proofs
+
+endmodule