#
# Option specification file for CVC4
# See src/options/base_options for a description of this file format
#

module QUANTIFIERS "theory/quantifiers/options.h" Quantifiers

# 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 /--disable-miniscope-quant bool :default true
 disable 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 /--disable-miniscope-quant-fv bool :default true
 disable miniscope quantifiers for ground subformulas

# Whether to prenex (nested universal) quantifiers
option prenexQuant /--disable-prenex-quant bool :default true
 disable prenexing of 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 false
 enable variable elimination of quantified formulas

# Whether to CNF quantifier bodies
option cnfQuant --cnf-quant bool :default false
 apply CNF conversion to quantified formulas

option clauseSplit --clause-split bool :default false
 apply clause splitting 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 :default false
 apply skolemization eagerly to bodies of quantified formulas
option iteRemoveQuant --ite-remove-quant bool :default false
 apply ite removal to bodies of quantifiers
# Whether to perform agressive miniscoping
option aggressiveMiniscopeQuant --ag-miniscope-quant bool :default false
 perform aggressive miniscoping for quantifiers
# Whether to perform quantifier macro expansion
option macrosQuant --macros-quant bool :default false
 perform quantifiers macro expansions
# Whether to perform first-order propagation
option foPropQuant --fo-prop-quant bool :default false
 perform first-order propagation on quantifiers

# Whether to use smart triggers
option smartTriggers /--disable-smart-triggers bool :default true
 disable smart triggers
# Whether to use relevent triggers
option relevantTriggers /--disable-relevant-triggers bool :default true
 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)

# Whether to consider terms in the bodies of quantifiers for matching
option registerQuantBodyTerms --register-quant-body-terms bool :default false
 consider ground terms within bodies of quantified formulas for matching

option instWhenMode --inst-when=MODE CVC4::theory::quantifiers::InstWhenMode :default CVC4::theory::quantifiers::INST_WHEN_FULL :read-write :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToInstWhenMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkInstWhenMode :predicate-include "theory/quantifiers/options_handlers.h"
 when to apply instantiation
 
option eagerInstQuant --eager-inst-quant bool :default false
 apply quantifier instantiation eagerly

option literalMatchMode --literal-matching=MODE CVC4::theory::quantifiers::LiteralMatchMode :default CVC4::theory::quantifiers::LITERAL_MATCH_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToLiteralMatchMode :handler-include "theory/quantifiers/options_handlers.h" :predicate CVC4::theory::quantifiers::checkLiteralMatchMode :predicate-include "theory/quantifiers/options_handlers.h"
 choose literal matching mode

option cbqi --enable-cbqi/--disable-cbqi bool :default false
 turns on counterexample-based quantifier instantiation [off by default]
/turns off counterexample-based quantifier instantiation


option userPatternsQuant /--ignore-user-patterns bool :default true
 ignore user-provided patterns for quantifier instantiation

option flipDecision --flip-decision/ bool :default false
 turns on flip decision heuristic

option internalReps /--disable-quant-internal-reps bool :default true
 disables instantiating with representatives chosen by quantifiers engine

option finiteModelFind --finite-model-find bool :default false
 use finite model finding heuristic for quantifier instantiation

option fmfModelBasedInst /--disable-fmf-mbqi bool :default true
 disable model-based quantifier instantiation for finite model finding

option fmfFullModelCheck --fmf-fmc bool :default false
 enable full model check for finite model finding
option fmfFullModelCheckSimple /--disable-fmf-fmc-simple bool :default true
 disable simple models in full model check for finite model finding

option fmfOneInstPerRound --fmf-one-inst-per-round bool :default false
 only add one instantiation per quantifier per round for fmf
option fmfOneQuantPerRound --fmf-one-quant-per-round bool :default false
 only add instantiations for one quantifier per round for fmf 
option fmfInstEngine --fmf-inst-engine bool :default false
 use instantiation engine in conjunction with finite model finding
option fmfRelevantDomain --fmf-relevant-domain bool :default false
 use relevant domain computation, similar to complete instantiation (Ge, deMoura 09)
option fmfNewInstGen --fmf-new-inst-gen bool :default false
 use new inst gen technique for answering sat without exhaustive instantiation
option fmfInstGen --fmf-inst-gen/--disable-fmf-inst-gen bool :read-write :default true
 enable Inst-Gen instantiation techniques for finite model finding (default)
/disable 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 axiomInstMode --axiom-inst=MODE CVC4::theory::quantifiers::AxiomInstMode :default CVC4::theory::quantifiers::AXIOM_INST_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToAxiomInstMode :handler-include "theory/quantifiers/options_handlers.h"
 policy for instantiating axioms


endmodule