z3-src 501.0.0

Source distribution of the Z3 SMT solver, for use as a build dependency
Documentation
def_module_params(module_name='lp',
                  class_name='lp_params_helper',
                  description='linear programming parameters',
                  export=True,
                  params=(('dio', BOOL, True, 'use Diophantine equalities'),
                          ('dio_branching_period', UINT, 100, 'Period of calling branching on undef in Diophantine handler'),
                          ('dio_cuts_enable_gomory', BOOL, False, 'enable Gomory cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                          ('dio_gomory_enable_period', UINT, 16, 'number of consecutive unproductive (undef) Diophantine-handler calls after which the controller starts running Gomory cuts and the gcd test alongside dio; a dio conflict resets the count and stops them; set very large to never start them this way so Gomory follows dio_cuts_enable_gomory only'),
                          ('dio_cuts_enable_hnf', BOOL, True, 'enable hnf cuts together with Diophantine cuts, only relevant when dioph_eq is true'),
                          ('dio_ignore_big_nums', BOOL, True, 'Ignore the terms with big numbers in the Diophantine handler, only relevant when dioph_eq is true'),
                          ('dio_calls_period', UINT, 1, 'Period of calling the Diophantine handler in the final_check()'),
                          ('dio_calls_period_decrease', UINT, 2, 'Amount by which dio_calls_period is decreased on each final_check() call where the Diophantine handler is not triggered, until it returns to its initial value'),
                          ('dio_run_gcd', BOOL, False, 'Run the GCD heuristic if dio is on, if dio is disabled the option is not used'),
                          ('dio_undo_max_work', UINT, 1000000, 'work budget, in machine words, for eliminating the columns of the retired terms from the certificate matrix of the Diophantine handler; when a scope pop exceeds it the Diophantine state is discarded and rebuilt lazily on the next check instead of being updated incrementally; 0 means no budget'),
                          ('lcube', BOOL, True, 'use the largest cube test for integer feasibility'),
                          ('lcube_flips', UINT, 16, 'maximal number of coordinate flips when repairing the rounded largest cube center, only relevant when lcube is true'),
                          ('int_hammer_period', UINT, 4, 'period (in final_check calls) for the integer cut/cube heuristics (find_cube, hnf, gomory); a smaller value calls them more often'),
                          ('random_hammers', BOOL, True, 'draw the periodic integer heuristic gates (find_cube, lcube, hnf, gomory, dio) at random with the same 1/period rate instead of a deterministic every-k-th-call modulus'),
                         ))