Refactor mkoptions (#1631)

This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation.

The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick.

This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part.

1 files changed, 84 insertions, 0 deletions

diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
new file mode 100644
index 000000000..5ad691e62
--- /dev/null
+++ b/src/options/prop_options.toml
@@ -0,0 +1,84 @@
+id     = "PROP"
+name   = "SAT layer"
+header = "options/prop_options.h"
+
+[[option]]
+  name       = "satRandomFreq"
+  smt_name   = "random-frequency"
+  category   = "regular"
+  long       = "random-freq=P"
+  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]]
+  name       = "satRandomSeed"
+  smt_name   = "random-seed"
+  category   = "regular"
+  long       = "random-seed=S"
+  type       = "uint32_t"
+  default    = "0"
+  help       = "sets the random seed for the sat solver"
+
+[[option]]
+  name       = "satVarDecay"
+  category   = "regular"
+  type       = "double"
+  default    = "0.95"
+  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
+  help       = "variable activity decay factor for Minisat"
+
+[[option]]
+  name       = "satClauseDecay"
+  category   = "regular"
+  type       = "double"
+  default    = "0.999"
+  predicates = ["doubleGreaterOrEqual0", "doubleLessOrEqual1"]
+  help       = "clause activity decay factor for Minisat"
+
+[[option]]
+  name       = "satRestartFirst"
+  category   = "regular"
+  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]]
+  name       = "satRestartInc"
+  category   = "regular"
+  long       = "restart-int-inc=F"
+  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]]
+  name       = "sat_refine_conflicts"
+  category   = "regular"
+  long       = "refine-conflicts"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "refine theory conflict clauses (default false)"
+
+[[option]]
+  name       = "minisatUseElim"
+  category   = "regular"
+  long       = "minisat-elimination"
+  type       = "bool"
+  default    = "true"
+  help       = "use Minisat elimination"
+
+[[option]]
+  name       = "minisatDumpDimacs"
+  category   = "regular"
+  long       = "minisat-dump-dimacs"
+  type       = "bool"
+  default    = "false"
+  read_only  = true
+  help       = "instead of solving minisat dumps the asserted clauses in Dimacs format"