# See src/options/base_options for a description of this file format
#
-# FIXME: need to add support for SMT-LIBv2-required options:
-#
-# expand-definitions
-# regular-output-channel
-# diagnostic-output-channel
-# produce-unsat-cores
-#
-
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 lazyDefinitionExpansion --lazy-definition-expansion bool
- expand define-funs/LAMBDAs lazily
+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)
-common-option produceModels produce-models -m --produce-models bool :predicate CVC4::SmtEngine::beforeSearch :predicate-include "smt/smt_engine.h"
+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
-common-option produceAssignments produce-assignments --produce-assignments bool
+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
+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*
# portfolio options
-option threads --threads=N unsigned :default 2
- Total number of threads
option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
The input channel to receive notfication events for new lemmas
option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
The output channel to receive notfication events for new lemmas
+option forceNoLimitCpuWhileDump --force-no-limit-cpu-while-dump bool :default false
+ Force no CPU limit when dumping models and proofs
+
endmodule
projects / cvc5.git / blobdiff