CLI Refactoring

[madmike200590]

Alpha's command line interface has been growing organically for quite some time. Right now, we have a lot of different flags and options that are partly related and - in some cases - influence each other in a rather intransparent fashion.

In order to make the CLI a bit more approachable, it would be useful to group related options by category, e.g.

• preprocessing (re-writing options, ...)
• grounding (for grounder type, heuristics etc)
• solving
• output formatting

One way to achieve this from a programming point of view would be switching to a more powerful argument parsing library - one I can think of right now is argparse4j, which supports subcommands which could be used for grouping of options.

This task is divided into two basic steps:

• Specfiy how an ideal CLI should look (i.e. complete usage)
• Implement result of step 1 using a suitable library

[lorenzleutgeb]

That's quite tough. Some inspiration:

clingo options

$ clingo --help=3
clingo version 5.4.0
usage: clingo [number] [options] [files]

Clasp.Config Options:

  --configuration=<arg>   : Set default configuration [auto]
      <arg>: {auto|frumpy|jumpy|tweety|handy|crafty|trendy|many|<file>}
        auto  : Select configuration based on problem type
        frumpy: Use conservative defaults
        jumpy : Use aggressive defaults
        tweety: Use defaults geared towards asp problems
        handy : Use defaults geared towards large problems
        crafty: Use defaults geared towards crafted problems
        trendy: Use defaults geared towards industrial problems
        many  : Use default portfolio to configure solver(s)
        <file>: Use configuration file to configure solver(s)
  --tester=<options>      : Pass (quoted) string of <options> to tester
  --stats[=<n>[,<t>]],-s  : Enable {1=basic|2=full} statistics (<t> for tester)
  --[no-]parse-ext        : Enable extensions in non-aspif input
  --[no-]parse-maxsat     : Treat dimacs input as MaxSAT problem

Clasp.Context Options:

  --share=<arg>|no        : Configure physical sharing of constraints [auto]
      <arg>: {auto|problem|learnt|all}
  --learn-explicit        : Do not use Short Implication Graph for learning
  --sat-prepro[=<arg>|no] : Run SatELite-like preprocessing (Implicit: 2)
      <arg>: <level>[,<limit>...]
        <level> : Set preprocessing level to <level  {1..3}>
          1: Variable elimination with subsumption (VE)
          2: VE with limited blocked clause elimination (BCE)
          3: Full BCE followed by VE
        <limit> : [<key {iter|occ|time|frozen|clause}>=]<n> (0=no limit)
          iter  : Set iteration limit to <n>           [0]
          occ   : Set variable occurrence limit to <n> [0]
          time  : Set time limit to <n> seconds        [0]
          frozen: Set frozen variables limit to <n>%   [0]
          size  : Set size limit to <n>*1000 clauses   [4000]

Clasp.ASP Options:

  --trans-ext=<mode>|no   : Configure handling of extended rules
      <mode>: {all|choice|card|weight|integ|dynamic}
        all    : Transform all extended rules to basic rules
        choice : Transform choice rules, but keep cardinality and weight rules
        card   : Transform cardinality rules, but keep choice and weight rules
        weight : Transform cardinality and weight rules, but keep choice rules
        scc    : Transform "recursive" cardinality and weight rules
        integ  : Transform cardinality integrity constraints
        dynamic: Transform "simple" extended rules, but keep more complex ones
  --eq=<n>                : Configure equivalence preprocessing
      Run for at most <n> iterations (-1=run to fixpoint)
  --[no-]backprop         : Use backpropagation in ASP-preprocessing
  --supp-models           : Compute supported models
  --no-ufs-check          : Disable unfounded set check
  --no-gamma              : Do not add gamma rules for non-hcf disjunctions
  --eq-dfs                : Enable df-order in eq-preprocessing

Clasp.Solving Options:

  --solve-limit=<n>[,<m>] : Stop search after <n> conflicts or <m> restarts

  --parallel-mode,-t <arg>: Run parallel search with given number of threads
      <arg>: <n {1..64}>[,<mode {compete|split}>]
        <n>   : Number of threads to use in search
        <mode>: Run competition or splitting based search [compete]

  --global-restarts=<X>   : Configure global restart policy
      <X>: <n>[,<sched>]
        <n> : Maximal number of global restarts (0=disable)
     <sched>: Restart schedule [x,100,1.5] (<type {F|L|x|+}>)

  --distribute=<arg>|no   : Configure nogood distribution [conflict,global,4]
      <arg>: <type>[,<mode>][,<lbd {0..127}>][,<size>]
        <type> : Distribute {all|short|conflict|loop} nogoods
        <mode> : Use {global|local} distribution   [global]
        <lbd>  : Distribute only if LBD  <= <lbd>  [4]
        <size> : Distribute only if size <= <size> [-1]
  --integrate=<arg>       : Configure nogood integration [gp]
      <arg>: <pick>[,<n>][,<topo>]
        <pick>: Add {all|unsat|gp(unsat wrt guiding path)|active} nogoods
        <n>   : Always keep at least last <n> integrated nogoods   [1024]
        <topo>: Accept nogoods from {all|ring|cube|cubex} peers    [all]

  --enum-mode,-e <arg>    : Configure enumeration algorithm [auto]
      <arg>: {bt|record|brave|cautious|auto}
        bt      : Backtrack decision literals from solutions
        record  : Add nogoods for computed solutions
        domRec  : Add nogoods over true domain atoms
        brave   : Compute brave consequences (union of models)
        cautious: Compute cautious consequences (intersection of models)
        auto    : Use bt for enumeration and record for optimization
  --project[=<arg>|no]    : Enable projective solution enumeration
      <arg>: {show|project|auto}[,<bt {0..3}>] (Implicit: auto,3)
        Project to atoms in show or project directives, or
        select depending on the existence of a project directive
      <bt> : Additional options for enumeration algorithm 'bt'
        Use activity heuristic (1) when selecting backtracking literal
        and/or progress saving (2) when retracting solution literals
  --models,-n <n>         : Compute at most <n> models (0 for all)

  --opt-mode=<arg>        : Configure optimization algorithm
      <arg>: <mode {opt|enum|optN|ignore}>[,<bound>...]
        opt   : Find optimal model
        enum  : Find models with costs <= <bound>
        optN  : Find optimum, then enumerate optimal models
        ignore: Ignore optimize statements
      <bound> : Set initial bound for objective function(s)

