X-Git-Url: https://git.libre-soc.org/?a=blobdiff_plain;f=src%2Fsmt%2Foptions;h=3ee3dbecbee510085bba0a53de2664c17e377196;hb=41c09b51a7000fe5eb6b702d4ef9a1644129410b;hp=f82867b68c640bb7c05ef3dbbba6cbb9c6825167;hpb=65f720aac2d497c6e829d9c76638073a10060e7d;p=cvc5.git diff --git a/src/smt/options b/src/smt/options index f82867b68..3ee3dbecb 100644 --- a/src/smt/options +++ b/src/smt/options @@ -5,73 +5,104 @@ module SMT "smt/options.h" SMT layer -common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h" +common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h" dump preprocessed assertions, etc., see --dump=help -common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" +common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h" all dumping goes to FILE (instead of stdout) +expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""' + set the logic, and override all further user attempts to change it + option simplificationMode simplification-mode --simplification=MODE SimplificationMode :handler CVC4::smt::stringToSimplificationMode :default SIMPLIFICATION_MODE_BATCH :read-write :include "smt/simplification_mode.h" :handler-include "smt/options_handlers.h" choose simplification mode, see --simplification=help alias --no-simplification = --simplification=none turn off all simplification (same as --simplification=none) -option doStaticLearning static-learning /--no-static-learning bool :default true +option doStaticLearning static-learning --static-learning bool :default true use static learning (on by default) -/turn off static learning (e.g. diamond-breaking) 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::smt::beforeSearch :predicate-include "smt/smt_engine.h" support the get-value and get-model commands -option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - after SAT/INVALID, double-check that the generated model satisfies all user assertions -common-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions +option dumpModels --dump-models bool :default false :link --produce-models + output models after every SAT/INVALID/UNKNOWN response +option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on proof generation -# this is just a placeholder for later; it doesn't show up in command-line options listings -common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" - turn on unsat core generation (NOT YET SUPPORTED) -common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + after UNSAT/VALID, machine-check the generated proof +option dumpProofs --dump-proofs bool :default false :link --proof + 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 unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + turn on unsat core generation +option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" + output unsat cores after every UNSAT/VALID response + +option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" support the get-assignment command -option modelFormatMode --model-format=MODE ModelFormatMode :handler CVC4::smt::stringToModelFormatMode :default MODEL_FORMAT_MODE_DEFAULT :read-write :include "smt/model_format_mode.h" :handler-include "smt/options_handlers.h" - print format mode for models, see --model-format=help # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive" # is a mode in which the assertion list must be kept. So it belongs here. -common-option interactive interactive-mode --interactive bool :read-write +common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write force interactive mode option doITESimp --ite-simp bool :read-write turn on ite simplification (Kim (and Somenzi) et al., SAT 2009) -/turn off 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) -/turn off unconstrained simplification (see Bruttomesso/Brummayer PhD thesis) option repeatSimp --repeat-simp bool :read-write make multiple passes with nonclausal simplifier -/do not make multiple passes with nonclausal simplifier -common-option incrementalSolving incremental -i --incremental bool +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 - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h" set the regular output channel of the solver option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h" set the diagnostic output channel of the solver -common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long" +common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long" enable time limiting (give milliseconds) -common-option perCallMillisecondLimit --tlimit-per=MS "unsigned long" +common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long" enable time limiting per query (give milliseconds) -common-option cumulativeResourceLimit --rlimit=N "unsigned long" - enable resource limiting -common-option perCallResourceLimit --rlimit-per=N "unsigned long" +common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long" + enable resource limiting (currently, roughly the number of SAT conflicts) +common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long" enable resource limiting per query -option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h" +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::smt::checkReplayFilename :handler-include "smt/options_handlers.h" replay decisions from file -option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h" +undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h" log decisions and propagations to file option replayStream ExprStream* @@ -81,7 +112,7 @@ option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_i option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h" The output channel to receive notfication events for new lemmas -option optionWithOnlyAlternate /--optionWithOnlyAlternate bool - option with only an alternate +option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false + Force no CPU limit when dumping models and proofs endmodule