2 # Option specification file for CVC4
3 # See src/options/base_options for a description of this file format
6 module SMT "smt/options.h" SMT layer
8 common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
9 dump preprocessed assertions, etc., see --dump=help
10 common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
11 all dumping goes to FILE (instead of stdout)
13 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 '""'
14 set the logic, and override all further user attempts to change it
16 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"
17 choose simplification mode, see --simplification=help
18 alias --no-simplification = --simplification=none
19 turn off all simplification (same as --simplification=none)
21 option doStaticLearning static-learning --static-learning bool :default true
22 use static learning (on by default)
24 option expandDefinitions expand-definitions bool :default false
25 always expand symbol definitions in output
26 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
27 support the get-value and get-model commands
28 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"
29 after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
30 option dumpModels --dump-models bool :default false :link --produce-models
31 output models after every SAT/INVALID/UNKNOWN response
32 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
33 turn on proof generation
34 option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
35 after UNSAT/VALID, machine-check the generated proof
36 option dumpProofs --dump-proofs bool :default false :link --proof
37 output proofs after every UNSAT/VALID response
38 # this is just a placeholder for later; it doesn't show up in command-line options listings
39 undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
40 turn on unsat core generation (NOT YET SUPPORTED)
41 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
42 support the get-assignment command
44 # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive"
45 # is a mode in which the assertion list must be kept. So it belongs here.
46 common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write
47 force interactive mode
49 option doITESimp --ite-simp bool :read-write
50 turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
52 option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
53 do the ite simplification pass again if repeating simplification
55 option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
56 enables simplifyWithCare in ite simplificiation
58 option compressItes --simp-ite-compress bool :default false :read-write
59 enables compressing ites after ite simplification
61 option unconstrainedSimp --unconstrained-simp bool :default false :read-write
62 turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
64 option repeatSimp --repeat-simp bool :read-write
65 make multiple passes with nonclausal simplifier
67 option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
68 post ite compression enables zombie removal while the number of nodes is above this threshold
70 option sortInference --sort-inference bool :read-write :default false
71 calculate sort inference of input problem, convert the input based on monotonic sorts
73 common-option incrementalSolving incremental -i --incremental bool :default true
74 enable incremental solving
76 option abstractValues abstract-values --abstract-values bool :default false
77 in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
78 option modelUninterpDtEnum --model-u-dt-enum bool :default false
79 in models, output uninterpreted sorts as datatype enumerations
81 option - regular-output-channel argument :handler CVC4::smt::setRegularOutputChannel :handler-include "smt/options_handlers.h"
82 set the regular output channel of the solver
83 option - diagnostic-output-channel argument :handler CVC4::smt::setDiagnosticOutputChannel :handler-include "smt/options_handlers.h"
84 set the diagnostic output channel of the solver
86 common-option cumulativeMillisecondLimit tlimit --tlimit=MS "unsigned long"
87 enable time limiting (give milliseconds)
88 common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long"
89 enable time limiting per query (give milliseconds)
90 common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
91 enable resource limiting (currently, roughly the number of SAT conflicts)
92 common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
93 enable resource limiting per query
95 expert-option rewriteApplyToConst rewrite-apply-to-const --rewrite-apply-to-const bool :default false
96 eliminate function applications, rewriting e.g. f(5) to a new symbol f_5
98 # --replay is currently broken; don't document it for 1.0
99 undocumented-option replayFilename --replay=FILE std::string :handler CVC4::smt::checkReplayFilename :handler-include "smt/options_handlers.h"
100 replay decisions from file
101 undocumented-option replayLog --replay-log=FILE std::ostream* :handler CVC4::smt::checkReplayLogFilename :handler-include "smt/options_handlers.h"
102 log decisions and propagations to file
103 option replayStream ExprStream*
106 option lemmaInputChannel LemmaInputChannel* :default NULL :include "util/lemma_input_channel.h"
107 The input channel to receive notfication events for new lemmas
108 option lemmaOutputChannel LemmaOutputChannel* :default NULL :include "util/lemma_output_channel.h"
109 The output channel to receive notfication events for new lemmas