mirror of
https://github.com/Z3Prover/z3
synced 2025-05-11 09:44:43 +00:00
10 lines
1.1 KiB
Text
10 lines
1.1 KiB
Text
def_module_params('rcf',
|
|
description='real closed fields',
|
|
export=True,
|
|
params=(('use_prem', BOOL, True, "use pseudo-remainder instead of remainder when computing GCDs and Sturm-Tarski sequences"),
|
|
('clean_denominators', BOOL, True, "clean denominators before root isolation"),
|
|
('initial_precision', UINT, 24, "a value k that is the initial interval size (as 1/2^k) when creating transcendentals and approximated division"),
|
|
('inf_precision', UINT, 24, "a value k that is the initial interval size (i.e., (0, 1/2^l)) used as an approximation for infinitesimal values"),
|
|
('max_precision', UINT, 128, "during sign determination we switch from interval arithmetic to complete methods when the interval size is less than 1/2^k, where k is the max_precision"),
|
|
('lazy_algebraic_normalization', BOOL, True, "during sturm-seq and square-free polynomial computations, only normalize algebraic polynomial expressions when the definining polynomial is monic")
|
|
))
|