diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 689a0fa8c..e1fa18d48 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2240,10 +2240,9 @@ app * ast_manager::mk_app(func_decl * decl, unsigned num_args, expr * const * ar r = mk_app_core(decl, args[j-1], args[j]); -- j; while (j > 0) { - // TODO: non-deterministic parameter evaluation --j; - r = mk_app_core(decl, args[j], r); - // TODO: non-deterministic parameter evaluation + expr * arg = args[j]; + r = mk_app_core(decl, arg, r); } } else if (decl->is_left_associative()) { diff --git a/src/ast/rewriter/quant_hoist.cpp b/src/ast/rewriter/quant_hoist.cpp index 3f07d88f0..9d9edf40a 100644 --- a/src/ast/rewriter/quant_hoist.cpp +++ b/src/ast/rewriter/quant_hoist.cpp @@ -249,8 +249,11 @@ 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); - // TODO: non-deterministic parameter evaluation - result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3)); + expr_ref disj1(m); + expr_ref disj2(m); + disj1 = m.mk_or(ntt1, tt2); + disj2 = m.mk_or(tt1, tt3); + result = m.mk_and(disj1, disj2); } else { result = m.mk_ite(t1, tt2, tt3); @@ -264,8 +267,11 @@ 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); - // TODO: non-deterministic parameter evaluation - result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1)); + expr_ref disj1(m); + expr_ref disj2(m); + disj1 = m.mk_or(ntt1, tt2); + disj2 = m.mk_or(ntt2, tt1); + result = m.mk_and(disj1, disj2); } else { // the formula contains a quantifier, but it is "inaccessible" diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index de85b374a..82bb6181f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2764,8 +2764,11 @@ br_status seq_rewriter::mk_re_reverse(expr* r, expr_ref& result) { return BR_REWRITE2; } else if (m().is_ite(r, p, r1, r2)) { - // TODO: non-deterministic parameter evaluation - result = m().mk_ite(p, re().mk_reverse(r1), re().mk_reverse(r2)); + expr_ref then_branch(m()); + expr_ref else_branch(m()); + then_branch = re().mk_reverse(r1); + else_branch = re().mk_reverse(r2); + result = m().mk_ite(p, then_branch, else_branch); return BR_REWRITE2; } else if (re().is_opt(r, r1)) { @@ -4283,9 +4286,13 @@ 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); } - // TODO: non-deterministic parameter evaluation - fmls.push_back(m().mk_and(re().mk_in_re(x, prefix), - re().mk_in_re(y, suffix))); + expr_ref in_prefix(m()); + expr_ref in_suffix(m()); + in_prefix = re().mk_in_re(x, prefix); + in_suffix = re().mk_in_re(y, suffix); + expr_ref conjunct(m()); + conjunct = m().mk_and(in_prefix, in_suffix); + fmls.push_back(conjunct); } result = mk_or(fmls); return true; @@ -6178,4 +6185,3 @@ bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) { } return low <= high; } - diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index d993fa20b..08d3734cd 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -143,13 +143,23 @@ struct th_rewriter_cfg : public default_rewriter_cfg { expr * x; unsigned val; if (m_bv_rw.is_eq_bit(lhs, x, val)) { - // TODO: non-deterministic parameter evaluation - result = m().mk_eq(x, m().mk_ite(rhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); + expr_ref then_val(m()); + expr_ref else_val(m()); + then_val = m_bv_rw.mk_numeral(val, 1); + else_val = m_bv_rw.mk_numeral(1 - val, 1); + expr_ref ite_branch(m()); + ite_branch = m().mk_ite(rhs, then_val, else_val); + result = m().mk_eq(x, ite_branch); return BR_REWRITE2; } if (m_bv_rw.is_eq_bit(rhs, x, val)) { - // TODO: non-deterministic parameter evaluation - result = m().mk_eq(x, m().mk_ite(lhs, m_bv_rw.mk_numeral(val, 1), m_bv_rw.mk_numeral(1-val, 1))); + expr_ref then_val(m()); + expr_ref else_val(m()); + then_val = m_bv_rw.mk_numeral(val, 1); + else_val = m_bv_rw.mk_numeral(1 - val, 1); + expr_ref ite_branch(m()); + ite_branch = m().mk_ite(lhs, then_val, else_val); + result = m().mk_eq(x, ite_branch); return BR_REWRITE2; } return BR_FAILED; diff --git a/src/model/model_smt2_pp.cpp b/src/model/model_smt2_pp.cpp index ba54258c1..dca944172 100644 --- a/src/model/model_smt2_pp.cpp +++ b/src/model/model_smt2_pp.cpp @@ -123,11 +123,19 @@ 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); - // TODO: non-deterministic parameter evaluation - format * f_args[2] = { mk_compose(m, - mk_string(m, "((x "), - mk_indent(m, 4, mk_compose(m, f_s.get(), mk_string(m, "))")))), - f_cond }; + format * prefix_kw = mk_string(m, "((x "); + format * suffix_kw = mk_string(m, "))"); + format * seq_args[2] = { f_s.get(), suffix_kw }; + format_ref seq_block(fm(m)); + seq_block = mk_compose(m, 2, seq_args); + format_ref indented_block(fm(m)); + indented_block = mk_indent(m, 4, seq_block.get()); + format * indented_ptr = indented_block.get(); + format * compose_args[2] = { prefix_kw, indented_ptr }; + format_ref head_block(fm(m)); + head_block = mk_compose(m, 2, compose_args); + format * head_ptr = head_block.get(); + format * f_args[2] = { head_ptr, f_cond }; format_ref f_card(fm(m)); f_card = mk_indent(m, indent, mk_seq1(m, f_args, f_args+2, f2f(), "forall")); pp_indent(out, indent); @@ -253,13 +261,22 @@ 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)); - // TODO: non-deterministic parameter evaluation - f_entries.push_back(mk_group(m, mk_compose(m, - mk_string(m, "(ite "), - mk_indent(m, 5, f_entry_cond), - mk_indent(m, TAB_SZ, mk_compose(m, - mk_line_break(m), - f_result.get()))))); + format * ite_kw = mk_string(m, "(ite "); + format_ref guard_indent(fm(m)); + guard_indent = mk_indent(m, 5, f_entry_cond); + format * entry_line_break = mk_line_break(m); + format * result_ptr = f_result.get(); + format * result_nodes[2] = { entry_line_break, result_ptr }; + format_ref result_compose(fm(m)); + result_compose = mk_compose(m, 2, result_nodes); + format_ref result_indent(fm(m)); + result_indent = mk_indent(m, TAB_SZ, result_compose.get()); + format * guard_ptr = guard_indent.get(); + format * result_indent_ptr = result_indent.get(); + format * ite_args[3] = { ite_kw, guard_ptr, result_indent_ptr }; + format_ref ite_body(fm(m)); + ite_body = mk_compose(m, 3, ite_args); + f_entries.push_back(mk_group(m, ite_body.get())); } f_entries.push_back(mk_indent(m, TAB_SZ, mk_compose(m, mk_line_break(m), @@ -274,21 +291,30 @@ 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(); - // TODO: non-deterministic parameter evaluation - def = mk_indent(m, indent, mk_compose(m, - // TODO: non-deterministic parameter evaluation - mk_compose(m, - mk_string(m, "(define-fun "), - mk_string(m, fname), - mk_string(m, " "), - mk_compose(m, - f_domain, - mk_string(m, " "), - f_range)), - mk_indent(m, TAB_SZ, mk_compose(m, - mk_line_break(m), - body.get(), - mk_string(m, ")"))))); + format * define_kw = mk_string(m, "(define-fun "); + format * fname_fmt = mk_string(m, fname); + format * space_fmt = mk_string(m, " "); + format * domain_range_args[3] = { f_domain, space_fmt, f_range }; + format_ref domain_range(fm(m)); + domain_range = mk_compose(m, 3, domain_range_args); + format * domain_range_ptr = domain_range.get(); + format * header_args[4] = { define_kw, fname_fmt, space_fmt, domain_range_ptr }; + format_ref header(fm(m)); + header = mk_compose(m, 4, header_args); + format * def_line_break = mk_line_break(m); + format * body_ptr = body.get(); + format * rp_fmt = mk_string(m, ")"); + format * tail_args[3] = { def_line_break, body_ptr, rp_fmt }; + format_ref tail_block(fm(m)); + tail_block = mk_compose(m, 3, tail_args); + format_ref body_indent(fm(m)); + body_indent = mk_indent(m, TAB_SZ, tail_block.get()); + format * header_ptr = header.get(); + format * body_indent_ptr = body_indent.get(); + format * def_args[2] = { header_ptr, body_indent_ptr }; + format_ref def_body(fm(m)); + def_body = mk_compose(m, 2, def_args); + def = mk_indent(m, indent, def_body.get()); pp_indent(out, indent); pp(out, def.get(), m); out << "\n"; diff --git a/src/smt/theory_array_base.cpp b/src/smt/theory_array_base.cpp index 8b7abc482..1de3de252 100644 --- a/src/smt/theory_array_base.cpp +++ b/src/smt/theory_array_base.cpp @@ -360,8 +360,13 @@ namespace smt { ctx.mark_as_relevant(sel1_eq_sel2); if (m.has_trace_stream()) { app_ref body(m); - // TODO: non-deterministic parameter evaluation - body = m.mk_implies(m.mk_not(ctx.bool_var2expr(n1_eq_n2.var())), m.mk_not(ctx.bool_var2expr(sel1_eq_sel2.var()))); + expr_ref lhs(ctx.bool_var2expr(n1_eq_n2.var()), m); + expr_ref not_lhs(m); + not_lhs = m.mk_not(lhs); + expr_ref rhs(ctx.bool_var2expr(sel1_eq_sel2.var()), m); + expr_ref not_rhs(m); + not_rhs = m.mk_not(rhs); + body = m.mk_implies(not_lhs, not_rhs); 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 44e1d4508..773cf1755 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -241,9 +241,17 @@ namespace smt { expr_ref eq(m.mk_eq(e1, e2), m); literal l = ~mk_literal(eq); std::function logfn = [&]() { - // TODO: non-deterministic parameter evaluation - // TODO: non-deterministic parameter evaluation - return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq)); + expr_ref bit1(m); + expr_ref bit2(m); + bit1 = mk_bit2bool(e1, idx); + bit2 = mk_bit2bool(e2, idx); + expr_ref not_bit2(m); + not_bit2 = m.mk_not(bit2); + expr_ref antecedent(m); + antecedent = m.mk_eq(bit1, not_bit2); + expr_ref consequent(m); + consequent = m.mk_not(eq); + return m.mk_implies(antecedent, consequent); }; scoped_trace_stream ts(*this, logfn); ctx.mk_th_axiom(get_id(), 1, &l); @@ -458,8 +466,13 @@ namespace smt { e2 = mk_bit2bool(o2, i); literal eq = mk_eq(e1, e2, true); std::function logfn = [&]() { - // TODO: non-deterministic parameter evaluation - return m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var()))); + expr_ref eq_expr(ctx.bool_var2expr(eq.var()), m); + expr_ref neq_expr(m); + neq_expr = m.mk_not(eq_expr); + expr_ref oeq_expr(ctx.bool_var2expr(oeq.var()), m); + expr_ref not_oeq(m); + not_oeq = m.mk_not(oeq_expr); + return m.mk_implies(neq_expr, not_oeq); }; scoped_trace_stream st(*this, logfn); ctx.mk_th_axiom(get_id(), l1, ~l2, ~eq);