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

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
new file mode 100644
index 000000000..5bc20f9a8
--- /dev/null
+++ b/src/options/quantifiers_options
@@ -0,0 +1,297 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module QUANTIFIERS "options/quantifiers_options.h" Quantifiers
+
+#### rewriter options
+
+# Whether to mini-scope quantifiers.
+# For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to
+# ( forall x. P( x ) ) ^ ( forall x. Q( x ) )
+option miniscopeQuant --miniscope-quant bool :default true :read-write
+ miniscope quantifiers
+# Whether to mini-scope quantifiers based on formulas with no free variables.
+# For example, forall x. ( P( x ) V Q ) will be rewritten to
+# ( forall x. P( x ) ) V Q
+option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
+ miniscope quantifiers for ground subformulas
+option quantSplit --quant-split bool :default true
+ apply splitting to quantified formulas based on variable disjoint disjuncts
+option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToPrenexQuantMode :handler-include "options/options_handler_interface.h"
+ prenex mode for quantified formulas
+# Whether to variable-eliminate quantifiers.
+# For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
+#   forall y. P( c, y )
+option varElimQuant --var-elim-quant bool :default true
+ enable simple variable elimination for quantified formulas
+option dtVarExpandQuant --dt-var-exp-quant bool :default true
+ expand datatype variables bound to one constructor in quantifiers
+#ite lift mode for quantified formulas
+option iteLiftQuant --ite-lift-quant=MODE CVC4::theory::quantifiers::IteLiftQuantMode :default CVC4::theory::quantifiers::ITE_LIFT_QUANT_MODE_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler CVC4::options::stringToIteLiftQuantMode :handler-include "options/options_handler_interface.h"
+ ite lifting mode for quantified formulas
+option condVarSplitQuant --cond-var-split-quant bool :default true
+ split quantified formulas that lead to variable eliminations
+option condVarSplitQuantAgg --cond-var-split-agg-quant bool :default false
+ aggressive split quantified formulas that lead to variable eliminations
+option iteDtTesterSplitQuant --ite-dtt-split-quant bool :read-write :default false
+ split ites with dt testers as conditions
+# Whether to CNF quantifier bodies
+# option cnfQuant --cnf-quant bool :default false
+#  apply CNF conversion to quantified formulas
+option nnfQuant --nnf-quant bool :default true
+ apply NNF conversion to quantified formulas
+# Whether to pre-skolemize quantifier bodies.
+# For example, forall x. ( P( x ) => (exists y. f( y ) = x) ) will be rewritten to
+#   forall x. P( x ) => f( S( x ) ) = x
+option preSkolemQuant --pre-skolem-quant bool :read-write :default false
+ apply skolemization eagerly to bodies of quantified formulas
+option preSkolemQuantNested --pre-skolem-quant-nested bool :read-write :default true
+ apply skolemization to nested quantified formulass
+option preSkolemQuantAgg --pre-skolem-quant-agg bool :read-write :default true
+ apply skolemization to quantified formulas aggressively
+option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
+ perform aggressive miniscoping for quantifiers
+option elimTautQuant --elim-taut-quant bool :default true
+ eliminate tautological disjuncts of quantified formulas
+option purifyQuant --purify-quant bool :default false
+ purify quantified formulas
+ 
+#### E-matching options
+ 
+option eMatching --e-matching bool :read-write :default true
+ whether to do heuristic E-matching
+
+option termDbMode --term-db-mode CVC4::theory::quantifiers::TermDbMode :default CVC4::theory::quantifiers::TERM_DB_ALL :read-write :include "options/quantifiers_modes.h" :handler  CVC4::options::stringToTermDbMode :handler-include "options/options_handler_interface.h"
+ which ground terms to consider for instantiation
+option registerQuantBodyTerms --register-quant-body-terms bool :default false
+ consider ground terms within bodies of quantified formulas for matching
+ 
+option smartTriggers --smart-triggers bool :default true
+ enable smart triggers
+option relevantTriggers --relevant-triggers bool :default false
+ prefer triggers that are more relevant based on SInE style analysis
+option relationalTriggers --relational-triggers bool :default false
+ choose relational triggers such as x = f(y), x >= f(y)
+option purifyTriggers --purify-triggers bool :default false :read-write
+ purify triggers, e.g. f( x+1 ) becomes f( y ), x mapsto y-1
+option purifyDtTriggers --purify-dt-triggers bool :default false :read-write
+ purify dt triggers, match all constructors of correct form instead of selectors
+option pureThTriggers --pure-th-triggers bool :default false :read-write
+ use pure theory terms as single triggers
+option partialTriggers --partial-triggers bool :default false :read-write
+ use triggers that do not contain all free variables
+option multiTriggerWhenSingle --multi-trigger-when-single bool :default false
+ select multi triggers when single triggers exist
+option multiTriggerPriority --multi-trigger-priority bool :default false
+ only try multi triggers if single triggers give no instantiations
+option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_DEFAULT :read-write :include "options/quantifiers_modes.h" :handler  CVC4::options::stringToTriggerSelMode :handler-include "options/options_handler_interface.h"
+ selection mode for triggers
+option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :include "options/quantifiers_modes.h" :handler CVC4::options::stringToUserPatMode :handler-include "options/options_handler_interface.h"
+ policy for handling user-provided patterns for quantifier instantiation
+option incrementTriggers --increment-triggers bool :default true
+ generate additional triggers as needed during search
+ 
+option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL_LAST_CALL :read-write :include "options/quantifiers_modes.h" :handler CVC4::options::stringToInstWhenMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkInstWhenMode :predicate-include "options/options_handler_interface.h"
+ when to apply instantiation
+ 
+option instMaxLevel --inst-max-level=N int :read-write :default -1
+ maximum inst level of terms used to instantiate quantified formulas with (-1 == no limit, default)
+option instLevelInputOnly --inst-level-input-only bool :default true
+ only input terms are assigned instantiation level zero
+option internalReps --quant-internal-reps bool :default true
+ instantiate with representatives chosen by quantifiers engine
+ 
+option eagerInstQuant --eager-inst-quant bool :default false
+ apply quantifier instantiation eagerly
+
+option fullSaturateQuant --full-saturate-quant bool :default false :read-write
+ when all other quantifier instantiation strategies fail, instantiate with ground terms from relevant domain, then arbitrary ground terms before answering unknown
+option fullSaturateQuantRd --full-saturate-quant-rd bool :default true
+ whether to use relevant domain first for full saturation instantiation strategy
+option fullSaturateInst --fs-inst bool :default false
+ interleave full saturate instantiation with other techniques
+
+option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToLiteralMatchMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkLiteralMatchMode :predicate-include "options/options_handler_interface.h"
+ choose literal matching mode
+
+### finite model finding options
+ 
+option finiteModelFind finite-model-find --finite-model-find bool :default false :read-write
+ use finite model finding heuristic for quantifier instantiation
+
+option quantFunWellDefined --quant-fun-wd bool :default false
+ assume that function defined by quantifiers are well defined
+option fmfFunWellDefined --fmf-fun bool :default false :read-write
+ find models for recursively defined functions, assumes functions are admissible
+option fmfFunWellDefinedRelevant --fmf-fun-rlv bool :default false
+ find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant
+option fmfEmptySorts --fmf-empty-sorts bool :default false
+ allow finite model finding to assume sorts that do not occur in ground assertions are empty
+ 
+option mbqiMode --mbqi=MODE CVC4::theory::quantifiers::MbqiMode :read-write :default CVC4::theory::quantifiers::MBQI_FMC :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMbqiMode :handler-include "options/options_handler_interface.h" :predicate CVC4::options::checkMbqiMode :predicate-include "options/options_handler_interface.h"
+ choose mode for model-based quantifier instantiation
+option fmfOneInstPerRound --mbqi-one-inst-per-round bool :read-write :default false
+ only add one instantiation per quantifier per round for mbqi
+option fmfOneQuantPerRound --mbqi-one-quant-per-round bool :default false
+ only add instantiations for one quantifier per round for mbqi
+
+option fmfInstEngine --fmf-inst-engine bool :default false
+ use instantiation engine in conjunction with finite model finding
+option fmfInstGen --fmf-inst-gen bool :default true
+ enable Inst-Gen instantiation techniques for finite model finding 
+option fmfInstGenOneQuantPerRound --fmf-inst-gen-one-quant-per-round bool :default false
+ only perform Inst-Gen instantiation techniques on one quantifier per round
+option fmfFreshDistConst --fmf-fresh-dc bool :default false
+ use fresh distinguished representative when applying Inst-Gen techniques
+option fmfFmcSimple --fmf-fmc-simple bool :default true
+ simple models in full model check for finite model finding
+option fmfBoundInt fmf-bound-int --fmf-bound-int bool :default false :read-write
+ finite model finding on bounded integer quantification
+option fmfBoundIntLazy --fmf-bound-int-lazy bool :default false :read-write
+ enforce bounds for bounded integer quantification lazily via use of proxy variables
+ 
+### conflict-based instantiation options 
+ 
+option quantConflictFind --quant-cf bool :read-write :default true
+ enable conflict find mechanism for quantifiers
+option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default CVC4::theory::quantifiers::QCF_PROP_EQ :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfMode :handler-include "options/options_handler_interface.h"
+ what effort to apply conflict find mechanism
+option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "options/quantifiers_modes.h" :handler CVC4::options::stringToQcfWhenMode :handler-include "options/options_handler_interface.h"
+ when to invoke conflict find mechanism for quantifiers
+option qcfTConstraint --qcf-tconstraint bool :read-write :default false
+ enable entailment checks for t-constraints in qcf algorithm
+option qcfAllConflict --qcf-all-conflict bool :read-write :default false
+ add all available conflicting instances during conflict-based instantiation
+
+option instNoEntail --inst-no-entail bool :read-write :default true
+ do not consider instances of quantified formulas that are currently entailed
+ 
+### rewrite rules options 
+ 
+option quantRewriteRules --rewrite-rules bool :default false
+ use rewrite rules module
+option rrOneInstPerRound --rr-one-inst-per-round bool :default false
+ add one instance of rewrite rule per round
+ 
+### induction options 
+ 
+option quantInduction --quant-ind bool :default false
+ use all available techniques for inductive reasoning
+option dtStcInduction --dt-stc-ind bool :read-write :default false
+ apply strengthening for existential quantification over datatypes based on structural induction
+option intWfInduction --int-wf-ind bool :read-write :default false
+ apply strengthening for integers based on well-founded induction
+option conjectureGen --conjecture-gen bool :read-write :default false
+ generate candidate conjectures for inductive proofs
+ 
+option conjectureGenPerRound --conjecture-gen-per-round=N int :default 1
+ number of conjectures to generate per instantiation round 
+option conjectureNoFilter --conjecture-no-filter bool :default false
+ do not filter conjectures
+option conjectureFilterActiveTerms --conjecture-filter-active-terms bool :read-write :default true
+ filter based on active terms
+option conjectureFilterCanonical --conjecture-filter-canonical bool :read-write :default true
+ filter based on canonicity
+option conjectureFilterModel --conjecture-filter-model bool :read-write :default true
+ filter based on model
+option conjectureGenGtEnum --conjecture-gen-gt-enum=N int :default 50
+ number of ground terms to generate for model filtering
+option conjectureUeeIntro --conjecture-gen-uee-intro bool :default false
+ more aggressive merging for universal equality engine, introduces terms
+  
+### synthesis options 
+
+option ceGuidedInst --cegqi bool :default false :read-write
+  counterexample-guided quantifier instantiation
+option ceGuidedInstFair --cegqi-fair=MODE CVC4::theory::quantifiers::CegqiFairMode :default CVC4::theory::quantifiers::CEGQI_FAIR_DT_SIZE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToCegqiFairMode :handler-include "options/options_handler_interface.h"
+  if and how to apply fairness for cegqi
+option cegqiSingleInv --cegqi-si bool :default false :read-write
+  process single invocation synthesis conjectures
+option cegqiSingleInvPartial --cegqi-si-partial bool :default false
+  combined techniques for synthesis conjectures that are partially single invocation 
+option cegqiSingleInvReconstruct --cegqi-si-reconstruct bool :default true
+  reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvReconstructConst --cegqi-si-reconstruct-const bool :default true
+  include constants when reconstruct solutions for single invocation conjectures in original grammar
+option cegqiSingleInvAbort --cegqi-si-abort bool :default false
+  abort if synthesis conjecture is not single invocation
+option cegqiSingleInvMultiInstAbort --cegqi-si-multi-inst-abort bool :default false
+  abort if synthesis conjecture is single invocation with no ITE in grammar and multiple instantiations are tried
+  
+option sygusNormalForm --sygus-nf bool :default true
+  only search for sygus builtin terms that are in normal form
+option sygusNormalFormArg --sygus-nf-arg bool :default true
+  account for relationship between arguments of operations in sygus normal form
+option sygusNormalFormGlobal --sygus-nf-sym bool :default true
+  narrow sygus search space based on global state of current candidate program
+option sygusNormalFormGlobalGen --sygus-nf-sym-gen bool :default true
+  generalize lemmas for global search space narrowing
+option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
+  generalize based on arguments in global search space narrowing
+option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
+  generalize based on content in global search space narrowing
+  
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "options/quantifiers_modes.h" :handler CVC4::options::stringToSygusInvTemplMode :handler-include "options/options_handler_interface.h"
+  template mode for sygus invariant synthesis
+
+# approach applied to general quantified formulas
+option cbqiSplx --cbqi-splx bool :read-write :default false
+ turns on old implementation of counterexample-based quantifier instantiation
+option cbqi --cbqi bool :read-write :default false
+ turns on counterexample-based quantifier instantiation
+option recurseCbqi --cbqi-recurse bool :default true
+ turns on recursive counterexample-based quantifier instantiation
+option cbqiSat --cbqi-sat bool :read-write :default true
+ answer sat when quantifiers are asserted with counterexample-based quantifier instantiation
+option cbqiModel --cbqi-model bool :read-write :default true
+ guide instantiations by model values for counterexample-based quantifier instantiation
+option cbqiAll --cbqi-all bool :read-write :default false
+ apply counterexample-based instantiation to all quantified formulas
+option cbqiUseInfInt --cbqi-use-inf-int bool :read-write :default false
+ use integer infinity for vts in counterexample-based quantifier instantiation
+option cbqiUseInfReal --cbqi-use-inf-real bool :read-write :default false
+ use real infinity for vts in counterexample-based quantifier instantiation
+option cbqiPreRegInst --cbqi-prereg-inst bool :read-write :default false
+  preregister ground instantiations in counterexample-based quantifier instantiation
+option cbqiMinBounds --cbqi-min-bounds bool :default false
+  use minimally constrained lower/upper bound for counterexample-based quantifier instantiation
+option cbqiSymLia --cbqi-sym-lia bool :default false
+  use symbolic integer division in substitutions for counterexample-based quantifier instantiation
+option cbqiRoundUpLowerLia --cbqi-round-up-lia bool :default false
+  round up integer lower bounds in substitutions for counterexample-based quantifier instantiation
+option cbqiMidpoint --cbqi-midpoint bool :default false
+  choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation
+option cbqiNopt --cbqi-nopt bool :default true
+  non-optimal bounds for counterexample-based quantifier instantiation
+ 
+### local theory extensions options 
+
+option localTheoryExt --local-t-ext bool :default false
+  do instantiation based on local theory extensions
+option ltePartialInst --lte-partial-inst bool :default false
+  partially instantiate local theory quantifiers
+option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
+  treat arguments of inst closure as restricted terms for instantiation
+ 
+### reduction options
+
+option quantAlphaEquiv --quant-alpha-equiv bool :default true
+  infer alpha equivalence between quantified formulas
+option macrosQuant --macros-quant bool :read-write :default false
+ perform quantifiers macro expansion
+option macrosQuantMode --macros-quant-mode=MODE CVC4::theory::quantifiers::MacrosQuantMode :default CVC4::theory::quantifiers::MACROS_QUANT_MODE_GROUND_UF :include "options/quantifiers_modes.h" :handler CVC4::options::stringToMacrosQuantMode :handler-include "options/options_handler_interface.h"
+ mode for quantifiers macro expansion
+
+### recursive function options
+
+#option funDefs --fun-defs bool :default false
+#  enable specialized techniques for recursive function definitions
+ 
+### e-unification options
+
+option quantEqualityEngine --quant-ee bool :default false
+  maintain congrunce closure over universal equalities
+ 
+endmodule