mirror of
https://github.com/Z3Prover/z3
synced 2026-01-22 10:04:45 +00:00
ccc2a34444
default behavior is conservative: if the body of a recursive function contains uninterpreted variables they are not rewritten. Model evaluation will bind values to uninterpreted variables so the filter should not apply here.
15 lines
1.3 KiB
Text
15 lines
1.3 KiB
Text
def_module_params('rewriter',
|
|
description='new formula simplification module used in the tactic framework, and new solvers',
|
|
export=True,
|
|
params=(max_memory_param(),
|
|
max_steps_param(),
|
|
("push_ite_arith", BOOL, False, "push if-then-else over arithmetic terms."),
|
|
("push_ite_bv", BOOL, False, "push if-then-else over bit-vector terms."),
|
|
("pull_cheap_ite", BOOL, False, "pull if-then-else terms when cheap."),
|
|
("bv_ineq_consistency_test_max", UINT, 0, "max size of conjunctions on which to perform consistency test based on inequalities on bitvectors."),
|
|
("unfold_recursive_functions", BOOL, False, "apply simplification recursively on recursive functions."),
|
|
("cache_all", BOOL, False, "cache all intermediate results."),
|
|
("enable_der", BOOL, True, "enable destructive equality resolution to quantifiers."),
|
|
("rewrite_patterns", BOOL, False, "rewrite patterns."),
|
|
("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))
|
|
|