Clasp.Search Options:

  --opt-strategy=<arg>    : Configure optimization strategy
      <arg>: {bb|usc}[,<tactics>]
        bb : Model-guided optimization with <tactics {lin|hier|inc|dec}> [lin]
          lin : Basic lexicographical descent
          hier: Hierarchical (highest priority criteria first) descent 
          inc : Hierarchical descent with exponentially increasing steps
          dec : Hierarchical descent with exponentially decreasing steps
        usc: Core-guided optimization with <tactics>: <relax>[,<opts>]
          <relax>: Relaxation algorithm {oll|one|k|pmres}                [oll]
            oll    : Use strategy from unclasp
            one    : Add one cardinality constraint per core
            k[,<n>]: Add cardinality constraints of bounded size ([0]=dynamic)
            pmres  : Add clauses of size 3
          <opts> : Tactics <list {disjoint|succinct|stratify}>|<mask {0..7}>
            disjoint: Disjoint-core preprocessing                    (1)
            succinct: No redundant (symmetry) constraints            (2)
            stratify: Stratification heuristic for handling weights  (4)
  --opt-usc-shrink=<arg>  : Enable core-shrinking in core-guided optimization
      <arg>: <algo>[,<limit> (0=no limit)]
        <algo> : Use algorithm {lin|inv|bin|rgs|exp|min}
          lin  : Forward linear search unsat
          inv  : Inverse linear search not unsat
          bin  : Binary search
          rgs  : Repeated geometric sequence until unsat
          exp  : Exponential search until unsat
          min  : Linear search for subset minimal core
        <limit>: Limit solve calls to 2^<n> conflicts [10]
  --opt-heuristic=<list>  : Use opt. in <list {sign|model}> heuristics
  --[no-]restart-on-model : Restart after each model

  --lookahead[=<arg>|no]  : Configure failed-literal detection (fld)
      <arg>: <type>[,<limit>] / Implicit: atom
        <type> : Run fld via {atom|body|hybrid} lookahead
        <limit>: Disable fld after <limit> applications ([0]=no limit)
      --lookahead=atom is default if --no-lookback is used

  --heuristic=<heu>       : Configure decision heuristic
      <heu>: {Berkmin|Vmtf|Vsids|Domain|Unit|None}[,<n>]
        Berkmin: Use BerkMin-like heuristic (Check last <n> nogoods [0]=all)
        Vmtf   : Use Siege-like heuristic (Move <n> literals to the front [8])
        Vsids  : Use Chaff-like heuristic (Use 1.0/0.<n> as decay factor  [95])
        Domain : Use domain knowledge in Vsids-like heuristic
        Unit   : Use Smodels-like heuristic (Default if --no-lookback)
        None   : Select the first free variable
  --[no-]init-moms        : Initialize heuristic with MOMS-score
  --score-res=<score>     : Resolution score {auto|min|set|multiset}
  --score-other=<arg>     : Score other learnt nogoods: {auto|no|loop|all}
  --sign-def=<sign>       : Default sign: {asp|pos|neg|rnd}
  --[no-]sign-fix         : Disable sign heuristics and use default signs only
  --[no-]berk-huang       : Enable Huang-scoring in Berkmin
  --[no-]vsids-acids      : Enable acids-scheme in Vsids/Domain
  --vsids-progress=<arg>  : Enable dynamic decaying scheme in Vsids/Domain
      <arg>: <n>[,<i {1..100}>][,<c>]|(0=disable)
        <n> : Set initial decay factor to 1.0/0.<n>
        <i> : Set decay update to <i>/100.0      [1]
        <c> : Decrease decay every <c> conflicts [5000]
  --[no-]nant             : Prefer negative antecedents of P in heuristic
  --dom-mod=<arg>         : Default modification for domain heuristic
      <arg>: (no|<mod>[,<pick>])
        <mod>  : Modifier {level|pos|true|neg|false|init|factor}
        <pick> : Apply <mod> to (all | <list {scc|hcc|disj|opt|show}>) atoms
  --save-progress[=<n>]   : Use RSat-like progress saving on backjumps > <n>
  --init-watches=<arg>    : Watched literal initialization: {rnd|first|least}
  --update-mode=<mode>    : Process messages on {propagate|conflict}
  --acyc-prop[={0..1}]    : Use backward inference in acyc propagation
  --seed=<n>              : Set random number generator's seed to <n>
  --partial-check[=<arg>] : Configure partial stability tests
      <arg>: <p>[,<h>] / Implicit: 50
        <p>: Partial check skip percentage
        <h>: Init/update value for high bound ([0]=umax)
  --sign-def-disj=<sign>  : Default sign for atoms in disjunctions
  --rand-freq=<p>|no      : Make random decisions with probability <p>
  --rand-prob=<n>[,<m>]   : Do <n> random searches with [<m>=100] conflicts

