diff options
Diffstat (limited to 'src/options/quantifiers_options')
| -rw-r--r-- | src/options/quantifiers_options | 421 |
1 files changed, 0 insertions, 421 deletions
diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options deleted file mode 100644 index 6552b9157..000000000 --- a/src/options/quantifiers_options +++ /dev/null @@ -1,421 +0,0 @@ -# -# 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 :read-write - apply splitting to quantified formulas based on variable disjoint disjuncts -option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_QUANT_SIMPLE :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode - prenex mode for quantified formulas -option prenexQuantUser --prenex-quant-user bool :default false :read-write - prenex quantified formulas with user patterns -# 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 varIneqElimQuant --var-ineq-elim-quant bool :default true - enable variable elimination based on infinite projection of unbound arithmetic variables -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 stringToIteLiftQuantMode - 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 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 formulas -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 elimExtArithQuant --elim-ext-arith-quant bool :read-write :default true - eliminate extended arithmetic symbols in quantified formulas -option condRewriteQuant --cond-rewrite-quant bool :default true - conditional rewriting of quantified formulas -option globalNegate --global-negate bool :read-write :default false - do global negation of input formula - -#### 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 stringToTermDbMode - 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 inferArithTriggerEq --infer-arith-trigger-eq bool :default false - infer equalities for trigger terms based on solving arithmetic equalities -option inferArithTriggerEqExp --infer-arith-trigger-eq-exp bool :default false - record explanations for inferArithTriggerEq - -option strictTriggers --strict-triggers bool :default false - only instantiate quantifiers with user patterns based on 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 multiTriggerCache --multi-trigger-cache bool :default false - caching version of multi triggers -option multiTriggerLinear --multi-trigger-linear bool :default true - implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms -option triggerSelMode --trigger-sel CVC4::theory::quantifiers::TriggerSelMode :default CVC4::theory::quantifiers::TRIGGER_SEL_MIN :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerSelMode - selection mode for triggers -option triggerActiveSelMode --trigger-active-sel CVC4::theory::quantifiers::TriggerActiveSelMode :default CVC4::theory::quantifiers::TRIGGER_ACTIVE_SEL_ALL :read-write :include "options/quantifiers_modes.h" :handler stringToTriggerActiveSelMode - selection mode to activate triggers -option userPatternsQuant --user-pat=MODE CVC4::theory::quantifiers::UserPatMode :default CVC4::theory::quantifiers::USER_PAT_MODE_TRUST :read-write :include "options/quantifiers_modes.h" :handler stringToUserPatMode - 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 stringToInstWhenMode :predicate checkInstWhenMode - when to apply instantiation -option instWhenStrictInterleave --inst-when-strict-interleave bool :default true :read-write - ensure theory combination and standard quantifier effort strategies take turns -option instWhenPhase --inst-when-phase=N int :read-write :default 2 :read-write - instantiation rounds quantifiers takes (>=1) before allowing theory combination to happen -option instWhenTcFirst --inst-when-tc-first bool :default true :read-write - allow theory combination to happen once initially, before quantifier strategies are run -option quantModelEe --quant-model-ee bool :default false - use equality engine of model for last call effort - -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 quantRepMode --quant-rep-mode=MODE CVC4::theory::quantifiers::QuantRepMode :default CVC4::theory::quantifiers::QUANT_REP_MODE_FIRST :read-write :include "options/quantifiers_modes.h" :handler stringToQuantRepMode - selection mode for representatives in quantifiers engine -option instRelevantCond --inst-rlv-cond bool :default false - add relevancy conditions for instantiations - -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 fullSaturateInterleave --fs-interleave 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_USE :include "options/quantifiers_modes.h" :handler stringToLiteralMatchMode :predicate checkLiteralMatchMode - 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 stringToMbqiMode :predicate checkMbqiMode - 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 mbqiInterleave --mbqi-interleave bool :default false - interleave model-based quantifier instantiation with other techniques - -option fmfInstEngine --fmf-inst-engine bool :default false :read-write - 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 fmfBound fmf-bound --fmf-bound bool :default false :read-write - finite model finding on bounded quantification -option fmfBoundLazy --fmf-bound-lazy bool :default false :read-write - enforce bounds for bounded quantification lazily via use of proxy variables -option fmfBoundMinMode --fmf-bound-min-mode=MODE CVC4::theory::quantifiers::FmfBoundMinMode :default CVC4::theory::quantifiers::FMF_BOUND_MIN_INT_RANGE :include "options/quantifiers_modes.h" :handler stringToFmfBoundMinMode - mode for which types of bounds to minimize via first decision heuristics - -### 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 stringToQcfMode - 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 stringToQcfWhenMode - 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 qcfNestedConflict --qcf-nested-conflict bool :default false - consider conflicts for nested quantifiers -option qcfVoExp --qcf-vo-exp bool :default false - qcf experimental variable ordering - -option instNoEntail --inst-no-entail bool :read-write :default true - do not consider instances of quantified formulas that are currently entailed -option instNoModelTrue --inst-no-model-true bool :read-write :default false - do not consider instances of quantified formulas that are currently true in model, if it is available - -option instPropagate --inst-prop bool :read-write :default false - internal propagation for instantiations for selecting relevant instances - -option qcfEagerTest --qcf-eager-test bool :default true - optimization, test qcf instances eagerly -option qcfEagerCheckRd --qcf-eager-check-rd bool :default true - optimization, eagerly check relevant domain of matched position -option qcfSkipRd --qcf-skip-rd bool :default false - optimization, skip instances based on possibly irrelevant portions of quantified formulas - -### 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 -option conjectureGenMaxDepth --conjecture-gen-max-depth=N int :default 3 - maximum depth of terms to consider for conjectures - -### synthesis options - -option ceGuidedInst --cegqi bool :default false :read-write - counterexample-guided quantifier instantiation for sygus -option cegqiSingleInvMode --cegqi-si=MODE CVC4::theory::quantifiers::CegqiSingleInvMode :default CVC4::theory::quantifiers::CEGQI_SI_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToCegqiSingleInvMode :read-write - mode for processing 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 cegqiSolMinCore --cegqi-si-sol-min-core bool :default false - minimize solutions for single invocation conjectures based on unsat core -option cegqiSolMinInst --cegqi-si-sol-min-inst bool :default true - minimize individual instantiations for single invocation conjectures based on unsat core -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 sygusPbe --sygus-pbe bool :default true :read-write - sygus advanced pruning based on examples -option sygusQePreproc --sygus-qe-preproc bool :default false - use quantifier elimination as a preprocessing step for sygus - -option sygusMinGrammar --sygus-min-grammar bool :default true - statically minimize sygus grammars -option sygusAddConstGrammar --sygus-add-const-grammar bool :default true - statically add constants appearing in conjecture to grammars -option sygusGrammarNorm --sygus-grammar-norm bool :default false - statically normalize sygus grammars based on flattening (linearization) -option sygusTemplEmbedGrammar --sygus-templ-embed-grammar bool :default false - embed sygus templates into grammars - -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 stringToSygusInvTemplMode - template mode for sygus invariant synthesis -option sygusInvAutoUnfold --sygus-auto-unfold bool :default true - enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems -option sygusUnifCondSol --sygus-unif-csol bool :default true - enable new approach which unifies conditional solutions - -option sygusDirectEval --sygus-direct-eval bool :default true - direct unfolding of evaluation functions -option sygusUnfoldBool --sygus-unfold-bool bool :default true - do unfolding of Boolean evaluation functions that appear in refinement lemmas -option sygusCRefEval --sygus-cref-eval bool :default true - direct evaluation of refinement lemmas for conflict analysis -option sygusCRefEvalMinExp --sygus-cref-eval-min-exp bool :default true - use min explain for direct evaluation of refinement lemmas for conflict analysis - -option sygusStream --sygus-stream bool :read-write :default false - enumerate a stream of solutions instead of terminating after the first one - -option cegisSample --cegis-sample=MODE CVC4::theory::quantifiers::CegisSampleMode :read-write :default CVC4::theory::quantifiers::CEGIS_SAMPLE_NONE :include "options/quantifiers_modes.h" :handler stringToCegisSampleMode - mode for using samples in the counterexample-guided inductive synthesis loop - -# internal uses of sygus -option sygusRew --sygus-rr bool :default false - use sygus to enumerate and verify correctness of rewrite rules via sampling -option sygusRewSynth --sygus-rr-synth bool :read-write :default false - use sygus to enumerate candidate rewrite rules via sampling -option sygusRewVerify --sygus-rr-verify bool :read-write :default false - use sygus to verify the correctness of rewrite rules via sampling -option sygusSamples --sygus-samples=N int :read-write :default 1000 :read-write - number of points to consider when doing sygus rewriter sample testing -option sygusSampleGrammar --sygus-sample-grammar bool :default true - when applicable, use grammar for choosing sample points - -# CEGQI applied to general quantified formulas -option cbqi --cbqi bool :read-write :default false - turns on counterexample-based quantifier instantiation -option cbqiFullEffort --cbqi-full bool :read-write :default false - turns on full effort counterexample-based quantifier instantiation, which may resort to model-value 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 cbqiMultiInst --cbqi-multi-inst bool :read-write :default false - when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation -option cbqiRepeatLit --cbqi-repeat-lit bool :read-write :default false - solve literals more than once in counterexample-based quantifier instantiation -option cbqiInnermost --cbqi-innermost bool :read-write :default true - only process innermost quantified formulas in counterexample-based quantifier instantiation -option cbqiNestedQE --cbqi-nested-qe bool :read-write :default false - process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation - -# CEGQI for arithmetic -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 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 :read-write :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 -option cbqiLitDepend --cbqi-lit-dep bool :default true - dependency lemmas for quantifier alternation in counterexample-based quantifier instantiation - -# CEGQI for EPR -option quantEpr --quant-epr bool :default false :read-write - infer whether in effectively propositional fragment, use for cbqi -option quantEprMatching --quant-epr-match bool :default true - use matching heuristics for EPR instantiation - -# CEGQI for BV -option cbqiBv cbqi-bv --cbqi-bv bool :read-write :default true - use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors -option cbqiBvInterleaveValue --cbqi-bv-interleave-value bool :read-write :default false - interleave model value instantiation with word-level inversion approach -option cbqiBvIneqMode --cbqi-bv-ineq=MODE CVC4::theory::quantifiers::CbqiBvIneqMode :read-write :default CVC4::theory::quantifiers::CBQI_BV_INEQ_EQ_BOUNDARY :include "options/quantifiers_modes.h" :handler stringToCbqiBvIneqMode - choose mode for handling bit-vector inequalities with counterexample-guided instantiation -option cbqiBvRmExtract --cbqi-bv-rm-extract bool :read-write :default true - replaces extract terms with variables for counterexample-guided instantiation for bit-vectors -option cbqiBvLinearize --cbqi-bv-linear bool :read-write :default true - linearize adder chains for variables -option cbqiBvConcInv cbqi-bv-concat-inv --cbqi-bv-concat-inv bool :read-write :default true - compute inverse for concat over equalities rather than producing an invertibility condition - -### 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 stringToMacrosQuantMode - mode for quantifiers macro expansion -option quantDynamicSplit --quant-dsplit-mode=MODE CVC4::theory::quantifiers::QuantDSplitMode :read-write :default CVC4::theory::quantifiers::QUANT_DSPLIT_MODE_NONE :include "options/quantifiers_modes.h" :handler stringToQuantDSplitMode - mode for dynamic quantifiers splitting -option quantAntiSkolem --quant-anti-skolem bool :read-write :default false - perform anti-skolemization for quantified formulas - -### 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 - -### higher-order options - -option hoMatching --ho-matching bool :default true - do higher-order matching algorithm for triggers with variable operators -option hoMatchingVarArgPriority --ho-matching-var-priority bool :default true - give priority to variable arguments over constant arguments - -option hoMergeTermDb --ho-merge-term-db bool :default true - merge term indices modulo equality - -### proof options - -option trackInstLemmas --track-inst-lemmas bool :read-write :default false - track instantiation lemmas (for proofs, unsat cores, qe and synthesis minimization) - -endmodule |