def_module_params('nlsat',
description='nonlinear solver',
export=True,
params=(max_memory_param(),
('simple_check', BOOL, False, "precheck polynomials using variables sign"),
('variable_ordering_strategy', UINT, 0, "Variable Ordering Strategy, 0 for none, 1 for BROWN, 2 for TRIANGULAR, 3 for ONLYPOLY"),
('lazy', UINT, 0, "how lazy the solver is."),
('reorder', BOOL, True, "reorder variables."),
('log_lemmas', BOOL, False, "display lemmas as self-contained SMT formulas"),
('log_lemma_smtrat', BOOL, False, "log lemmas to be readable by smtrat"),
('dump_mathematica', BOOL, False, "display lemmas as matematica"),
('check_lemmas', BOOL, False, "check lemmas on the fly using an independent nlsat solver"),
('simplify_conflicts', BOOL, True, "simplify conflicts using equalities before resolving them in nlsat solver."),
('minimize_conflicts', BOOL, False, "minimize conflicts"),
('randomize', BOOL, True, "randomize selection of a witness in nlsat."),
('max_conflicts', UINT, UINT_MAX, "maximum number of conflicts."),
('shuffle_vars', BOOL, False, "use a random variable order."),
('inline_vars', BOOL, False, "inline variables that can be isolated from equations (not supported in incremental mode)"),
('seed', UINT, 0, "random seed."),
('factor', BOOL, True, "factor polynomials produced during conflict resolution."),
('add_all_coeffs', BOOL, False, "add all polynomial coefficients during projection."),
('zero_disc', BOOL, False, "add_zero_assumption to the vanishing discriminant."),
('known_sat_assignment_file_name', STRING, "", "the file name of a known solution: used for debugging only"),
('lws', BOOL, True, "apply levelwise."),
('lws_spt_threshold', UINT, 4, "minimum both-side polynomial count to apply spanning tree optimization; < 2 disables spanning tree"),
('lws_witness_subs_lc', BOOL, True, "try substitute the non-nullified witness by the lc"),
('lws_witness_subs_disc', BOOL, True, "try substitute the non-nullified witness by the discriminant"),
('canonicalize', BOOL, True, "canonicalize polynomials.")
))