Clasp.Lookback Options:

  --no-lookback           : Disable all lookback strategies

  --forget-on-step=<opts> : Configure forgetting on (incremental) step
      <opts>: <list {varScores|signs|lemmaScores|lemmas}>|<mask {0..15}>

  --strengthen=<X>|no     : Use MiniSAT-like conflict nogood strengthening
      <X>: <mode>[,<type>][,<bump {yes|no}>]
        <mode>: Use {local|recursive} self-subsumption check
        <type>: Follow {all|short|binary} antecedents [all]
        <bump>: Bump activities of antecedents        [yes]
  --otfs[={0..2}]         : Enable {1=partial|2=full} on-the-fly subsumption
  --update-lbd=<arg>|no   : Configure LBD updates during conflict resolution
      <arg>: <mode {less|glucose|pseudo}>[,<n {0..127}>]
        less   : update to X = new LBD   iff X   < previous LBD
        glucose: update to X = new LBD   iff X+1 < previous LBD
        pseudo : update to X = new LBD+1 iff X   < previous LBD
           <n> : Protect updated nogoods on next reduce if X <= <n>
  --update-act            : Enable LBD-based activity bumping
  --reverse-arcs[={0..3}] : Enable ManySAT-like inverse-arc learning
  --contraction=<arg>|no  : Configure handling of long learnt nogoods
      <arg>: <n>[,<rep>]
        <n>  : Contract nogoods if size > <n> (0=disable)
        <rep>: Nogood replacement {no|decisionSeq|allUIP|dynamic} [no]

  --loops=<type>          : Configure learning of loop nogoods
      <type>: {common|distinct|shared|no}
        common  : Create loop nogoods for atoms in an unfounded set
        distinct: Create distinct loop nogood for each atom in an unfounded set
        shared  : Create loop formula for a whole unfounded set
        no      : Do not learn loop formulas

  --restarts,-r <sched>|no: Configure restart policy
      <sched>: <type {D|F|L|x|+}>,<n {1..umax}>[,<args>][,<lim>]
        F,<n>    : Run fixed sequence of <n> conflicts
        L,<n>    : Run Luby et al.'s sequence with unit length <n>
        x,<n>,<f>: Run geometric seq. of <n>*(<f>^i) conflicts  (<f> >= 1.0)
        +,<n>,<m>: Run arithmetic seq. of <n>+(<m>*i) conflicts (<m {0..umax}>)
        ...,<lim>: Repeat seq. every <lim>+j restarts           (<type> != F)
        D,<n>,<f>: Restart based on moving LBD average over last <n> conflicts
                   Mavg(<n>,LBD)*<f> > avg(LBD)
                   use conflict level average if <lim> > 0 and avg(LBD) > <lim>
      no|0       : Disable restarts
  --reset-restarts=<arg>  : Update restart seq. on model {no|repeat|disable}
  --[no-]local-restarts   : Use Ryvchin et al.'s local restarts
  --counter-restarts=<arg>: Use counter implication restarts
      <arg>: (<rate>[,<bump>] | {0|no})
      <rate>: Interval in number of restarts
      <bump>: Bump factor applied to indegrees
  --block-restarts=<arg>  : Use glucose-style blocking restarts
      <arg>: <n>[,<R {1.0..5.0}>][,<c>]
        <n>: Window size for moving average (0=disable blocking)
        <R>: Block restart if assignment > average * <R>  [1.4]
        <c>: Disable blocking for the first <c> conflicts [10000]

  --shuffle=<n1>,<n2>|no  : Shuffle problem after <n1>+(<n2>*i) restarts

  --deletion,-d <arg>|no  : Configure deletion algorithm [basic,75,0]
      <arg>: <algo>[,<n {1..100}>][,<sc>]
        <algo>: Use {basic|sort|ipSort|ipHeap} algorithm
        <n>   : Delete at most <n>% of nogoods on reduction    [75]
        <sc>  : Use {activity|lbd|mixed} nogood scores    [activity]
      no      : Disable nogood deletion
  --del-grow=<arg>|no     : Configure size-based deletion policy
      <arg>: <f>[,<g>][,<sched>] (<f> >= 1.0)
        <f>     : Keep at most T = X*(<f>^i) learnt nogoods with X being the
                  initial limit and i the number of times <sched> fired
        <g>     : Stop growth once T > P*<g> (0=no limit)      [3.0]
        <sched> : Set grow schedule (<type {F|L|x|+}>) [grow on restart]
  --del-cfl=<sched>|no    : Configure conflict-based deletion policy
      <sched>:   <type {F|L|x|+}>,<args>... (see restarts)
  --del-init=<arg>        : Configure initial deletion limit
      <arg>: <f>[,<n>,<o>] (<f> > 0)
        <f>    : Set initial limit to P=estimated problem size/<f> [3.0]
        <n>,<o>: Clamp initial limit to the range [<n>,<n>+<o>]
  --del-estimate[=0..3]   : Use estimated problem complexity in limits
  --del-max=<n>,<X>|no    : Keep at most <n> learnt nogoods taking up to <X> MB
  --del-glue=<arg>        : Configure glue clause handling
      <arg>: <n {0..15}>[,<m {0|1}>]
        <n>: Do not delete nogoods with LBD <= <n>
        <m>: Count (0) or ignore (1) glue clauses in size limit [0]
  --del-on-restart=<n>    : Delete <n>% of learnt nogoods on each restart

Gringo Options:

  --text                  : Print plain text format
  --const,-c <id>=<term>  : Replace term occurrences of <id> with <term>
  --output,-o <arg>       : Choose output format:
      intermediate: print intermediate format
      text        : print plain text format
      reify       : print program as reified facts
      smodels     : print smodels format
                    (only supports basic features)
  --output-debug=<arg>    : Print debug information during output:
      none     : no additional info
      text     : print rules as plain text (prefix %)
      translate: print translated rules as plain text (prefix %%)
      all      : combines text and translate
  --warn,-W <warn>        : Enable/disable warnings:
      none:                     disable all warnings
      all:                      enable all warnings
      [no-]atom-undefined:      a :- b.
      [no-]file-included:       #include "a.lp". #include "a.lp".
      [no-]operation-undefined: p(1/0).
      [no-]variable-unbounded:  $x > 10.
      [no-]global-variable:     :- #count { X } = 1, X = 1.
      [no-]other:               clasp related and uncategorized warnings
  --rewrite-minimize      : Rewrite minimize constraints into rules
  --keep-facts            : Do not remove facts from normal rules
  --reify-sccs            : Calculate SCCs for reified output
  --reify-steps           : Add step numbers to reified output

Basic Options:

  --help[=<n>],-h         : Print {1=basic|2=more|3=full} help and exit
  --version,-v            : Print version information and exit
  --verbose[=<n>],-V      : Set verbosity level to <n>
  --time-limit=<n>        : Set time limit to <n> seconds (0=no limit)
  --fast-exit             : Force fast exit (do not call dtors)
  --print-portfolio       : Print default portfolio and exit
  --quiet[=<levels>],-q   : Configure printing of models, costs, and calls
      <levels>: <mod>[,<cost>][,<call>]
        <mod> : print {0=all|1=last|2=no} models
        <cost>: print {0=all|1=last|2=no} optimize values [<mod>]
        <call>: print {0=all|1=last|2=no} call steps      [2]
  --pre[=<fmt>]           : Print simplified program and exit
      <fmt>: Set output format to {aspif|smodels} (implicit: aspif)
  --outf=<n>              : Use {0=default|1=competition|2=JSON|3=no} output
  --out-atomf=<arg>       : Set atom format string (<Pre>?%0<Post>?)
  --out-ifs=<arg>         : Set internal field separator
  --out-hide-aux          : Hide auxiliary atoms in answers
  --lemma-in=<file>       : Read additional lemmas from <file>
  --lemma-out=<file>      : Log learnt lemmas to <file>
  --lemma-out-lbd=<n>     : Only log lemmas with lbd <= <n>
  --lemma-out-max=<n>     : Stop logging after <n> lemmas
  --lemma-out-dom=<arg>   : Log lemmas over <arg {input|output}> variables
  --lemma-out-txt         : Log lemmas as ground integrity constraints
  --hcc-out=<file>        : Write non-hcf programs to <file>.#scc
  --compute=<lit>         : Force given literal to true
  --mode=<arg>            : Run in {clingo|clasp|gringo} mode

usage: clingo [number] [options] [files]
Default command-line:
clingo --configuration=auto --share=auto --distribute=conflict,global,4 
       --integrate=gp --enum-mode=auto --deletion=basic,75,0 --del-init=3.0 
       --verbose=1 
[asp] --configuration=tweety
[cnf] --configuration=trendy
[opb] --configuration=trendy

Default configurations:
[tweety]:
 --eq=3 --trans-ext=dynamic --heuristic=Vsids,92 --restarts=L,60
 --deletion=basic,50 --del-max=2000000 --del-estimate=1 --del-cfl=+,2000,100,20
 --del-grow=0 --del-glue=2,0 --strengthen=recursive,all --otfs=2 --init-moms
 --score-other=all --update-lbd=less --save-progress=160 --init-watches=least
 --local-restarts --loops=shared
