From ea2a84332513a7823e8e5c96f039fd048cb43dc5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 30 Jun 2022 19:59:46 -0700 Subject: [PATCH] flat only 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. --- src/ast/rewriter/th_rewriter.cpp | 2 +- src/params/rewriter_params.pyg | 1 - 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 5b0df8147..c69534b08 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -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(); diff --git a/src/params/rewriter_params.pyg b/src/params/rewriter_params.pyg index 18bb29e56..290f7b1da 100644 --- a/src/params/rewriter_params.pyg +++ b/src/params/rewriter_params.pyg @@ -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."),