blob: fea609bb5843683c1971238cc1b684e908287ab5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
|
#
# 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 --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
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"
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
|