[trendy]:
 --sat-p=2,iter=20,occ=25,time=240 --trans-ext=dynamic --heuristic=Vsids
 --restarts=D,100,0.7 --deletion=basic,50 --del-init=3.0,500,19500
 --del-grow=1.1,20.0,x,100,1.5 --del-cfl=+,10000,2000 --del-glue=2
 --strengthen=recursive --update-lbd=less --otfs=2 --save-p=75
 --counter-restarts=3,1023 --reverse-arcs=2 --contraction=250 --loops=common
[frumpy]:
 --eq=5 --heuristic=Berkmin --restarts=x,100,1.5 --deletion=basic,75
 --del-init=3.0,200,40000 --del-max=400000 --contraction=250 --loops=common
 --save-p=180 --del-grow=1.1 --strengthen=local --sign-def-disj=pos
[crafty]:
 --sat-p=2,iter=10,occ=25,time=240 --trans-ext=dynamic --backprop
 --heuristic=Vsids --save-p=180 --restarts=x,128,1.5 --deletion=basic,75
 --del-init=10.0,1000,9000 --del-grow=1.1,20.0 --del-cfl=+,10000,1000
 --del-glue=2 --otfs=2 --reverse-arcs=1 --counter-restarts=3,9973
 --contraction=250
[jumpy]:
 --sat-p=2,iter=20,occ=25,time=240 --trans-ext=dynamic --heuristic=Vsids
 --restarts=L,100 --deletion=basic,75,mixed --del-init=3.0,1000,20000
 --del-grow=1.1,25,x,100,1.5 --del-cfl=x,10000,1.1 --del-glue=2
 --update-lbd=glucose --strengthen=recursive --otfs=2 --save-p=70
[handy]:
 --sat-p=2,iter=10,occ=25,time=240 --trans-ext=dynamic --backprop
 --heuristic=Vsids --restarts=D,100,0.7 --deletion=sort,50,mixed
 --del-max=200000 --del-init=20.0,1000,14000 --del-cfl=+,4000,600 --del-glue=2
 --update-lbd=less --strengthen=recursive --otfs=2 --save-p=20
 --contraction=600 --loops=distinct --counter-restarts=7,1023 --reverse-arcs=2

clingo is part of Potassco: https://potassco.org/clingo
Get help/report bugs via : https://potassco.org/support

[lorenzleutgeb]

As discussed yesterday, I took a look at candidate libraries for argument parsing. There's a list here.

I took a closer look at two more modern libraries:

JCommander

• Supports reading arguments from a file (not like I described yesterday in the sense of a configuration file, but still a little better than working with the shell history)

picocli

• Supports reading arguments from a file (the same way that JCommander does)
• Supports "argument groups"

You may use this link to GitHub Compare to get a rough overview of activity of the three candidates mentioned so far.

Ideas

TODO...

---

Note: I'll edit here as I find out more...

[madmike200590]

I quickly skimmed the getting started guides for both JCommander and picocli - both look really promising to me, and I like the annotation-based approach a lot!

Something came to my mind though - If we were to use one of these and annotate our SystemConfig and InputConfig classes accordingly, wouldn't we introduce a compile-time dependency of the Alpha class on CLI-specific libraries?
Right now, Alpha, as the main API entry point, is configured using a SystemConfig and can be called using InputConfigs.
The way I see it, once issue #108 is through, i.e. we split Alpha into modules, Alpha would reside in a module called alpha-api or something like that and be included by every other module. I think it would be strange for an api module to depend on CLI-specfic stuff, especially since parsing of command-line arguments is not the only way to obtain SystemConfigs and InputConfigs (especially when using Alpha as a library).

Can you think of a way to decouple that? Or am I overengineering it? (Or would it really be that bad for the API module to depend on e.g. picocli..?)
I'm thinking we could do some kind of separation into "entities" and "DTOs", where the types used by the API would be the "DTOs", i.e. non-annotated classes, and the CLI has it's annotated "entity" types, with a mapping between them. However, that feels a bit too "heavy" in this case, so I'm not sure it's the way to go.

[lorenzleutgeb]

There are many ways to decouple that. You could for example have CliSystemConfig extends SystemConfig or something like static SystemConfig map(CliSystemConfig config) or some other subtype of SystemConfig that delegates to an object populated by command line argument parsing.

[lorenzleutgeb]

I just had to look up the options for Z3. Wanted to post it here so you get a feel of how they structure their parameters:

Z3 options

Global parameters
    auto_config (bool) (default: true)
    debug_ref_count (bool) (default: false)
    dot_proof_file (string) (default: proof.dot)
    dump_models (bool) (default: false)
    memory_high_watermark (unsigned int) (default: 0)
    memory_max_alloc_count (unsigned int) (default: 0)
    memory_max_size (unsigned int) (default: 0)
    model (bool) (default: true)
    model_validate (bool) (default: false)
    proof (bool) (default: false)
    rlimit (unsigned int) (default: 0)
    smtlib2_compliant (bool) (default: false)
    stats (bool) (default: false)
    timeout (unsigned int) (default: 4294967295)
    trace (bool) (default: false)
    trace_file_name (string) (default: z3.log)
    type_check (bool) (default: true)
    unsat_core (bool) (default: false)
    verbose (unsigned int) (default: 0)
    warning (bool) (default: true)
    well_sorted_check (bool) (default: false)

To set a module parameter, use <module-name>.<parameter-name>=value
Example:  pp.decimal=true

[module] pi, description: pattern inference (heuristics) for universal formulas (without annotation)
    arith (unsigned int) (default: 1)
    arith_weight (unsigned int) (default: 5)
    block_loop_patterns (bool) (default: true)
    max_multi_patterns (unsigned int) (default: 0)
    non_nested_arith_weight (unsigned int) (default: 10)
    pull_quantifiers (bool) (default: true)
    use_database (bool) (default: false)
    warnings (bool) (default: false)
[module] tactic, description: tactic parameters
    blast_term_ite.max_inflation (unsigned int) (default: 4294967295)
    blast_term_ite.max_steps (unsigned int) (default: 4294967295)
    default_tactic (symbol) (default: )
    propagate_values.max_rounds (unsigned int) (default: 4)
    solve_eqs.context_solve (bool) (default: true)
    solve_eqs.ite_solver (bool) (default: true)
    solve_eqs.max_occs (unsigned int) (default: 4294967295)
    solve_eqs.theory_solver (bool) (default: true)
