diff options
Diffstat (limited to 'src/options/smt_options')
| -rw-r--r-- | src/options/smt_options | 51 |
1 files changed, 28 insertions, 23 deletions
diff --git a/src/options/smt_options b/src/options/smt_options index b99a8a83b..bc2586fe0 100644 --- a/src/options/smt_options +++ b/src/options/smt_options @@ -5,15 +5,15 @@ 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" +common-option dumpModeString dump --dump=MODE std::string :default "" :notify notifyDumpMode 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" +common-option dumpToFileName dump-to --dump-to=FILE std::string :notify notifyDumpToFile 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 +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 CVC4::options::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "options/simplification_mode.h" :handler-include "options/options_handler_interface.h" +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) @@ -23,35 +23,35 @@ option doStaticLearning static-learning --static-learning bool :default true 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" +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 :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +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 +option dumpModels --dump-models bool :default false :link --produce-models :link-smt 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" +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 :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" :read-write +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 +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 CVC4::options::proofEnabledBuild CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +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 :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +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 :predicate CVC4::options::beforeSearch :predicate-include "options/options_handler_interface.h" +option produceAssignments produce-assignments --produce-assignments bool :default false :notify notifyBeforeSearch 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 +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 CVC4::options::beforeSearch CVC4::options::setProduceAssertions :predicate-include "options/options_handler_interface.h" :read-write +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 @@ -86,18 +86,18 @@ option abstractValues abstract-values --abstract-values bool :default false 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" +option regularChannelName regular-output-channel std::string :notify notifySetRegularOutputChannel set the regular output channel of the solver -option - diagnostic-output-channel argument :handler CVC4::options::setDiagnosticOutputChannel :handler-include "options/options_handler_interface.h" +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 CVC4::options::tlimitHandler :handler-include "options/options_handler_interface.h" +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 CVC4::options::tlimitPerHandler :handler-include "options/options_handler_interface.h" +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 CVC4::options::rlimitHandler :handler-include "options/options_handler_interface.h" +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 CVC4::options::rlimitPerHandler :handler-include "options/options_handler_interface.h" +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) @@ -145,14 +145,19 @@ expert-option bvSatConflictStep bv-sat-conflict-step --bv-sat-conflict-step unsi 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" +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 -option solveIntAsBV --solve-int-as-bv uint32_t :default 0 +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 |