diff options
Diffstat (limited to 'src/smt/options')
-rw-r--r-- | src/smt/options | 81 |
1 files changed, 81 insertions, 0 deletions
diff --git a/src/smt/options b/src/smt/options new file mode 100644 index 000000000..5ee65e50a --- /dev/null +++ b/src/smt/options @@ -0,0 +1,81 @@ +# +# Option specification file for CVC4 +# 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" + dump preprocessed assertions, etc., see --dump=help +common-option - --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 + +option simplificationMode --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 + 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" + support the get-value and get-model commands +common-option produceAssignments produce-assignments --produce-assignments bool + support the get-assignment command + +# 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 + 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 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 + enable incremental solving + +common-option cumulativeMillisecondLimit --tlimit=MS "unsigned long" + enable time limiting (give milliseconds) +common-option perCallMillisecondLimit --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" + enable resource limiting per query + +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" + 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 + +endmodule |