[module] pp, description: pretty printer
    bounded (bool) (default: false)
    bv_literals (bool) (default: true)
    bv_neg (bool) (default: false)
    decimal (bool) (default: false)
    decimal_precision (unsigned int) (default: 10)
    fixed_indent (bool) (default: false)
    flat_assoc (bool) (default: true)
    fp_real_literals (bool) (default: false)
    max_depth (unsigned int) (default: 5)
    max_indent (unsigned int) (default: 4294967295)
    max_num_lines (unsigned int) (default: 4294967295)
    max_ribbon (unsigned int) (default: 80)
    max_width (unsigned int) (default: 80)
    min_alias_size (unsigned int) (default: 10)
    pretty_proof (bool) (default: false)
    simplify_implies (bool) (default: true)
    single_line (bool) (default: false)
[module] sat, description: propositional SAT solver
    abce (bool) (default: false)
    acce (bool) (default: false)
    asymm_branch (bool) (default: true)
    asymm_branch.all (bool) (default: false)
    asymm_branch.delay (unsigned int) (default: 1)
    asymm_branch.limit (unsigned int) (default: 100000000)
    asymm_branch.rounds (unsigned int) (default: 2)
    asymm_branch.sampled (bool) (default: true)
    ate (bool) (default: true)
    backtrack.conflicts (unsigned int) (default: 4000)
    backtrack.scopes (unsigned int) (default: 100)
    bca (bool) (default: false)
    bce (bool) (default: false)
    bce_at (unsigned int) (default: 2)
    bce_delay (unsigned int) (default: 2)
    binspr (bool) (default: false)
    blocked_clause_limit (unsigned int) (default: 100000000)
    branching.anti_exploration (bool) (default: false)
    branching.heuristic (symbol) (default: vsids)
    burst_search (unsigned int) (default: 100)
    cardinality.encoding (symbol) (default: grouped)
    cardinality.solver (bool) (default: true)
    cce (bool) (default: false)
    core.minimize (bool) (default: false)
    core.minimize_partial (bool) (default: false)
    ddfw.init_clause_weight (unsigned int) (default: 8)
    ddfw.reinit_base (unsigned int) (default: 10000)
    ddfw.restart_base (unsigned int) (default: 100000)
    ddfw.threads (unsigned int) (default: 0)
    ddfw.use_reward_pct (unsigned int) (default: 15)
    ddfw_search (bool) (default: false)
    dimacs.core (bool) (default: false)
    drat.activity (bool) (default: false)
    drat.binary (bool) (default: false)
    drat.check_sat (bool) (default: false)
    drat.check_unsat (bool) (default: false)
    drat.file (symbol) (default: )
    dyn_sub_res (bool) (default: true)
    elim_vars (bool) (default: true)
    elim_vars_bdd (bool) (default: true)
    elim_vars_bdd_delay (unsigned int) (default: 3)
    force_cleanup (bool) (default: false)
    gc (symbol) (default: glue_psm)
    gc.burst (bool) (default: false)
    gc.defrag (bool) (default: true)
    gc.increment (unsigned int) (default: 500)
    gc.initial (unsigned int) (default: 20000)
    gc.k (unsigned int) (default: 7)
    gc.small_lbd (unsigned int) (default: 3)
    inprocess.max (unsigned int) (default: 4294967295)
    local_search (bool) (default: false)
    local_search_dbg_flips (bool) (default: false)
    local_search_mode (symbol) (default: wsat)
    local_search_threads (unsigned int) (default: 0)
    lookahead.cube.cutoff (symbol) (default: depth)
    lookahead.cube.depth (unsigned int) (default: 1)
    lookahead.cube.fraction (double) (default: 0.4)
    lookahead.cube.freevars (double) (default: 0.8)
    lookahead.cube.psat.clause_base (double) (default: 2)
    lookahead.cube.psat.trigger (double) (default: 5)
    lookahead.cube.psat.var_exp (double) (default: 1)
    lookahead.delta_fraction (double) (default: 1.0)
    lookahead.double (bool) (default: true)
    lookahead.global_autarky (bool) (default: false)
    lookahead.preselect (bool) (default: false)
    lookahead.reward (symbol) (default: march_cu)
    lookahead.use_learned (bool) (default: false)
    lookahead_scores (bool) (default: false)
    lookahead_simplify (bool) (default: false)
    lookahead_simplify.bca (bool) (default: true)
    max_conflicts (unsigned int) (default: 4294967295)
    max_memory (unsigned int) (default: 4294967295)
    minimize_lemmas (bool) (default: true)
    override_incremental (bool) (default: false)
    pb.lemma_format (symbol) (default: cardinality)
    pb.min_arity (unsigned int) (default: 9)
    pb.resolve (symbol) (default: cardinality)
    pb.solver (symbol) (default: solver)
    phase (symbol) (default: caching)
    phase.sticky (bool) (default: true)
    prob_search (bool) (default: false)
    probing (bool) (default: true)
    probing_binary (bool) (default: true)
    probing_cache (bool) (default: true)
    probing_cache_limit (unsigned int) (default: 1024)
    probing_limit (unsigned int) (default: 5000000)
    propagate.prefetch (bool) (default: true)
    random_freq (double) (default: 0.01)
    random_seed (unsigned int) (default: 0)
    reorder.activity_scale (unsigned int) (default: 100)
    reorder.base (unsigned int) (default: 4294967295)
    reorder.itau (double) (default: 4.0)
    rephase.base (unsigned int) (default: 1000)
    resolution.cls_cutoff1 (unsigned int) (default: 100000000)
    resolution.cls_cutoff2 (unsigned int) (default: 700000000)
    resolution.limit (unsigned int) (default: 500000000)
    resolution.lit_cutoff_range1 (unsigned int) (default: 700)
    resolution.lit_cutoff_range2 (unsigned int) (default: 400)
    resolution.lit_cutoff_range3 (unsigned int) (default: 300)
    resolution.occ_cutoff (unsigned int) (default: 10)
    resolution.occ_cutoff_range1 (unsigned int) (default: 8)
    resolution.occ_cutoff_range2 (unsigned int) (default: 5)
    resolution.occ_cutoff_range3 (unsigned int) (default: 3)
    restart (symbol) (default: ema)
    restart.emafastglue (double) (default: 0.03)
    restart.emaslowglue (double) (default: 1e-05)
    restart.factor (double) (default: 1.5)
    restart.fast (bool) (default: true)
    restart.initial (unsigned int) (default: 2)
    restart.margin (double) (default: 1.1)
    restart.max (unsigned int) (default: 4294967295)
    retain_blocked_clauses (bool) (default: true)
    scc (bool) (default: true)
    scc.tr (bool) (default: true)
    search.sat.conflicts (unsigned int) (default: 400)
    search.unsat.conflicts (unsigned int) (default: 400)
    simplify.delay (unsigned int) (default: 0)
    subsumption (bool) (default: true)
    subsumption.limit (unsigned int) (default: 100000000)
    threads (unsigned int) (default: 1)
    unit_walk (bool) (default: false)
    unit_walk_threads (unsigned int) (default: 0)
    variable_decay (unsigned int) (default: 110)
    xor.solver (bool) (default: false)
