mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

add option for flat_and_or

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-08 12:19:27 -08:00
parent 10fb71cf93
commit 8afec86fe8
1 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/params/bool_rewriter_params.pyg
View file

@ -1,8 +1,9 @@
def_module_params(module_name='rewriter', def_module_params(module_name='rewriter',
class_name='bool_rewriter_params', class_name='bool_rewriter_params',
export=True, export=True,
params=(("ite_extra_rules", BOOL, False, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"), params=(("ite_extra_rules", BOOL, True, "extra ite simplifications, these additional simplifications may reduce size locally but increase globally"),
("flat", BOOL, True, "create nary applications for and,or,+,*,bvadd,bvmul,bvand,bvor,bvxor"), ("flat", BOOL, True, "create nary applications for +,*,bvadd,bvmul,bvand,bvor,bvxor"),
("flat_and_or", BOOL, True, "create nary applications for and,or"),
("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"), ("elim_and", BOOL, False, "conjunctions are rewritten using negation and disjunctions"),
('elim_ite', BOOL, True, "eliminate ite in favor of and/or"), ('elim_ite', BOOL, True, "eliminate ite in favor of and/or"),
("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"), ("local_ctx", BOOL, False, "perform local (i.e., cheap) context simplifications"),