Skip to content

Commit

Permalink
flat only
Browse files Browse the repository at this point in the history
remove option for uzers (users who are in reality fuzzers) to toggle flat option. The legacy arithmetic solver bakes in assumptions about flat format so it isn't helpful to expose this to fuzzers, I mean uzers.
  • Loading branch information
NikolajBjorner committed Jul 1, 2022
1 parent b618537 commit ea2a843
Show file tree
Hide file tree
Showing 2 changed files with 1 addition and 2 deletions.
2 changes: 1 addition & 1 deletion src/ast/rewriter/th_rewriter.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -78,7 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {

void updt_local_params(params_ref const & _p) {
rewriter_params p(_p);
m_flat = p.flat();
m_flat = true;
m_max_memory = megabytes_to_bytes(p.max_memory());
m_max_steps = p.max_steps();
m_pull_cheap_ite = p.pull_cheap_ite();
Expand Down
1 change: 0 additions & 1 deletion src/params/rewriter_params.pyg
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,6 @@ def_module_params('rewriter',
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."),
Expand Down

0 comments on commit ea2a843

Please sign in to comment.