[module] model
    compact (bool) (default: true)
    completion (bool) (default: false)
    inline_def (bool) (default: false)
    partial (bool) (default: false)
    v1 (bool) (default: false)
    v2 (bool) (default: false)
[module] solver, description: solver parameters
    cancel_backup_file (symbol) (default: )
    enforce_model_conversion (bool) (default: false)
    smtlib2_log (symbol) (default: )
    timeout (unsigned int) (default: 4294967295)
[module] opt, description: optimization parameters
    dump_benchmarks (bool) (default: false)
    dump_models (bool) (default: false)
    elim_01 (bool) (default: true)
    enable_sat (bool) (default: true)
    enable_sls (bool) (default: false)
    maxlex.enable (bool) (default: true)
    maxres.add_upper_bound_block (bool) (default: false)
    maxres.hill_climb (bool) (default: true)
    maxres.max_core_size (unsigned int) (default: 3)
    maxres.max_correction_set_size (unsigned int) (default: 3)
    maxres.max_num_cores (unsigned int) (default: 4294967295)
    maxres.maximize_assignment (bool) (default: false)
    maxres.pivot_on_correction_set (bool) (default: true)
    maxres.wmax (bool) (default: false)
    maxsat_engine (symbol) (default: maxres)
    optsmt_engine (symbol) (default: basic)
    pb.compile_equality (bool) (default: false)
    pp.neat (bool) (default: true)
    priority (symbol) (default: lex)
    rlimit (unsigned int) (default: 0)
    solution_prefix (symbol) (default: )
    timeout (unsigned int) (default: 4294967295)
[module] parallel, description: parameters for parallel solver
    conquer.backtrack_frequency (unsigned int) (default: 10)
    conquer.batch_size (unsigned int) (default: 100)
    conquer.delay (unsigned int) (default: 10)
    conquer.restart.max (unsigned int) (default: 5)
    enable (bool) (default: false)
    simplify.exp (double) (default: 1)
    simplify.inprocess.max (unsigned int) (default: 2)
    simplify.max_conflicts (unsigned int) (default: 4294967295)
    simplify.restart.max (unsigned int) (default: 5000)
    threads.max (unsigned int) (default: 10000)
[module] lp
    bprop_on_pivoted_rows (bool) (default: true)
    enable_hnf (bool) (default: true)
    min (bool) (default: false)
    print_stats (bool) (default: false)
    rep_freq (unsigned int) (default: 0)
    simplex_strategy (unsigned int) (default: 0)
[module] nnf, description: negation normal form
    ignore_labels (bool) (default: false)
    max_memory (unsigned int) (default: 4294967295)
    mode (symbol) (default: skolem)
    sk_hack (bool) (default: false)
[module] algebraic, description: real algebraic number package
    factor (bool) (default: true)
    factor_max_prime (unsigned int) (default: 31)
    factor_num_primes (unsigned int) (default: 1)
    factor_search_size (unsigned int) (default: 5000)
    min_mag (unsigned int) (default: 16)
    zero_accuracy (unsigned int) (default: 0)
[module] combined_solver, description: combines two solvers: non-incremental (solver1) and incremental (solver2)
    ignore_solver1 (bool) (default: false)
    solver2_timeout (unsigned int) (default: 4294967295)
    solver2_unknown (unsigned int) (default: 1)
[module] rcf, description: real closed fields
    clean_denominators (bool) (default: true)
    inf_precision (unsigned int) (default: 24)
    initial_precision (unsigned int) (default: 24)
    lazy_algebraic_normalization (bool) (default: true)
    max_precision (unsigned int) (default: 128)
    use_prem (bool) (default: true)
[module] model_evaluator
    array_as_stores (bool) (default: true)
    array_equalities (bool) (default: true)
    completion (bool) (default: false)
    max_memory (unsigned int) (default: 4294967295)
    max_steps (unsigned int) (default: 4294967295)
[module] ackermannization, description: tactics based on solving UF-theories via ackermannization (see also ackr module)
    eager (bool) (default: true)
    inc_sat_backend (bool) (default: false)
    sat_backend (bool) (default: false)
[module] nlsat, description: nonlinear solver
    check_lemmas (bool) (default: false)
    factor (bool) (default: true)
    inline_vars (bool) (default: false)
    lazy (unsigned int) (default: 0)
    log_lemmas (bool) (default: false)
    max_conflicts (unsigned int) (default: 4294967295)
    max_memory (unsigned int) (default: 4294967295)
    minimize_conflicts (bool) (default: false)
    randomize (bool) (default: true)
    reorder (bool) (default: true)
    seed (unsigned int) (default: 0)
    shuffle_vars (bool) (default: false)
    simplify_conflicts (bool) (default: true)
[module] parser
    error_for_visual_studio (bool) (default: false)
    ignore_bad_patterns (bool) (default: true)
    ignore_user_patterns (bool) (default: false)
[module] rewriter, description: new formula simplification module used in the tactic framework, and new solvers
    algebraic_number_evaluator (bool) (default: true)
    arith_ineq_lhs (bool) (default: false)
    arith_lhs (bool) (default: false)
    bit2bool (bool) (default: true)
    blast_distinct (bool) (default: false)
    blast_distinct_threshold (unsigned int) (default: 4294967295)
    blast_eq_value (bool) (default: false)
    bv_extract_prop (bool) (default: false)
    bv_ineq_consistency_test_max (unsigned int) (default: 0)
    bv_ite2id (bool) (default: false)
    bv_le_extra (bool) (default: false)
    bv_not_simpl (bool) (default: false)
    bv_sort_ac (bool) (default: false)
    bv_trailing (bool) (default: false)
    bv_urem_simpl (bool) (default: false)
    bvnot2arith (bool) (default: false)
    cache_all (bool) (default: false)
    div0_ackermann_limit (unsigned int) (default: 1000)
    elim_and (bool) (default: false)
    elim_ite (bool) (default: true)
    elim_rem (bool) (default: false)
    elim_sign_ext (bool) (default: true)
    elim_to_real (bool) (default: false)
    eq2ineq (bool) (default: false)
    expand_nested_stores (bool) (default: false)
    expand_power (bool) (default: false)
    expand_select_store (bool) (default: false)
    expand_store_eq (bool) (default: false)
    expand_tan (bool) (default: false)
    flat (bool) (default: true)
    gcd_rounding (bool) (default: false)
    hi_div0 (bool) (default: true)
    hi_fp_unspecified (bool) (default: false)
    hoist_cmul (bool) (default: false)
    hoist_ite (bool) (default: false)
    hoist_mul (bool) (default: false)
    ignore_patterns_on_ground_qbody (bool) (default: true)
    ite_extra_rules (bool) (default: false)
    local_ctx (bool) (default: false)
    local_ctx_limit (unsigned int) (default: 4294967295)
    max_degree (unsigned int) (default: 64)
    max_memory (unsigned int) (default: 4294967295)
    max_steps (unsigned int) (default: 4294967295)
    mul2concat (bool) (default: false)
    mul_to_power (bool) (default: false)
    pull_cheap_ite (bool) (default: false)
    push_ite_arith (bool) (default: false)
    push_ite_bv (bool) (default: false)
    push_to_real (bool) (default: true)
    rewrite_patterns (bool) (default: false)
    som (bool) (default: false)
    som_blowup (unsigned int) (default: 10)
    sort_store (bool) (default: false)
    sort_sums (bool) (default: false)
    split_concat_eq (bool) (default: false)
    udiv2mul (bool) (default: false)
