From 51f6dfeb831d02c41a7c38f9069179ba3f6a0032 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 28 Oct 2025 18:01:44 -0700 Subject: [PATCH] fix some argument-evaluation non-determinism, and mark the rest Signed-off-by: Lev Nachmanson --- src/ast/bv_decl_plugin.cpp | 31 +++- src/ast/char_decl_plugin.cpp | 18 +- .../converters/generic_model_converter.cpp | 1 + src/ast/format.h | 10 + src/ast/fpa/fpa2bv_converter.cpp | 173 ++++++++++++++---- src/ast/fpa/fpa2bv_rewriter.cpp | 1 + src/ast/normal_forms/pull_quant.cpp | 10 +- src/ast/rewriter/arith_rewriter.cpp | 54 +++++- src/ast/rewriter/bv2int_translator.cpp | 42 ++++- src/ast/rewriter/bv_rewriter.cpp | 122 +++++++++--- src/ast/rewriter/enum2bv_rewriter.cpp | 1 + src/ast/rewriter/factor_rewriter.cpp | 2 + src/ast/rewriter/fpa_rewriter.cpp | 2 + src/ast/rewriter/poly_rewriter_def.h | 1 + src/ast/rewriter/quant_hoist.cpp | 16 +- src/ast/rewriter/rewriter_def.h | 2 + src/ast/rewriter/seq_rewriter.cpp | 2 + src/ast/rewriter/th_rewriter.cpp | 2 + src/ast/sls/sls_array_plugin.cpp | 1 + src/ast/sls/sls_datatype_plugin.cpp | 1 + src/ast/sls/sls_seq_plugin.cpp | 1 + src/model/model_smt2_pp.cpp | 4 + src/muz/rel/check_relation.cpp | 1 + src/muz/rel/dl_base.cpp | 1 + src/muz/rel/dl_bound_relation.cpp | 3 + src/muz/rel/dl_finite_product_relation.cpp | 1 + src/muz/rel/dl_interval_relation.cpp | 1 + src/muz/spacer/spacer_convex_closure.cpp | 8 +- src/muz/spacer/spacer_generalizers.cpp | 1 + src/muz/spacer/spacer_qe_project.cpp | 17 +- src/muz/spacer/spacer_util.cpp | 10 +- src/muz/transforms/dl_mk_array_blast.cpp | 1 + src/muz/transforms/dl_mk_scale.cpp | 1 + src/opt/opt_context.cpp | 1 + src/qe/mbp/mbp_arith.cpp | 8 +- src/qe/mbp/mbp_arrays.cpp | 10 +- src/qe/mbp/mbp_solve_plugin.cpp | 8 +- src/qe/nlarith_util.cpp | 76 +++++++- src/qe/nlqsat.cpp | 2 + src/qe/qe_arith_plugin.cpp | 8 +- src/sat/smt/arith_axioms.cpp | 11 +- src/sat/smt/q_solver.cpp | 8 +- src/sat/tactic/sat2goal.cpp | 1 + src/smt/seq_regex.cpp | 1 + src/smt/theory_array_base.cpp | 8 +- src/smt/theory_bv.cpp | 3 + src/smt/theory_char.cpp | 1 + src/smt/theory_datatype.cpp | 1 + src/smt/theory_dl.cpp | 1 + src/smt/theory_lra.cpp | 10 +- src/smt/theory_special_relations.cpp | 47 ++++- src/tactic/aig/aig.cpp | 17 +- src/tactic/arith/bv2real_rewriter.cpp | 9 + src/tactic/arith/factor_tactic.cpp | 8 +- src/tactic/arith/lia2card_tactic.cpp | 1 + src/tactic/arith/pb2bv_tactic.cpp | 11 +- src/tactic/arith/purify_arith_tactic.cpp | 25 +++ src/tactic/bv/bv1_blaster_tactic.cpp | 1 + src/tactic/bv/bvarray2uf_rewriter.cpp | 26 ++- src/tactic/fd_solver/enum2bv_solver.cpp | 8 +- src/tactic/fd_solver/smtfd_solver.cpp | 18 +- src/util/sorting_network.h | 14 +- 62 files changed, 765 insertions(+), 120 deletions(-) diff --git a/src/ast/bv_decl_plugin.cpp b/src/ast/bv_decl_plugin.cpp index 83c0e2772..c5b64fb79 100644 --- a/src/ast/bv_decl_plugin.cpp +++ b/src/ast/bv_decl_plugin.cpp @@ -47,8 +47,22 @@ void bv_decl_plugin::set_manager(ast_manager * m, family_id id) { for (unsigned i = 1; i <= 64; i++) mk_bv_sort(i); - m_bit0 = m->mk_const_decl(symbol("bit0"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT0)); - m_bit1 = m->mk_const_decl(symbol("bit1"), get_bv_sort(1), func_decl_info(m_family_id, OP_BIT1)); + //non-deterministic order change start + { + auto symbol_1 = symbol("bit0"); + auto get_bv_sort_2 = get_bv_sort(1); + auto func_decl_info_3 = func_decl_info(m_family_id, OP_BIT0); + m_bit0 = m->mk_const_decl(symbol_1, get_bv_sort_2, func_decl_info_3); + } + //non-deterministic order change end + //non-deterministic order change start + { + auto symbol_1 = symbol("bit1"); + auto get_bv_sort_2 = get_bv_sort(1); + auto func_decl_info_3 = func_decl_info(m_family_id, OP_BIT1); + m_bit1 = m->mk_const_decl(symbol_1, get_bv_sort_2, func_decl_info_3); + } + //non-deterministic order change end m->inc_ref(m_bit0); m->inc_ref(m_bit1); @@ -509,7 +523,13 @@ func_decl * bv_decl_plugin::mk_mkbv(unsigned arity, sort * const * domain) { unsigned bv_size = arity; m_mkbv.reserve(bv_size+1); if (m_mkbv[bv_size] == 0) { - m_mkbv[bv_size] = m_manager->mk_func_decl(m_mkbv_sym, arity, domain, get_bv_sort(bv_size), func_decl_info(m_family_id, OP_MKBV)); + //non-deterministic order change start + { + auto get_bv_sort_1 = get_bv_sort(bv_size); + auto func_decl_info_2 = func_decl_info(m_family_id, OP_MKBV); + m_mkbv[bv_size] = m_manager->mk_func_decl(m_mkbv_sym, arity, domain, get_bv_sort_1, func_decl_info_2); + } + //non-deterministic order change end m_manager->inc_ref(m_mkbv[bv_size]); } return m_mkbv[bv_size]; @@ -578,21 +598,25 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p case OP_CONCAT: if (!get_concat_size(arity, domain, r_size)) m_manager->raise_exception("invalid concat application"); + //non-deterministic order no change: too complex return m_manager->mk_func_decl(m_concat_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k)); case OP_SIGN_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid sign_extend application"); + //non-deterministic order no change: too complex return m_manager->mk_func_decl(m_sign_extend_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ZERO_EXT: if (!get_extend_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid zero_extend application"); + //non-deterministic order no change: too complex return m_manager->mk_func_decl(m_zero_extend_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_EXTRACT: if (!get_extract_size(num_parameters, parameters, arity, domain, r_size)) m_manager->raise_exception("invalid extract application"); + //non-deterministic order no change: too complex return m_manager->mk_func_decl(m_extract_sym, arity, domain, get_bv_sort(r_size), func_decl_info(m_family_id, k, num_parameters, parameters)); case OP_ROTATE_LEFT: @@ -616,6 +640,7 @@ func_decl * bv_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, p m_manager->raise_exception("repeat expects one nonzero integer parameter"); if (!get_bv_size(domain[0], bv_size)) m_manager->raise_exception("repeat expects an argument with bit-vector sort"); + //non-deterministic order no change: too complex return m_manager->mk_func_decl(m_repeat_sym, arity, domain, get_bv_sort(bv_size * parameters[0].get_int()), func_decl_info(m_family_id, k, num_parameters, parameters)); default: diff --git a/src/ast/char_decl_plugin.cpp b/src/ast/char_decl_plugin.cpp index 6a94db121..e85cb9522 100644 --- a/src/ast/char_decl_plugin.cpp +++ b/src/ast/char_decl_plugin.cpp @@ -66,7 +66,14 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, msg << "incorrect number of arguments passed. Expected one character, received " << arity; else { arith_util a(m); - return m.mk_func_decl(symbol("char.to_int"), arity, domain, a.mk_int(), func_decl_info(m_family_id, k, 0, nullptr)); + //non-deterministic order change start + { + auto symbol_1 = symbol("char.to_int"); + auto mk_int_2 = a.mk_int(); + auto func_decl_info_3 = func_decl_info(m_family_id, k, 0, nullptr); + return m.mk_func_decl(symbol_1, arity, domain, mk_int_2, func_decl_info_3); + } + //non-deterministic order change end } m.raise_exception(msg.str()); case OP_CHAR_TO_BV: @@ -79,7 +86,14 @@ func_decl* char_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, else { bv_util b(m); unsigned sz = num_bits(); - return m.mk_func_decl(symbol("char.to_bv"), arity, domain, b.mk_sort(sz), func_decl_info(m_family_id, k, 0, nullptr)); + //non-deterministic order change start + { + auto symbol_1 = symbol("char.to_bv"); + auto mk_sort_2 = b.mk_sort(sz); + auto func_decl_info_3 = func_decl_info(m_family_id, k, 0, nullptr); + return m.mk_func_decl(symbol_1, arity, domain, mk_sort_2, func_decl_info_3); + } + //non-deterministic order change end } m.raise_exception(msg.str()); case OP_CHAR_FROM_BV: { diff --git a/src/ast/converters/generic_model_converter.cpp b/src/ast/converters/generic_model_converter.cpp index ed73106b2..7bd7563a4 100644 --- a/src/ast/converters/generic_model_converter.cpp +++ b/src/ast/converters/generic_model_converter.cpp @@ -262,6 +262,7 @@ expr_ref generic_model_converter::simplify_def(entry const& e) { rep.apply_substitution(c, m.mk_true(), result1); rep.apply_substitution(c, m.mk_false(), result2); th_rewriter rw(m); + //non-deterministic order no change: too complex expr_ref result(m.mk_and(m.mk_implies(result2, c), m.mk_implies(c, result1)), m); rw(result); return result; diff --git a/src/ast/format.h b/src/ast/format.h index 2714d54b7..3490d0645 100644 --- a/src/ast/format.h +++ b/src/ast/format.h @@ -90,15 +90,18 @@ namespace format_ns { format * mk_seq1(ast_manager & m, It const & begin, It const & end, ToDoc proc, char const * header, char const * lp = "(", char const * rp = ")") { if (begin == end) + //non-deterministic order no change: too complex return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); unsigned indent = static_cast(strlen(lp) + strlen(header) + 1); It it = begin; format * first = proc(*it); ++it; + //non-deterministic order no change: too complex return mk_group(m, mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_indent(m, indent, + //non-deterministic order no change: too complex mk_compose(m, mk_string(m, " "), first, @@ -146,6 +149,7 @@ namespace format_ns { unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { SASSERT(i >= 1); if (begin == end) + //non-deterministic order no change: too complex return mk_compose(m, mk_string(m, lp), mk_string(m, header), mk_string(m, rp)); unsigned idx = 0; It end1 = begin; @@ -155,9 +159,12 @@ namespace format_ns { format * first = proc(*it); ++it; return mk_group(m, + //non-deterministic order no change: too complex mk_compose(m, + //non-deterministic order no change: too complex mk_compose(m, mk_string(m, lp), mk_string(m, header)), mk_group(m, mk_indent(m, static_cast(strlen(header) + strlen(lp) + 1), + //non-deterministic order no change: too complex mk_compose(m, mk_string(m, " "), first, mk_seq(m, it, end1, proc)))), mk_indent(m, indent, mk_seq(m, end1, end, proc)), @@ -174,13 +181,16 @@ namespace format_ns { format * mk_seq4(ast_manager & m, It const & begin, It const & end, ToDoc proc, unsigned indent = FORMAT_DEFAULT_INDENT, char const * lp = "(", char const * rp = ")") { if (begin == end) + //non-deterministic order no change: too complex return mk_compose(m, mk_string(m, lp), mk_string(m, rp)); unsigned indent1 = static_cast(strlen(lp)); It it = begin; format * first = proc(*it); ++it; + //non-deterministic order no change: too complex return mk_group(m, mk_compose(m, mk_indent(m, indent1, mk_compose(m, mk_string(m, lp), first)), + //non-deterministic order no change: too complex mk_indent(m, indent, mk_compose(m, mk_seq(m, it, end, proc), mk_string(m, rp))))); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index f03dcbe1a..94dd002db 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -300,9 +300,16 @@ void fpa2bv_converter::mk_uf(func_decl * f, unsigned num, expr * const * args, e bv_rng = m_bv_util.mk_sort(bv_sz); func_decl * bv_f = mk_bv_uf(f, f->get_domain(), bv_rng); bv_app = m.mk_app(bv_f, num, args); - flt_app = m_util.mk_fp(m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app), - m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app), - m_bv_util.mk_extract(sbits-2, 0, bv_app)); + //non-deterministic order change start + { + auto mk_extract_1 = m_bv_util.mk_extract(bv_sz-1, bv_sz-1, bv_app); + auto mk_extract_2 = m_bv_util.mk_extract(sbits+ebits-2, sbits-1, bv_app); + auto mk_extract_3 = m_bv_util.mk_extract(sbits-2, 0, bv_app); + flt_app = m_util.mk_fp(mk_extract_1, + mk_extract_2, + mk_extract_3); + } + //non-deterministic order change end new_eq = m.mk_eq(fapp, flt_app); m_extra_assertions.push_back(extra_quantify(new_eq)); result = flt_app; @@ -1245,9 +1252,16 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r dbg_decouple("fpa2bv_rem_y_sig_eq_rndd_sig", y_sig_eq_rndd_sig); expr_ref adj_cnd(m); - adj_cnd = m.mk_or(m.mk_and(rndd_exp_eq_y_exp, y_sig_le_rndd_sig), - m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_le_rndd_sig, m.mk_not(y_sig_eq_rndd_sig)), - m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_eq_rndd_sig, m.mk_not(huge_div_is_even))); + //non-deterministic order change start + { + auto mk_and_1 = m.mk_and(rndd_exp_eq_y_exp, y_sig_le_rndd_sig); + auto mk_and_2 = m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_le_rndd_sig, m.mk_not(y_sig_eq_rndd_sig)); + auto mk_and_3 = m.mk_and(rndd_exp_eq_y_exp_m1, y_sig_eq_rndd_sig, m.mk_not(huge_div_is_even)); + adj_cnd = m.mk_or(mk_and_1, + mk_and_2, + mk_and_3); + } + //non-deterministic order change end dbg_decouple("fpa2bv_rem_adj_cnd", adj_cnd); expr_ref rndd(m), rounded_sub_y(m), rounded_add_y(m), add_cnd(m), adjusted(m); @@ -1646,9 +1660,15 @@ void fpa2bv_converter::mk_fma(func_decl * f, unsigned num, expr * const * args, // Alignment shift with sticky bit computation. expr_ref shifted_big(m), shifted_f_sig(m); expr_ref alignment_sticky_raw(m), alignment_sticky(m); - shifted_big = m_bv_util.mk_bv_lshr( - m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)), - m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta)); + //non-deterministic order change start + { + auto mk_concat_1 = m_bv_util.mk_concat(f_sig, m_bv_util.mk_numeral(0, sbits)); + auto mk_zero_extend_2 = m_bv_util.mk_zero_extend((3*sbits+3)-(ebits+2), exp_delta); + shifted_big = m_bv_util.mk_bv_lshr( + mk_concat_1, + mk_zero_extend_2); + } + //non-deterministic order change end shifted_f_sig = m_bv_util.mk_extract(3*sbits+2, sbits, shifted_big); alignment_sticky_raw = m_bv_util.mk_extract(sbits-1, 0, shifted_big); alignment_sticky = m.mk_app(m_bv_util.get_fid(), OP_BREDOR, alignment_sticky_raw.get()); @@ -1876,7 +1896,13 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, res_sgn = zero1; expr_ref real_exp(m); - real_exp = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(1, a_exp), m_bv_util.mk_zero_extend(1, a_lz)); + //non-deterministic order change start + { + auto mk_sign_extend_1 = m_bv_util.mk_sign_extend(1, a_exp); + auto mk_zero_extend_2 = m_bv_util.mk_zero_extend(1, a_lz); + real_exp = m_bv_util.mk_bv_sub(mk_sign_extend_1, mk_zero_extend_2); + } + //non-deterministic order change end res_exp = m_bv_util.mk_sign_extend(2, m_bv_util.mk_extract(ebits, 1, real_exp)); expr_ref e_is_odd(m); @@ -1907,7 +1933,13 @@ void fpa2bv_converter::mk_sqrt(func_decl * f, unsigned num, expr * const * args, S = m_bv_util.mk_concat(zero1, m_bv_util.mk_extract(sbits+4, 1, S)); expr_ref twoQ_plus_S(m); - twoQ_plus_S = m_bv_util.mk_bv_add(m_bv_util.mk_concat(Q, zero1), m_bv_util.mk_concat(zero1, S)); + //non-deterministic order change start + { + auto mk_concat_1 = m_bv_util.mk_concat(Q, zero1); + auto mk_concat_2 = m_bv_util.mk_concat(zero1, S); + twoQ_plus_S = m_bv_util.mk_bv_add(mk_concat_1, mk_concat_2); + } + //non-deterministic order change end T = m_bv_util.mk_bv_sub(m_bv_util.mk_concat(R, zero1), twoQ_plus_S); dbg_decouple("fpa2bv_sqrt_T", T); @@ -2098,8 +2130,14 @@ void fpa2bv_converter::mk_round_to_integral(sort * s, expr_ref & rm, expr_ref & expr_ref shift(m), shifted_sig(m), div(m), rem(m); shift = m_bv_util.mk_bv_sub(m_bv_util.mk_numeral(sbits - 1, sbits), m_bv_util.mk_sign_extend(sbits-ebits, a_exp)); - shifted_sig = m_bv_util.mk_bv_lshr(m_bv_util.mk_concat(a_sig, zero_s), - m_bv_util.mk_concat(zero_s, shift)); + //non-deterministic order change start + { + auto mk_concat_1 = m_bv_util.mk_concat(a_sig, zero_s); + auto mk_concat_2 = m_bv_util.mk_concat(zero_s, shift); + shifted_sig = m_bv_util.mk_bv_lshr(mk_concat_1, + mk_concat_2); + } + //non-deterministic order change end div = m_bv_util.mk_extract(2*sbits-1, sbits, shifted_sig); rem = m_bv_util.mk_extract(sbits-1, 0, shifted_sig); @@ -2451,9 +2489,16 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args (void)to_sbits; SASSERT((unsigned)sz == to_sbits + to_ebits); - result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv), - m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv), - m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv)); + //non-deterministic order change start + { + auto mk_extract_1 = m_bv_util.mk_extract(sz - 1, sz - 1, bv); + auto mk_extract_2 = m_bv_util.mk_extract(sz - 2, sz - to_ebits - 1, bv); + auto mk_extract_3 = m_bv_util.mk_extract(sz - to_ebits - 2, 0, bv); + result = m_util.mk_fp(mk_extract_1, + mk_extract_2, + mk_extract_3); + } + //non-deterministic order change end } else if (num == 2 && m_util.is_rm(args[0]) && @@ -2611,7 +2656,13 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r // subtract lz for subnormal numbers. expr_ref exp_sub_lz(m); - exp_sub_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), m_bv_util.mk_sign_extend(2, lz)); + //non-deterministic order change start + { + auto mk_sign_extend_1 = m_bv_util.mk_sign_extend(2, exp); + auto mk_sign_extend_2 = m_bv_util.mk_sign_extend(2, lz); + exp_sub_lz = m_bv_util.mk_bv_sub(mk_sign_extend_1, mk_sign_extend_2); + } + //non-deterministic order change end dbg_decouple("fpa2bv_to_float_exp_sub_lz", exp_sub_lz); // check whether exponent is within roundable (to_ebits+2) range. @@ -2844,6 +2895,8 @@ void fpa2bv_converter::mk_to_fp_real(func_decl * f, sort * s, expr * rm, expr * expr_ref pzero(m), nzero(m); mk_pzero(result->get_sort(), pzero); mk_nzero(result->get_sort(), nzero); + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex m_extra_assertions.push_back(m.mk_implies(m.mk_eq(x, zero), m.mk_or(m.mk_eq(result, pzero), m.mk_eq(result, nzero)))); } @@ -3398,8 +3451,14 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args // x is of the form +- [1].[sig][r][g][s] ... and at least bv_sz + 3 long expr_ref exp_m_lz(m), e_m_lz_m_bv_sz(m), shift(m), is_neg_shift(m), big_sig(m); - exp_m_lz = m_bv_util.mk_bv_sub(m_bv_util.mk_sign_extend(2, exp), - m_bv_util.mk_zero_extend(2, lz)); + //non-deterministic order change start + { + auto mk_sign_extend_1 = m_bv_util.mk_sign_extend(2, exp); + auto mk_zero_extend_2 = m_bv_util.mk_zero_extend(2, lz); + exp_m_lz = m_bv_util.mk_bv_sub(mk_sign_extend_1, + mk_zero_extend_2); + } + //non-deterministic order change end // big_sig is +- [... bv_sz+2 bits ...][1].[r][ ... sbits-1 ... ] big_sig = m_bv_util.mk_concat(m_bv_util.mk_zero_extend(bv_sz + 2, sig), bv0); @@ -3465,10 +3524,18 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args expr_ref ul(m), in_range(m); if (!is_signed) { ul = m_bv_util.mk_zero_extend(3, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz))); - in_range = m.mk_and(m.mk_or(m.mk_not(x_is_neg), - m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz+3))), - m.mk_not(ovfl), - m_bv_util.mk_ule(pre_rounded, ul)); + //non-deterministic order no change: too complex + //non-deterministic order change start + { + auto mk_or_1 = m.mk_or(m.mk_not(x_is_neg), + m.mk_eq(pre_rounded, m_bv_util.mk_numeral(0, bv_sz+3))); + auto mk_not_2 = m.mk_not(ovfl); + auto mk_ule_3 = m_bv_util.mk_ule(pre_rounded, ul); + in_range = m.mk_and(mk_or_1, + mk_not_2, + mk_ule_3); + } + //non-deterministic order change end } else { expr_ref ll(m); @@ -3482,9 +3549,16 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args ul = m_bv_util.mk_numeral(0, 4); ovfl = m.mk_or(ovfl, m_bv_util.mk_sle(pre_rounded, m_bv_util.mk_bv_neg(m_bv_util.mk_numeral(1, bv_sz + 3)))); pre_rounded = m.mk_ite(x_is_neg, m_bv_util.mk_bv_neg(pre_rounded), pre_rounded); - in_range = m.mk_and(m.mk_not(ovfl), - m_bv_util.mk_sle(ll, pre_rounded), - m_bv_util.mk_sle(pre_rounded, ul)); + //non-deterministic order change start + { + auto mk_not_1 = m.mk_not(ovfl); + auto mk_sle_2 = m_bv_util.mk_sle(ll, pre_rounded); + auto mk_sle_3 = m_bv_util.mk_sle(pre_rounded, ul); + in_range = m.mk_and(mk_not_1, + mk_sle_2, + mk_sle_3); + } + //non-deterministic order change end dbg_decouple("fpa2bv_to_bv_in_range_ll", ll); } dbg_decouple("fpa2bv_to_bv_in_range_ovfl", ovfl); @@ -4188,8 +4262,14 @@ void fpa2bv_converter::round(sort * s, expr_ref & rm, expr_ref & sgn, expr_ref & SASSERT(m_bv_util.get_bv_size(inc) == 1 && is_well_sorted(m, inc)); dbg_decouple("fpa2bv_rnd_inc", inc); - sig = m_bv_util.mk_bv_add(m_bv_util.mk_zero_extend(1, sig), - m_bv_util.mk_zero_extend(sbits, inc)); + //non-deterministic order change start + { + auto mk_zero_extend_1 = m_bv_util.mk_zero_extend(1, sig); + auto mk_zero_extend_2 = m_bv_util.mk_zero_extend(sbits, inc); + sig = m_bv_util.mk_bv_add(mk_zero_extend_1, + mk_zero_extend_2); + } + //non-deterministic order change end SASSERT(is_well_sorted(m, sig)); dbg_decouple("fpa2bv_rnd_sig_plus_inc", sig); @@ -4367,9 +4447,16 @@ void fpa2bv_converter_wrapped::mk_const(func_decl* f, expr_ref& result) { unsigned bv_sz = m_bv_util.get_bv_size(bv); unsigned sbits = m_util.get_sbits(s); SASSERT(bv_sz == m_util.get_ebits(s) + sbits); - result = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv), - m_bv_util.mk_extract(sbits - 2, 0, bv)); + //non-deterministic order change start + { + auto mk_extract_1 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, bv); + auto mk_extract_2 = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, bv); + auto mk_extract_3 = m_bv_util.mk_extract(sbits - 2, 0, bv); + result = m_util.mk_fp(mk_extract_1, + mk_extract_2, + mk_extract_3); + } + //non-deterministic order change end SASSERT(m_util.is_float(result)); m_const2bv.insert(f, result); m.inc_ref(f); @@ -4419,19 +4506,35 @@ app_ref fpa2bv_converter_wrapped::unwrap(expr* e, sort* s) { if (m_util.is_rm(s)) { SASSERT(bv_sz == 3); - res = m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)), m_util.mk_round_nearest_ties_to_away(), + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_AWAY, 3)); + auto mk_round_nearest_ties_to_away_2 = m_util.mk_round_nearest_ties_to_away(); + res = m.mk_ite(mk_eq_1, mk_round_nearest_ties_to_away_2, + //non-deterministic order no change: too complex m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TIES_TO_EVEN, 3)), m_util.mk_round_nearest_ties_to_even(), + //non-deterministic order no change: too complex m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_NEGATIVE, 3)), m_util.mk_round_toward_negative(), + //non-deterministic order no change: too complex m.mk_ite(m.mk_eq(e, m_bv_util.mk_numeral(BV_RM_TO_POSITIVE, 3)), m_util.mk_round_toward_positive(), m_util.mk_round_toward_zero())))); + } + //non-deterministic order change end } else { SASSERT(m_util.is_float(s)); unsigned sbits = m_util.get_sbits(s); SASSERT(bv_sz == m_util.get_ebits(s) + sbits); - res = m_util.mk_fp(m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e), - m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e), - m_bv_util.mk_extract(sbits - 2, 0, e)); + //non-deterministic order change start + { + auto mk_extract_1 = m_bv_util.mk_extract(bv_sz - 1, bv_sz - 1, e); + auto mk_extract_2 = m_bv_util.mk_extract(bv_sz - 2, sbits - 1, e); + auto mk_extract_3 = m_bv_util.mk_extract(sbits - 2, 0, e); + res = m_util.mk_fp(mk_extract_1, + mk_extract_2, + mk_extract_3); + } + //non-deterministic order change end } return res; diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index bba7adb60..9e540428d 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -258,6 +258,7 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res unsigned ebits = m_conv.fu().get_ebits(s); unsigned sbits = m_conv.fu().get_sbits(s); new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); + //non-deterministic order no change: too complex new_exp = m_conv.fu().mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), m_conv.bu().mk_extract(ebits - 1, 0, new_var), m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var)); diff --git a/src/ast/normal_forms/pull_quant.cpp b/src/ast/normal_forms/pull_quant.cpp index 9f57f826a..63fcb30c2 100644 --- a/src/ast/normal_forms/pull_quant.cpp +++ b/src/ast/normal_forms/pull_quant.cpp @@ -265,8 +265,14 @@ struct pull_quant::imp { return BR_FAILED; if (m.proofs_enabled()) { - result_pr = m.mk_pull_quant(m.mk_app(f, num, args), - to_quantifier(result.get())); + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(f, num, args); + auto get_2 = to_quantifier(result.get()); + result_pr = m.mk_pull_quant(mk_app_1, + get_2); + } + //non-deterministic order change end } return BR_DONE; } diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index d5ad70a1f..43a12f273 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -622,7 +622,13 @@ br_status arith_rewriter::factor_le_ge_eq(expr * arg1, expr * arg2, op_kind kind return BR_FAILED; expr_ref f2 = remove_factor(f, arg1); expr* z = m_util.mk_numeral(rational(0), m_util.is_int(arg1)); - result = m.mk_or(m_util.mk_eq(f, z), m_util.mk_eq(f2, z)); + //non-deterministic order change start + { + auto mk_eq_1 = m_util.mk_eq(f, z); + auto mk_eq_2 = m_util.mk_eq(f2, z); + result = m.mk_or(mk_eq_1, mk_eq_2); + } + //non-deterministic order change end switch (kind) { case EQ: break; @@ -868,8 +874,14 @@ bool arith_rewriter::mk_eq_mod(expr* arg1, expr* arg2, expr_ref& result) { rational g = gcd(p, k, a, b); if (g == 1) { expr_ref nb(m_util.mk_numeral(b, true), m); - result = m.mk_eq(m_util.mk_mod(u, y), - m_util.mk_mod(m_util.mk_mul(nb, arg2), y)); + //non-deterministic order change start + { + auto mk_mod_1 = m_util.mk_mod(u, y); + auto mk_mod_2 = m_util.mk_mod(m_util.mk_mul(nb, arg2), y); + result = m.mk_eq(mk_mod_1, + mk_mod_2); + } + //non-deterministic order change end return true; } } @@ -1202,7 +1214,13 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul } br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) { - result = m.mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0)); + //non-deterministic order change start + { + auto mk_mod_1 = m_util.mk_mod(arg, m_util.mk_int(k)); + auto mk_int_2 = m_util.mk_int(0); + result = m.mk_eq(mk_mod_1, mk_int_2); + } + //non-deterministic order change end return BR_REWRITE2; } @@ -1229,7 +1247,14 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } if (arg1 == arg2) { expr_ref zero(m_util.mk_int(0), m); - result = m.mk_ite(m.mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(arg1, zero); + auto mk_idiv_2 = m_util.mk_idiv(zero, zero); + auto mk_int_3 = m_util.mk_int(1); + result = m.mk_ite(mk_eq_1, mk_idiv_2, mk_int_3); + } + //non-deterministic order change end return BR_REWRITE3; } if (is_num2 && v2.is_pos() && m_util.is_add(arg1)) { @@ -1327,6 +1352,7 @@ expr_ref arith_rewriter::remove_divisor(expr* arg, expr* num, expr* den) { den = args2.empty() ? m_util.mk_int(1) : m_util.mk_mul(args2.size(), args2.data()); expr_ref d(m_util.mk_idiv(num, den), m); expr_ref nd(m_util.mk_idiv(m_util.mk_uminus(num), m_util.mk_uminus(den)), m); + //non-deterministic order no change: too complex return expr_ref(m.mk_ite(m.mk_eq(zero, arg), m_util.mk_idiv(zero, zero), m.mk_ite(m_util.mk_ge(arg, zero), @@ -1427,7 +1453,13 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul expr* x = nullptr, * y = nullptr, * z = nullptr; if (is_num2 && v2.is_pos() && m_util.is_mul(arg1, x, y) && m_util.is_numeral(x, v1, is_int) && v1 > 0 && divides(v1, v2)) { - result = m_util.mk_mul(m_util.mk_int(v1), m_util.mk_mod(y, m_util.mk_int(v2/v1))); + //non-deterministic order change start + { + auto mk_int_1 = m_util.mk_int(v1); + auto mk_mod_2 = m_util.mk_mod(y, m_util.mk_int(v2/v1)); + result = m_util.mk_mul(mk_int_1, mk_mod_2); + } + //non-deterministic order change end return BR_REWRITE1; } @@ -2083,12 +2115,14 @@ expr * arith_rewriter::mk_sin_value(rational const & k) { if (k_prime == rational(1, 12) || k_prime == rational(11, 12)) { // sin(1/12 pi) == sin(11/12 pi) == [sqrt(6) - sqrt(2)]/4 // sin(13/12 pi) == sin(23/12 pi) == -[sqrt(6) - sqrt(2)]/4 + //non-deterministic order no change: too complex expr * result = m_util.mk_div(m_util.mk_sub(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false)); return neg ? m_util.mk_uminus(result) : result; } if (k_prime == rational(5, 12) || k_prime == rational(7, 12)) { // sin(5/12 pi) == sin(7/12 pi) == [sqrt(6) + sqrt(2)]/4 // sin(17/12 pi) == sin(19/12 pi) == -[sqrt(6) + sqrt(2)]/4 + //non-deterministic order no change: too complex expr * result = m_util.mk_div(m_util.mk_add(mk_sqrt(rational(6)), mk_sqrt(rational(2))), m_util.mk_numeral(rational(4), false)); return neg ? m_util.mk_uminus(result) : result; } @@ -2267,7 +2301,13 @@ br_status arith_rewriter::mk_tan_core(expr * arg, expr_ref & result) { end: if (m_expand_tan) { - result = m_util.mk_div(m_util.mk_sin(arg), m_util.mk_cos(arg)); + //non-deterministic order change start + { + auto mk_sin_1 = m_util.mk_sin(arg); + auto mk_cos_2 = m_util.mk_cos(arg); + result = m_util.mk_div(mk_sin_1, mk_cos_2); + } + //non-deterministic order change end return BR_REWRITE2; } return BR_FAILED; diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp index da15bde2b..eb6e384c2 100644 --- a/src/ast/rewriter/bv2int_translator.cpp +++ b/src/ast/rewriter/bv2int_translator.cpp @@ -222,6 +222,7 @@ void bv2int_translator::translate_bv(app* e) { auto A = rational::power_of_two(sz - n); auto B = rational::power_of_two(n); auto hi = mul(r, a.mk_int(A)); + //non-deterministic order no change: too complex auto lo = amod(e, a.mk_idiv(umod(e, 0), a.mk_int(B)), A); r = add(hi, lo); } @@ -364,7 +365,13 @@ void bv2int_translator::translate_bv(app* e) { rational N = bv_size(e); expr* x = umod(e, 0), * y = umod(e, 1); expr* signx = a.mk_ge(x, a.mk_int(N / 2)); - r = m.mk_ite(signx, a.mk_int(-1), a.mk_int(0)); + //non-deterministic order change start + { + auto mk_int_1 = a.mk_int(-1); + auto mk_int_2 = a.mk_int(0); + r = m.mk_ite(signx, mk_int_1, mk_int_2); + } + //non-deterministic order change end IF_VERBOSE(4, verbose_stream() << "ashr " << mk_bounded_pp(e, m) << " " << bv.get_bv_size(e) << "\n"); for (unsigned i = 0; i < sz; ++i) { expr* d = a.mk_idiv(x, a.mk_int(rational::power_of_two(i))); @@ -431,7 +438,15 @@ void bv2int_translator::translate_bv(app* e) { break; case OP_BCOMP: bv_expr = e->get_arg(0); - r = m.mk_ite(m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)), a.mk_int(1), a.mk_int(0)); + //non-deterministic order no change: too complex + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1)); + auto mk_int_2 = a.mk_int(1); + auto mk_int_3 = a.mk_int(0); + r = m.mk_ite(mk_eq_1, mk_int_2, mk_int_3); + } + //non-deterministic order change end break; case OP_BSMOD_I: case OP_BSMOD: { @@ -449,6 +464,7 @@ void bv2int_translator::translate_bv(app* e) { r = a.mk_uminus(u); r = m.mk_ite(m.mk_and(m.mk_not(signx), signy), add(u, y), r); r = m.mk_ite(m.mk_and(signx, m.mk_not(signy)), a.mk_sub(y, u), r); + //non-deterministic order no change: too complex r = m.mk_ite(m.mk_and(m.mk_not(signx), m.mk_not(signy)), u, r); r = if_eq(u, 0, a.mk_int(0), r); r = if_eq(y, 0, x, r); @@ -472,6 +488,7 @@ void bv2int_translator::translate_bv(app* e) { y = m.mk_ite(signy, a.mk_sub(a.mk_int(N), y), y); expr* d = a.mk_idiv(x, y); r = m.mk_ite(m.mk_iff(signx, signy), d, a.mk_uminus(d)); + //non-deterministic order no change: too complex r = if_eq(y, 0, m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)), r); break; } @@ -566,17 +583,27 @@ void bv2int_translator::translate_basic(app* e) { rational N = rational::power_of_two(bv.get_bv_size(bv_expr)); if (a.is_numeral(arg(0)) || a.is_numeral(arg(1)) || is_bounded(arg(0), N) || is_bounded(arg(1), N)) { + //non-deterministic order no change: too complex set_translated(e, m.mk_eq(umod(bv_expr, 0), umod(bv_expr, 1))); } else { - m_args[0] = a.mk_sub(arg(0), arg(1)); + //non-deterministic order change start + { + auto arg_1 = arg(0); + auto arg_2 = arg(1); + m_args[0] = a.mk_sub(arg_1, arg_2); + } + //non-deterministic order change end + //non-deterministic order no change: too complex set_translated(e, m.mk_eq(umod(bv_expr, 0), a.mk_int(0))); } } else + //non-deterministic order no change: too complex set_translated(e, m.mk_eq(arg(0), arg(1))); } else if (m.is_ite(e)) + //non-deterministic order no change: too complex set_translated(e, m.mk_ite(arg(0), arg(1), arg(2))); else if (m_is_plugin) set_translated(e, e); @@ -661,7 +688,13 @@ expr* bv2int_translator::amod(expr* bv_expr, expr* x, rational const& N) { rational v; expr* r = nullptr, * c = nullptr, * t = nullptr, * e = nullptr; if (m.is_ite(x, c, t, e)) - r = m.mk_ite(c, amod(bv_expr, t, N), amod(bv_expr, e, N)); + //non-deterministic order change start + { + auto amod_1 = amod(bv_expr, t, N); + auto amod_2 = amod(bv_expr, e, N); + r = m.mk_ite(c, amod_1, amod_2); + } + //non-deterministic order change end else if (a.is_idiv(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N && is_non_negative(bv_expr, e)) r = x; else if (a.is_mod(x, t, e) && a.is_numeral(t, v) && 0 <= v && v < N) @@ -684,6 +717,7 @@ void bv2int_translator::translate_eq(expr* e) { ensure_translated(y); m_args.reset(); m_args.push_back(a.mk_sub(translated(x), translated(y))); + //non-deterministic order no change: too complex set_translated(e, m.mk_eq(umod(x, 0), a.mk_int(0))); } m_preds.push_back(e); diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 18e82de72..d11283c8c 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -384,8 +384,14 @@ br_status bv_rewriter::rw_leq_overflow(bool is_signed, expr * a, expr * b, expr_ } else { SASSERT(lower.is_pos()); - result = m.mk_and(m_util.mk_ule(mk_numeral(lower, sz), common), - m_util.mk_ule(common, mk_numeral(upper, sz))); + //non-deterministic order change start + { + auto mk_ule_1 = m_util.mk_ule(mk_numeral(lower, sz), common); + auto mk_ule_2 = m_util.mk_ule(common, mk_numeral(upper, sz)); + result = m.mk_and(mk_ule_1, + mk_ule_2); + } + //non-deterministic order change end } return BR_REWRITE2; } @@ -447,8 +453,14 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr return BR_DONE; } if (common > 0) { - result = m_util.mk_ule(concat(numa - common, a->get_args() + common), - concat(numb - common, b->get_args() + common)); + //non-deterministic order change start + { + auto get_args_1 = concat(numa - common, a->get_args() + common); + auto get_args_2 = concat(numb - common, b->get_args() + common); + result = m_util.mk_ule(get_args_1, + get_args_2); + } + //non-deterministic order change end return BR_REWRITE2; } } @@ -469,7 +481,9 @@ br_status bv_rewriter::rw_leq_concats(bool is_signed, expr * _a, expr * _b, expr return BR_DONE; } if (new_numa != numa) { + //non-deterministic order no change: too complex result = is_signed ? m_util.mk_sle(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())) + //non-deterministic order no change: too complex : m_util.mk_ule(concat(new_numa, a->get_args()), concat(new_numb, b->get_args())); return BR_REWRITE2; } @@ -870,7 +884,13 @@ br_status bv_rewriter::mk_extract(unsigned high, unsigned low, expr * arg, expr_ expr* c = nullptr, *t = nullptr, *e = nullptr; if (m.is_ite(arg, c, t, e) && (t->get_ref_count() == 1 || e->get_ref_count() == 1 || !m.is_ite(t) || !m.is_ite(e))) { - result = m.mk_ite(c, m_mk_extract(high, low, t), m_mk_extract(high, low, e)); + //non-deterministic order change start + { + auto m_mk_extract_1 = m_mk_extract(high, low, t); + auto m_mk_extract_2 = m_mk_extract(high, low, e); + result = m.mk_ite(c, m_mk_extract_1, m_mk_extract_2); + } + //non-deterministic order change end return BR_REWRITE2; } @@ -1083,7 +1103,13 @@ br_status bv_rewriter::mk_bv_ashr(expr * arg1, expr * arg2, expr_ref & result) { // (bvlshr x k) -> (concat bv0:k (extract [n-1:k] x)) unsigned k = r2.get_unsigned(); - result = m_util.mk_concat(mk_zero(k), m_mk_extract(bv_size - 1, k, arg1)); + //non-deterministic order change start + { + auto mk_zero_1 = mk_zero(k); + auto m_mk_extract_2 = m_mk_extract(bv_size - 1, k, arg1); + result = m_util.mk_concat(mk_zero_1, m_mk_extract_2); + } + //non-deterministic order change end return BR_REWRITE2; } #if 0 @@ -1120,9 +1146,16 @@ br_status bv_rewriter::mk_bv_sdiv_core(expr * arg1, expr * arg2, bool hi_div0, e } else { // The "hardware interpretation" for (bvsdiv x 0) is (ite (bvslt x #x0000) #x0001 #xffff) - result = m.mk_ite(m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)), - mk_one(bv_size), - mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size)); + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(get_fid(), OP_SLT, arg1, mk_zero(bv_size)); + auto mk_one_2 = mk_one(bv_size); + auto mk_numeral_3 = mk_numeral(rational::power_of_two(bv_size) - numeral(1), bv_size); + result = m.mk_ite(mk_app_1, + mk_one_2, + mk_numeral_3); + } + //non-deterministic order change end return BR_REWRITE2; } } @@ -1250,9 +1283,16 @@ br_status bv_rewriter::mk_bv_srem_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), - m.mk_app(get_fid(), OP_BSREM0, arg1), - m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2)); + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(arg2, mk_zero(bv_size)); + auto mk_app_2 = m.mk_app(get_fid(), OP_BSREM0, arg1); + auto mk_app_3 = m.mk_app(get_fid(), OP_BSREM_I, arg1, arg2); + result = m.mk_ite(mk_eq_1, + mk_app_2, + mk_app_3); + } + //non-deterministic order change end return BR_REWRITE2; } @@ -1467,9 +1507,16 @@ br_status bv_rewriter::mk_bv_smod_core(expr * arg1, expr * arg2, bool hi_div0, e } bv_size = get_bv_size(arg2); - result = m.mk_ite(m.mk_eq(arg2, mk_zero(bv_size)), - m.mk_app(get_fid(), OP_BSMOD0, arg1), - m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2)); + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(arg2, mk_zero(bv_size)); + auto mk_app_2 = m.mk_app(get_fid(), OP_BSMOD0, arg1); + auto mk_app_3 = m.mk_app(get_fid(), OP_BSMOD_I, arg1, arg2); + result = m.mk_ite(mk_eq_1, + mk_app_2, + mk_app_3); + } + //non-deterministic order change end return BR_REWRITE2; } @@ -1686,7 +1733,13 @@ br_status bv_rewriter::mk_concat(unsigned num_args, expr * const * args, expr_re ptr_buffer args1, args2; for (unsigned i = 0; i < new_args.size(); ++i) args1.push_back(y), args2.push_back(z); - result = m.mk_ite(x, m_util.mk_concat(args1), m_util.mk_concat(args2)); + //non-deterministic order change start + { + auto mk_concat_1 = m_util.mk_concat(args1); + auto mk_concat_2 = m_util.mk_concat(args2); + result = m.mk_ite(x, mk_concat_1, mk_concat_2); + } + //non-deterministic order change end return BR_REWRITE2; } } @@ -2336,9 +2389,16 @@ br_status bv_rewriter::mk_bv_comp(expr * arg1, expr * arg2, expr_ref & result) { return BR_DONE; } - result = m.mk_ite(m.mk_eq(arg1, arg2), - mk_one(1), - mk_zero(1)); + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(arg1, arg2); + auto mk_one_2 = mk_one(1); + auto mk_zero_3 = mk_zero(1); + result = m.mk_ite(mk_eq_1, + mk_one_2, + mk_zero_3); + } + //non-deterministic order change end return BR_REWRITE2; } @@ -2618,6 +2678,7 @@ br_status bv_rewriter::mk_blast_eq_value(expr * lhs, expr * rhs, expr_ref & resu ptr_buffer new_args; for (unsigned i = 0; i < sz; i++) { bool bit0 = (v % two).is_zero(); + //non-deterministic order no change: too complex new_args.push_back(m.mk_eq(m_mk_extract(i,i, lhs), mk_numeral(bit0 ? 0 : 1, 1))); div(v, two, v); @@ -2663,6 +2724,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { unsigned rsz1 = sz1 - low1; unsigned rsz2 = sz2 - low2; if (rsz1 == rsz2) { + //non-deterministic order no change: too complex new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), m_mk_extract(sz2 - 1, low2, arg2))); low1 = 0; @@ -2672,6 +2734,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { continue; } else if (rsz1 < rsz2) { + //non-deterministic order no change: too complex new_eqs.push_back(m.mk_eq(m_mk_extract(sz1 - 1, low1, arg1), m_mk_extract(rsz1 + low2 - 1, low2, arg2))); low1 = 0; @@ -2679,6 +2742,7 @@ br_status bv_rewriter::mk_eq_concat(expr * lhs, expr * rhs, expr_ref & result) { --i1; } else { + //non-deterministic order no change: too complex new_eqs.push_back(m.mk_eq(m_mk_extract(rsz2 + low1 - 1, low1, arg1), m_mk_extract(sz2 - 1, low2, arg2))); low1 += rsz2; @@ -3110,10 +3174,16 @@ br_status bv_rewriter::mk_distinct(unsigned num_args, expr * const * args, expr_ br_status bv_rewriter::mk_bvsmul_overflow(unsigned num, expr * const * args, expr_ref & result) { SASSERT(num == 2); - result = m.mk_or( - m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])), - m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1])) + //non-deterministic order change start + { + auto mk_not_1 = m.mk_not(m_util.mk_bvsmul_no_ovfl(args[0], args[1])); + auto mk_not_2 = m.mk_not(m_util.mk_bvsmul_no_udfl(args[0], args[1])); + result = m.mk_or( + mk_not_1, + mk_not_2 ); + } + //non-deterministic order change end return BR_REWRITE_FULL; } @@ -3279,7 +3349,13 @@ br_status bv_rewriter::mk_bvsdiv_overflow(unsigned num, expr * const * args, exp auto sz = get_bv_size(args[1]); auto minSigned = mk_numeral(rational::power_of_two(sz-1), sz); auto minusOne = mk_numeral(rational::power_of_two(sz) - 1, sz); - result = m.mk_and(m.mk_eq(args[0], minSigned), m.mk_eq(args[1], minusOne)); + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(args[0], minSigned); + auto mk_eq_2 = m.mk_eq(args[1], minusOne); + result = m.mk_and(mk_eq_1, mk_eq_2); + } + //non-deterministic order change end return BR_REWRITE_FULL; } diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index a8171c230..083c089e1 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -74,6 +74,7 @@ struct enum2bv_rewriter::imp { if (is_unate(s)) { expr_ref one(m_bv.mk_numeral(rational::one(), 1), m); for (unsigned i = 0; i + 2 < domain_size; ++i) { + //non-deterministic order no change: too complex bounds.push_back(m.mk_implies(m.mk_eq(one, m_bv.mk_extract(i + 1, i + 1, x)), m.mk_eq(one, m_bv.mk_extract(i, i, x)))); } diff --git a/src/ast/rewriter/factor_rewriter.cpp b/src/ast/rewriter/factor_rewriter.cpp index 2220d8613..4d66b4932 100644 --- a/src/ast/rewriter/factor_rewriter.cpp +++ b/src/ast/rewriter/factor_rewriter.cpp @@ -141,7 +141,9 @@ void factor_rewriter::mk_is_negative(expr_ref& result, expr_ref_vector& eqs) { pos0 = pos; } else { + //non-deterministic order no change: too complex tmp = m().mk_or(m().mk_and(pos, pos0), m().mk_and(neg, neg0)); + //non-deterministic order no change: too complex neg0 = m().mk_or(m().mk_and(neg, pos0), m().mk_and(pos, neg0)); pos0 = tmp; } diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index 474d1c958..590cfef0b 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -494,6 +494,7 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { } if (m_util.is_ninf(arg1)) { // -oo < arg2 --> not(arg2 = -oo) and not(arg2 = NaN) + //non-deterministic order no change: too complex result = m().mk_and(m().mk_not(m().mk_eq(arg2, arg1)), mk_neq_nan(arg2)); return BR_REWRITE3; } @@ -509,6 +510,7 @@ br_status fpa_rewriter::mk_lt(expr * arg1, expr * arg2, expr_ref & result) { } if (m_util.is_pinf(arg2)) { // arg1 < +oo --> not(arg1 = +oo) and not(arg1 = NaN) + //non-deterministic order no change: too complex result = m().mk_and(m().mk_not(m().mk_eq(arg1, arg2)), mk_neq_nan(arg1)); return BR_REWRITE3; } diff --git a/src/ast/rewriter/poly_rewriter_def.h b/src/ast/rewriter/poly_rewriter_def.h index f0f564816..3e0330b54 100644 --- a/src/ast/rewriter/poly_rewriter_def.h +++ b/src/ast/rewriter/poly_rewriter_def.h @@ -1065,6 +1065,7 @@ template expr* poly_rewriter::apply_hoist(expr* a, numeral const& g, obj_hashtable const& shared) { expr* c = nullptr, *t = nullptr, *e = nullptr; if (M().is_ite(a, c, t, e)) { + //non-deterministic order no change: too complex return M().mk_ite(c, apply_hoist(t, g, shared), apply_hoist(e, g, shared)); } rational k; diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index d649737f5..d8cb500ed 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -249,7 +249,13 @@ private: pull_quantifier(t1, qt, vars, tt1, use_fresh, rewrite_ok); nt1 = m.mk_not(t1); pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); - result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3)); + //non-deterministic order change start + { + auto mk_or_1 = m.mk_or(ntt1, tt2); + auto mk_or_2 = m.mk_or(tt1, tt3); + result = m.mk_and(mk_or_1, mk_or_2); + } + //non-deterministic order change end } else { result = m.mk_ite(t1, tt2, tt3); @@ -263,7 +269,13 @@ private: nt2 = m.mk_not(t2); pull_quantifier(nt1, qt, vars, ntt1, use_fresh, rewrite_ok); pull_quantifier(nt2, qt, vars, ntt2, use_fresh, rewrite_ok); - result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1)); + //non-deterministic order change start + { + auto mk_or_1 = m.mk_or(ntt1, tt2); + auto mk_or_2 = m.mk_or(ntt2, tt1); + result = m.mk_and(mk_or_1, mk_or_2); + } + //non-deterministic order change end } else { // the formula contains a quantifier, but it is "inaccessible" diff --git a/src/ast/rewriter/rewriter_def.h b/src/ast/rewriter/rewriter_def.h index 7a0a1f61a..befcfb01e 100644 --- a/src/ast/rewriter/rewriter_def.h +++ b/src/ast/rewriter/rewriter_def.h @@ -574,6 +574,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { num_no_pats = j; } if (ProofGen) { + //non-deterministic order no change: too complex quantifier_ref new_q(m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body), m()); m_pr = nullptr; if (q != new_q) { @@ -599,6 +600,7 @@ void rewriter_tpl::process_quantifier(quantifier * q, frame & fr) { TRACE(reduce_quantifier_bug, tout << mk_ismt2_pp(q, m()) << " " << mk_ismt2_pp(new_body, m()) << "\n";); if (!m_cfg.reduce_quantifier(q, new_body, new_pats.data(), new_no_pats.data(), m_r, m_pr)) { if (fr.m_new_child) { + //non-deterministic order no change: too complex m_r = m().update_quantifier(q, num_pats, new_pats.data(), num_no_pats, new_no_pats.data(), new_body); } else { diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index d708af9e0..42f2c8a62 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2764,6 +2764,7 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (m().is_ite(r, p, r1, r2)) { + //non-deterministic order no change: too complex result = m().mk_ite(p, re().mk_reverse(r1), re().mk_reverse(r2)); return BR_REWRITE2; } @@ -4282,6 +4283,7 @@ bool seq_rewriter::rewrite_contains_pattern(expr* a, expr* b, expr_ref& result) suffix = re().mk_concat(suffix, re().mk_to_re(e)); suffix = re().mk_concat(suffix, full); } + //non-deterministic order no change: too complex fmls.push_back(m().mk_and(re().mk_in_re(x, prefix), re().mk_in_re(y, suffix))); } diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index f35d666d6..22412bbb8 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -143,10 +143,12 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr * x; unsigned val; if (m_bv_rw.is_eq_bit(lhs, x, val)) { + //non-deterministic order no change: too complex result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); return BR_REWRITE2; } if (m_bv_rw.is_eq_bit(rhs, x, val)) { + //non-deterministic order no change: too complex result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); return BR_REWRITE2; } diff --git a/src/ast/sls/sls_array_plugin.cpp b/src/ast/sls/sls_array_plugin.cpp index 9b2948ed9..ea33b71ff 100644 --- a/src/ast/sls/sls_array_plugin.cpp +++ b/src/ast/sls/sls_array_plugin.cpp @@ -414,6 +414,7 @@ namespace sls { } expr_ref sel1(a.mk_select(args1), m); expr_ref sel2(a.mk_select(args2), m); + //non-deterministic order no change: too complex bool r = ctx.add_constraint(m.mk_implies(m.mk_eq(sel1, sel2), m.mk_eq(x, y))); if (r) ++m_stats.m_num_axioms; diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp index b2b6baa2c..8dc1ec1a4 100644 --- a/src/ast/sls/sls_datatype_plugin.cpp +++ b/src/ast/sls/sls_datatype_plugin.cpp @@ -254,6 +254,7 @@ namespace sls { expr_ref_vector args(m); for (auto a : acc) args.push_back(m.mk_app(a, t)); + //non-deterministic order no change: too complex m_axioms.push_back(m.mk_iff(m.mk_app(r, t), m.mk_eq(t, m.mk_app(c, args)))); } } diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp index f74261da2..16f863ee9 100644 --- a/src/ast/sls/sls_seq_plugin.cpp +++ b/src/ast/sls/sls_seq_plugin.cpp @@ -161,6 +161,7 @@ namespace sls { if (r == 0 || sx.length() == 0) // create lemma: len(x) = 0 <=> x = "" + //non-deterministic order no change: too complex ctx.add_constraint(m.mk_eq(m.mk_eq(e, a.mk_int(0)), m.mk_eq(x, seq.str.mk_string("")))); if (ctx.rand(2) == 0 && update(e, rational(sx.length()))) diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index f26b67797..c72fee8a3 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -123,6 +123,7 @@ static void pp_uninterp_sorts(std::ostream & out, ast_printer_context & ctx, mod f_cond = f_conds[0]; format_ref f_s(fm(m)); ctx.pp(s, f_s); + //non-deterministic order no change: too complex format * f_args[2] = { mk_compose(m, mk_string(m, "((x "), mk_indent(m, 4, mk_compose(m, f_s.get(), mk_string(m, "))")))), @@ -252,6 +253,7 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co ctx.pp(e->get_result(), f_result); if (i > 0) f_entries.push_back(mk_line_break(m)); + //non-deterministic order no change: too complex f_entries.push_back(mk_group(m, mk_compose(m, mk_string(m, "(ite "), mk_indent(m, 5, f_entry_cond), @@ -272,7 +274,9 @@ static void pp_funs(std::ostream & out, ast_printer_context & ctx, model_core co fname = mk_smt2_quoted_symbol(f->get_name()); else fname = f->get_name().str(); + //non-deterministic order no change: too complex def = mk_indent(m, indent, mk_compose(m, + //non-deterministic order no change: too complex mk_compose(m, mk_string(m, "(define-fun "), mk_string(m, fname), diff --git a/src/muz/rel/check_relation.cpp b/src/muz/rel/check_relation.cpp index e54714205..087bf3ec2 100644 --- a/src/muz/rel/check_relation.cpp +++ b/src/muz/rel/check_relation.cpp @@ -533,6 +533,7 @@ namespace datalog { unsigned c1 = m_cols[0]; for (unsigned i = 1; i < m_cols.size(); ++i) { unsigned c2 = m_cols[i]; + //non-deterministic order no change: too complex conds.push_back(m.mk_eq(m.mk_var(c1, sig[c1]), m.mk_var(c2, sig[c2]))); } cond = mk_and(m, conds.size(), conds.data()); diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 2377d6e09..6b67795b4 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -454,6 +454,7 @@ namespace datalog { r.get_fact(fact); conjs.reset(); for (unsigned i = 0; i < fact.size(); ++i) { + //non-deterministic order no change: too complex conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); } brw.mk_and(conjs.size(), conjs.data(), fml); diff --git a/src/muz/rel/dl_bound_relation.cpp b/src/muz/rel/dl_bound_relation.cpp index ad8419632..c70f27c53 100644 --- a/src/muz/rel/dl_bound_relation.cpp +++ b/src/muz/rel/dl_bound_relation.cpp @@ -658,16 +658,19 @@ namespace datalog { relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { if (i != find(i)) { + //non-deterministic order no change: too complex conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), m.mk_var(find(i), sig[find(i)]))); continue; } uint_set2 const& upper = (*this)[i]; uint_set::iterator it = upper.lt.begin(), end = upper.lt.end(); for (; it != end; ++it) { + //non-deterministic order no change: too complex conjs.push_back(arith.mk_lt(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it]))); } it = upper.le.begin(), end = upper.le.end(); for (; it != end; ++it) { + //non-deterministic order no change: too complex conjs.push_back(arith.mk_le(m.mk_var(i, sig[i]), m.mk_var(*it, sig[*it]))); } } diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 293cc72e2..1061a192f 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -2363,6 +2363,7 @@ namespace datalog { unsigned rel_idx = static_cast(fact[fact_sz-1]); m_others[rel_idx]->to_formula(tmp); for (unsigned i = 0; i + 1 < fact_sz; ++i) { + //non-deterministic order no change: too complex conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), util.mk_numeral(fact[i], sig[i]))); } sh(tmp, fact_sz-1, tmp); diff --git a/src/muz/rel/dl_interval_relation.cpp b/src/muz/rel/dl_interval_relation.cpp index 81c630ec6..2f095c97a 100644 --- a/src/muz/rel/dl_interval_relation.cpp +++ b/src/muz/rel/dl_interval_relation.cpp @@ -375,6 +375,7 @@ namespace datalog { relation_signature const& sig = get_signature(); for (unsigned i = 0; i < sig.size(); ++i) { if (i != find(i)) { + //non-deterministic order no change: too complex conjs.push_back(m.mk_eq(m.mk_var(i, sig[i]), m.mk_var(find(i), sig[find(i)]))); continue; diff --git a/src/muz/spacer/spacer_convex_closure.cpp b/src/muz/spacer/spacer_convex_closure.cpp index 88a592162..855c13768 100644 --- a/src/muz/spacer/spacer_convex_closure.cpp +++ b/src/muz/spacer/spacer_convex_closure.cpp @@ -378,7 +378,13 @@ void convex_closure::cc_1dim(const expr_ref &var, expr_ref_vector &out) { expr *convex_closure::mk_eq_mod(expr *v, rational d, rational r) { expr *res = nullptr; if (m_arith.is_int(v)) { - res = m.mk_eq(m_arith.mk_mod(v, m_arith.mk_int(d)), m_arith.mk_int(r)); + //non-deterministic order change start + { + auto mk_mod_1 = m_arith.mk_mod(v, m_arith.mk_int(d)); + auto mk_int_2 = m_arith.mk_int(r); + res = m.mk_eq(mk_mod_1, mk_int_2); + } + //non-deterministic order change end } else if (m_bv.is_bv(v)) { res = m.mk_eq(m_bv.mk_bv_urem(v, m_bv.mk_numeral(d, m_bv_sz)), m_bv.mk_numeral(r, m_bv_sz)); diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp index 0fa8ae932..b071af11a 100644 --- a/src/muz/spacer/spacer_generalizers.cpp +++ b/src/muz/spacer/spacer_generalizers.cpp @@ -251,6 +251,7 @@ void lemma_array_eq_generalizer::operator() (lemma_ref &lemma) expr_ref_vector eqs(m); for (unsigned i = 0, sz = vsymbs.size(); i < sz; ++i) { for (unsigned j = i + 1; j < sz; ++j) { + //non-deterministic order no change: too complex eqs.push_back(m.mk_eq(m.mk_const(vsymbs.get(i)), m.mk_const(vsymbs.get(j)))); } diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 609703fb2..5ed6b491e 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -559,6 +559,7 @@ class arith_project_util { tout << "lcm of divs: " << lcm_divs << "\n";); } + //non-deterministic order no change: too complex expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); expr_ref x_term_val(m); @@ -626,8 +627,14 @@ class arith_project_util { // (lcm_coeffs * var_val) % lcm_divs instead rational var_val_num; VERIFY(a.is_numeral(var_val, var_val_num)); - x_term_val = a.mk_numeral( - mod(lcm_coeffs * var_val_num, lcm_divs), a.mk_int()); + //non-deterministic order change start + { + auto mod_1 = mod(lcm_coeffs * var_val_num, lcm_divs); + auto mk_int_2 = a.mk_int(); + x_term_val = a.mk_numeral( + mod_1, mk_int_2); + } + //non-deterministic order change end TRACE(qe, tout << "Substitution for (lcm_coeffs * x): " << mk_pp(x_term_val, m) << "\n";); } @@ -648,6 +655,7 @@ class arith_project_util { // syntactic structure m_rw(new_lit); new_lit = m.mk_eq( + //non-deterministic order no change: too complex a.mk_mod(new_lit, a.mk_numeral(m_divs[i], a.mk_int())), z); } else if (m_eq[i] || (num_pos == 0 && m_coeffs[i].is_pos()) || @@ -738,6 +746,7 @@ class arith_project_util { mk_add(m_terms.get(max_t), a.mk_numeral(offset, a.mk_int())); if (m_strict[max_t]) { x_term_val = a.mk_add( + //non-deterministic order no change: too complex x_term_val, a.mk_numeral(rational::one(), a.mk_int())); } if (m_coeffs[max_t].is_pos()) { @@ -976,6 +985,7 @@ class arith_project_util { return; } + //non-deterministic order no change: too complex expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); bool is_mod_eq = false; @@ -1021,6 +1031,7 @@ class arith_project_util { lits.push_back(a.mk_le(z, t2)); // t2 < abs (num_val) lits.push_back( + //non-deterministic order no change: too complex a.mk_lt(t2, a.mk_numeral(abs(num_val), a.mk_int()))); new_fml = m.mk_and(lits.size(), lits.data()); @@ -1073,6 +1084,7 @@ class arith_project_util { */ void mk_lit_substitutes(expr_ref const &x_term_val, expr_map &map, unsigned idx) { + //non-deterministic order no change: too complex expr_ref z(a.mk_numeral(rational::zero(), a.mk_int()), m); expr_ref cxt(m), new_lit(m); for (unsigned i = 0; i < m_lits.size(); ++i) { @@ -1101,6 +1113,7 @@ class arith_project_util { // top-level operator m_rw(cxt); new_lit = m.mk_eq( + //non-deterministic order no change: too complex a.mk_mod(cxt, a.mk_numeral(m_divs[i], a.mk_int())), z); } } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index dd75f86e8..10f839833 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -359,8 +359,14 @@ void expand_literals(ast_manager &m, expr_ref_vector &conjs) { rational two(2); for (unsigned j = 0; j < bv_size; ++j) { parameter p(j); - expr *e = m.mk_eq(m.mk_app(bv.get_family_id(), OP_BIT1), - bv.mk_extract(j, j, c)); + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(bv.get_family_id(), OP_BIT1); + auto mk_extract_2 = bv.mk_extract(j, j, c); + expr *e = m.mk_eq(mk_app_1, + mk_extract_2); + } + //non-deterministic order change end if ((r % two).is_zero()) { e = m.mk_not(e); } r = div(r, two); if (j == 0) diff --git a/src/muz/transforms/dl_mk_array_blast.cpp b/src/muz/transforms/dl_mk_array_blast.cpp index 16f09f24c..b6308023b 100644 --- a/src/muz/transforms/dl_mk_array_blast.cpp +++ b/src/muz/transforms/dl_mk_array_blast.cpp @@ -227,6 +227,7 @@ namespace datalog { for (unsigned j = 0; j < args1.size(); ++j) { eqs.push_back(m.mk_eq(args1[j], args2[j])); } + //non-deterministic order no change: too complex conjs.push_back(m.mk_implies(m.mk_and(eqs.size(), eqs.data()), m.mk_eq(v1, v2))); } } diff --git a/src/muz/transforms/dl_mk_scale.cpp b/src/muz/transforms/dl_mk_scale.cpp index b6178bb81..724fac7fc 100644 --- a/src/muz/transforms/dl_mk_scale.cpp +++ b/src/muz/transforms/dl_mk_scale.cpp @@ -55,6 +55,7 @@ namespace datalog { for (unsigned i = 0; i < old_p->get_arity(); ++i) { subst.push_back(m.mk_var(i, old_p->get_domain(i))); } + //non-deterministic order no change: too complex subst.push_back(a.mk_numeral(rational(1), a.mk_real())); SASSERT(!new_fi->is_partial() && new_fi->num_entries() == 0); diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 388befe93..d0a9ec931 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1066,6 +1066,7 @@ namespace opt { expr_ref_vector soft(m); for (unsigned k = 1; k <= min_cardinality; ++k) { auto p_k = m.mk_fresh_const("p", m.mk_bool_sort()); + //non-deterministic order no change: too complex soft.push_back(m.mk_ite(p_k, a.mk_int(1), a.mk_int(0))); for (auto c : cardinalities) // p_k => c >= k diff --git a/src/qe/mbp/mbp_arith.cpp b/src/qe/mbp/mbp_arith.cpp index b7b896640..516b8185b 100644 --- a/src/qe/mbp/mbp_arith.cpp +++ b/src/qe/mbp/mbp_arith.cpp @@ -577,7 +577,13 @@ namespace mbp { case opt::t_le: t = a.mk_le(t, s); break; case opt::t_eq: t = a.mk_eq(t, s); break; case opt::t_divides: - t = a.mk_eq(a.mk_mod(t, a.mk_int(r.m_mod)), a.mk_int(0)); + //non-deterministic order change start + { + auto mk_mod_1 = a.mk_mod(t, a.mk_int(r.m_mod)); + auto mk_int_2 = a.mk_int(0); + t = a.mk_eq(mk_mod_1, mk_int_2); + } + //non-deterministic order change end break; default: UNREACHABLE(); diff --git a/src/qe/mbp/mbp_arrays.cpp b/src/qe/mbp/mbp_arrays.cpp index 201096bcd..c5bba387c 100644 --- a/src/qe/mbp/mbp_arrays.cpp +++ b/src/qe/mbp/mbp_arrays.cpp @@ -866,8 +866,14 @@ namespace mbp { SASSERT(xs.size() == ys.size() && !xs.empty()); expr_ref result(mk_lt(xs.back(), ys.back()), m); for (unsigned i = xs.size()-1; i-- > 0; ) { - result = m.mk_or(mk_lt(xs[i], ys[i]), - m.mk_and(m.mk_eq(xs[i], ys[i]), result)); + //non-deterministic order change start + { + auto mk_lt_1 = mk_lt(xs[i], ys[i]); + auto mk_and_2 = m.mk_and(m.mk_eq(xs[i], ys[i]), result); + result = m.mk_or(mk_lt_1, + mk_and_2); + } + //non-deterministic order change end } return result; } diff --git a/src/qe/mbp/mbp_solve_plugin.cpp b/src/qe/mbp/mbp_solve_plugin.cpp index 6770e335b..34aa0deab 100644 --- a/src/qe/mbp/mbp_solve_plugin.cpp +++ b/src/qe/mbp/mbp_solve_plugin.cpp @@ -287,8 +287,14 @@ namespace mbp { }; // `first` is a value, different from 0 - res = m.mk_and(m.mk_eq(second, a.mk_idiv(lhs, first)), + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(second, a.mk_idiv(lhs, first)); + res = m.mk_and(mk_eq_1, + //non-deterministic order no change: too complex m.mk_eq(a.mk_int(0), a.mk_mod(lhs, first))); + } + //non-deterministic order change end return true; } diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index 60ff87537..828ed2b40 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -389,6 +389,7 @@ namespace nlarith { }; expr* mk_abs(expr* e) { + //non-deterministic order no change: too complex return m().mk_ite(mk_lt(e), mk_uminus(e), e); } @@ -405,6 +406,7 @@ namespace nlarith { } else { expr* half = A.mk_numeral(rational(1,2), false); + //non-deterministic order no change: too complex result = A.mk_div(mk_add(s.m_a, mk_mul(num(s.m_b), A.mk_power(mk_abs(s.m_c), half))), s.m_d); } return result; @@ -439,10 +441,13 @@ namespace nlarith { expr* result = to_expr(s); if (is_strict(cmp)) { if (p.m_a == z()) { + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex result = mk_add(result, mk_mul(mk_epsilon(), m().mk_ite(mk_lt(p.m_b),num(1),num(-1)))); } else { if (s.m_b > 0) { + //non-deterministic order no change: too complex result = mk_add(result, mk_mul(num(-1),mk_epsilon())); } else { @@ -481,6 +486,7 @@ namespace nlarith { } app* sq1(expr * e) { + //non-deterministic order no change: too complex return mk_add(num(1), sq(e)); } @@ -591,7 +597,13 @@ namespace nlarith { app_ref t1(m()), a2(m()), d(m()); expr_ref cond(m()), t2(m()), branch(m()); expr_ref_vector es(m()), subst(m()); - d = mk_sub(mk_mul(b,b), mk_mul(num(4), a, c)); + //non-deterministic order change start + { + auto mk_mul_1 = mk_mul(b,b); + auto mk_mul_2 = mk_mul(num(4), a, c); + d = mk_sub(mk_mul_1, mk_mul_2); + } + //non-deterministic order change end a2 = mk_mul(a, num(2)); TRACE(nlarith, @@ -1054,9 +1066,23 @@ namespace nlarith { r = I.mk_lt(ad); } else { - aabbc = I.mk_sub(I.mk_mul(a,a), I.mk_mul(b,b,c)); - r = I.mk_or(I.mk_and(I.mk_lt(ad), I.mk_gt(aabbc)), + //non-deterministic order change start + { + auto mk_mul_1 = I.mk_mul(a,a); + auto mk_mul_2 = I.mk_mul(b,b,c); + aabbc = I.mk_sub(mk_mul_1, mk_mul_2); + } + //non-deterministic order change end + //non-deterministic order no change: too complex + //non-deterministic order change start + { + auto mk_and_1 = I.mk_and(I.mk_lt(ad), I.mk_gt(aabbc)); + r = I.mk_or(mk_and_1, + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex I.mk_and(I.mk_le(bd), I.mk_or(I.mk_lt(ad), I.mk_lt(aabbc)))); + } + //non-deterministic order change end } } @@ -1071,8 +1097,20 @@ namespace nlarith { r = I.mk_eq(a); } else { - aabbc = I.mk_sub(I.mk_mul(a, a), I.mk_mul(b, b, c)); - r = I.mk_and(I.mk_le(I.mk_mul(a, b)), I.mk_eq(aabbc)); + //non-deterministic order change start + { + auto mk_mul_1 = I.mk_mul(a, a); + auto mk_mul_2 = I.mk_mul(b, b, c); + aabbc = I.mk_sub(mk_mul_1, mk_mul_2); + } + //non-deterministic order change end + //non-deterministic order change start + { + auto mk_le_1 = I.mk_le(I.mk_mul(a, b)); + auto mk_eq_2 = I.mk_eq(aabbc); + r = I.mk_and(mk_le_1, mk_eq_2); + } + //non-deterministic order change end } } @@ -1091,9 +1129,22 @@ namespace nlarith { r = I.mk_le(ad); } else { - aabbc = I.mk_sub(I.mk_mul(a, a), I.mk_mul(b, b, c)); - r = I.mk_or(I.mk_and(I.mk_le(ad), I.mk_ge(aabbc)), + //non-deterministic order change start + { + auto mk_mul_1 = I.mk_mul(a, a); + auto mk_mul_2 = I.mk_mul(b, b, c); + aabbc = I.mk_sub(mk_mul_1, mk_mul_2); + } + //non-deterministic order change end + //non-deterministic order no change: too complex + //non-deterministic order change start + { + auto mk_and_1 = I.mk_and(I.mk_le(ad), I.mk_ge(aabbc)); + r = I.mk_or(mk_and_1, + //non-deterministic order no change: too complex I.mk_and(I.mk_le(bd), I.mk_le(aabbc))); + } + //non-deterministic order change end } } }; @@ -1203,6 +1254,7 @@ namespace nlarith { return e; } else { + //non-deterministic order no change: too complex return I.mk_or(e, I.mk_and(I.mk_eq(t), mk_lt(p, i))); } } @@ -1233,6 +1285,7 @@ namespace nlarith { return e; } else { + //non-deterministic order no change: too complex return I.mk_or(e, I.mk_and(I.mk_eq(t), mk_lt(p, i))); } } @@ -1311,8 +1364,15 @@ namespace nlarith { // = // (d*dr*p[i] + a*ar + b*br*c + (a*br + ar*b)*sqrt(c))/d*dr // + //non-deterministic order no change: too complex app_ref tmp1(mk_add(mk_mul(d, dr, p[i]), mk_mul(a, ar), mk_mul(b, br, c)), m()); - br = mk_add(mk_mul(a, br), mk_mul(ar, b)); + //non-deterministic order change start + { + auto mk_mul_1 = mk_mul(a, br); + auto mk_mul_2 = mk_mul(ar, b); + br = mk_add(mk_mul_1, mk_mul_2); + } + //non-deterministic order change end dr = mk_mul(d, dr); ar = tmp1; } diff --git a/src/qe/nlqsat.cpp b/src/qe/nlqsat.cpp index 66da9d707..1389bbca0 100644 --- a/src/qe/nlqsat.cpp +++ b/src/qe/nlqsat.cpp @@ -656,6 +656,7 @@ namespace qe { expr_ref den_is0(m.mk_eq(divs[i].den, arith.mk_real(0)), m); paxioms.push_back(m.mk_or(den_is0, m.mk_eq(divs[i].num, arith.mk_mul(divs[i].den, divs[i].name)))); for (unsigned j = i + 1; j < divs.size(); ++j) { + //non-deterministic order no change: too complex paxioms.push_back(m.mk_or(m.mk_not(m.mk_eq(divs[i].den, divs[j].den)), m.mk_not(m.mk_eq(divs[i].num, divs[j].num)), m.mk_eq(divs[i].name, divs[j].name))); @@ -665,6 +666,7 @@ namespace qe { expr_ref v0(m.mk_var(0, arith.mk_real()), m); expr_ref v1(m.mk_var(1, arith.mk_real()), m); for (auto const& p : divs) { + //non-deterministic order no change: too complex body = m.mk_ite(m.mk_and(m.mk_eq(v0, p.num), m.mk_eq(v1, p.den)), p.name, body); } m_div_mc->add(arith.mk_div0(), body); diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 05b611644..f2315d836 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -468,7 +468,13 @@ namespace qe { // ax + t = 0 void mk_eq(rational const& a, app* x, expr* t, expr_ref& result) { - result = m_arith.mk_eq(mk_add(mk_mul(a, x), t), mk_zero(x)); + //non-deterministic order change start + { + auto mk_add_1 = mk_add(mk_mul(a, x), t); + auto mk_zero_2 = mk_zero(x); + result = m_arith.mk_eq(mk_add_1, mk_zero_2); + } + //non-deterministic order change end } void mk_and(unsigned sz, expr*const* args, expr_ref& result) { diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 49736e4c3..ef816a822 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -262,7 +262,13 @@ namespace arith { // x mod 2^{i + 1} >= 2^i means the i'th bit is 1. auto bitof = [&](expr* x, unsigned i) { expr_ref r(m); - r = a.mk_ge(a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))), a.mk_int(rational::power_of_two(i))); + //non-deterministic order change start + { + auto mk_mod_1 = a.mk_mod(x, a.mk_int(rational::power_of_two(i+1))); + auto mk_int_2 = a.mk_int(rational::power_of_two(i)); + r = a.mk_ge(mk_mod_1, mk_int_2); + } + //non-deterministic order change end return mk_literal(r); }; @@ -390,8 +396,11 @@ namespace arith { // y >= sz & x >= 2^{sz-1} => n = -1 // y = 0 => n = x auto signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); + //non-deterministic order no change: too complex add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), signx, mk_literal(m.mk_eq(n, a.mk_int(0)))); + //non-deterministic order no change: too complex add_clause(~mk_literal(a.mk_ge(a.mk_mod(y, a.mk_int(N)), a.mk_int(sz))), ~signx, mk_literal(m.mk_eq(n, a.mk_int(N-1)))); + //non-deterministic order no change: too complex add_clause(~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x))); } else diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp index d48374081..6b63a3581 100644 --- a/src/sat/smt/q_solver.cpp +++ b/src/sat/smt/q_solver.cpp @@ -341,7 +341,13 @@ namespace q { } if (m.is_not(arg, z) && m.is_iff(z, x, y) && is_literal(x) && is_literal(y)) { e1 = m.mk_or(x, y); - e2 = m.mk_or(mk_not(m, x), mk_not(m, y)); + //non-deterministic order change start + { + auto mk_not_1 = mk_not(m, x); + auto mk_not_2 = mk_not(m, y); + e2 = m.mk_or(mk_not_1, mk_not_2); + } + //non-deterministic order change end return true; } return false; diff --git a/src/sat/tactic/sat2goal.cpp b/src/sat/tactic/sat2goal.cpp index ab8b8d8ee..d54e78332 100644 --- a/src/sat/tactic/sat2goal.cpp +++ b/src/sat/tactic/sat2goal.cpp @@ -253,6 +253,7 @@ struct sat2goal::imp { s.collect_bin_clauses(bin_clauses, m_learned, false); for (sat::solver::bin_clause const& bc : bin_clauses) { checkpoint(); + //non-deterministic order no change: too complex r.assert_expr(m.mk_or(lit2expr(mc, bc.first), lit2expr(mc, bc.second))); } // collect clauses diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 64487a21e..a4feb1118 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -396,6 +396,7 @@ namespace smt { else if (re().is_empty(r2)) r = r1; else + //non-deterministic order no change: too complex r = re().mk_union(re().mk_diff(r1, r2), re().mk_diff(r2, r1)); rewrite(r); return r; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 9d1775a3b..6062edf7a 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -360,7 +360,13 @@ namespace smt { ctx.mark_as_relevant(sel1_eq_sel2); if (m.has_trace_stream()) { app_ref body(m); - body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))); + //non-deterministic order change start + { + auto mk_not_1 = m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())); + auto mk_not_2 = m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var())); + body = m.mk_implies(mk_not_1, mk_not_2); + } + //non-deterministic order change end log_axiom_instantiation(body); } assert_axiom(n1_eq_n2, ~sel1_eq_sel2); diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 7b0afd7e1..241861538 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -241,6 +241,8 @@ namespace smt { expr_ref eq(m.mk_eq(e1, e2), m); literal l = ~mk_literal(eq); std::function logfn = [&]() { + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq)); }; scoped_trace_stream ts(*this, logfn); @@ -456,6 +458,7 @@ namespace smt { e2 = mk_bit2bool(o2, i); literal eq = mk_eq(e1, e2, true); std::function logfn = [&]() { + //non-deterministic order no change: too complex return m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var()))); }; scoped_trace_stream st(*this, logfn); diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp index a5a52b4b2..98bc60239 100644 --- a/src/smt/theory_char.cpp +++ b/src/smt/theory_char.cpp @@ -259,6 +259,7 @@ namespace smt { unsigned p = 0; arith_util a(m); for (auto b : bits) { + //non-deterministic order no change: too complex sum.push_back(m.mk_ite(b, a.mk_int(1 << p), a.mk_int(0))); p++; } diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d541781ea..98720c7db 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -247,6 +247,7 @@ namespace smt { assert_eq_axiom(arg, acc_own, is_con); } // update_field is identity if 'n' is not created by a matching constructor. + //non-deterministic order no change: too complex app_ref imp(m.mk_implies(m.mk_not(rec_app), m.mk_eq(n->get_expr(), arg1)), m); assert_eq_axiom(n, arg1, ~is_con); diff --git a/src/smt/theory_dl.cpp b/src/smt/theory_dl.cpp index 822f7b0e7..309f38a1e 100644 --- a/src/smt/theory_dl.cpp +++ b/src/smt/theory_dl.cpp @@ -252,6 +252,7 @@ namespace smt { get_rep(s, r, v); app_ref lt(m()), le(m()); lt = u().mk_lt(x,y); + //non-deterministic order no change: too complex le = b().mk_ule(m().mk_app(r,y),m().mk_app(r,x)); if (m().has_trace_stream()) { app_ref body(m()); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2c58400ba..909978399 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2589,6 +2589,7 @@ public: if (valy >= sz || valy == 0) return true; unsigned k = valy.get_unsigned(); + //non-deterministic order no change: too complex sat::literal signx = mk_literal(a.mk_ge(x, a.mk_int(N/2))); sat::literal eq; expr* xdiv2k; @@ -3371,7 +3372,13 @@ public: tout << " ==> " << pp(x) << " = " << pp(y) << "\n"; ); - std::function fn = [&]() { return m.mk_eq(x->get_expr(), y->get_expr()); }; + std::function fn = [&]() { //non-deterministic order change start + { + auto get_expr_1 = x->get_expr(); + auto get_expr_2 = y->get_expr(); + return m.mk_eq(get_expr_1, get_expr_2); + } + //non-deterministic order change end }; scoped_trace_stream _sts(th, fn); if (params().m_arith_validate) @@ -3871,6 +3878,7 @@ public: flet _svalid(s_validating, true); context nctx(m, ctx().get_fparams(), ctx().get_params()); add_background(nctx); + //non-deterministic order no change: too complex expr_ref neq(m.mk_not(m.mk_eq(x->get_expr(), y->get_expr())), m); nctx.assert_expr(neq); cancel_eh eh(m.limit()); diff --git a/src/smt/theory_special_relations.cpp b/src/smt/theory_special_relations.cpp index 9daf3ab2e..e69606a16 100644 --- a/src/smt/theory_special_relations.cpp +++ b/src/smt/theory_special_relations.cpp @@ -803,7 +803,13 @@ namespace smt { r.pop(1); fi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(fn, fi); - result = arith.mk_le(m.mk_app(fn,m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(fn,m.mk_var(0, *ty)); + auto mk_app_2 = m.mk_app(fn, m.mk_var(1, *ty)); + result = arith.mk_le(mk_app_1, mk_app_2); + } + //non-deterministic order change end return result; } @@ -823,7 +829,13 @@ namespace smt { } fi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(fn, fi); - result = m.mk_eq(m.mk_app(fn, m.mk_var(0, *ty)), m.mk_app(fn, m.mk_var(1, *ty))); + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(fn, m.mk_var(0, *ty)); + auto mk_app_2 = m.mk_app(fn, m.mk_var(1, *ty)); + result = m.mk_eq(mk_app_1, mk_app_2); + } + //non-deterministic order change end return result; } @@ -848,7 +860,9 @@ namespace smt { hifi->set_else(arith.mk_numeral(rational(0), true)); mg.get_model().register_decl(lofn, lofi); mg.get_model().register_decl(hifn, hifi); + //non-deterministic order no change: too complex result = m.mk_and(arith.mk_le(m.mk_app(lofn, m.mk_var(0, *ty)), m.mk_app(lofn, m.mk_var(1, *ty))), + //non-deterministic order no change: too complex arith.mk_le(m.mk_app(hifn, m.mk_var(1, *ty)), m.mk_app(hifn, m.mk_var(0, *ty)))); return result; } @@ -923,11 +937,17 @@ namespace smt { expr* x = xV, *S = SV; expr_ref mem_body(m); - mem_body = m.mk_ite(m.mk_app(is_nil, S), + //non-deterministic order change start + { + auto mk_app_1 = m.mk_app(is_nil, S); + mem_body = m.mk_ite(mk_app_1, F, + //non-deterministic order no change: too complex m.mk_ite(m.mk_eq(m.mk_app(hd, S), x), T, - m.mk_app(memf, x, m.mk_app(tl, S)))); + m.mk_app(memf, x, m.mk_app(tl, S)))); + } + //non-deterministic order change end recfun_replace rep(m); var* vars[2] = { xV, SV }; p.set_definition(rep, mem, false, 2, vars, mem_body); @@ -947,9 +967,16 @@ namespace smt { var_ref SV(m.mk_var(1, listS), m); var_ref tupV(m.mk_var(0, tup), m); expr* a = aV, *b = bV, *A = AV, *S = SV, *t = tupV; - next_body = m.mk_ite(m.mk_and(m.mk_app(memf, a, A), m.mk_not(m.mk_app(memf, b, S))), - m.mk_app(pair, m.mk_app(cons, b, m.mk_app(fst, t)), m.mk_app(cons, b, m.mk_app(snd, t))), + //non-deterministic order no change: too complex + //non-deterministic order change start + { + auto mk_and_1 = m.mk_and(m.mk_app(memf, a, A), m.mk_not(m.mk_app(memf, b, S))); + auto mk_app_2 = m.mk_app(pair, m.mk_app(cons, b, m.mk_app(fst, t)), m.mk_app(cons, b, m.mk_app(snd, t))); + next_body = m.mk_ite(mk_and_1, + mk_app_2, t); + } + //non-deterministic order change end recfun_replace rep(m); var* vars[5] = { aV, bV, AV, SV, tupV }; @@ -981,9 +1008,15 @@ namespace smt { expr_ref Ap(m.mk_app(fst, connected_body.get()), m); expr_ref Sp(m.mk_app(snd, connected_body.get()), m); - connected_body = m.mk_ite(m.mk_eq(Ap, nilc), F, + //non-deterministic order change start + { + auto mk_eq_1 = m.mk_eq(Ap, nilc); + connected_body = m.mk_ite(mk_eq_1, F, + //non-deterministic order no change: too complex m.mk_ite(m.mk_app(memf, dst, Ap), T, m.mk_app(connectedf, Ap, dst, Sp))); + } + //non-deterministic order change end TRACE(special_relations, tout << connected_body << "\n";); recfun_replace rep(m); diff --git a/src/tactic/aig/aig.cpp b/src/tactic/aig/aig.cpp index fe66fcbfd..e0fcb6da7 100644 --- a/src/tactic/aig/aig.cpp +++ b/src/tactic/aig/aig.cpp @@ -879,10 +879,23 @@ struct aig_manager::imp { } expr * r; if (m.is_not_eq(t, e)) { - r = ast_mng.mk_iff(get_cached(c), get_cached(t)); + //non-deterministic order change start + { + auto get_cached_1 = get_cached(c); + auto get_cached_2 = get_cached(t); + r = ast_mng.mk_iff(get_cached_1, get_cached_2); + } + //non-deterministic order change end } else { - r = ast_mng.mk_ite(get_cached(c), get_cached(t), get_cached(e)); + //non-deterministic order change start + { + auto get_cached_1 = get_cached(c); + auto get_cached_2 = get_cached(t); + auto get_cached_3 = get_cached(e); + r = ast_mng.mk_ite(get_cached_1, get_cached_2, get_cached_3); + } + //non-deterministic order change end } cache_result(n, r); TRACE(aig2expr, tout << "caching ITE/IFF "; m.display_ref(tout, n); tout << "\n";); diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index cf1cb5c79..3b6dfd65d 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -443,9 +443,11 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re expr_ref gt_proxy(m().mk_not(le_proxy), m()); expr_ref s2_is_nonpos(m_bv.mk_sle(s2, m_bv.mk_numeral(rational(0), s2_size)), m()); + //non-deterministic order no change: too complex expr_ref under(u().mk_bv_add(u().mk_bv_mul(rational(4), s1), u().mk_bv_mul(rational(5), s2)), m()); expr_ref z1(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(under)), m()); expr_ref le_under(m_bv.mk_sle(under, z1), m()); + //non-deterministic order no change: too complex expr_ref over(u().mk_bv_add(u().mk_bv_mul(rational(2), s1), u().mk_bv_mul(rational(3), s2)), m()); expr_ref z2(m_bv.mk_numeral(rational(0), m_bv.get_bv_size(over)), m()); expr_ref le_over(m_bv.mk_sle(over, z2), m()); @@ -462,8 +464,10 @@ bool bv2real_rewriter::mk_le(expr* s, expr* t, bool is_pos, bool is_neg, expr_re // predicate may occur in negative polarity. if (is_neg) { // s1 + s2*sqrt(2) > 0 <== s2 > 0 & s1 + s2*(5/4) > 0; 4*s1 + 5*s2 > 0 + //non-deterministic order no change: too complex expr* e3 = m().mk_implies(m().mk_and(gt_proxy, m().mk_not(s2_is_nonpos)), m().mk_not(le_under)); // s1 + s2*sqrt(2) > 0 <== s2 <= 0 & s1 + s2*(3/2) > 0 <=> 2*s1 + 3*s2 > 0 + //non-deterministic order no change: too complex expr* e4 = m().mk_implies(m().mk_and(gt_proxy, s2_is_nonpos), m().mk_not(le_over)); u().add_side_condition(e3); u().add_side_condition(e4); @@ -543,7 +547,9 @@ br_status bv2real_rewriter::mk_le(expr * s, expr * t, expr_ref & result) { expr* ge = m_bv.mk_sle(t22, t12); expr* le = m_bv.mk_sle(t12, t22); expr* e1 = m().mk_or(gz1, gz2); + //non-deterministic order no change: too complex expr* e2 = m().mk_or(m().mk_not(gz1), m().mk_not(lz2), ge); + //non-deterministic order no change: too complex expr* e3 = m().mk_or(m().mk_not(gz2), m().mk_not(lz1), le); result = m().mk_and(e1, e2, e3); TRACE(bv2real_rewriter, tout << "\n";); @@ -587,6 +593,7 @@ br_status bv2real_rewriter::mk_eq(expr * s, expr * t, expr_ref & result) { u().align_divisors(s1, s2, t1, t2, d1, d2); u().align_sizes(s1, t1); u().align_sizes(s2, t2); + //non-deterministic order no change: too complex result = m().mk_and(m().mk_eq(s1, t1), m().mk_eq(s2, t2)); return BR_DONE; } @@ -650,7 +657,9 @@ br_status bv2real_rewriter::mk_mul(expr* s, expr* t, expr_ref& result) { if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) { // s1*t1 + r1*(s2*t2) + (s1*t2 + s2*t2)*r1 expr_ref u1(m()), u2(m()); + //non-deterministic order no change: too complex u1 = u().mk_bv_add(u().mk_bv_mul(s1, t1), u().mk_bv_mul(r1, u().mk_bv_mul(t2, s2))); + //non-deterministic order no change: too complex u2 = u().mk_bv_add(u().mk_bv_mul(s1, t2), u().mk_bv_mul(s2, t1)); rational tmp = d1*d2; if (u().mk_bv2real(u1, u2, tmp, r1, result)) { diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 9438ccd09..0a9b2bb72 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -63,7 +63,13 @@ class factor_tactic : public tactic { m_expr2poly.to_expr(fs[i], true, arg); args.push_back(arg); } - result = m.mk_eq(mk_mul(args.size(), args.data()), mk_zero_for(arg)); + //non-deterministic order change start + { + auto size_1 = mk_mul(args.size(), args.data()); + auto mk_zero_for_2 = mk_zero_for(arg); + result = m.mk_eq(size_1, mk_zero_for_2); + } + //non-deterministic order change end } // p1^k1 * p2^k2 = 0 --> p1 = 0 or p2 = 0 diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index d1133cccc..c6335adc8 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -260,6 +260,7 @@ public: return m_pb.mk_eq(sz, weights, args, w); } else { + //non-deterministic order no change: too complex return m.mk_and(mk_ge(sz, weights, args, w), mk_le(sz, weights, args, w)); } } diff --git a/src/tactic/arith/pb2bv_tactic.cpp b/src/tactic/arith/pb2bv_tactic.cpp index de4eaea25..2d7774d35 100644 --- a/src/tactic/arith/pb2bv_tactic.cpp +++ b/src/tactic/arith/pb2bv_tactic.cpp @@ -623,8 +623,14 @@ private: if (is_uninterp_const(lhs) && is_uninterp_const(rhs)) { add_bounds_dependencies(lhs); add_bounds_dependencies(rhs); - r = m.mk_iff(mon_lit2lit(lit(lhs, false)), - mon_lit2lit(lit(rhs, !pos))); + //non-deterministic order change start + { + auto mon_lit2lit_1 = mon_lit2lit(lit(lhs, false)); + auto mon_lit2lit_2 = mon_lit2lit(lit(rhs, !pos)); + r = m.mk_iff(mon_lit2lit_1, + mon_lit2lit_2); + } + //non-deterministic order change end return; } k = EQ; @@ -807,6 +813,7 @@ private: for (unsigned i = 0; i < sz; i += 2) { app * x_i = to_app(m_p[i].m_lit.var()); app * y_i = to_app(m_p[i+1].m_lit.var()); + //non-deterministic order no change: too complex eqs.push_back(m.mk_eq(int2lit(x_i), int2lit(y_i))); } m_b_rw.mk_and(eqs.size(), eqs.data(), r); diff --git a/src/tactic/arith/purify_arith_tactic.cpp b/src/tactic/arith/purify_arith_tactic.cpp index 86352510e..f477b4675 100644 --- a/src/tactic/arith/purify_arith_tactic.cpp +++ b/src/tactic/arith/purify_arith_tactic.cpp @@ -331,12 +331,14 @@ struct purify_arith_proc { expr * x = args[0]; expr * y = args[1]; // y = 0 \/ y*k = x + //non-deterministic order no change: too complex push_cnstr(OR(EQ(y, mk_real_zero()), EQ(u().mk_mul(y, k), x))); push_cnstr_pr(result_pr); rational r; if (complete()) { // y != 0 \/ k = div-0(x) + //non-deterministic order no change: too complex push_cnstr(OR(NOT(EQ(y, mk_real_zero())), EQ(k, u().mk_div(x, mk_real_zero())))); push_cnstr_pr(result_pr); @@ -375,6 +377,7 @@ struct purify_arith_proc { // y < 0 implies k2 < -y ---> y >= 0 \/ k2 < -y // expr * zero = mk_int_zero(); + //non-deterministic order no change: too complex push_cnstr(OR(EQ(y, zero), EQ(x, u().mk_add(u().mk_mul(k1, y), k2)))); push_cnstr_pr(result_pr, mod_pr); @@ -389,9 +392,11 @@ struct purify_arith_proc { rational r; if (complete() && (!u().is_numeral(y, r) || r.is_zero())) { + //non-deterministic order no change: too complex push_cnstr(OR(NOT(EQ(y, zero)), EQ(k1, u().mk_idiv(x, zero)))); push_cnstr_pr(result_pr); + //non-deterministic order no change: too complex push_cnstr(OR(NOT(EQ(y, zero)), EQ(k2, u().mk_mod(x, zero)))); push_cnstr_pr(mod_pr); } @@ -463,8 +468,10 @@ struct purify_arith_proc { } // (^ x 0) --> k | x != 0 implies k = 1, x = 0 implies k = 0^0 + //non-deterministic order no change: too complex push_cnstr(OR(EQ(x, zero), EQ(k, one))); push_cnstr_pr(result_pr); + //non-deterministic order no change: too complex push_cnstr(OR(NOT(EQ(x, zero)), EQ(k, p0))); push_cnstr_pr(result_pr); } @@ -482,6 +489,7 @@ struct purify_arith_proc { SASSERT(n.is_even()); // (^ x (/ 1 n)) --> k | x >= 0 implies (x = k^n and k >= 0), x < 0 implies k = neg-root(x, n) // when n is even + //non-deterministic order no change: too complex push_cnstr(OR(NOT(u().mk_ge(x, zero)), AND(EQ(x, u().mk_power(k, u().mk_numeral(n, false))), u().mk_ge(k, zero)))); @@ -600,8 +608,11 @@ struct purify_arith_proc { expr * pi2 = u().mk_mul(u().mk_numeral(rational(1,2), false), u().mk_pi()); expr * mpi2 = u().mk_mul(u().mk_numeral(rational(-1,2), false), u().mk_pi()); // -1 <= x <= 1 implies sin(k) = x, -pi/2 <= k <= pi/2 + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex push_cnstr(OR(OR(NOT(u().mk_ge(x, mone)), NOT(u().mk_le(x, one))), + //non-deterministic order no change: too complex AND(EQ(x, u().mk_sin(k)), AND(u().mk_ge(k, mpi2), u().mk_le(k, pi2))))); @@ -642,8 +653,11 @@ struct purify_arith_proc { expr * pi = u().mk_pi(); expr * zero = u().mk_numeral(rational(0), false); // -1 <= x <= 1 implies cos(k) = x, 0 <= k <= pi + //non-deterministic order no change: too complex + //non-deterministic order no change: too complex push_cnstr(OR(OR(NOT(u().mk_ge(x, mone)), NOT(u().mk_le(x, one))), + //non-deterministic order no change: too complex AND(EQ(x, u().mk_cos(k)), AND(u().mk_ge(k, zero), u().mk_le(k, pi))))); @@ -678,6 +692,7 @@ struct purify_arith_proc { // tan(k) = x, -pi/2 < k < pi/2 expr * pi2 = u().mk_mul(u().mk_numeral(rational(1,2), false), u().mk_pi()); expr * mpi2 = u().mk_mul(u().mk_numeral(rational(-1,2), false), u().mk_pi()); + //non-deterministic order no change: too complex push_cnstr(AND(EQ(x, u().mk_tan(k)), AND(u().mk_gt(k, mpi2), u().mk_lt(k, pi2)))); @@ -804,7 +819,9 @@ struct purify_arith_proc { auto const& p1 = divs[i]; for (unsigned j = i + 1; j < divs.size(); ++j) { auto const& p2 = divs[j]; + //non-deterministic order no change: too complex m_goal.assert_expr(m().mk_implies( + //non-deterministic order no change: too complex m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), m().mk_eq(p1.d, p2.d))); } @@ -813,7 +830,9 @@ struct purify_arith_proc { auto const& p1 = mods[i]; for (unsigned j = i + 1; j < mods.size(); ++j) { auto const& p2 = mods[j]; + //non-deterministic order no change: too complex m_goal.assert_expr(m().mk_implies( + //non-deterministic order no change: too complex m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), m().mk_eq(p1.d, p2.d))); } @@ -822,7 +841,9 @@ struct purify_arith_proc { auto const& p1 = idivs[i]; for (unsigned j = i + 1; j < idivs.size(); ++j) { auto const& p2 = idivs[j]; + //non-deterministic order no change: too complex m_goal.assert_expr(m().mk_implies( + //non-deterministic order no change: too complex m().mk_and(m().mk_eq(p1.x, p2.x), m().mk_eq(p1.y, p2.y)), m().mk_eq(p1.d, p2.d))); } @@ -843,6 +864,7 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_real()), m()); expr_ref v1(m().mk_var(1, u().mk_real()), m()); for (auto const& p : divs) { + //non-deterministic order no change: too complex body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); } fmc->add(u().mk_div0(), body); @@ -852,6 +874,7 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_int()), m()); expr_ref v1(m().mk_var(1, u().mk_int()), m()); for (auto const& p : mods) { + //non-deterministic order no change: too complex body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); } @@ -864,6 +887,7 @@ struct purify_arith_proc { expr_ref v0(m().mk_var(0, u().mk_int()), m()); expr_ref v1(m().mk_var(1, u().mk_int()), m()); for (auto const& p : idivs) { + //non-deterministic order no change: too complex body = m().mk_ite(m().mk_and(m().mk_eq(v0, p.x), m().mk_eq(v1, p.y)), p.d, body); } fmc->add(u().mk_idiv0(), body); @@ -881,6 +905,7 @@ struct purify_arith_proc { for (auto const& kv : m_sin_cos) { emc->add(kv.m_key->get_decl(), m().mk_ite(u().mk_ge(kv.m_value.first, mk_real_zero()), u().mk_acos(kv.m_value.second), + //non-deterministic order no change: too complex u().mk_add(u().mk_acos(u().mk_uminus(kv.m_value.second)), u().mk_pi()))); } diff --git a/src/tactic/bv/bv1_blaster_tactic.cpp b/src/tactic/bv/bv1_blaster_tactic.cpp index 090bd3e48..88f6cabed 100644 --- a/src/tactic/bv/bv1_blaster_tactic.cpp +++ b/src/tactic/bv/bv1_blaster_tactic.cpp @@ -156,6 +156,7 @@ class bv1_blaster_tactic : public tactic { bit_buffer new_ites; unsigned num = t_bits.size(); for (unsigned i = 0; i < num; i++) + //non-deterministic order no change: too complex new_ites.push_back(t_bits[i] == e_bits[i] ? t_bits[i] : m().mk_ite(c, t_bits[i], e_bits[i])); result = butil().mk_concat(new_ites.size(), new_ites.data()); } diff --git a/src/tactic/bv/bvarray2uf_rewriter.cpp b/src/tactic/bv/bvarray2uf_rewriter.cpp index 5d5797dfa..0f22bf1ab 100644 --- a/src/tactic/bv/bvarray2uf_rewriter.cpp +++ b/src/tactic/bv/bvarray2uf_rewriter.cpp @@ -149,7 +149,13 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); expr_ref body(m_manager); - body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get())); + //non-deterministic order change start + { + auto mk_app_1 = m_manager.mk_app(f_t, x.get()); + auto mk_app_2 = m_manager.mk_app(f_s, x.get()); + body = m_manager.mk_eq(mk_app_1, mk_app_2); + } + //non-deterministic order change end result = m_manager.mk_forall(1, sorts, names, body); res = BR_DONE; @@ -295,8 +301,14 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr new_args.push_back(m_manager.mk_app(ss[i].get(), x.get())); expr_ref body(m_manager); - body = m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), - m_manager.mk_app(map_f, num, new_args.data())); + //non-deterministic order change start + { + auto mk_app_1 = m_manager.mk_app(f_t, x.get()); + auto mk_app_2 = m_manager.mk_app(map_f, num, new_args.data()); + body = m_manager.mk_eq(mk_app_1, + mk_app_2); + } + //non-deterministic order change end expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); extra_assertions.push_back(frllx); @@ -330,9 +342,15 @@ br_status bvarray2uf_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr var_ref x(m_manager.mk_var(0, sorts[0]), m_manager); expr_ref body(m_manager); - body = m_manager.mk_or(m_manager.mk_eq(x, i), + //non-deterministic order change start + { + auto mk_eq_1 = m_manager.mk_eq(x, i); + body = m_manager.mk_or(mk_eq_1, + //non-deterministic order no change: too complex m_manager.mk_eq(m_manager.mk_app(f_t, x.get()), m_manager.mk_app(f_s, x.get()))); + } + //non-deterministic order change end expr_ref frllx(m_manager.mk_forall(1, sorts, names, body), m_manager); extra_assertions.push_back(frllx); diff --git a/src/tactic/fd_solver/enum2bv_solver.cpp b/src/tactic/fd_solver/enum2bv_solver.cpp index 061f67010..e7a4525ff 100644 --- a/src/tactic/fd_solver/enum2bv_solver.cpp +++ b/src/tactic/fd_solver/enum2bv_solver.cpp @@ -178,7 +178,13 @@ public: expr_ref head(m); ptr_vector const& enums = *dt.get_datatype_constructors(f->get_range()); if (enums.size() > num.get_unsigned()) { - head = m.mk_eq(m.mk_const(f), m.mk_const(enums[num.get_unsigned()])); + //non-deterministic order change start + { + auto mk_const_1 = m.mk_const(f); + auto mk_const_2 = m.mk_const(enums[num.get_unsigned()]); + head = m.mk_eq(mk_const_1, mk_const_2); + } + //non-deterministic order change end consequences[i] = m.mk_implies(a, head); } } diff --git a/src/tactic/fd_solver/smtfd_solver.cpp b/src/tactic/fd_solver/smtfd_solver.cpp index fda2f8688..9101d54ad 100644 --- a/src/tactic/fd_solver/smtfd_solver.cpp +++ b/src/tactic/fd_solver/smtfd_solver.cpp @@ -314,13 +314,26 @@ namespace smtfd { } family_id fid = a->get_family_id(); if (m.is_eq(a)) { - r = m.mk_eq(m_args.get(0), m_args.get(1)); + //non-deterministic order change start + { + auto get_1 = m_args.get(0); + auto get_2 = m_args.get(1); + r = m.mk_eq(get_1, get_2); + } + //non-deterministic order change end } else if (m.is_distinct(a)) { r = m.mk_distinct(m_args.size(), m_args.data()); } else if (m.is_ite(a)) { - r = m.mk_ite(m_args.get(0), m_args.get(1), m_args.get(2)); + //non-deterministic order change start + { + auto get_1 = m_args.get(0); + auto get_2 = m_args.get(1); + auto get_3 = m_args.get(2); + r = m.mk_ite(get_1, get_2, get_3); + } + //non-deterministic order change end } else if (bvfid == fid || bfid == fid || pbfid == fid) { r = m.mk_app(a->get_decl(), m_args.size(), m_args.data()); @@ -1157,6 +1170,7 @@ namespace smtfd { expr_ref a1(m_autil.mk_select(args), m); args[0] = b; expr_ref b1(m_autil.mk_select(args), m); + //non-deterministic order no change: too complex expr_ref ext(m.mk_iff(m.mk_eq(a1, b1), m.mk_eq(a, b)), m); if (!m.is_true(eval_abs(ext))) { TRACE(smtfd, tout << mk_bounded_pp(a, m, 2) << " " << mk_bounded_pp(b, m, 2) << "\n";); diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index e77757aea..18b1f73a1 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -343,6 +343,7 @@ Notes: return mk_not(out[k]); } else { + //non-deterministic order no change: too complex return mk_min(out[k-1], mk_not(out[k])); } case sorting_network_encoding::unate_at_most: @@ -384,6 +385,7 @@ Notes: } literal eq(unsigned k, unsigned n, unsigned const* ws, literal const* xs) { + //non-deterministic order no change: too complex return mk_and(ge(k, n, ws, xs), le(k, n, ws, xs)); #if 0 m_t = EQ; @@ -479,7 +481,12 @@ Notes: for (unsigned j = last; j-- > 0; ) { // c'[j] <-> (xs[i] & c[j-1]) | c[j] literal c0 = j > 0 ? carry[j-1] : ctx.mk_true(); - carry[j] = mk_or(mk_and(xs[i], c0), carry[j]); + //non-deterministic order change start + { + auto mk_and_1 = mk_and(xs[i], c0); + carry[j] = mk_or(mk_and_1, carry[j]); + } + //non-deterministic order change end } } switch (cmp) { @@ -490,6 +497,7 @@ Notes: case GE_FULL: return carry[k-1]; case EQ: + //non-deterministic order no change: too complex return mk_and(mk_not(carry[k]), carry[k-1]); default: UNREACHABLE(); @@ -522,6 +530,7 @@ Notes: // out[i] = c + x[i] + y[i] // c' = c&x[i] | c&y[i] | x[i]&y[i]; literal_vector ors; + //non-deterministic order no change: too complex ors.push_back(mk_and(c, mk_not(x[i]), mk_not(y[i]))); ors.push_back(mk_and(x[i], mk_not(c), mk_not(y[i]))); ors.push_back(mk_and(y[i], mk_not(c), mk_not(x[i]))); @@ -578,7 +587,9 @@ Notes: literal_vector eqs; SASSERT(kvec.size() == out.size()); for (unsigned i = 0; i < num_bits; ++i) { + //non-deterministic order no change: too complex eqs.push_back(mk_or(mk_not(kvec[i]), out[i])); + //non-deterministic order no change: too complex eqs.push_back(mk_or(kvec[i], mk_not(out[i]))); } eqs.push_back(mk_not(ovfl)); @@ -686,6 +697,7 @@ Notes: case 1: return ands[0]; case 2: + //non-deterministic order no change: too complex return mk_min(ands[0], ands[1]); default: { return ctx.mk_min(ands.size(), ands.data());