#
# 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 dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode
 dump preprocessed assertions, etc., see --dump=help
common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile
 all dumping goes to FILE (instead of stdout)

expert-option forceLogicString force-logic --force-logic=LOGIC std::string :default "" :notify notifyForceLogic
 set the logic, and override all further user attempts to change it

option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.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 :notify notifyBeforeSearch
 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 :notify notifyBeforeSearch
 after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
option dumpModels --dump-models bool :default false :link --produce-models :link-smt produce-models
 output models after every SAT/INVALID/UNKNOWN response
option omitDontCares --omit-dont-cares bool :default false
 When producing a model, omit variables whose value does not matter
option proof produce-proofs --proof bool :default false :predicate proofEnabledBuild :notify notifyBeforeSearch
 turn on proof generation
option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :notify notifyBeforeSearch :read-write
 after UNSAT/VALID, machine-check the generated proof
option dumpProofs --dump-proofs bool :default false :link --proof :link-smt produce-proofs
 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 proofEnabledBuild :notify :notify notifyBeforeSearch
 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 :notify notifyBeforeSearch
 output unsat cores after every UNSAT/VALID response

option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch
 support the get-assignment command

undocumented-option interactiveMode interactive-mode bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
 deprecated name for produce-assertions
common-option produceAssertions produce-assertions --produce-assertions bool :predicate setProduceAssertions :read-write :notify notifyBeforeSearch
 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 regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel
 set the regular output channel of the solver
option diagnosticChannelName diagnostic-output-channel std::string :notify notifySetDiagnosticOutputChannel
 set the diagnostic output channel of the solver

common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" :handler tlimitHandler :notify notifyTlimit
 enable time limiting (give milliseconds)
common-option perCallMillisecondLimit  tlimit-per --tlimit-per=MS "unsigned long" :handler tlimitPerHandler :notify notifyTlimitPer
 enable time limiting per query (give milliseconds)
common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" :handler rlimitHandler :notify notifyRlimit
 enable resource limiting (currently, roughly the number of SAT conflicts)
common-option perCallResourceLimit reproducible-resource-limit --rlimit-per=N "unsigned long" :handler rlimitPerHandler :notify notifyRlimitPer
 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 replayInputFilename --replay=FILE std::string :handler checkReplayFilename
 replay decisions from file

# --replay is currently broken; don't document it for 1.0
undocumented-option replayLogFilename --replay-log=FILE std::string :handler checkReplayFilename :notify notifySetReplayLogFilename :notify notifyBeforeSearch
 replay decisions from file

option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
 Force no CPU limit when dumping models and proofs

undocumented-option solveIntAsBV --solve-int-as-bv uint32_t :default 0
 attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)

endmodule