From 4e883ffc0b88256a966183ac6b87bb5767154cdf Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 6 Oct 2012 18:53:27 +0000 Subject: * Clean up some options documentation * Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.) --- src/smt/options | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) (limited to 'src/smt/options') diff --git a/src/smt/options b/src/smt/options index 24c8b5e43..5be462195 100644 --- a/src/smt/options +++ b/src/smt/options @@ -15,9 +15,8 @@ option simplificationMode simplification-mode --simplification=MODE Simplificati 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) option expandDefinitions expand-definitions bool :default false always expand symbol definitions in output @@ -25,15 +24,13 @@ common-option produceModels produce-models -m --produce-models bool :default fal support the get-value and get-model commands option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" after SAT/INVALID, double-check that the generated model satisfies all user assertions -common-option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +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 # this is just a placeholder for later; it doesn't show up in command-line options listings -common-option unsatCores produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" turn on unsat core generation (NOT YET SUPPORTED) -common-option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" +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. @@ -42,15 +39,12 @@ common-option interactive interactive-mode --interactive bool :read-write 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 @@ -69,9 +63,10 @@ common-option cumulativeResourceLimit --rlimit=N "unsigned long" 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 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* -- cgit v1.2.3