[module] fp, description: fixedpoint parameters
    bmc.linear_unrolling_depth (unsigned int) (default: 4294967295)
    datalog.all_or_nothing_deltas (bool) (default: false)
    datalog.check_relation (symbol) (default: null)
    datalog.compile_with_widening (bool) (default: false)
    datalog.dbg_fpr_nonempty_relation_signature (bool) (default: false)
    datalog.default_relation (symbol) (default: pentagon)
    datalog.default_table (symbol) (default: sparse)
    datalog.default_table_checked (bool) (default: false)
    datalog.default_table_checker (symbol) (default: null)
    datalog.explanations_on_relation_level (bool) (default: false)
    datalog.generate_explanations (bool) (default: false)
    datalog.initial_restart_timeout (unsigned int) (default: 0)
    datalog.magic_sets_for_queries (bool) (default: false)
    datalog.output_profile (bool) (default: false)
    datalog.print.tuples (bool) (default: true)
    datalog.profile_timeout_milliseconds (unsigned int) (default: 0)
    datalog.similarity_compressor (bool) (default: true)
    datalog.similarity_compressor_threshold (unsigned int) (default: 11)
    datalog.subsumption (bool) (default: true)
    datalog.timeout (unsigned int) (default: 0)
    datalog.unbound_compressor (bool) (default: true)
    datalog.use_map_names (bool) (default: true)
    engine (symbol) (default: auto-config)
    generate_proof_trace (bool) (default: false)
    print_aig (symbol) (default: )
    print_answer (bool) (default: false)
    print_boogie_certificate (bool) (default: false)
    print_certificate (bool) (default: false)
    print_fixedpoint_extensions (bool) (default: true)
    print_low_level_smt2 (bool) (default: false)
    print_statistics (bool) (default: false)
    print_with_variable_declarations (bool) (default: true)
    spacer.blast_term_ite_inflation (unsigned int) (default: 3)
    spacer.ctp (bool) (default: true)
    spacer.dump_benchmarks (bool) (default: false)
    spacer.dump_threshold (double) (default: 5.0)
    spacer.elim_aux (bool) (default: true)
    spacer.eq_prop (bool) (default: true)
    spacer.gpdr (bool) (default: false)
    spacer.gpdr.bfs (bool) (default: true)
    spacer.ground_pobs (bool) (default: true)
    spacer.iuc (unsigned int) (default: 1)
    spacer.iuc.arith (unsigned int) (default: 1)
    spacer.iuc.debug_proof (bool) (default: false)
    spacer.iuc.old_hyp_reducer (bool) (default: false)
    spacer.iuc.print_farkas_stats (bool) (default: false)
    spacer.iuc.split_farkas_literals (bool) (default: false)
    spacer.keep_proxy (bool) (default: true)
    spacer.max_level (unsigned int) (default: 4294967295)
    spacer.max_num_contexts (unsigned int) (default: 500)
    spacer.mbqi (bool) (default: true)
    spacer.min_level (unsigned int) (default: 0)
    spacer.native_mbp (bool) (default: true)
    spacer.order_children (unsigned int) (default: 0)
    spacer.p3.share_invariants (bool) (default: false)
    spacer.p3.share_lemmas (bool) (default: false)
    spacer.print_json (symbol) (default: )
    spacer.propagate (bool) (default: true)
    spacer.push_pob (bool) (default: false)
    spacer.push_pob_max_depth (unsigned int) (default: 4294967295)
    spacer.q3 (bool) (default: true)
    spacer.q3.instantiate (bool) (default: true)
    spacer.q3.qgen.normalize (bool) (default: true)
    spacer.q3.use_qgen (bool) (default: false)
    spacer.random_seed (unsigned int) (default: 0)
    spacer.reach_dnf (bool) (default: true)
    spacer.reset_pob_queue (bool) (default: true)
    spacer.restart_initial_threshold (unsigned int) (default: 10)
    spacer.restarts (bool) (default: false)
    spacer.simplify_lemmas_post (bool) (default: false)
    spacer.simplify_lemmas_pre (bool) (default: false)
    spacer.simplify_pob (bool) (default: false)
    spacer.use_array_eq_generalizer (bool) (default: true)
    spacer.use_bg_invs (bool) (default: false)
    spacer.use_derivations (bool) (default: true)
    spacer.use_euf_gen (bool) (default: false)
    spacer.use_inc_clause (bool) (default: true)
    spacer.use_inductive_generalizer (bool) (default: true)
    spacer.use_lemma_as_cti (bool) (default: false)
    spacer.use_lim_num_gen (bool) (default: false)
    spacer.validate_lemmas (bool) (default: false)
    spacer.weak_abs (bool) (default: true)
    tab.selection (symbol) (default: weight)
    validate (bool) (default: false)
    xform.array_blast (bool) (default: false)
    xform.array_blast_full (bool) (default: false)
    xform.bit_blast (bool) (default: false)
    xform.coalesce_rules (bool) (default: false)
    xform.coi (bool) (default: true)
    xform.compress_unbound (bool) (default: true)
    xform.elim_term_ite (bool) (default: false)
    xform.elim_term_ite.inflation (unsigned int) (default: 3)
    xform.fix_unbound_vars (bool) (default: false)
    xform.inline_eager (bool) (default: true)
    xform.inline_linear (bool) (default: true)
    xform.inline_linear_branch (bool) (default: false)
    xform.instantiate_arrays (bool) (default: false)
    xform.instantiate_arrays.enforce (bool) (default: false)
    xform.instantiate_arrays.nb_quantifier (unsigned int) (default: 1)
    xform.instantiate_arrays.slice_technique (symbol) (default: no-slicing)
    xform.instantiate_quantifiers (bool) (default: false)
    xform.karr (bool) (default: false)
    xform.magic (bool) (default: false)
    xform.quantify_arrays (bool) (default: false)
    xform.scale (bool) (default: false)
    xform.slice (bool) (default: true)
    xform.subsumption_checker (bool) (default: true)
    xform.tail_simplifier_pve (bool) (default: true)
    xform.transform_arrays (bool) (default: false)
    xform.unfold_rules (unsigned int) (default: 0)
