CLI Refactoring - Githubissues

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= : Set default configuration [auto] : {auto|frumpy|jumpy|tweety|handy|crafty|trendy|many|} 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) : Use configuration file to configure solver(s) --tester= : Pass (quoted) string of to tester --stats[=[,]],-s : Enable {1=basic|2=full} statistics ( for tester) --[no-]parse-ext : Enable extensions in non-aspif input --[no-]parse-maxsat : Treat dimacs input as MaxSAT problem Clasp.Context Options: --share=|no : Configure physical sharing of constraints [auto] : {auto|problem|learnt|all} --learn-explicit : Do not use Short Implication Graph for learning --sat-prepro[=|no] : Run SatELite-like preprocessing (Implicit: 2) : [,...] : Set preprocessing level to 1: Variable elimination with subsumption (VE) 2: VE with limited blocked clause elimination (BCE) 3: Full BCE followed by VE : [=] (0=no limit) iter : Set iteration limit to [0] occ : Set variable occurrence limit to [0] time : Set time limit to seconds [0] frozen: Set frozen variables limit to % [0] size : Set size limit to *1000 clauses [4000] Clasp.ASP Options: --trans-ext=|no : Configure handling of extended rules : {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= : Configure equivalence preprocessing Run for at most 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=[,] : Stop search after conflicts or restarts --parallel-mode,-t : Run parallel search with given number of threads : [,] : Number of threads to use in search : Run competition or splitting based search [compete] --global-restarts= : Configure global restart policy : [,] : Maximal number of global restarts (0=disable) : Restart schedule [x,100,1.5] () --distribute=|no : Configure nogood distribution [conflict,global,4] : [,][,][,] : Distribute {all|short|conflict|loop} nogoods : Use {global|local} distribution [global] : Distribute only if LBD <= [4] : Distribute only if size <= [-1] --integrate= : Configure nogood integration [gp] : [,][,] : Add {all|unsat|gp(unsat wrt guiding path)|active} nogoods : Always keep at least last integrated nogoods [1024] : Accept nogoods from {all|ring|cube|cubex} peers [all] --enum-mode,-e : Configure enumeration algorithm [auto] : {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[=|no] : Enable projective solution enumeration : {show|project|auto}[,] (Implicit: auto,3) Project to atoms in show or project directives, or select depending on the existence of a project directive : 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 : Compute at most models (0 for all) --opt-mode= : Configure optimization algorithm : [,...] opt : Find optimal model enum : Find models with costs <= optN : Find optimum, then enumerate optimal models ignore: Ignore optimize statements : Set initial bound for objective function(s) Clasp.Search Options: --opt-strategy= : Configure optimization strategy : {bb|usc}[,] bb : Model-guided optimization with [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 : [,] : Relaxation algorithm {oll|one|k|pmres} [oll] oll : Use strategy from unclasp one : Add one cardinality constraint per core k[,]: Add cardinality constraints of bounded size ([0]=dynamic) pmres : Add clauses of size 3 : Tactics | disjoint: Disjoint-core preprocessing (1) succinct: No redundant (symmetry) constraints (2) stratify: Stratification heuristic for handling weights (4) --opt-usc-shrink= : Enable core-shrinking in core-guided optimization : [, (0=no limit)] : 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 solve calls to 2^ conflicts [10] --opt-heuristic= : Use opt. in heuristics --[no-]restart-on-model : Restart after each model --lookahead[=|no] : Configure failed-literal detection (fld) : [,] / Implicit: atom : Run fld via {atom|body|hybrid} lookahead : Disable fld after applications ([0]=no limit) --lookahead=atom is default if --no-lookback is used --heuristic= : Configure decision heuristic : {Berkmin|Vmtf|Vsids|Domain|Unit|None}[,] Berkmin: Use BerkMin-like heuristic (Check last nogoods [0]=all) Vmtf : Use Siege-like heuristic (Move literals to the front [8]) Vsids : Use Chaff-like heuristic (Use 1.0/0. 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= : Resolution score {auto|min|set|multiset} --score-other= : Score other learnt nogoods: {auto|no|loop|all} --sign-def= : 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= : Enable dynamic decaying scheme in Vsids/Domain : [,][,]|(0=disable) : Set initial decay factor to 1.0/0. : Set decay update to /100.0 [1] : Decrease decay every conflicts [5000] --[no-]nant : Prefer negative antecedents of P in heuristic --dom-mod= : Default modification for domain heuristic : (no|[,]) : Modifier {level|pos|true|neg|false|init|factor} : Apply to (all | ) atoms --save-progress[=] : Use RSat-like progress saving on backjumps > --init-watches= : Watched literal initialization: {rnd|first|least} --update-mode= : Process messages on {propagate|conflict} --acyc-prop[={0..1}] : Use backward inference in acyc propagation --seed= : Set random number generator's seed to --partial-check[=] : Configure partial stability tests :
[,] / Implicit: 50
: Partial check skip percentage : Init/update value for high bound ([0]=umax) --sign-def-disj= : Default sign for atoms in disjunctions --rand-freq=
|no : Make random decisions with probability
--rand-prob=[,] : Do random searches with [=100] conflicts Clasp.Lookback Options: --no-lookback : Disable all lookback strategies --forget-on-step= : Configure forgetting on (incremental) step : | --strengthen=|no : Use MiniSAT-like conflict nogood strengthening : [,][,] : Use {local|recursive} self-subsumption check : Follow {all|short|binary} antecedents [all] : Bump activities of antecedents [yes] --otfs[={0..2}] : Enable {1=partial|2=full} on-the-fly subsumption --update-lbd=|no : Configure LBD updates during conflict resolution : [,] 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 : Protect updated nogoods on next reduce if X <= --update-act : Enable LBD-based activity bumping --reverse-arcs[={0..3}] : Enable ManySAT-like inverse-arc learning --contraction=|no : Configure handling of long learnt nogoods : [,] : Contract nogoods if size > (0=disable) : Nogood replacement {no|decisionSeq|allUIP|dynamic} [no] --loops= : Configure learning of loop nogoods : {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 |no: Configure restart policy : ,[,][,] F, : Run fixed sequence of conflicts L, : Run Luby et al.'s sequence with unit length x,,: Run geometric seq. of *(^i) conflicts ( >= 1.0) +,,: Run arithmetic seq. of +(*i) conflicts () ...,: Repeat seq. every +j restarts ( != F) D,,: Restart based on moving LBD average over last conflicts Mavg(,LBD)* > avg(LBD) use conflict level average if > 0 and avg(LBD) > no|0 : Disable restarts --reset-restarts= : Update restart seq. on model {no|repeat|disable} --[no-]local-restarts : Use Ryvchin et al.'s local restarts --counter-restarts=: Use counter implication restarts : ([,] | {0|no}) : Interval in number of restarts : Bump factor applied to indegrees --block-restarts= : Use glucose-style blocking restarts : [,][,] : Window size for moving average (0=disable blocking) : Block restart if assignment > average * [1.4] : Disable blocking for the first conflicts [10000] --shuffle=,|no : Shuffle problem after +(*i) restarts --deletion,-d |no : Configure deletion algorithm [basic,75,0] : [,][,] : Use {basic|sort|ipSort|ipHeap} algorithm : Delete at most % of nogoods on reduction [75] : Use {activity|lbd|mixed} nogood scores [activity] no : Disable nogood deletion --del-grow=|no : Configure size-based deletion policy : [,][,] ( >= 1.0) : Keep at most T = X*(^i) learnt nogoods with X being the initial limit and i the number of times fired : Stop growth once T > P* (0=no limit) [3.0] : Set grow schedule () [grow on restart] --del-cfl=|no : Configure conflict-based deletion policy : ,... (see restarts) --del-init= : Configure initial deletion limit : [,,] ( > 0) : Set initial limit to P=estimated problem size/ [3.0] ,: Clamp initial limit to the range [,+] --del-estimate[=0..3] : Use estimated problem complexity in limits --del-max=,|no : Keep at most learnt nogoods taking up to MB --del-glue= : Configure glue clause handling : [,] : Do not delete nogoods with LBD <= : Count (0) or ignore (1) glue clauses in size limit [0] --del-on-restart= : Delete % of learnt nogoods on each restart Gringo Options: --text : Print plain text format --const,-c = : Replace term occurrences of with --output,-o : 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= : 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 : 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[=],-h : Print {1=basic|2=more|3=full} help and exit --version,-v : Print version information and exit --verbose[=],-V : Set verbosity level to --time-limit= : Set time limit to seconds (0=no limit) --fast-exit : Force fast exit (do not call dtors) --print-portfolio : Print default portfolio and exit --quiet[=],-q : Configure printing of models, costs, and calls : [,][,] : print {0=all|1=last|2=no} models : print {0=all|1=last|2=no} optimize values [] : print {0=all|1=last|2=no} call steps [2] --pre[=] : Print simplified program and exit : Set output format to {aspif|smodels} (implicit: aspif) --outf= : Use {0=default|1=competition|2=JSON|3=no} output --out-atomf= : Set atom format string (
?%0?) --out-ifs= : Set internal field separator --out-hide-aux : Hide auxiliary atoms in answers --lemma-in= : Read additional lemmas from --lemma-out= : Log learnt lemmas to --lemma-out-lbd= : Only log lemmas with lbd <= --lemma-out-max= : Stop logging after lemmas --lemma-out-dom= : Log lemmas over variables --lemma-out-txt : Log lemmas as ground integrity constraints --hcc-out= : Write non-hcf programs to .#scc --compute= : Force given literal to true --mode= : 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 ```

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 .=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) ```

alpha-asp / Alpha

CLI Refactoring #264

JCommander

picocli

Ideas