mirror of
https://github.com/Z3Prover/z3
synced 2025-06-12 17:06:14 +00:00
14 lines
1.2 KiB
Text
14 lines
1.2 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(),
|
|
("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"),
|
|
("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."),
|
|
("cache_all", BOOL, False, "cache all intermediate results."),
|
|
("rewrite_patterns", BOOL, False, "rewrite patterns."),
|
|
("ignore_patterns_on_ground_qbody", BOOL, True, "ignores patterns on quantifiers that don't mention their bound variables.")))
|
|
|