From 4d6977eaea52c90302fa5540efacb6c9c2228975 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 28 Oct 2015 12:53:53 -0700 Subject: [PATCH] Remove old_simplify.bv.hi_div0 option, reconciling it with rewriter.bv.hi_div0. To address issue #237 Signed-off-by: Nikolaj Bjorner --- src/ast/simplifier/bv_simplifier_params.cpp | 5 ++++- src/ast/simplifier/bv_simplifier_params_helper.pyg | 4 +--- 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/ast/simplifier/bv_simplifier_params.cpp b/src/ast/simplifier/bv_simplifier_params.cpp index aa9dcfc2d..5d6cd363f 100644 --- a/src/ast/simplifier/bv_simplifier_params.cpp +++ b/src/ast/simplifier/bv_simplifier_params.cpp @@ -18,9 +18,12 @@ Revision History: --*/ #include"bv_simplifier_params.h" #include"bv_simplifier_params_helper.hpp" +#include"bv_rewriter_params.hpp" void bv_simplifier_params::updt_params(params_ref const & _p) { bv_simplifier_params_helper p(_p); - m_hi_div0 = p.bv_hi_div0(); + bv_rewriter_params rp(_p); + m_hi_div0 = rp.hi_div0(); m_bv2int_distribute = p.bv_bv2int_distribute(); + } diff --git a/src/ast/simplifier/bv_simplifier_params_helper.pyg b/src/ast/simplifier/bv_simplifier_params_helper.pyg index 24bc86150..6bcf83207 100644 --- a/src/ast/simplifier/bv_simplifier_params_helper.pyg +++ b/src/ast/simplifier/bv_simplifier_params_helper.pyg @@ -1,6 +1,4 @@ def_module_params(class_name='bv_simplifier_params_helper', module_name="old_simplify", # Parameters will be in the old_simplify module export=True, - params=( - ('bv.hi_div0', BOOL, True, 'if true, then Z3 uses the usual hardware interpretation for division (rem, mod) by zero; otherwise, these operations are considered uninterpreted'), - ('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators'))) + params=(('bv.bv2int_distribute', BOOL, True, 'if true, then int2bv is distributed over arithmetical operators'),))