another 16 nond args fixed

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>

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);
+                expr * arg = args[j];
-            // TODO: non-deterministic parameter evaluation
+                r = mk_app_core(decl, arg, r);
             }
         }
         else if (decl->is_left_associative()) {

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
+                    expr_ref disj1(m);
-                    result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(tt1, tt3));
+                    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
+                expr_ref disj1(m);
-                result = m.mk_and(m.mk_or(ntt1, tt2), m.mk_or(ntt2, tt1));
+                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"

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
+        expr_ref then_branch(m());
-        result = m().mk_ite(p, re().mk_reverse(r1), re().mk_reverse(r2));
+        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
+        expr_ref in_prefix(m());
-        fmls.push_back(m().mk_and(re().mk_in_re(x, prefix),
+        expr_ref in_suffix(m());
-                                  re().mk_in_re(y, suffix)));
+        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;
 }
-

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
+            expr_ref then_val(m());
-            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 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
+            expr_ref then_val(m());
-            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 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;

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 * prefix_kw = mk_string(m, "((x ");
-        format * f_args[2] = { mk_compose(m, 
+        format * suffix_kw = mk_string(m, "))");
-                                          mk_string(m, "((x "),
+        format * seq_args[2] = { f_s.get(), suffix_kw };
-                                          mk_indent(m, 4, mk_compose(m, f_s.get(), mk_string(m, "))")))),
+        format_ref seq_block(fm(m));
-                               f_cond };
+        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<format**, f2f>(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
+                format * ite_kw = mk_string(m, "(ite ");
-                f_entries.push_back(mk_group(m, mk_compose(m, 
+                format_ref guard_indent(fm(m));
-                                                           mk_string(m, "(ite "),
+                guard_indent = mk_indent(m, 5, f_entry_cond);
-                                                           mk_indent(m, 5, f_entry_cond),
+                format * entry_line_break = mk_line_break(m);
-                                                           mk_indent(m, TAB_SZ, mk_compose(m, 
+                format * result_ptr = f_result.get();
-                                                                                           mk_line_break(m),
+                format * result_nodes[2] = { entry_line_break, result_ptr };
-                                                                                           f_result.get())))));
+                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
+        format * define_kw = mk_string(m, "(define-fun ");
-        def = mk_indent(m, indent, mk_compose(m, 
+        format * fname_fmt = mk_string(m, fname);
-                                              // TODO: non-deterministic parameter evaluation
+        format * space_fmt = mk_string(m, " ");
-                                              mk_compose(m, 
+        format * domain_range_args[3] = { f_domain, space_fmt, f_range };
-                                                         mk_string(m, "(define-fun "),
+        format_ref domain_range(fm(m));
-                                                         mk_string(m, fname),
+        domain_range = mk_compose(m, 3, domain_range_args);
-                                                         mk_string(m, " "),
+        format * domain_range_ptr = domain_range.get();
-                                                         mk_compose(m, 
+        format * header_args[4] = { define_kw, fname_fmt, space_fmt, domain_range_ptr };
-                                                                    f_domain,
+        format_ref header(fm(m));
-                                                                    mk_string(m, " "),
+        header = mk_compose(m, 4, header_args);
-                                                                    f_range)),
+        format * def_line_break = mk_line_break(m);
-                                              mk_indent(m, TAB_SZ, mk_compose(m, 
+        format * body_ptr = body.get();
-                                                                              mk_line_break(m),
+        format * rp_fmt = mk_string(m, ")");
-                                                                              body.get(),
+        format * tail_args[3] = { def_line_break, body_ptr, rp_fmt };
-                                                                              mk_string(m, ")")))));
+        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";

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
+            expr_ref lhs(ctx.bool_var2expr(n1_eq_n2.var()), 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())));
+            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);

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<expr*(void)> logfn = [&]() {
-            // TODO: non-deterministic parameter evaluation
+            expr_ref bit1(m);
-            // TODO: non-deterministic parameter evaluation
+            expr_ref bit2(m);
-            return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq));
+            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<expr*()> logfn = [&]() {
-                // TODO: non-deterministic parameter evaluation
+                expr_ref eq_expr(ctx.bool_var2expr(eq.var()), m);
-                return m.mk_implies(m.mk_not(ctx.bool_var2expr(eq.var())), m.mk_not(ctx.bool_var2expr(oeq.var())));
+                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);