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