diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 452a915d1..4ce41040b 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1461,6 +1461,9 @@ def pyg_default_as_c_literal(p): return 'symbol("%s")' % p[2] return p[2] +def to_c_method(s): + return s.replace('.', '_') + def def_module_params(module_name, export, params, class_name=None): pyg = get_curr_pyg() dirname = os.path.split(get_curr_pyg())[0] @@ -1493,10 +1496,10 @@ def def_module_params(module_name, export, params, class_name=None): for param in params: if export: out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % - (TYPE2CTYPE[param[1]], param[0], TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) else: out.write(' %s %s() const { return p.%s("%s", %s); }\n' % - (TYPE2CTYPE[param[1]], param[0], TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) out.write('};\n') if is_verbose(): print "Generated '%s'" % hpp diff --git a/src/ast/simplifier/arith_simplifier_params.h b/src/ast/simplifier/arith_simplifier_params.h index f1b22b09a..5a00f6337 100644 --- a/src/ast/simplifier/arith_simplifier_params.h +++ b/src/ast/simplifier/arith_simplifier_params.h @@ -19,13 +19,20 @@ Revision History: #ifndef _ARITH_SIMPLIFIER_PARAMS_H_ #define _ARITH_SIMPLIFIER_PARAMS_H_ -struct arith_simplifier_params { +#include"arith_simplifier_params_helper.hpp" + +struct arith_simplifier_params { bool m_arith_expand_eqs; bool m_arith_process_all_eqs; - arith_simplifier_params(): - m_arith_expand_eqs(false), - m_arith_process_all_eqs(false) { + arith_simplifier_params(params_ref const & p = params_ref()) { + updt_params(p); + } + + void updt_params(params_ref const & _p) { + arith_simplifier_params_helper p(_p); + m_arith_expand_eqs = p.arith_expand_eqs(); + m_arith_process_all_eqs = p.arith_process_all_eqs(); } }; diff --git a/src/ast/simplifier/arith_simplifier_params_helper.pyg b/src/ast/simplifier/arith_simplifier_params_helper.pyg new file mode 100644 index 000000000..9cd79bebc --- /dev/null +++ b/src/ast/simplifier/arith_simplifier_params_helper.pyg @@ -0,0 +1,6 @@ +def_module_params(class_name='arith_simplifier_params_helper', + module_name="old_simplify", # Parameters will be in the old_simplify module + export=True, + params=( + ('arith.expand_eqs', BOOL, False, 'expand equalities into two inequalities'), + ('arith.process_all_eqs', BOOL, False, 'put all equations in the form (= t c), where c is a numeral'))) diff --git a/src/ast/simplifier/array_simplifier_params.h b/src/ast/simplifier/array_simplifier_params.h index 8b9f3e37e..6c203ed63 100644 --- a/src/ast/simplifier/array_simplifier_params.h +++ b/src/ast/simplifier/array_simplifier_params.h @@ -19,13 +19,20 @@ Revision History: #ifndef _ARRAY_SIMPLIFIER_PARAMS_H_ #define _ARRAY_SIMPLIFIER_PARAMS_H_ +#include"array_simplifier_params_helper.hpp" + struct array_simplifier_params { bool m_array_canonize_simplify; bool m_array_simplify; // temporary hack for disabling array simplifier plugin. - array_simplifier_params(): - m_array_canonize_simplify(false), - m_array_simplify(true) { + array_simplifier_params(params_ref const & p = params_ref()) { + updt_params(p); + } + + void updt_params(params_ref const & _p) { + array_simplifier_params_helper p(_p); + m_array_canonize_simplify = p.array_canonize(); + m_array_simplify = p.array_simplify(); } }; diff --git a/src/ast/simplifier/array_simplifier_params_helper.pyg b/src/ast/simplifier/array_simplifier_params_helper.pyg new file mode 100644 index 000000000..93c184c23 --- /dev/null +++ b/src/ast/simplifier/array_simplifier_params_helper.pyg @@ -0,0 +1,6 @@ +def_module_params(class_name='array_simplifier_params_helper', + module_name="old_simplify", # Parameters will be in the old_simplify module + export=True, + params=( + ('array.canonize', BOOL, False, 'normalize array terms into normal form during simplification'), + ('array.simplify', BOOL, True, 'enable/disable array simplifications'))) diff --git a/src/ast/simplifier/bv_simplifier_params.h b/src/ast/simplifier/bv_simplifier_params.h index 4bec70285..85d969d48 100644 --- a/src/ast/simplifier/bv_simplifier_params.h +++ b/src/ast/simplifier/bv_simplifier_params.h @@ -19,13 +19,20 @@ Revision History: #ifndef _BV_SIMPLIFIER_PARAMS_H_ #define _BV_SIMPLIFIER_PARAMS_H_ +#include"bv_simplifier_params_helper.hpp" + struct bv_simplifier_params { bool m_hi_div0; //!< if true, uses the hardware interpretation for div0, mod0, ... if false, div0, mod0, ... are considered uninterpreted. bool m_bv2int_distribute; //!< if true allows downward propagation of bv2int. - bv_simplifier_params(): - m_hi_div0(true), - m_bv2int_distribute(true) { + bv_simplifier_params(params_ref const & p = params_ref()) { + updt_params(p); + } + + void updt_params(params_ref const & _p) { + bv_simplifier_params_helper p(_p); + m_hi_div0 = p.bv_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 new file mode 100644 index 000000000..24bc86150 --- /dev/null +++ b/src/ast/simplifier/bv_simplifier_params_helper.pyg @@ -0,0 +1,6 @@ +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')))