diff options
Diffstat (limited to 'src/options/smt_options.toml')
| -rw-r--r-- | src/options/smt_options.toml | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 24ae162da..3d0cb6d8d 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -8,7 +8,6 @@ header = "options/smt_options.h" category = "common" long = "dump=MODE" type = "std::string" - read_only = true help = "dump preprocessed assertions, etc., see --dump=help" [[option]] @@ -17,7 +16,6 @@ header = "options/smt_options.h" category = "common" long = "dump-to=FILE" type = "std::string" - read_only = true help = "all dumping goes to FILE (instead of stdout)" [[option]] @@ -50,7 +48,6 @@ header = "options/smt_options.h" long = "static-learning" type = "bool" default = "true" - read_only = true help = "use static learning (on by default)" [[option]] @@ -59,7 +56,6 @@ header = "options/smt_options.h" category = "regular" type = "bool" default = "false" - read_only = true help = "always expand symbol definitions in output" [[option]] @@ -91,7 +87,6 @@ header = "options/smt_options.h" long = "dump-models" type = "bool" default = "false" - read_only = true help = "output models after every SAT/INVALID/UNKNOWN response" [[option]] @@ -144,7 +139,6 @@ header = "options/smt_options.h" long = "dump-proofs" type = "bool" default = "false" - read_only = true help = "output proofs after every UNSAT/VALID response" [[option]] @@ -160,7 +154,6 @@ header = "options/smt_options.h" long = "dump-instantiations" type = "bool" default = "false" - read_only = true help = "output instantiations of quantified formulas after every UNSAT/VALID response" [[option]] @@ -190,7 +183,6 @@ header = "options/smt_options.h" long = "sygus-print-callbacks" type = "bool" default = "true" - read_only = true help = "use sygus print callbacks to print sygus terms in the user-provided form (disable for debugging)" [[option]] @@ -246,7 +238,6 @@ header = "options/smt_options.h" long = "dump-unsat-cores-full" type = "bool" default = "false" - read_only = true help = "dump the full unsat core, including unlabeled assertions" [[option]] @@ -255,7 +246,6 @@ header = "options/smt_options.h" long = "produce-unsat-assumptions" type = "bool" default = "false" - read_only = true help = "turn on unsat assumptions generation" [[option]] @@ -366,7 +356,6 @@ header = "options/smt_options.h" long = "simp-ite-hunt-zombies=N" type = "uint32_t" default = "524288" - read_only = true help = "post ite compression enables zombie removal while the number of nodes is above this threshold" [[option]] @@ -392,7 +381,6 @@ header = "options/smt_options.h" long = "abstract-values" type = "bool" default = "false" - read_only = true help = "in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard" [[option]] @@ -402,7 +390,6 @@ header = "options/smt_options.h" long = "model-u-print=MODE" type = "ModelUninterpPrintMode" default = "None" - read_only = true help = "determines how to print uninterpreted elements in models" help_mode = "uninterpreted elements in models printing modes." [[option.mode.DtEnum]] @@ -425,7 +412,6 @@ header = "options/smt_options.h" long = "model-witness-value" type = "bool" default = "false" - read_only = true help = "in models, use a witness constant for choice functions" [[option]] @@ -433,7 +419,6 @@ header = "options/smt_options.h" smt_name = "regular-output-channel" category = "regular" type = "std::string" - read_only = true help = "set the regular output channel of the solver" [[option]] @@ -441,7 +426,6 @@ header = "options/smt_options.h" smt_name = "diagnostic-output-channel" category = "regular" type = "std::string" - read_only = true help = "set the diagnostic output channel of the solver" [[option]] @@ -450,7 +434,6 @@ header = "options/smt_options.h" long = "force-no-limit-cpu-while-dump" type = "bool" default = "false" - read_only = true help = "Force no CPU limit when dumping models and proofs" [[option]] @@ -459,7 +442,6 @@ header = "options/smt_options.h" long = "foreign-theory-rewrite" type = "bool" default = "false" - read_only = true help = "Cross-theory rewrites" [[option]] @@ -489,7 +471,6 @@ header = "options/smt_options.h" long = "bvand-integer-granularity=N" type = "uint32_t" default = "1" - read_only = true help = "granularity to use in --solve-bv-as-int mode and for iand operator (experimental)" [[option]] @@ -498,7 +479,6 @@ header = "options/smt_options.h" long = "iand-mode=mode" type = "IandMode" default = "VALUE" - read_only = true help = "Set the refinement scheme for integer AND" help_mode = "Refinement modes for integer AND" [[option.mode.VALUE]] @@ -517,7 +497,6 @@ header = "options/smt_options.h" long = "solve-int-as-bv=N" type = "uint32_t" default = "0" - read_only = true help = "attempt to solve a pure integer satisfiable problem by bitblasting in sufficient bitwidth (experimental)" [[option]] @@ -526,7 +505,6 @@ header = "options/smt_options.h" long = "solve-real-as-int" type = "bool" default = "false" - read_only = true help = "attempt to solve a pure real satisfiable problem as an integer problem (for non-linear)" [[option]] @@ -535,7 +513,6 @@ header = "options/smt_options.h" long = "produce-interpols=MODE" type = "ProduceInterpols" default = "NONE" - read_only = true help = "support the get-interpol command" help_mode = "Interpolants grammar mode" [[option.mode.NONE]] @@ -563,7 +540,6 @@ header = "options/smt_options.h" long = "produce-abducts" type = "bool" default = "false" - read_only = true help = "support the get-abduct command" [[option]] @@ -572,7 +548,6 @@ header = "options/smt_options.h" long = "check-interpols" type = "bool" default = "false" - read_only = true help = "checks whether produced solutions to get-interpol are correct" [[option]] @@ -581,5 +556,4 @@ header = "options/smt_options.h" long = "check-abducts" type = "bool" default = "false" - read_only = true help = "checks whether produced solutions to get-abduct are correct" |