def_module_params('opt', 
                  description='optimization parameters',
                  export=True,
                  params=(('optsmt_engine', SYMBOL, 'basic', "select optimization engine: 'basic', 'symba'"),
                          ('maxsat_engine', SYMBOL, 'maxres', "select engine for maxsat: 'core_maxsat', 'wmax', 'maxres', 'pd-maxres'"),
                          ('priority', SYMBOL, 'lex', "select how to priortize objectives: 'lex' (lexicographic), 'pareto', 'box'"),
                          ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                          ('dump_models', BOOL, False, 'display intermediary models to stdout'),
                          ('solution_prefix', SYMBOL, '', "path prefix to dump intermediary, but non-optimal, solutions"),
                          ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                          ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
                          ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsat'),
                          ('enable_lns', BOOL, False, 'enable LNS during weighted maxsat'),
                          ('lns_conflicts', UINT, 1000, 'initial conflict count for LNS search'),
                          ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                          ('elim_01', BOOL, True, 'eliminate 01 variables'),
                          ('pp.neat', BOOL, True, 'use neat (as opposed to less readable, but faster) pretty printer when displaying context'),
                          ('pb.compile_equality', BOOL, False, 'compile arithmetical equalities into pseudo-Boolean equality (instead of two inequalites)'),
                          ('pp.wcnf', BOOL, False, 'print maxsat benchmark into wcnf format'),
                          ('maxlex.enable', BOOL, True, 'enable maxlex heuristic for lexicographic MaxSAT problems'),
                          ('maxres.hill_climb', BOOL, True, 'give preference for large weight cores'),
                          ('maxres.add_upper_bound_block', BOOL, False, 'restict upper bound with constraint'),
                          ('maxres.max_num_cores', UINT, UINT_MAX, 'maximal number of cores per round'),
                          ('maxres.max_core_size', UINT, 3, 'break batch of generated cores if size reaches this number'),
                          ('maxres.maximize_assignment', BOOL, False, 'find an MSS/MCS to improve current assignment'), 
                          ('maxres.max_correction_set_size', UINT, 3, 'allow generating correction set constraints up to maximal size'),
                          ('maxres.wmax', BOOL, False, 'use weighted theory solver to constrain upper bounds'),
                          ('maxres.pivot_on_correction_set', BOOL, True, 'reduce soft constraints if the current correction set is smaller than current core')

                          ))