[module] smt, description: smt solver based on lazy smt
    arith.auto_config_simplex (bool) (default: false)
    arith.branch_cut_ratio (unsigned int) (default: 2)
    arith.dump_lemmas (bool) (default: false)
    arith.eager_eq_axioms (bool) (default: true)
    arith.euclidean_solver (bool) (default: false)
    arith.greatest_error_pivot (bool) (default: false)
    arith.ignore_int (bool) (default: false)
    arith.int_eq_branch (bool) (default: false)
    arith.nl (bool) (default: true)
    arith.nl.branching (bool) (default: true)
    arith.nl.gb (bool) (default: true)
    arith.nl.rounds (unsigned int) (default: 1024)
    arith.propagate_eqs (bool) (default: true)
    arith.propagation_mode (unsigned int) (default: 2)
    arith.random_initial_value (bool) (default: false)
    arith.reflect (bool) (default: true)
    arith.solver (unsigned int) (default: 2)
    array.extensional (bool) (default: true)
    array.weak (bool) (default: false)
    auto_config (bool) (default: true)
    bv.enable_int2bv (bool) (default: true)
    bv.reflect (bool) (default: true)
    case_split (unsigned int) (default: 1)
    clause_proof (bool) (default: false)
    core.extend_nonlocal_patterns (bool) (default: false)
    core.extend_patterns (bool) (default: false)
    core.extend_patterns.max_distance (unsigned int) (default: 4294967295)
    core.minimize (bool) (default: false)
    core.validate (bool) (default: false)
    dack (unsigned int) (default: 1)
    dack.eq (bool) (default: false)
    dack.factor (double) (default: 0.1)
    dack.gc (unsigned int) (default: 2000)
    dack.gc_inv_decay (double) (default: 0.8)
    dack.threshold (unsigned int) (default: 10)
    delay_units (bool) (default: false)
    delay_units_threshold (unsigned int) (default: 32)
    dt_lazy_splits (unsigned int) (default: 1)
    ematching (bool) (default: true)
    lemma_gc_strategy (unsigned int) (default: 0)
    logic (symbol) (default: )
    macro_finder (bool) (default: false)
    max_conflicts (unsigned int) (default: 4294967295)
    mbqi (bool) (default: true)
    mbqi.force_template (unsigned int) (default: 10)
    mbqi.id (string) (default: )
    mbqi.max_cexs (unsigned int) (default: 1)
    mbqi.max_cexs_incr (unsigned int) (default: 0)
    mbqi.max_iterations (unsigned int) (default: 1000)
    mbqi.trace (bool) (default: false)
    pb.conflict_frequency (unsigned int) (default: 1000)
    pb.learn_complements (bool) (default: true)
    phase_selection (unsigned int) (default: 3)
    pull_nested_quantifiers (bool) (default: false)
    qi.cost (string) (default: (+ weight generation))
    qi.eager_threshold (double) (default: 10.0)
    qi.lazy_threshold (double) (default: 20.0)
    qi.max_instances (unsigned int) (default: 4294967295)
    qi.max_multi_patterns (unsigned int) (default: 0)
    qi.profile (bool) (default: false)
    qi.profile_freq (unsigned int) (default: 4294967295)
    qi.quick_checker (unsigned int) (default: 0)
    quasi_macros (bool) (default: false)
    random_seed (unsigned int) (default: 0)
    recfun.depth (unsigned int) (default: 2)
    recfun.native (bool) (default: true)
    refine_inj_axioms (bool) (default: true)
    relevancy (unsigned int) (default: 2)
    restart.max (unsigned int) (default: 4294967295)
    restart_factor (double) (default: 1.1)
    restart_strategy (unsigned int) (default: 1)
    restricted_quasi_macros (bool) (default: false)
    seq.split_w_len (bool) (default: true)
    str.aggressive_length_testing (bool) (default: false)
    str.aggressive_unroll_testing (bool) (default: true)
    str.aggressive_value_testing (bool) (default: false)
    str.binary_search_start (unsigned int) (default: 64)
    str.fast_length_tester_cache (bool) (default: false)
    str.fast_value_tester_cache (bool) (default: true)
    str.finite_overlap_models (bool) (default: false)
    str.overlap_priority (double) (default: -0.1)
    str.regex_automata (bool) (default: true)
    str.regex_automata_difficulty_threshold (unsigned int) (default: 1000)
    str.regex_automata_failed_automaton_threshold (unsigned int) (default: 10)
    str.regex_automata_failed_intersection_threshold (unsigned int) (default: 10)
    str.regex_automata_intersection_difficulty_threshold (unsigned int) (default: 1000)
    str.regex_automata_length_attempt_threshold (unsigned int) (default: 10)
    str.string_constant_cache (bool) (default: true)
    str.strong_arrangements (bool) (default: true)
    str.use_binary_search (bool) (default: false)
    string_solver (symbol) (default: seq)
    theory_aware_branching (bool) (default: false)
    theory_case_split (bool) (default: false)
[module] sls, description: Experimental Stochastic Local Search Solver (for QFBV only).
    early_prune (bool) (default: true)
    max_memory (unsigned int) (default: 4294967295)
    max_restarts (unsigned int) (default: 4294967295)
    paws_init (unsigned int) (default: 40)
    paws_sp (unsigned int) (default: 52)
    random_offset (bool) (default: true)
    random_seed (unsigned int) (default: 0)
    rescore (bool) (default: true)
    restart_base (unsigned int) (default: 100)
    restart_init (bool) (default: false)
    scale_unsat (double) (default: 0.5)
    track_unsat (bool) (default: false)
    vns_mc (unsigned int) (default: 0)
    vns_repick (bool) (default: false)
    walksat (bool) (default: true)
    walksat_repick (bool) (default: true)
    walksat_ucb (bool) (default: true)
    walksat_ucb_constant (double) (default: 20.0)
    walksat_ucb_forget (double) (default: 1.0)
    walksat_ucb_init (bool) (default: false)
    walksat_ucb_noise (double) (default: 0.0002)
    wp (unsigned int) (default: 100)

[lorenzleutgeb]

Another note: I used Picocli for ATLAS, which can be compiled to an x86_64 ELF binary via GraalVM Native Image. Since native images would also be interesting for Alpha, I'd like to recommend Picocli.