From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 10 May 2021 21:37:12 +0000 (+0200)
Subject: Remove read_only from options. (#6513)
X-Git-Tag: cvc5-1.0.0~1775
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d5987a99361f227cf2ea1404fec594f4a998be70;p=cvc5.git

Remove read_only from options. (#6513)

This PR removes the possibility of declaring options read_only.
It's only effect is making an attempts to disallow changing the respective option from within our internal code (by not providing a setter method). However, a "read-only" option can still be set via the setOption() methods that is also used by the API, and by SMT-LIB's set-option.
---

diff --git a/src/options/README b/src/options/README
index 5467d20c4..868690b85 100644
--- a/src/options/README
+++ b/src/options/README
@@ -41,9 +41,6 @@ Options
     predicates ... (list)   functions that check whether given option value is
                             valid
     includes   ... (list)   header files required by handler/predicates
-    read_only  ... (bool)   true: option should not provide a ::set method,
-                            false (default): option should provide a ::set
-                            method to set the option value
     alternate  ... (bool)   true (default): add --no-<long> alternative option
                             false: omit --no-<long> alternative option
     help       ... (string) documentation (required if category is not
@@ -71,7 +68,6 @@ Options
       handler    = "stringToOutputLanguage"
       predicates = []
       includes   = ["options/language.h"]
-      read_only  = false
       help       = "force output language (default is \"auto\"; see --output-lang help)"
 
 
diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 20ae73fce..2afe92ccd 100644
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -8,7 +8,6 @@ header = "options/arith_options.h"
   long       = "unate-lemmas=MODE"
   type       = "ArithUnateLemmaMode"
   default    = "ALL"
-  read_only  = true
   help       = "determines which lemmas to add before solving (default is 'all', see --unate-lemmas=help)"
   help_mode  = "Unate lemmas are generated before SAT search begins using the relationship of constant terms and polynomials."
 [[option.mode.ALL]]
@@ -29,7 +28,6 @@ header = "options/arith_options.h"
   long       = "arith-prop=MODE"
   type       = "ArithPropagationMode"
   default    = "BOTH_PROP"
-  read_only  = true
   help       = "turns on arithmetic propagation (default is 'old', see --arith-prop=help)"
   help_mode  = "This decides on kind of propagation arithmetic attempts to do during the search."
 [[option.mode.NO_PROP]]
@@ -77,7 +75,6 @@ header = "options/arith_options.h"
   long       = "error-selection-rule=RULE"
   type       = "ErrorSelectionRule"
   default    = "MINIMUM_AMOUNT"
-  read_only  = true
   help       = "change the pivot rule for the basic variable (default is 'min', see --pivot-rule help)"
   help_mode  = "This decides on the rule used by simplex during heuristic rounds for deciding the next basic variable to select."
 [[option.mode.MINIMUM_AMOUNT]]
@@ -99,7 +96,6 @@ header = "options/arith_options.h"
   long       = "simplex-check-period=N"
   type       = "uint16_t"
   default    = "200"
-  read_only  = true
   help       = "the number of pivots to do in simplex before rechecking for a conflict on all variables"
 
 # This is the pivots per basic variable that can be done using heuristic choices
@@ -120,7 +116,6 @@ header = "options/arith_options.h"
   long       = "prop-row-length=N"
   type       = "uint16_t"
   default    = "16"
-  read_only  = true
   help       = "sets the maximum row length to be used in propagation"
 
 [[option]]
@@ -129,7 +124,6 @@ header = "options/arith_options.h"
   long       = "dio-solver"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "turns on Linear Diophantine Equation solver (Griggio, JSAT 2012)"
 
 # Whether to split (= x y) into (and (<= x y) (>= x y)) in
@@ -158,7 +152,6 @@ header = "options/arith_options.h"
   long       = "miplib-trick-subs=N"
   type       = "unsigned"
   default    = "1"
-  read_only  = true
   help       = "do substitution for miplib 'tmp' vars if defined in <= N eliminated vars"
 
 [[option]]
@@ -175,7 +168,6 @@ header = "options/arith_options.h"
   long       = "maxCutsInContext=N"
   type       = "unsigned"
   default    = "65535"
-  read_only  = true
   help       = "maximum cuts in a given context before signalling a restart"
 
 [[option]]
@@ -184,7 +176,6 @@ header = "options/arith_options.h"
   long       = "revert-arith-models-on-unsat"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "revert the arithmetic model to a known safe model on unsat if one is cached"
 
 [[option]]
@@ -281,7 +272,6 @@ header = "options/arith_options.h"
   long       = "se-solve-int"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "attempt to use the approximate solve integer method on standard effort"
 
 [[option]]
@@ -290,7 +280,6 @@ header = "options/arith_options.h"
   long       = "lemmas-on-replay-failure"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "attempt to use external lemmas if approximate solve integer failed"
 
 [[option]]
@@ -299,7 +288,6 @@ header = "options/arith_options.h"
   long       = "dio-turns=N"
   type       = "int"
   default    = "10"
-  read_only  = true
   help       = "turns in a row dio solver cutting gets"
 
 [[option]]
@@ -308,7 +296,6 @@ header = "options/arith_options.h"
   long       = "rr-turns=N"
   type       = "int"
   default    = "3"
-  read_only  = true
   help       = "round robin turn"
 
 [[option]]
@@ -317,7 +304,6 @@ header = "options/arith_options.h"
   long       = "dio-repeat"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "handle dio solver constraints in mass or one at a time"
 
 [[option]]
@@ -326,7 +312,6 @@ header = "options/arith_options.h"
   long       = "replay-early-close-depth=N"
   type       = "int"
   default    = "1"
-  read_only  = true
   help       = "multiples of the depths to try to close the approx log eagerly"
 
 [[option]]
@@ -335,7 +320,6 @@ header = "options/arith_options.h"
   long       = "replay-failure-penalty=N"
   type       = "int"
   default    = "100"
-  read_only  = true
   help       = "number of solve integer attempts to skips after a numeric failure"
 
 [[option]]
@@ -344,7 +328,6 @@ header = "options/arith_options.h"
   long       = "replay-num-err-penalty=N"
   type       = "int"
   default    = "4194304"
-  read_only  = true
   help       = "number of solve integer attempts to skips after a numeric failure"
 
 [[option]]
@@ -353,7 +336,6 @@ header = "options/arith_options.h"
   long       = "replay-reject-cut=N"
   type       = "unsigned"
   default    = "25500"
-  read_only  = true
   help       = "maximum complexity of any coefficient while replaying cuts"
 
 [[option]]
@@ -362,7 +344,6 @@ header = "options/arith_options.h"
   long       = "replay-lemma-reject-cut=N"
   type       = "unsigned"
   default    = "25500"
-  read_only  = true
   help       = "maximum complexity of any coefficient while outputting replaying cut lemmas"
 
 [[option]]
@@ -371,7 +352,6 @@ header = "options/arith_options.h"
   long       = "replay-soi-major-threshold=T"
   type       = "double"
   default    = ".01"
-  read_only  = true
   help       = "threshold for a major tolerance failure by the approximate solver"
 
 [[option]]
@@ -380,7 +360,6 @@ header = "options/arith_options.h"
   long       = "replay-soi-major-threshold-pen=N"
   type       = "int"
   default    = "50"
-  read_only  = true
   help       = "threshold for a major tolerance failure by the approximate solver"
 
 [[option]]
@@ -389,7 +368,6 @@ header = "options/arith_options.h"
   long       = "replay-soi-minor-threshold=T"
   type       = "double"
   default    = ".0001"
-  read_only  = true
   help       = "threshold for a minor tolerance failure by the approximate solver"
 
 [[option]]
@@ -398,7 +376,6 @@ header = "options/arith_options.h"
   long       = "replay-soi-minor-threshold-pen=N"
   type       = "int"
   default    = "10"
-  read_only  = true
   help       = "threshold for a minor tolerance failure by the approximate solver"
 
 [[option]]
@@ -407,7 +384,6 @@ header = "options/arith_options.h"
   long       = "pp-assert-max-sub-size=N"
   type       = "unsigned"
   default    = "2"
-  read_only  = true
   help       = "threshold for substituting an equality in ppAssert"
 
 [[option]]
@@ -416,7 +392,6 @@ header = "options/arith_options.h"
   long       = "arith-no-partial-fun"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "do not use partial function semantics for arithmetic (not SMT LIB compliant)"
 
 [[option]]
@@ -441,7 +416,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-rbound"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use resolution-style inference for inferring new bounds in non-linear incremental linearization solver"
 
 [[option]]
@@ -450,7 +424,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-factor"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use factoring inference in non-linear incremental linearization solver"
 
 [[option]]
@@ -475,7 +448,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-tf-tplanes"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use non-terminating tangent plane strategy for transcendental functions for non-linear incremental linearization solver"
 
 [[option]]
@@ -484,7 +456,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-ent-conf"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "check for entailed conflicts in non-linear solver"
 
 [[option]]
@@ -493,7 +464,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-rewrite"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do context-dependent simplification based on rewrites in non-linear solver"
 
 [[option]]
@@ -502,7 +472,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-purify"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "purify non-linear terms at preprocess"
 
 [[option]]
@@ -511,7 +480,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-split-zero"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "initial splits on zero for all variables"
 
 [[option]]
@@ -528,7 +496,6 @@ header = "options/arith_options.h"
   long       = "nl-ext-inc-prec"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "whether to increment the precision for irrational function constraints"
 
 [[option]]
@@ -555,7 +522,6 @@ header = "options/arith_options.h"
   long       = "arith-brab"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "whether to use simple rounding, similar to a unit-cube test, for integers"
 
 [[option]]
diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index 75e33e551..eb3a13778 100644
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -71,7 +71,6 @@ header = "options/base_options.h"
   long       = "verbose"
   type       = "void"
   handler    = "increaseVerbosity"
-  read_only  = true
   help       = "increase verbosity (may be repeated)"
 
 [[option]]
@@ -80,7 +79,6 @@ header = "options/base_options.h"
   long       = "quiet"
   type       = "void"
   handler    = "decreaseVerbosity"
-  read_only  = true
   help       = "decrease verbosity (may be repeated)"
 
 [[option]]
@@ -90,7 +88,6 @@ header = "options/base_options.h"
   category   = "common"
   type       = "bool"
   predicates = ["setStats"]
-  read_only  = true
   help       = "give statistics on exit"
 
 [[option]]
@@ -100,7 +97,6 @@ header = "options/base_options.h"
   category   = "expert"
   type       = "bool"
   predicates = ["setStats"]
-  read_only  = true
   help       = "print unchanged (defaulted) statistics as well"
 
 [[option]]
@@ -110,7 +106,6 @@ header = "options/base_options.h"
   category   = "expert"
   type       = "bool"
   predicates = ["setStats"]
-  read_only  = true
   help       = "print expert (non-public) statistics as well"
 
 [[option]]
@@ -121,7 +116,6 @@ header = "options/base_options.h"
   type       = "bool"
   predicates = ["setStats"]
   default    = "false"
-  read_only  = true
   help       = "in incremental mode, print stats after every satisfiability or validity query"
 
 [[option]]
@@ -136,7 +130,6 @@ header = "options/base_options.h"
   category   = "regular"
   long       = "preprocess-only"
   type       = "bool"
-  read_only  = true
   help       = "exit after preprocessing input"
 
 [[option]]
@@ -146,7 +139,6 @@ header = "options/base_options.h"
   long       = "trace=TAG"
   type       = "std::string"
   handler    = "enableTraceTag"
-  read_only  = true
   help       = "trace something (e.g. -t pushpop), can repeat"
 
 [[option]]
@@ -156,7 +148,6 @@ header = "options/base_options.h"
   long       = "debug=TAG"
   type       = "std::string"
   handler    = "enableDebugTag"
-  read_only  = true
   help       = "debug something (e.g. -d arith), can repeat"
 
 [[option]]
@@ -164,5 +155,4 @@ header = "options/base_options.h"
   category   = "regular"
   long       = "print-success"
   type       = "bool"
-  read_only  = true
   help       = "print the \"success\" output required of SMT-LIBv2"
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index 18f190ff1..e6ef18311 100644
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -160,7 +160,6 @@ header = "options/bv_options.h"
   long       = "bv-num-func=N"
   type       = "unsigned"
   default    = "1"
-  read_only  = true
   help       = "number of function symbols in conflicts that are generalized"
 
 [[option]]
@@ -177,7 +176,6 @@ header = "options/bv_options.h"
   long       = "bv-quick-xplain"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "minimize bv conflicts using the QuickXplain algorithm"
 
 [[option]]
@@ -194,7 +192,6 @@ header = "options/bv_options.h"
   long       = "bv-gauss-elim"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "simplify formula via Gaussian Elimination if applicable"
 
 [[option]]
diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index 164dd736b..cf1ac5f49 100644
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -29,7 +29,6 @@ header = "options/datatypes_options.h"
   long       = "dt-polite-optimize"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "turn on optimization for polite combination"
 
 [[option]]
@@ -38,7 +37,6 @@ header = "options/datatypes_options.h"
   long       = "dt-binary-split"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "do binary splits for datatype constructor types"
 
 [[option]]
@@ -47,7 +45,6 @@ header = "options/datatypes_options.h"
   long       = "cdt-bisimilar"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do bisimilarity check for co-datatypes"
 
 [[option]]
@@ -56,7 +53,6 @@ header = "options/datatypes_options.h"
   long       = "dt-cyclic"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do cyclicity check for datatypes"
 
 [[option]]
@@ -65,7 +61,6 @@ header = "options/datatypes_options.h"
   long       = "dt-infer-as-lemmas"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "always send lemmas out instead of making internal inferences"
 
 [[option]]
@@ -74,7 +69,6 @@ header = "options/datatypes_options.h"
   long       = "dt-blast-splits"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "when applicable, blast splitting lemmas for all variables at once"
 
 [[option]]
@@ -83,7 +77,6 @@ header = "options/datatypes_options.h"
   long       = "dt-nested-rec"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "allow nested recursion in datatype definitions"
 
 [[option]]
@@ -92,7 +85,6 @@ header = "options/datatypes_options.h"
   long       = "dt-share-sel"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "internally use shared selectors across multiple constructors"
 
 [[option]]
@@ -101,7 +93,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-sym-break"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "simple sygus symmetry breaking lemmas"
 
 [[option]]
@@ -110,7 +101,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-sym-break-agg"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use aggressive checks for simple sygus symmetry breaking lemmas"
 
 [[option]]
@@ -119,7 +109,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-sym-break-dynamic"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "dynamic sygus symmetry breaking lemmas"
 
 [[option]]
@@ -136,7 +125,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-sym-break-lazy"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "lazily add symmetry breaking lemmas for terms"
 
 [[option]]
@@ -145,7 +133,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-sym-break-rlv"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "add relevancy conditions to symmetry breaking lemmas"
 
 [[option]]
@@ -154,7 +141,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-fair=MODE"
   type       = "SygusFairMode"
   default    = "DT_SIZE"
-  read_only  = true
   help       = "if and how to apply fairness for sygus"
   help_mode  = "Modes for enforcing fairness for counterexample guided quantifier instantion."
 [[option.mode.DIRECT]]
@@ -179,7 +165,6 @@ header = "options/datatypes_options.h"
   long       = "sygus-fair-max"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use max instead of sum for multi-function sygus conjectures"
 
 [[option]]
@@ -188,5 +173,4 @@ header = "options/datatypes_options.h"
   long       = "sygus-abort-size=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "tells enumerative sygus to only consider solutions up to term size N (-1 == no limit, default)"
diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index c614ab3db..68698b3a1 100644
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -34,7 +34,6 @@ header = "options/decision_options.h"
   type       = "decision::DecisionWeight"
   default    = "0"
   includes   = ["options/decision_weight.h"]
-  read_only  = true
   help       = "ignore all nodes greater than threshold in first attempt to pick decision"
 
 [[option]]
@@ -43,7 +42,6 @@ header = "options/decision_options.h"
   long       = "decision-use-weight"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use the weight nodes (locally, by looking at children) to direct recursive search"
 
 
@@ -53,7 +51,6 @@ header = "options/decision_options.h"
   long       = "decision-random-weight=N"
   type       = "int"
   default    = "0"
-  read_only  = true
   help       = "assign random weights to nodes between 0 and N-1 (0: disable)"
 
 [[option]]
@@ -62,7 +59,6 @@ header = "options/decision_options.h"
   long       = "decision-weight-internal=HOW"
   type       = "DecisionWeightInternal"
   default    = "OFF"
-  read_only  = true
   help       = "compute weights of internal nodes using children: off, max, sum, usr1"
   help_mode  = "Decision weight internal mode."
 [[option.mode.OFF]]
diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 368fb34e4..34a4fb979 100644
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -9,7 +9,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "0"
   predicates = ["setDefaultExprDepthPredicate"]
-  read_only  = true
   help       = "print exprs to depth N (0 == default, -1 == no limit)"
 
 [[option]]
@@ -20,7 +19,6 @@ header = "options/expr_options.h"
   type       = "int"
   default    = "1"
   predicates = ["setDefaultDagThreshPredicate"]
-  read_only  = true
   help       = "dagify common subexprs appearing > N times (1 == default, 0 == don't dagify)"
 
 [[option]]
@@ -29,5 +27,4 @@ header = "options/expr_options.h"
   long       = "type-checking"
   type       = "bool"
   default    = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
-  read_only  = true
   help       = "type check expressions"
diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index f0d767276..f014068f3 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -8,7 +8,6 @@ header = "options/main_options.h"
   short      = "V"
   long       = "version"
   type       = "bool"
-  read_only  = true
   alternate  = false
   help       = "identify this cvc5 binary"
 
@@ -18,7 +17,6 @@ header = "options/main_options.h"
   short      = "h"
   long       = "help"
   type       = "bool"
-  read_only  = true
   alternate  = false
   help       = "full command line reference"
 
@@ -27,7 +25,6 @@ header = "options/main_options.h"
   long       = "show-config"
   type       = "void"
   handler    = "showConfiguration"
-  read_only  = true
   help       = "show cvc5 static configuration"
 
 [[option]]
@@ -35,7 +32,6 @@ header = "options/main_options.h"
   long       = "copyright"
   type       = "void"
   handler    = "copyright"
-  read_only  = true
   help       = "show cvc5 copyright information"
 
 [[option]]
@@ -45,7 +41,6 @@ header = "options/main_options.h"
   long       = "seed=N"
   type       = "uint64_t"
   default    = "0"
-  read_only  = true
   help       = "seed for random number generator"
 
 [[option]]
@@ -53,7 +48,6 @@ header = "options/main_options.h"
   long       = "show-debug-tags"
   type       = "void"
   handler    = "showDebugTags"
-  read_only  = true
   help       = "show all available tags for debugging"
 
 [[option]]
@@ -61,7 +55,6 @@ header = "options/main_options.h"
   long       = "show-trace-tags"
   type       = "void"
   handler    = "showTraceTags"
-  read_only  = true
   help       = "show all available tags for tracing"
 
 [[option]]
@@ -70,7 +63,6 @@ header = "options/main_options.h"
   long       = "early-exit"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do not run destructors at exit; default on except in debug builds"
 
 [[option]]
@@ -86,7 +78,6 @@ header = "options/main_options.h"
   long       = "interactive-prompt"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "interactive prompting while in interactive mode"
 
 [[option]]
@@ -95,7 +86,6 @@ header = "options/main_options.h"
   long       = "segv-spin"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "spin on segfault/other crash waiting for gdb"
 
 [[option]]
@@ -104,5 +94,4 @@ header = "options/main_options.h"
   long       = "tear-down-incremental=N"
   type       = "int"
   default    = "0"
-  read_only  = true
   help       = "implement PUSH/POP/multi-query by destroying and recreating SmtEngine every N queries"
diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index e2c138490..b632b3384 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -56,7 +56,7 @@ MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option']
 OPTION_ATTR_REQ = ['category', 'type']
 OPTION_ATTR_ALL = OPTION_ATTR_REQ + [
     'name', 'help', 'help_mode', 'smt_name', 'short', 'long', 'default',
-    'includes', 'handler', 'predicates', 'read_only',
+    'includes', 'handler', 'predicates',
     'alternate', 'mode'
 ]
 
@@ -134,15 +134,6 @@ TPL_OPTION_STRUCT_RW = \
   static constexpr const char* name = "{long_name}";
 }} thread_local {name};"""
 
-TPL_OPTION_STRUCT_RO = \
-"""extern struct {name}__option_t
-{{
-  typedef {type} type;
-  type operator()() const;
-  static constexpr const char* name = "{long_name}";
-}} thread_local {name};"""
-
-
 TPL_DECL_SET = \
 """template <> options::{name}__option_t::type& Options::ref(
     options::{name}__option_t);"""
@@ -260,12 +251,11 @@ class Option(object):
         self.__dict__ = dict((k, None) for k in OPTION_ATTR_ALL)
         self.includes = []
         self.predicates = []
-        self.read_only = False
         self.alternate = True    # add --no- alternative long option for bool
         self.filename = None
         for (attr, val) in d.items():
             assert attr in self.__dict__
-            if attr in ['read_only', 'alternate'] or val:
+            if attr == 'alternate' or val:
                 self.__dict__[attr] = val
 
 
@@ -274,6 +264,7 @@ def die(msg):
 
 
 def perr(filename, msg, option = None):
+    msg_suffix = ''
     if option:
         if option.name:
             msg_suffix = "option '{}' ".format(option.name)
@@ -461,7 +452,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
             holder_specs.append(TPL_HOLDER_MACRO_ATTR.format(name=option.name))
 
         # Generate module declaration
-        tpl_decl = TPL_OPTION_STRUCT_RO if option.read_only else TPL_OPTION_STRUCT_RW
+        tpl_decl = TPL_OPTION_STRUCT_RW
         if option.long:
             long_name = option.long.split('=')[0]
         else:
@@ -469,8 +460,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         decls.append(tpl_decl.format(name=option.name, type=option.type, long_name = long_name))
 
         # Generate module specialization
-        if not option.read_only:
-            specs.append(TPL_DECL_SET.format(name=option.name))
+        specs.append(TPL_DECL_SET.format(name=option.name))
         specs.append(TPL_DECL_OP_BRACKET.format(name=option.name))
         specs.append(TPL_DECL_WAS_SET_BY_USER.format(name=option.name))
 
@@ -492,8 +482,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         ### Generate code for {module.name}_options.cpp
 
         # Accessors
-        if not option.read_only:
-            accs.append(TPL_IMPL_SET.format(name=option.name))
+        accs.append(TPL_IMPL_SET.format(name=option.name))
         accs.append(TPL_IMPL_OP_BRACKET.format(name=option.name))
         accs.append(TPL_IMPL_WAS_SET_BY_USER.format(name=option.name))
 
diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 1a4b75429..56568bc0c 100644
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -7,7 +7,6 @@ header = "options/parser_options.h"
   category   = "common"
   long       = "strict-parsing"
   type       = "bool"
-  read_only  = true
   help       = "be less tolerant of non-conforming inputs"
 
 [[option]]
@@ -15,7 +14,6 @@ header = "options/parser_options.h"
   category   = "regular"
   long       = "mmap"
   type       = "bool"
-  read_only  = true
   help       = "memory map file input"
 
 [[option]]
@@ -24,7 +22,6 @@ header = "options/parser_options.h"
   category   = "regular"
   type       = "bool"
   default    = "DO_SEMANTIC_CHECKS_BY_DEFAULT"
-  read_only  = true
   help       = "enable semantic checks, including type checks"
 
 [[option]]
@@ -33,7 +30,6 @@ header = "options/parser_options.h"
   category   = "regular"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "force all declarations and definitions to be global"
 
 # this is to support security in the online version, and in other similar
@@ -54,7 +50,6 @@ header = "options/parser_options.h"
   long       = "filesystem-access"
   type       = "bool"
   default    = "true"
-  read_only  = true
 
 [[option]]
   name       = "forceLogicString"
@@ -62,5 +57,4 @@ header = "options/parser_options.h"
   category   = "expert"
   long       = "force-logic=LOGIC"
   type       = "std::string"
-  read_only  = true
   help       = "set the logic, and override all further user attempts to change it"
diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index f6a39e0fe..177307918 100644
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -26,7 +26,6 @@ header = "options/proof_options.h"
   long       = "proof-print-conclusion"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "Print conclusion of proof steps when printing AST"
 
 [[option]]
@@ -35,7 +34,6 @@ header = "options/proof_options.h"
   long       = "proof-pedantic=N"
   type       = "uint32_t"
   default    = "0"
-  read_only  = true
   help       = "assertion failure for any incorrect rule application or untrusted lemma having pedantic level <=N with proof"
 
 [[option]]
diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 5ad691e62..0670bb7da 100644
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -10,7 +10,6 @@ header = "options/prop_options.h"
   type       = "double"
   default    = "0.0"
   predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
-  read_only  = true
   help       = "sets the frequency of random decisions in the sat solver (P=0.0 by default)"
 
 [[option]]
@@ -44,7 +43,6 @@ header = "options/prop_options.h"
   long       = "restart-int-base=N"
   type       = "unsigned"
   default    = "25"
-  read_only  = true
   help       = "sets the base restart interval for the sat solver (N=25 by default)"
 
 [[option]]
@@ -54,7 +52,6 @@ header = "options/prop_options.h"
   type       = "double"
   default    = "3.0"
   predicates = ["doubleGreaterOrEqual0"]
-  read_only  = true
   help       = "sets the restart interval increase factor for the sat solver (F=3.0 by default)"
 
 [[option]]
@@ -63,7 +60,6 @@ header = "options/prop_options.h"
   long       = "refine-conflicts"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "refine theory conflict clauses (default false)"
 
 [[option]]
@@ -80,5 +76,4 @@ header = "options/prop_options.h"
   long       = "minisat-dump-dimacs"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "instead of solving minisat dumps the asserted clauses in Dimacs format"
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 076d26553..ce2e1ab32 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -67,7 +67,6 @@ header = "options/quantifiers_options.h"
   long       = "var-elim-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable simple variable elimination for quantified formulas"
 
 [[option]]
@@ -76,7 +75,6 @@ header = "options/quantifiers_options.h"
   long       = "var-ineq-elim-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable variable elimination based on infinite projection of unbound arithmetic variables"
 
 [[option]]
@@ -85,7 +83,6 @@ header = "options/quantifiers_options.h"
   long       = "dt-var-exp-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "expand datatype variables bound to one constructor in quantifiers"
 
 [[option]]
@@ -112,7 +109,6 @@ header = "options/quantifiers_options.h"
   long       = "cond-var-split-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "split quantified formulas that lead to variable eliminations"
 
 [[option]]
@@ -121,7 +117,6 @@ header = "options/quantifiers_options.h"
   long       = "cond-var-split-agg-quant"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "aggressive split quantified formulas that lead to variable eliminations"
 
 [[option]]
@@ -165,7 +160,6 @@ header = "options/quantifiers_options.h"
   long       = "ag-miniscope-quant"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "perform aggressive miniscoping for quantifiers"
 
 [[option]]
@@ -174,7 +168,6 @@ header = "options/quantifiers_options.h"
   long       = "elim-taut-quant"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "eliminate tautological disjuncts of quantified formulas"
 
 [[option]]
@@ -183,7 +176,6 @@ header = "options/quantifiers_options.h"
   long       = "ext-rewrite-quant"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "apply extended rewriting to bodies of quantified formulas"
 
 [[option]]
@@ -233,7 +225,6 @@ header = "options/quantifiers_options.h"
   long       = "register-quant-body-terms"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "consider ground terms within bodies of quantified formulas for matching"
 
 [[option]]
@@ -242,7 +233,6 @@ header = "options/quantifiers_options.h"
   long       = "strict-triggers"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "only instantiate quantifiers with user patterns based on triggers"
 
 [[option]]
@@ -251,7 +241,6 @@ header = "options/quantifiers_options.h"
   long       = "relevant-triggers"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "prefer triggers that are more relevant based on SInE style analysis"
 
 [[option]]
@@ -260,7 +249,6 @@ header = "options/quantifiers_options.h"
   long       = "relational-triggers"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "choose relational triggers such as x = f(y), x >= f(y)"
 
 [[option]]
@@ -285,7 +273,6 @@ header = "options/quantifiers_options.h"
   long       = "multi-trigger-when-single"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "select multi triggers when single triggers exist"
 
 [[option]]
@@ -294,7 +281,6 @@ header = "options/quantifiers_options.h"
   long       = "multi-trigger-priority"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "only try multi triggers if single triggers give no instantiations"
 
 [[option]]
@@ -303,7 +289,6 @@ header = "options/quantifiers_options.h"
   long       = "multi-trigger-cache"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "caching version of multi triggers"
 
 [[option]]
@@ -312,7 +297,6 @@ header = "options/quantifiers_options.h"
   long       = "multi-trigger-linear"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "implementation of multi triggers where maximum number of instantiations is linear wrt number of ground terms"
 
 # Trigger selection mode.
@@ -421,7 +405,6 @@ header = "options/quantifiers_options.h"
   long       = "increment-triggers"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "generate additional triggers as needed during search"
 
 [[option]]
@@ -490,7 +473,6 @@ header = "options/quantifiers_options.h"
   long       = "inst-level-input-only"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "only input terms are assigned instantiation level zero"
 
 [[option]]
@@ -525,7 +507,6 @@ header = "options/quantifiers_options.h"
   long       = "full-saturate-quant-rd"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "whether to use relevant domain first for enumerative instantiation strategy"
 
 [[option]]
@@ -534,7 +515,6 @@ header = "options/quantifiers_options.h"
   long       = "full-saturate-quant-limit=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "maximum number of rounds of enumerative instantiation to apply (-1 means no limit)"
   
 [[option]]
@@ -543,7 +523,6 @@ header = "options/quantifiers_options.h"
   long       = "fs-interleave"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "interleave enumerative instantiation with other techniques"
 
 [[option]]
@@ -552,7 +531,6 @@ header = "options/quantifiers_options.h"
   long       = "fs-stratify"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "stratify effort levels in enumerative instantiation, which favors speed over fairness"
 
 [[option]]
@@ -561,7 +539,6 @@ header = "options/quantifiers_options.h"
   long       = "fs-sum"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "enumerating tuples of quantifiers by increasing the sum of indices, rather than the maximum"
 
 [[option]]
@@ -570,7 +547,6 @@ header = "options/quantifiers_options.h"
   long       = "literal-matching=MODE"
   type       = "LiteralMatchMode"
   default    = "USE"
-  read_only  = true
   help       = "choose literal matching mode"
   help_mode  = "Literal match modes."
 [[option.mode.NONE]]
@@ -610,7 +586,6 @@ header = "options/quantifiers_options.h"
   long       = "quant-fun-wd"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "assume that function defined by quantifiers are well defined"
 
 [[option]]
@@ -627,7 +602,6 @@ header = "options/quantifiers_options.h"
   long       = "fmf-fun-rlv"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "find models for recursively defined functions, assumes functions are admissible, allows empty type when function is irrelevant"
 
 [[option]]
@@ -662,7 +636,6 @@ header = "options/quantifiers_options.h"
   long       = "mbqi-interleave"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "interleave model-based quantifier instantiation with other techniques"
 
 [[option]]
@@ -679,7 +652,6 @@ header = "options/quantifiers_options.h"
   long       = "fmf-fresh-dc"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use fresh distinguished representative when applying Inst-Gen techniques"
 
 [[option]]
@@ -688,7 +660,6 @@ header = "options/quantifiers_options.h"
   long       = "fmf-fmc-simple"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "simple models in full model check for finite model finding"
 
 [[option]]
@@ -721,7 +692,6 @@ header = "options/quantifiers_options.h"
   long       = "fmf-type-completion-thresh=N"
   type       = "int"
   default    = "1000"
-  read_only  = true
   help       = "the maximum cardinality of an interpreted type for which exhaustive enumeration in finite model finding is attempted"
 
 [[option]]
@@ -738,7 +708,6 @@ header = "options/quantifiers_options.h"
   long       = "quant-cf-mode=MODE"
   type       = "QcfMode"
   default    = "PROP_EQ"
-  read_only  = true
   help       = "what effort to apply conflict find mechanism"
   help_mode  = "Quantifier conflict find modes."
 [[option.mode.CONFLICT_ONLY]]
@@ -757,7 +726,6 @@ header = "options/quantifiers_options.h"
   long       = "quant-cf-when=MODE"
   type       = "QcfWhenMode"
   default    = "DEFAULT"
-  read_only  = true
   help       = "when to invoke conflict find mechanism for quantifiers"
   help_mode  = "Quantifier conflict find modes."
 [[option.mode.DEFAULT]]
@@ -795,7 +763,6 @@ header = "options/quantifiers_options.h"
   long       = "qcf-nested-conflict"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "consider conflicts for nested quantifiers"
 
 [[option]]
@@ -804,7 +771,6 @@ header = "options/quantifiers_options.h"
   long       = "qcf-vo-exp"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "qcf experimental variable ordering"
 
 [[option]]
@@ -821,7 +787,6 @@ header = "options/quantifiers_options.h"
   long       = "qcf-eager-test"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "optimization, test qcf instances eagerly"
 
 [[option]]
@@ -830,7 +795,6 @@ header = "options/quantifiers_options.h"
   long       = "qcf-eager-check-rd"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "optimization, eagerly check relevant domain of matched position"
 
 [[option]]
@@ -839,7 +803,6 @@ header = "options/quantifiers_options.h"
   long       = "qcf-skip-rd"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "optimization, skip instances based on possibly irrelevant portions of quantified formulas"
 
 ### Induction options
@@ -850,7 +813,6 @@ header = "options/quantifiers_options.h"
   long       = "quant-ind"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use all available techniques for inductive reasoning"
 
 [[option]]
@@ -883,7 +845,6 @@ header = "options/quantifiers_options.h"
   long       = "conjecture-gen-per-round=N"
   type       = "int"
   default    = "1"
-  read_only  = true
   help       = "number of conjectures to generate per instantiation round"
 
 [[option]]
@@ -892,7 +853,6 @@ header = "options/quantifiers_options.h"
   long       = "conjecture-no-filter"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "do not filter conjectures"
 
 [[option]]
@@ -925,7 +885,6 @@ header = "options/quantifiers_options.h"
   long       = "conjecture-gen-gt-enum=N"
   type       = "int"
   default    = "50"
-  read_only  = true
   help       = "number of ground terms to generate for model filtering"
 
 [[option]]
@@ -934,7 +893,6 @@ header = "options/quantifiers_options.h"
   long       = "conjecture-gen-uee-intro"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "more aggressive merging for universal equality engine, introduces terms"
 
 [[option]]
@@ -943,7 +901,6 @@ header = "options/quantifiers_options.h"
   long       = "conjecture-gen-max-depth=N"
   type       = "int"
   default    = "3"
-  read_only  = true
   help       = "maximum depth of terms to consider for conjectures"
 
 ### Synthesis options
@@ -954,7 +911,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-inference"
   type       = "bool"
   default    = "false"
-  read_only  = false
   help       = "attempt to preprocess arbitrary inputs to sygus conjectures"
 
 [[option]]
@@ -989,7 +945,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-si-partial"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "combined techniques for synthesis conjectures that are partially single invocation"
 
 # Solution reconstruction modes for single invocation conjectures
@@ -1025,7 +980,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-si-rcons-limit=N"
   type       = "int"
   default    = "10000"
-  read_only  = true
   help       = "number of rounds of enumeration to use during solution reconstruction (negative means unlimited)"
 
 [[option]]
@@ -1034,7 +988,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-si-reconstruct-const"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "include constants when reconstruct solutions for single invocation conjectures in original grammar"
 
 [[option]]
@@ -1043,7 +996,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-si-abort"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "abort if synthesis conjecture is not single invocation"
 
 [[option]]
@@ -1052,7 +1004,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-crepair-abort"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "abort if constant repair techniques are not applicable"
 
 # Modes for piecewise-independent unification for synthesis (see Barbosa et al
@@ -1109,7 +1060,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-qe-preproc"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use quantifier elimination as a preprocessing step for sygus"
 
 [[option]]
@@ -1141,7 +1091,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-active-gen=MODE"
   type       = "SygusActiveGenMode"
   default    = "AUTO"
-  read_only  = true
   help       = "mode for actively-generated sygus enumerators"
   help_mode  = "Modes for actively-generated sygus enumerators."
 [[option.mode.NONE]]
@@ -1174,7 +1123,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-min-grammar"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "statically minimize sygus grammars"
 
 [[option]]
@@ -1183,7 +1131,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-add-const-grammar"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "statically add constants appearing in conjecture to grammars"
 
 [[option]]
@@ -1192,7 +1139,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-grammar-norm"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "statically normalize sygus grammars based on flattening (linearization)"
 
 [[option]]
@@ -1201,7 +1147,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-templ-embed-grammar"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "embed sygus templates into grammars"
 
 [[option]]
@@ -1249,7 +1194,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-inv-templ-when-sg"
   type       = "bool"
   default    = "false"
-  read_only  = false
   help       = "use invariant templates (with solution reconstruction) for syntax guided problems"
 
 [[option]]
@@ -1258,7 +1202,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-auto-unfold"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "enable approach which automatically unfolds transition systems for directly solving invariant synthesis problems"
 
 [[option]]
@@ -1291,7 +1234,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-eval-unfold"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do unfolding of sygus evaluation functions"
 
 [[option]]
@@ -1300,7 +1242,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-eval-unfold-bool"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do unfolding of Boolean evaluation functions that appear in refinement lemmas"
 
 [[option]]
@@ -1377,7 +1318,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-rr"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use sygus to enumerate and verify correctness of rewrite rules"
 
 [[option]]
@@ -1450,7 +1390,6 @@ header = "options/quantifiers_options.h"
   long       = "sygus-sample-grammar"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "when applicable, use grammar for choosing sample points"
 
 [[option]]
@@ -1690,7 +1629,6 @@ header = "options/quantifiers_options.h"
   long       = "cegqi-min-bounds"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
 
 [[option]]
@@ -1699,7 +1637,6 @@ header = "options/quantifiers_options.h"
   long       = "cegqi-round-up-lia"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
 
 [[option]]
@@ -1716,7 +1653,6 @@ header = "options/quantifiers_options.h"
   long       = "cegqi-nopt"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "non-optimal bounds for counterexample-based quantifier instantiation"
 
 # CEGQI for BV
@@ -1795,7 +1731,6 @@ header = "options/quantifiers_options.h"
   long       = "quant-alpha-equiv"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "infer alpha equivalence between quantified formulas"
 
 [[option]]
@@ -1812,7 +1747,6 @@ header = "options/quantifiers_options.h"
   long       = "macros-quant-mode=MODE"
   type       = "MacrosQuantMode"
   default    = "GROUND_UF"
-  read_only  = true
   help       = "mode for quantifiers macro expansion"
   help_mode  = "Modes for quantifiers macro expansion."
 [[option.mode.ALL]]
@@ -1851,7 +1785,6 @@ header = "options/quantifiers_options.h"
   long       = "ho-matching"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do higher-order matching algorithm for triggers with variable operators"
 
 [[option]]
@@ -1860,7 +1793,6 @@ header = "options/quantifiers_options.h"
   long       = "ho-matching-var-priority"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "give priority to variable arguments over constant arguments"
 
 [[option]]
@@ -1869,7 +1801,6 @@ header = "options/quantifiers_options.h"
   long       = "ho-merge-term-db"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "merge term indices modulo equality"
 
 [[option]]
@@ -1878,7 +1809,6 @@ header = "options/quantifiers_options.h"
   long       = "ho-elim"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "eagerly eliminate higher-order constraints"
 
 [[option]]
@@ -1887,7 +1817,6 @@ header = "options/quantifiers_options.h"
   long       = "ho-elim-store-ax"
   type       = "bool"
   default    = "true"
-  read_only  = false
   help       = "use store axiom during ho-elim"
 
 ### Output options
diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 05dd613f1..8f1c28ca5 100644
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -47,7 +47,6 @@ header = "options/resource_manager_options.h"
   long       = "rweight=VAL=N"
   type       = "std::string"
   handler    = "setResourceWeight"
-  read_only  = true
   help       = "set a single resource weight"
 
 [[option]]
diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml
index e19790d7b..9e808df98 100644
--- a/src/options/sep_options.toml
+++ b/src/options/sep_options.toml
@@ -8,7 +8,6 @@ header = "options/sep_options.h"
   long       = "sep-check-neg"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "check negated spatial assertions"
 
 [[option]]
@@ -17,7 +16,6 @@ header = "options/sep_options.h"
   long       = "sep-exp"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "experimental flag for sep"
 
 [[option]]
@@ -26,7 +24,6 @@ header = "options/sep_options.h"
   long       = "sep-min-refine"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "only add refinement lemmas for minimal (innermost) assertions"
 
 [[option]]
@@ -35,7 +32,6 @@ header = "options/sep_options.h"
   long       = "sep-deq-c"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "assume cardinality elements are distinct"
 
 [[option]]
@@ -44,7 +40,6 @@ header = "options/sep_options.h"
   long       = "sep-pre-skolem-emp"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "eliminate emp constraint at preprocess time"
 
 [[option]]
@@ -53,5 +48,4 @@ header = "options/sep_options.h"
   long       = "sep-child-refine"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "child-specific refinements of negated star, positive wand"
diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index 766da793a..0f206f980 100644
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -8,7 +8,6 @@ header = "options/sets_options.h"
   long       = "sets-proxy-lemmas"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "introduce proxy variables eagerly to shorten lemmas"
 
 [[option]]
@@ -17,7 +16,6 @@ header = "options/sets_options.h"
   long       = "sets-infer-as-lemmas"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "send inferences as lemmas"
 
 [[option]]
@@ -26,5 +24,4 @@ header = "options/sets_options.h"
   long       = "sets-ext"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "enable extended symbols such as complement and universe in theory of sets"
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"
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 208b4483f..4672bbb6e 100644
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -24,7 +24,6 @@ header = "options/strings_options.h"
   long       = "strings-eager"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "strings eager check"
 
 [[option]]
@@ -33,7 +32,6 @@ header = "options/strings_options.h"
   long       = "strings-inm"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "internal for strings: ignore negative membership constraints (fragment checking is needed, left to users for now)"
 
 [[option]]
@@ -42,7 +40,6 @@ header = "options/strings_options.h"
   long       = "strings-lazy-pp"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "perform string preprocessing lazily"
 
 [[option]]
@@ -51,7 +48,6 @@ header = "options/strings_options.h"
   long       = "strings-len-norm"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "strings length normalization lemma"
 
 [[option]]
@@ -60,7 +56,6 @@ header = "options/strings_options.h"
   long       = "strings-infer-sym"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "strings split on empty string"
 
 [[option]]
@@ -69,7 +64,6 @@ header = "options/strings_options.h"
   long       = "strings-eager-len"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "strings eager length lemmas"
 
 [[option]]
@@ -78,7 +72,6 @@ header = "options/strings_options.h"
   long       = "strings-check-entail-len"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "check entailment between length terms to reduce splitting"
 
 [[option]]
@@ -112,7 +105,6 @@ header = "options/strings_options.h"
   long       = "strings-infer-as-lemmas"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "always send lemmas out instead of making internal inferences"
 
 [[option]]
@@ -121,7 +113,6 @@ header = "options/strings_options.h"
   long       = "strings-rexplain-lemmas"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "regression explanations for string lemmas"
 
 [[option]]
@@ -130,7 +121,6 @@ header = "options/strings_options.h"
   long       = "strings-min-prefix-explain"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "minimize explanations for prefix of normal forms in strings"
 
 [[option]]
@@ -139,7 +129,6 @@ header = "options/strings_options.h"
   long       = "strings-guess-model"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "use model guessing to avoid string extended function reductions"
 
 [[option]]
@@ -148,7 +137,6 @@ header = "options/strings_options.h"
   long       = "strings-lprop-csp"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "do length propagation based on constant splits"
 
 [[option]]
@@ -173,7 +161,6 @@ header = "options/strings_options.h"
   long       = "strings-ff"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "do flat form inferences"
 
 [[option]]
@@ -203,7 +190,6 @@ header = "options/strings_options.h"
   long       = "strings-unified-vspt"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use a single skolem for the variable splitting rule"
 
 [[option]]
diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index 388333124..a0f769684 100644
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -32,7 +32,6 @@ header = "options/theory_options.h"
   long       = "condense-function-values"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "condense values for functions in models rather than explicitly representing them"
 
 [[option]]
diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index a098061f8..bd0027fb4 100644
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -17,7 +17,6 @@ header = "options/uf_options.h"
   long       = "uf-ss-totality-limited=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "apply totality axioms, but only up to cardinality N (-1 == do not apply totality axioms, default)"
 
 [[option]]
@@ -26,7 +25,6 @@ header = "options/uf_options.h"
   long       = "uf-ss-totality-sym-break"
   type       = "bool"
   default    = "false"
-  read_only  = true
   help       = "apply symmetry breaking for totality axioms"
 
 [[option]]
@@ -35,7 +33,6 @@ header = "options/uf_options.h"
   long       = "uf-ss-abort-card=N"
   type       = "int"
   default    = "-1"
-  read_only  = true
   help       = "tells the uf with cardinality to only consider models that interpret uninterpreted sorts of cardinality at most N (-1 == no limit, default)"
 
 [[option]]
@@ -44,7 +41,6 @@ header = "options/uf_options.h"
   long       = "uf-ss=MODE"
   type       = "UfssMode"
   default    = "FULL"
-  read_only  = true
   help       = "mode of operation for uf with cardinality solver."
   help_mode  = "UF with cardinality options currently supported by the --uf-ss option when combined with finite model finding."
 [[option.mode.FULL]]
@@ -63,7 +59,6 @@ header = "options/uf_options.h"
   long       = "uf-ss-fair"
   type       = "bool"
   default    = "true"
-  read_only  = true
   help       = "use fair strategy for finite model finding multiple sorts"
 
 [[option]]