From 37c9f1c7c2279e00d55214dfeee9520e6454b8d0 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Wed, 29 Oct 2025 21:37:05 -0700 Subject: [PATCH] remove some non-deterministic behavior in theory_lra.cpp Signed-off-by: Lev Nachmanson --- src/ast/ast.cpp | 4 +- src/ast/ast_smt2_pp.cpp | 7 +++ src/ast/euf/euf_ac_plugin.cpp | 2 + src/ast/euf/euf_bv_plugin.cpp | 4 ++ src/ast/fpa/bv2fpa_converter.cpp | 1 + src/ast/fpa/fpa2bv_converter.cpp | 2 + src/ast/rewriter/arith_rewriter.cpp | 4 ++ src/ast/rewriter/bv2int_translator.cpp | 5 ++ src/ast/rewriter/bv_rewriter.cpp | 1 + src/ast/rewriter/enum2bv_rewriter.cpp | 1 + src/ast/rewriter/seq_axioms.cpp | 10 ++++ src/ast/rewriter/seq_rewriter.cpp | 3 ++ src/ast/rewriter/th_rewriter.cpp | 4 ++ src/math/lp/nla_common.cpp | 1 + src/math/polynomial/polynomial.cpp | 2 + src/model/model.cpp | 1 + src/model/model_evaluator.cpp | 1 + src/muz/spacer/spacer_context.cpp | 1 + src/nlsat/tactic/goal2nlsat.cpp | 1 + src/nlsat/tactic/qfnra_nlsat_tactic.cpp | 2 + src/opt/opt_context.cpp | 1 + src/qe/nlarith_util.cpp | 3 ++ src/sat/sat_solver/inc_sat_solver.cpp | 2 + src/sat/smt/arith_solver.cpp | 1 + src/smt/dyn_ack.cpp | 1 + src/smt/old_interval.cpp | 1 + src/smt/seq_regex.cpp | 1 + src/smt/theory_arith_nl.h | 3 ++ src/smt/theory_array_bapa.cpp | 1 + src/smt/theory_lra.cpp | 54 +++++++++++++++---- src/smt/theory_seq.cpp | 1 + src/smt/theory_utvpi.h | 1 + src/tactic/arith/bv2real_rewriter.cpp | 4 ++ src/tactic/arith/factor_tactic.cpp | 2 + src/tactic/arith/lia2card_tactic.cpp | 1 + src/tactic/core/special_relations_tactic.cpp | 1 + src/tactic/fpa/qffp_tactic.cpp | 3 ++ src/tactic/portfolio/default_tactic.cpp | 14 +++++ src/tactic/portfolio/smt_strategic_solver.cpp | 1 + src/tactic/sls/sls_tactic.cpp | 2 + src/tactic/smtlogics/nra_tactic.cpp | 2 + src/tactic/smtlogics/qfaufbv_tactic.cpp | 2 + src/tactic/smtlogics/qfauflia_tactic.cpp | 1 + src/tactic/smtlogics/qfbv_tactic.cpp | 5 ++ src/tactic/smtlogics/qfidl_tactic.cpp | 7 +++ src/tactic/smtlogics/qflia_tactic.cpp | 7 +++ src/tactic/smtlogics/qfnia_tactic.cpp | 5 ++ src/tactic/smtlogics/qfnra_tactic.cpp | 10 ++++ src/tactic/smtlogics/qfuf_tactic.cpp | 1 + src/tactic/smtlogics/qfufbv_tactic.cpp | 4 ++ src/tactic/smtlogics/quant_tactics.cpp | 11 ++++ src/tactic/ufbv/ufbv_tactic.cpp | 11 ++++ src/util/sorting_network.h | 7 +++ 53 files changed, 217 insertions(+), 11 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index e1fa18d48..1ce0be4b2 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -1714,7 +1714,7 @@ ast * ast_manager::register_node_core(ast * n) { } n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk(); - + // track_id(*this, n, 9213); // TRACE(ast, tout << (s_count++) << " Object " << n->m_id << " was created.\n";); @@ -2131,8 +2131,10 @@ expr* ast_manager::coerce_to(expr* e, sort* s) { if (s != se && s->get_family_id() == arith_family_id && is_bool(e)) { arith_util au(*this); if (s->get_decl_kind() == REAL_SORT) + // TODO: non-deterministic parameter evaluation return mk_ite(e, au.mk_real(1), au.mk_real(0)); else + // TODO: non-deterministic parameter evaluation return mk_ite(e, au.mk_int(1), au.mk_int(0)); } else { diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 72382e366..5a51fa4d2 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -592,17 +592,20 @@ class smt2_printer { } format * pp_attribute(char const * attr, format * f) { + // TODO: non-deterministic parameter evaluation return mk_compose(m(), mk_string(m(), attr), mk_indent(m(), static_cast(strlen(attr)), f)); } format * pp_simple_attribute(char const * attr, int v) { + // TODO: non-deterministic parameter evaluation return mk_compose(m(), mk_string(m(), attr), mk_int(m(), v)); } format * pp_simple_attribute(char const * attr, symbol const & s) { std::string str = ensure_quote(s); + // TODO: non-deterministic parameter evaluation return mk_compose(m(), mk_string(m(), attr), mk_string(m(), str)); } @@ -762,8 +765,10 @@ class smt2_printer { SASSERT(it < end); format * fname = m_env.pp_fdecl(t->get_decl(), len); if (len > MAX_INDENT) { + // TODO: non-deterministic parameter evaluation f = mk_group(m(), mk_compose(m(), mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), + // TODO: non-deterministic parameter evaluation mk_indent(m(), SMALL_INDENT, mk_compose(m(), mk_seq(m(), it, end, f2f()), mk_string(m(), ")"))))); @@ -771,8 +776,10 @@ class smt2_printer { else { format * first = *it; ++it; + // TODO: non-deterministic parameter evaluation f = mk_group(m(), mk_compose(m(), mk_indent(m(), 1, mk_compose(m(), mk_string(m(), "("), fname)), + // TODO: non-deterministic parameter evaluation mk_indent(m(), len + 2, mk_compose(m(), mk_string(m(), " "), first, diff --git a/src/ast/euf/euf_ac_plugin.cpp b/src/ast/euf/euf_ac_plugin.cpp index e89f18d58..04ee7afeb 100644 --- a/src/ast/euf/euf_ac_plugin.cpp +++ b/src/ast/euf/euf_ac_plugin.cpp @@ -1411,6 +1411,7 @@ namespace euf { m_monomial_table.insert(s1.m, s1); else if (s2.n->get_root() != s1.n->get_root()) { TRACE(plugin, tout << "merge shared " << g.bpp(s1.n->get_root()) << " and " << g.bpp(s2.n->get_root()) << "\n"); + // TODO: non-deterministic parameter evaluation push_merge(s1.n, s2.n, justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(s1.j), m_dep_manager.mk_leaf(s2.j)))); } } @@ -1463,6 +1464,7 @@ namespace euf { } justification ac_plugin::join(justification j, eq const& eq) { + // TODO: non-deterministic parameter evaluation return justification::dependent(m_dep_manager.mk_join(m_dep_manager.mk_leaf(j), m_dep_manager.mk_leaf(eq.j))); } diff --git a/src/ast/euf/euf_bv_plugin.cpp b/src/ast/euf/euf_bv_plugin.cpp index 6b90bfd3a..0ae215faa 100644 --- a/src/ast/euf/euf_bv_plugin.cpp +++ b/src/ast/euf/euf_bv_plugin.cpp @@ -167,6 +167,7 @@ namespace euf { unsigned lo, hi; for (enode* p : enode_parents(x)) { if (is_concat(p, a, b) && is_value(a) && is_value(b)) + // TODO: non-deterministic parameter evaluation push_merge(mk_concat(a->get_interpreted(), b->get_interpreted()), mk_value_concat(a, b)); if (is_extract(p, lo, hi)) { @@ -181,6 +182,7 @@ namespace euf { if (is_concat(sib, a, b)) { auto val_a = machine_div2k(val_x, width(b)); auto val_b = mod2k(val_x, width(b)); + // TODO: non-deterministic parameter evaluation push_merge(mk_concat(mk_value(val_a, width(a)), mk_value(val_b, width(b))), x->get_interpreted()); } } @@ -214,6 +216,8 @@ namespace euf { if (is_extract(p1, lo_, hi_) && lo_ == lo && hi_ == hi && p1->get_arg(0)->get_root() == arg_r) return; // add the axiom instead of merge(p, mk_extract(arg, lo, hi)), which would require tracking justifications + // TODO: non-deterministic parameter evaluation + // TODO: non-deterministic parameter evaluation push_merge(mk_concat(mk_extract(arg, mid + 1, hi), mk_extract(arg, lo, mid)), mk_extract(arg, lo, hi)); }; diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index fa801be14..329e8e5ec 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -459,6 +459,7 @@ void bv2fpa_converter::convert_min_max_specials(model_core * mc, model_core * ta auto fid = m_fpa_util.get_family_id(); auto k = is_decl_of(f, fid, OP_FPA_MIN) ? OP_FPA_MIN_I : OP_FPA_MAX_I; func_decl_ref min_max_i(m.mk_func_decl(fid, k, 0, nullptr, 2, pn_args), m); + // TODO: non-deterministic parameter evaluation expr_ref else_value(m.mk_app(min_max_i, m.mk_var(0, srt), m.mk_var(1, srt)), m); flt_fi->set_else(else_value); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 6fec67195..c11ae6ca6 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1207,6 +1207,7 @@ void fpa2bv_converter::mk_rem(sort * s, expr_ref & x, expr_ref & y, expr_ref & r lshift = edr_tmp; rshift = nedr_tmp; + // TODO: non-deterministic parameter evaluation shifted = m.mk_ite(exp_diff_is_neg, m_bv_util.mk_bv_ashr(a_sig_ext, rshift), m_bv_util.mk_bv_shl(a_sig_ext, lshift)); huge_rem = m_bv_util.mk_bv_urem(shifted, b_sig_ext); @@ -3460,6 +3461,7 @@ void fpa2bv_converter::mk_to_bv(func_decl * f, unsigned num, expr * const * args dbg_decouple("fpa2bv_to_bv_shift", shift); expr_ref big_sig_shifted(m), int_part(m), last(m), round(m), stickies(m), sticky(m); + // TODO: non-deterministic parameter evaluation big_sig_shifted = m.mk_ite(is_neg_shift, m_bv_util.mk_bv_lshr(big_sig, shift), m_bv_util.mk_bv_shl(big_sig, shift)); int_part = m_bv_util.mk_extract(big_sig_sz-1, big_sig_sz-(bv_sz+3), big_sig_shifted); diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 7daceeca8..4b9c6d246 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -1295,6 +1295,7 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu } if (get_divides(arg1, arg2, result)) { expr_ref zero(m_util.mk_int(0), m); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(m.mk_eq(zero, arg2), m_util.mk_idiv(arg1, zero), result); return BR_REWRITE_FULL; } @@ -1428,6 +1429,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul if (arg1 == arg2 && !is_num2) { expr_ref zero(m_util.mk_int(0), m); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(m.mk_eq(arg2, zero), m_util.mk_mod(zero, zero), zero); return BR_DONE; } @@ -1767,6 +1769,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res if (is_num_y && y.is_minus_one()) { result = m_util.mk_div(m_util.mk_real(1), ensure_real(arg1)); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), m_util.mk_real(0), result); @@ -1777,6 +1780,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res // (^ t -k) --> (^ (/ 1 t) k) result = m_util.mk_power(m_util.mk_div(m_util.mk_numeral(rational(1), false), arg1), m_util.mk_numeral(-y, false)); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(m.mk_eq(arg1, m_util.mk_numeral(rational(0), m_util.is_int(arg1))), m_util.mk_real(0), result); diff --git a/src/ast/rewriter/bv2int_translator.cpp b/src/ast/rewriter/bv2int_translator.cpp index 13c972ddf..43131c2c8 100644 --- a/src/ast/rewriter/bv2int_translator.cpp +++ b/src/ast/rewriter/bv2int_translator.cpp @@ -320,6 +320,7 @@ void bv2int_translator::translate_bv(app* e) { case OP_BUDIV: case OP_BUDIV_I: { expr* x = umod(e, 0), * y = umod(e, 1); + // TODO: non-deterministic parameter evaluation r = if_eq(y, 0, a.mk_int(-1), a.mk_idiv(x, y)); break; } @@ -400,6 +401,7 @@ void bv2int_translator::translate_bv(app* e) { r = arg(0); for (unsigned i = 1; i < args.size(); ++i) { expr* q = arg(i); + // TODO: non-deterministic parameter evaluation r = a.mk_sub(add(r, q), mul(a.mk_int(2), a.mk_band(sz, r, q))); } if (e->get_decl_kind() == OP_BXNOR) @@ -438,6 +440,7 @@ void bv2int_translator::translate_bv(app* e) { expr* lhs = umod(bv_expr, 0); expr* rhs = umod(bv_expr, 1); expr* eq = m.mk_eq(lhs, rhs); + // TODO: non-deterministic parameter evaluation r = m.mk_ite(eq, a.mk_int(1), a.mk_int(0)); break; } @@ -457,6 +460,7 @@ void bv2int_translator::translate_bv(app* e) { r = a.mk_uminus(u); expr* pos_neg = m.mk_and(m.mk_not(signx), signy); expr* neg_pos = m.mk_and(signx, m.mk_not(signy)); + // TODO: non-deterministic parameter evaluation expr* pos_pos = m.mk_and(m.mk_not(signx), m.mk_not(signy)); expr_ref add_u_y(m); add_u_y = add(u, y); @@ -485,6 +489,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)); + // TODO: non-deterministic parameter evaluation expr* zero_case = m.mk_ite(signx, a.mk_int(1), a.mk_int(-1)); r = if_eq(y, 0, zero_case, r); break; diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index 9c937f8c7..5dc48a5f7 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -945,6 +945,7 @@ br_status bv_rewriter::mk_bv_shl(expr * arg1, expr * arg2, expr_ref & result) { if (m_util.is_bv_shl(arg1, x, y)) { expr_ref sum(m_util.mk_bv_add(y, arg2), m); expr_ref cond(m_util.mk_ule(y, sum), m); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(cond, m_util.mk_bv_shl(x, sum), mk_zero(bv_size)); diff --git a/src/ast/rewriter/enum2bv_rewriter.cpp b/src/ast/rewriter/enum2bv_rewriter.cpp index 1a45ebd1b..2d91c489b 100644 --- a/src/ast/rewriter/enum2bv_rewriter.cpp +++ b/src/ast/rewriter/enum2bv_rewriter.cpp @@ -170,6 +170,7 @@ struct enum2bv_rewriter::imp { ptr_vector const& cs = *m_dt.get_datatype_constructors(s); f_def = m.mk_const(cs[nc-1]); for (unsigned i = nc - 1; i-- > 0; ) { + // TODO: non-deterministic parameter evaluation f_def = m.mk_ite(m.mk_eq(result, value2bv(i, s)), m.mk_const(cs[i]), f_def); } m_imp.m_enum2def.insert(f, f_def); diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 22114aecc..364b66b26 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -747,6 +747,7 @@ namespace seq { VERIFY (seq.str.is_stoi(e, _s)); expr_ref s(_s, m); m_rewrite(s); + // TODO: non-deterministic parameter evaluation auto stoi2 = [&](unsigned j) { return m_sk.mk("seq.stoi", s, a.mk_int(j), a.mk_int()); }; auto digit = [&](unsigned j) { return mk_digit2int(mk_nth(s, j)); }; auto is_digit_ = [&](unsigned j) { return is_digit(mk_nth(s, j)); }; @@ -754,7 +755,9 @@ namespace seq { expr_ref ge0 = mk_ge(e, 0); expr_ref lek = mk_le(len, k); add_clause(~lek, mk_eq(e, stoi2(k-1))); // len(s) <= k => stoi(s) = stoi(s, k-1) + // TODO: non-deterministic parameter evaluation add_clause(mk_le(len, 0), ~is_digit_(0), mk_eq(stoi2(0), digit(0))); // len(s) > 0, is_digit(nth(s, 0)) => stoi(s,0) = digit(s,0) + // TODO: non-deterministic parameter evaluation add_clause(mk_le(len, 0), is_digit_(0), mk_eq(stoi2(0), a.mk_int(-1))); // len(s) > 0, ~is_digit(nth(s, 0)) => stoi(s,0) = -1 for (unsigned i = 1; i < k; ++i) { @@ -766,8 +769,11 @@ namespace seq { // len(s) > i, stoi(s, i - 1) < 0 => stoi(s, i) = -1 // len(s) > i, ~is_digit(nth(s, i)) => stoi(s, i) = -1 + // TODO: non-deterministic parameter evaluation add_clause(mk_le(len, i), ~mk_ge(stoi2(i-1), 0), ~is_digit_(i), mk_eq(stoi2(i), a.mk_add(a.mk_mul(a.mk_int(10), stoi2(i-1)), digit(i)))); + // TODO: non-deterministic parameter evaluation add_clause(mk_le(len, i), is_digit_(i), mk_eq(stoi2(i), a.mk_int(-1))); + // TODO: non-deterministic parameter evaluation add_clause(mk_le(len, i), mk_ge(stoi2(i-1), 0), mk_eq(stoi2(i), a.mk_int(-1))); // stoi(s) >= 0, i < len(s) => is_digit(nth(s, i)) @@ -906,12 +912,16 @@ namespace seq { expr* e = nullptr; VERIFY(seq.str.is_itos(s, e)); expr_ref len = mk_len(s); + // TODO: non-deterministic parameter evaluation add_clause(mk_ge(e, 10), mk_le(len, 1)); + // TODO: non-deterministic parameter evaluation add_clause(mk_le(e, -1), mk_ge(len, 1)); rational lo(1); for (unsigned i = 1; i <= k; ++i) { lo *= rational(10); + // TODO: non-deterministic parameter evaluation add_clause(mk_ge(e, lo), mk_le(len, i)); + // TODO: non-deterministic parameter evaluation add_clause(mk_le(e, lo - 1), mk_ge(len, i + 1)); } } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 82bb6181f..4ba515d2c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1642,6 +1642,7 @@ br_status seq_rewriter::mk_seq_index(expr* a, expr* b, expr* c, expr_ref& result break; case same_length_c: result = m().mk_ite(m_autil.mk_le(c, minus_one()), minus_one(), + // TODO: non-deterministic parameter evaluation m().mk_ite(m().mk_eq(c, zero()), m().mk_ite(m().mk_eq(a, b), zero(), minus_one()), minus_one())); @@ -2995,6 +2996,7 @@ void seq_rewriter::mk_antimirov_deriv_rec(expr* e, expr* r, expr* path, expr_ref else if (neq_char(e, h)) result = nothing(); else + // TODO: non-deterministic parameter evaluation result = re().mk_ite_simplify(m().mk_eq(e, h), re().mk_to_re(t), nothing()); } else { @@ -4067,6 +4069,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) hd = mk_seq_first(r1); + // TODO: non-deterministic parameter evaluation m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 08d3734cd..cab60dc7e 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -258,6 +258,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { template br_status pull_ite_core(func_decl * p, app * ite, app * value, expr_ref & result) { if (m().is_eq(p)) { + // TODO: non-deterministic parameter evaluation result = m().mk_ite(ite->get_arg(0), mk_eq_value(ite->get_arg(1), value), mk_eq_value(ite->get_arg(2), value)); @@ -265,12 +266,14 @@ struct th_rewriter_cfg : public default_rewriter_cfg { } else { if (SWAP) { + // TODO: non-deterministic parameter evaluation result = m().mk_ite(ite->get_arg(0), m().mk_app(p, value, ite->get_arg(1)), m().mk_app(p, value, ite->get_arg(2))); return BR_REWRITE2; } else { + // TODO: non-deterministic parameter evaluation result = m().mk_ite(ite->get_arg(0), m().mk_app(p, ite->get_arg(1), value), m().mk_app(p, ite->get_arg(2), value)); @@ -317,6 +320,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return pull_ite_core(f, to_app(args[0]), to_app(args[1]), result); if (m().is_ite(args[1]) && to_app(args[0])->get_arg(0) == to_app(args[1])->get_arg(0)) { // (p (ite C A1 B1) (ite C A2 B2)) --> (ite (p A1 A2) (p B1 B2)) + // TODO: non-deterministic parameter evaluation result = m().mk_ite(to_app(args[0])->get_arg(0), m().mk_app(f, to_app(args[0])->get_arg(1), to_app(args[1])->get_arg(1)), m().mk_app(f, to_app(args[0])->get_arg(2), to_app(args[1])->get_arg(2))); diff --git a/src/math/lp/nla_common.cpp b/src/math/lp/nla_common.cpp index 258fca2bd..3b0902160 100644 --- a/src/math/lp/nla_common.cpp +++ b/src/math/lp/nla_common.cpp @@ -80,6 +80,7 @@ nex * common::nexvar(const rational & coeff, lpvar j, nex_creator& cn, u_depende if (!c().is_monic_var(j)) { c().insert_to_active_var_set(j); + // TODO: non-deterministic parameter evaluation return cn.mk_mul(cn.mk_scalar(coeff), cn.mk_var(j)); } const monic& m = c().emons()[j]; diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp index bf0e3005b..fbec59e20 100644 --- a/src/math/polynomial/polynomial.cpp +++ b/src/math/polynomial/polynomial.cpp @@ -2995,6 +2995,7 @@ namespace polynomial { polynomial * add(polynomial const * p1, polynomial const * p2) { numeral one(1); + // TODO: non-deterministic parameter evaluation return addmul(one, mk_unit(), p1, one, mk_unit(), p2); } @@ -3002,6 +3003,7 @@ namespace polynomial { numeral one(1); numeral minus_one; // It is incorrect to initialize with -1 when numeral_manager is GF_2 m_manager.set(minus_one, -1); + // TODO: non-deterministic parameter evaluation return addmul(one, mk_unit(), p1, minus_one, mk_unit(), p2); } diff --git a/src/model/model.cpp b/src/model/model.cpp index fa4e50e54..1bdda5448 100644 --- a/src/model/model.cpp +++ b/src/model/model.cpp @@ -625,6 +625,7 @@ void model::add_rec_funs() { expr_safe_replace subst(m); unsigned arity = f->get_arity(); for (unsigned i = 0; i < arity; ++i) { + // TODO: non-deterministic parameter evaluation subst.insert(m.mk_var(arity - i - 1, f->get_domain(i)), m.mk_var(i, f->get_domain(i))); } expr_ref bodyr(m); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 995feae62..337dd3a91 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -457,6 +457,7 @@ struct evaluator_cfg : public default_rewriter_cfg { if (interp) { var_subst vs(m, false); result = vs(fi->get_interp(), num, args); + // TODO: non-deterministic parameter evaluation result = m.mk_ite(m.mk_eq(m_au.mk_numeral(rational(0), args[1]->get_sort()), args[1]), result, m.mk_app(f, num, args)); return BR_DONE; } diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index 6917244ca..4f187b1e6 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -714,6 +714,7 @@ pred_transformer::pred_transformer(context& ctx, manager& pm, func_decl* head): m_extend_lit0(m), m_extend_lit(m), m_all_init(false), m_has_quantified_frame(false) { + // TODO: non-deterministic parameter evaluation m_solver = alloc(prop_solver, m, ctx.mk_solver0(), ctx.mk_solver1(), ctx.get_params(), head->get_name()); init_sig (); diff --git a/src/nlsat/tactic/goal2nlsat.cpp b/src/nlsat/tactic/goal2nlsat.cpp index 44f780600..af96c2106 100644 --- a/src/nlsat/tactic/goal2nlsat.cpp +++ b/src/nlsat/tactic/goal2nlsat.cpp @@ -125,6 +125,7 @@ struct goal2nlsat::imp { m_qm.div(lcm, d2, d2); m_qm.neg(d2); polynomial_ref p(m_pm); + // TODO: non-deterministic parameter evaluation p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2); TRACE(goal2nlsat_bug, tout << mk_pp(f, m) << " p: " << p << "\nk: " << k << "\n";); if (is_const(p)) { diff --git a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp index fc812c4f5..930ce0b21 100644 --- a/src/nlsat/tactic/qfnra_nlsat_tactic.cpp +++ b/src/nlsat/tactic/qfnra_nlsat_tactic.cpp @@ -44,6 +44,7 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) { return and_then( mk_report_verbose_tactic("(qfnra-nlsat-tactic)", 10), + // TODO: non-deterministic parameter evaluation and_then(using_params(mk_simplify_tactic(m, p), main_p), using_params(mk_purify_arith_tactic(m, p), @@ -54,6 +55,7 @@ tactic * mk_qfnra_nlsat_tactic(ast_manager & m, params_ref const & p) { mk_elim_term_ite_tactic(m, p), using_params(mk_purify_arith_tactic(m, p), purify_p)), + // TODO: non-deterministic parameter evaluation and_then(/* mk_degree_shift_tactic(m, p), */ // may affect full dimensionality detection factor, mk_solve_eqs_tactic(m, p), diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 90705ae98..c6306f12a 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -892,6 +892,7 @@ namespace opt { for (expr * a : asms) g->assert_expr(a, a); tactic_ref tac0 = + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m, m_params), mk_propagate_values_tactic(m), m_incremental ? mk_skip_tactic() : mk_solve_eqs_tactic(m), diff --git a/src/qe/nlarith_util.cpp b/src/qe/nlarith_util.cpp index 77dad4fdc..879000d25 100644 --- a/src/qe/nlarith_util.cpp +++ b/src/qe/nlarith_util.cpp @@ -555,6 +555,7 @@ namespace nlarith { tout << " 0 [-oo] --> " << mk_pp(t1.get(), m()) << "\n";); } TRACE(nlarith, tout << "inf-branch\n";); + // TODO: non-deterministic parameter evaluation bc.add_branch(mk_and(es.size(), es.data()), m().mk_true(), subst, mk_inf(bc), z(), z(), z()); } @@ -587,6 +588,7 @@ namespace nlarith { es.push_back(m().mk_implies(bc.preds(k), t2)); subst.push_back(t1); } + // TODO: non-deterministic parameter evaluation bc.add_branch(mk_and(es.size(), es.data()), cond, subst, mk_def(cmp, abc_poly(*this, z(), b, c), e0), a, b, c); } @@ -606,6 +608,7 @@ namespace nlarith { es.push_back(m().mk_implies(bc.preds(k), t1)); subst.push_back(t1); } + // TODO: non-deterministic parameter evaluation bc.add_branch(mk_and(es.size(), es.data()), cond, subst, mk_def(cmp, abc_poly(*this, a2, b, z()),e1), a, b, c); } } diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index 07e6d71de..c444f2ebf 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -655,10 +655,12 @@ public: sat_params sp(m_params); if (sp.euf()) m_preprocess = + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m)); else m_preprocess = + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_card2bv_tactic(m, m_params), // updates model converter diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp index 1695f5e41..3b20a7865 100644 --- a/src/sat/smt/arith_solver.cpp +++ b/src/sat/smt/arith_solver.cpp @@ -751,6 +751,7 @@ namespace arith { reset_evidence(); m_explanation.clear(); auto& dm = lp().dep_manager(); + // TODO: non-deterministic parameter evaluation auto* d = dm.mk_join(dm.mk_join(ci1, ci2), dm.mk_join(ci3, ci4)); for (auto ci : lp().flatten(d)) consume(rational::one(), ci); diff --git a/src/smt/dyn_ack.cpp b/src/smt/dyn_ack.cpp index 3a80908bd..83c73e070 100644 --- a/src/smt/dyn_ack.cpp +++ b/src/smt/dyn_ack.cpp @@ -482,6 +482,7 @@ namespace smt { clause_del_eh * del_eh = alloc(dyn_ack_clause_del_eh, *this); justification * js = nullptr; if (m.proofs_enabled()) { + // TODO: non-deterministic parameter evaluation js = alloc(dyn_ack_eq_justification, n1, n2, r, m.mk_eq(n1, r), m.mk_eq(n2, r), diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index 1cebba3e6..142561788 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -274,6 +274,7 @@ interval & interval::operator-=(interval const & other) { } v_dependency * interval::join(v_dependency * d1, v_dependency * d2, v_dependency * d3, v_dependency * d4) { + // TODO: non-deterministic parameter evaluation return m_manager.mk_join(m_manager.mk_join(d1, d2), m_manager.mk_join(d3,d4)); } diff --git a/src/smt/seq_regex.cpp b/src/smt/seq_regex.cpp index 0b84fe28d..eef3690ef 100644 --- a/src/smt/seq_regex.cpp +++ b/src/smt/seq_regex.cpp @@ -487,6 +487,7 @@ namespace smt { expr_ref emp(re().mk_empty(r->get_sort()), m); expr_ref n(m.mk_fresh_const("re.char", seq_sort), m); expr_ref is_non_empty = sk().mk_is_non_empty(r, r, n); + // TODO: non-deterministic parameter evaluation th.add_axiom(th.mk_eq(r1, r2, false), th.mk_literal(is_non_empty)); } diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 51c7f4499..2345fbc18 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -217,6 +217,7 @@ interval theory_arith::mk_interval_for(theory_var v) { if (l->get_value() == u->get_value() && !l->get_value().get_infinitesimal().to_rational().is_zero()) { return interval(m_dep_manager); } + // TODO: non-deterministic parameter evaluation return interval(m_dep_manager, l->get_value().get_rational().to_rational(), l->get_value().get_infinitesimal().to_rational().is_pos(), @@ -1711,6 +1712,7 @@ grobner::monomial * theory_arith::mk_gb_monomial(rational const & _coeff, e if (is_fixed(_var)) { if (!already_found.contains(_var)) { already_found.insert(_var); + // TODO: non-deterministic parameter evaluation dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(_var)), m_dep_manager.mk_leaf(upper(_var)))); } coeff *= lower_bound(_var).get_rational().to_rational(); @@ -1777,6 +1779,7 @@ void theory_arith::add_monomial_def_to_gb(theory_var v, grobner & gb) { monomials.push_back(new_m); rational coeff(-1); if (is_fixed(v)) { + // TODO: non-deterministic parameter evaluation dep = m_dep_manager.mk_join(dep, m_dep_manager.mk_join(m_dep_manager.mk_leaf(lower(v)), m_dep_manager.mk_leaf(upper(v)))); coeff *= lower_bound(v).get_rational().to_rational(); if (!coeff.is_zero()) diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index 72aea761d..cc4154cde 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -388,6 +388,7 @@ namespace smt { expr_ref le(m_arith.mk_le(sz->get_arg(1), nV), m); expr_ref fr(m.mk_app(fg.second, result), m); // set-has-size(a, k) => k <= n or g(f(a,n)) = n + // TODO: non-deterministic parameter evaluation mk_th_axiom(~mk_literal(sz), mk_literal(le), mk_eq(nV, fr)); return result; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 627396678..06f69a52b 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1303,8 +1303,17 @@ public: mk_axiom(eqz, eq); mk_axiom(eqz, mod_ge_0); - mk_axiom(mk_literal(a.mk_le(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, minus_q), mone))); - mk_axiom(mk_literal(a.mk_ge(q, zero)), mk_literal(a.mk_le(a.mk_add(mod, q), mone))); + literal q_le_zero = mk_literal(a.mk_le(q, zero)); + expr_ref mod_minus_q(a.mk_add(mod, minus_q), m); + expr_ref mod_minus_q_le_mone(a.mk_le(mod_minus_q, mone), m); + literal mod_minus_q_le_mone_lit = mk_literal(mod_minus_q_le_mone); + mk_axiom(q_le_zero, mod_minus_q_le_mone_lit); + + literal q_ge_zero = mk_literal(a.mk_ge(q, zero)); + expr_ref mod_plus_q(a.mk_add(mod, q), m); + expr_ref mod_plus_q_le_mone(a.mk_le(mod_plus_q, mone), m); + literal mod_plus_q_le_mone_lit = mk_literal(mod_plus_q_le_mone); + mk_axiom(q_ge_zero, mod_plus_q_le_mone_lit); expr* x = nullptr, * y = nullptr; @@ -2538,9 +2547,11 @@ public: // 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))); - return mk_literal(r); + expr_ref pow_i1(a.mk_int(rational::power_of_two(i + 1)), m); + expr_ref pow_i(a.mk_int(rational::power_of_two(i)), m); + expr_ref mod_expr(a.mk_mod(x, pow_i1), m); + expr_ref ge_expr(a.mk_ge(mod_expr, pow_i), m); + return mk_literal(ge_expr); }; if (a.is_band(n)) { @@ -2668,9 +2679,28 @@ public: // 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))); - ctx().mk_th_axiom(get_id(), ~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)))); - ctx().mk_th_axiom(get_id(), ~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)))); - ctx().mk_th_axiom(get_id(), ~mk_literal(a.mk_eq(a.mk_mod(y, a.mk_int(N)), a.mk_int(0))), mk_literal(m.mk_eq(n, x))); + expr_ref int_N(a.mk_int(N), m); + expr_ref int_sz(a.mk_int(sz), m); + expr_ref int_zero(a.mk_int(0), m); + expr_ref int_N_minus_one(a.mk_int(N - 1), m); + + expr_ref y_mod_N(a.mk_mod(y, int_N), m); + expr_ref y_mod_N_ge_sz(a.mk_ge(y_mod_N, int_sz), m); + literal y_mod_N_ge_sz_lit = mk_literal(y_mod_N_ge_sz); + + expr_ref n_eq_zero(m.mk_eq(n, int_zero), m); + literal n_eq_zero_lit = mk_literal(n_eq_zero); + ctx().mk_th_axiom(get_id(), ~y_mod_N_ge_sz_lit, signx, n_eq_zero_lit); + + expr_ref n_eq_N_minus_one(m.mk_eq(n, int_N_minus_one), m); + literal n_eq_N_minus_one_lit = mk_literal(n_eq_N_minus_one); + ctx().mk_th_axiom(get_id(), ~y_mod_N_ge_sz_lit, ~signx, n_eq_N_minus_one_lit); + + expr_ref y_mod_N_eq_zero(m.mk_eq(y_mod_N, int_zero), m); + literal y_mod_N_eq_zero_lit = mk_literal(y_mod_N_eq_zero); + expr_ref n_eq_x(m.mk_eq(n, x), m); + literal n_eq_x_lit = mk_literal(n_eq_x); + ctx().mk_th_axiom(get_id(), ~y_mod_N_eq_zero_lit, n_eq_x_lit); } else UNREACHABLE(); @@ -3744,8 +3774,12 @@ public: return; } expr_ref lce(a.mk_numeral(lc, is_int), m); - if (all_int) - guards.push_back(m.mk_eq(a.mk_mod(term, lce), a.mk_int(0))); + if (all_int) { + expr_ref term_mod_lce(a.mk_mod(term, lce), m); + expr_ref zero_int(a.mk_int(0), m); + expr_ref mod_eq_zero(m.mk_eq(term_mod_lce, zero_int), m); + guards.push_back(mod_eq_zero); + } else if (is_int) guards.push_back(a.mk_is_int(a.mk_div(term, lce))); if (is_int) diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 2a70f25d8..fc43c83fd 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -573,6 +573,7 @@ expr_ref theory_seq::mk_nth(expr* s, expr* idx) { void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) { m_sk.decompose(e, head, tail); add_axiom(~mk_eq_empty(e), mk_eq_empty(tail));; + // TODO: non-deterministic parameter evaluation add_axiom(mk_eq_empty(e), mk_eq(e, mk_concat(head, tail), false)); } diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h index 99344eb31..655c4ab50 100644 --- a/src/smt/theory_utvpi.h +++ b/src/smt/theory_utvpi.h @@ -171,6 +171,7 @@ namespace smt { struct var_value_eq { theory_utvpi & m_th; var_value_eq(theory_utvpi & th):m_th(th) {} + // TODO: non-deterministic parameter evaluation bool operator()(theory_var v1, theory_var v2) const { return m_th.mk_value(v1, false) == m_th.mk_value(v2, false) && m_th.is_int(v1) == m_th.is_int(v2); } }; diff --git a/src/tactic/arith/bv2real_rewriter.cpp b/src/tactic/arith/bv2real_rewriter.cpp index 660e92dd6..db9474a4a 100644 --- a/src/tactic/arith/bv2real_rewriter.cpp +++ b/src/tactic/arith/bv2real_rewriter.cpp @@ -585,6 +585,7 @@ br_status bv2real_rewriter::mk_ite(expr* c, 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); + // TODO: non-deterministic parameter evaluation if (u().mk_bv2real(m().mk_ite(c, s1, t1), m().mk_ite(c, s2, t2), d1, r1, result)) { return BR_DONE; } @@ -614,6 +615,7 @@ br_status bv2real_rewriter::mk_uminus(expr * s, expr_ref & result) { if (u().is_bv2real(s, s1, s2, d1, r1)) { s1 = u().mk_extend(1, s1); s2 = u().mk_extend(1, s2); + // TODO: non-deterministic parameter evaluation if (u().mk_bv2real(m_bv.mk_bv_neg(s1), m_bv.mk_bv_neg(s2), d1, r1, result)) { return BR_DONE; } @@ -636,6 +638,7 @@ br_status bv2real_rewriter::mk_add(expr* s, expr* t, expr_ref& result) { rational d1, d2, r1, r2; if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) { u().align_divisors(s1, s2, t1, t2, d1, d2); + // TODO: non-deterministic parameter evaluation if (u().mk_bv2real(u().mk_bv_add(s1, t1), u().mk_bv_add(t2, s2), d1, r1, result)) { return BR_DONE; } @@ -696,6 +699,7 @@ br_status bv2real_rewriter::mk_sub(expr* s, expr* t, expr_ref& result) { rational d1, d2, r1, r2; if (u().is_bv2real(s, s1, s2, d1, r1) && u().is_bv2real(t, t1, t2, d2, r2) && r1 == r2) { u().align_divisors(s1, s2, t1, t2, d1, d2); + // TODO: non-deterministic parameter evaluation if (u().mk_bv2real(u().mk_bv_sub(s1, t1), u().mk_bv_sub(s2, t2), d1, r1, result)) { return BR_DONE; } diff --git a/src/tactic/arith/factor_tactic.cpp b/src/tactic/arith/factor_tactic.cpp index 824fd0020..48acb09c3 100644 --- a/src/tactic/arith/factor_tactic.cpp +++ b/src/tactic/arith/factor_tactic.cpp @@ -157,6 +157,7 @@ class factor_tactic : public tactic { } } else { + // TODO: non-deterministic parameter evaluation args.push_back(m.mk_app(m_util.get_family_id(), k, mk_mul(odd_factors.size(), odd_factors.data()), mk_zero_for(odd_factors[0]))); } SASSERT(!args.empty()); @@ -188,6 +189,7 @@ class factor_tactic : public tactic { m_qm.div(lcm, d2, d2); m_qm.neg(d2); polynomial_ref p(m_pm); + // TODO: non-deterministic parameter evaluation p = m_pm.addmul(d1, m_pm.mk_unit(), p1, d2, m_pm.mk_unit(), p2); if (is_const(p)) return BR_FAILED; diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index cefa5079c..d178dec07 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -163,6 +163,7 @@ public: expr_ref v(m.mk_fresh_const(x->get_decl()->get_name(), m.mk_bool_sort()), m); if (last_v) axioms.push_back(m.mk_implies(v, last_v)); + // TODO: non-deterministic parameter evaluation xs.push_back(m.mk_ite(v, a.mk_int(1), a.mk_int(0))); m_mc->hide(v); last_v = v; diff --git a/src/tactic/core/special_relations_tactic.cpp b/src/tactic/core/special_relations_tactic.cpp index ec63543f2..2b6d0d5d7 100644 --- a/src/tactic/core/special_relations_tactic.cpp +++ b/src/tactic/core/special_relations_tactic.cpp @@ -77,6 +77,7 @@ void special_relations_tactic::initialize() { expr* pats[1] = { pat }; expr* pats0[1] = { pat0 }; + // TODO: non-deterministic parameter evaluation fml = m.mk_or(m.mk_not(Rxy), m.mk_not(Ryz), Rxz); q = m.mk_forall(3, As, xyz, fml, 0, symbol::null, symbol::null, 1, pats); register_pattern(m_pm.initialize(q), sr_transitive); diff --git a/src/tactic/fpa/qffp_tactic.cpp b/src/tactic/fpa/qffp_tactic.cpp index fbac861d8..98a1b0a39 100644 --- a/src/tactic/fpa/qffp_tactic.cpp +++ b/src/tactic/fpa/qffp_tactic.cpp @@ -82,6 +82,7 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("arith_lhs", true); simp_p.set_bool("elim_and", true); + // TODO: non-deterministic parameter evaluation tactic * preamble = and_then(mk_simplify_tactic(m, simp_p), mk_propagate_values_tactic(m, p), mk_fpa2bv_tactic(m, p), @@ -93,9 +94,11 @@ tactic * mk_qffp_tactic(ast_manager & m, params_ref const & p) { mk_bit_blaster_tactic(m, p), using_params(mk_simplify_tactic(m, p), simp_p), cond(mk_is_propositional_probe(), + // TODO: non-deterministic parameter evaluation cond(mk_produce_proofs_probe(), mk_smt_tactic(m, p), // `sat' does not support proofs. mk_psat_tactic(m, p)), + // TODO: non-deterministic parameter evaluation cond(mk_is_fp_qfnra_probe(), mk_qfnra_tactic(m, p), mk_smt_tactic(m, p)))); diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 883cacdab..b43515d2f 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -35,20 +35,34 @@ Notes: tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m, p), + // TODO: non-deterministic parameter evaluation + // TODO: non-deterministic parameter evaluation cond(mk_and(mk_is_propositional_probe(), mk_not(mk_produce_proofs_probe())), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_fd_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qfbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfbv_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qfaufbv_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfaufbv_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflia_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qfauflia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfauflia_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qflra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qflra_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qfnra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnra_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qfnia_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qfnia_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_lira_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_lira_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_nra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_nra_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qffp_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffp_tactic(m, p); }), + // TODO: non-deterministic parameter evaluation cond(mk_is_qffplra_probe(), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_qffplra_tactic(m, p); }), //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), + // TODO: non-deterministic parameter evaluation and_then(mk_preamble_tactic(m), mk_lazy_tactic(m, p, [&](auto& m, auto const& p) { return mk_smt_tactic(m, p);}))))))))))))))), p); return st; diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index ffd6450b3..3b089d6fd 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -185,6 +185,7 @@ public: if (!t) { t = mk_tactic_for_logic(m, p, l); } + // TODO: non-deterministic parameter evaluation return mk_combined_solver(mk_tactic2solver(m, t.get(), p, proofs_enabled, models_enabled, unsat_core_enabled, l), mk_solver_for_logic(m, p, l), p); diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp index 4467d6d85..497ca7924 100644 --- a/src/tactic/sls/sls_tactic.cpp +++ b/src/tactic/sls/sls_tactic.cpp @@ -245,6 +245,7 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p, bool add_nnf) gaussian_p.set_uint("gaussian_max_occs", 2); return and_then( + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m), using_params(mk_solve_eqs_tactic(m), gaussian_p), @@ -258,6 +259,7 @@ static tactic * mk_preamble(ast_manager & m, params_ref const & p, bool add_nnf) } tactic * mk_qfbv_sls_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * t = and_then(mk_preamble(m, p, true), mk_sls_tactic(m, p)); t->updt_params(p); return t; diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 4f3d18c1f..9bb4c7f6e 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -35,6 +35,7 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { p2.set_uint("seed", 13); p2.set_bool("factor", false); + // TODO: non-deterministic parameter evaluation return and_then( mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), @@ -44,6 +45,7 @@ tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) { or_else(try_for(mk_qfnra_nlsat_tactic(m, p), 5000), try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), mk_qfnra_nlsat_tactic(m, p2)), + // TODO: non-deterministic parameter evaluation or_else(mk_nlqsat_tactic(m, p), mk_smt_tactic(m, p)) )); diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp index acad15fd6..f960ee09a 100644 --- a/src/tactic/smtlogics/qfaufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp @@ -38,6 +38,7 @@ static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) { simp2_p.set_uint("local_ctx_limit", 10000000); + // TODO: non-deterministic parameter evaluation return and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), @@ -59,6 +60,7 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params( and_then(preamble_st, + // TODO: non-deterministic parameter evaluation cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m, p))), main_p); st->updt_params(p); diff --git a/src/tactic/smtlogics/qfauflia_tactic.cpp b/src/tactic/smtlogics/qfauflia_tactic.cpp index 5c2a92ef6..51aa95a73 100644 --- a/src/tactic/smtlogics/qfauflia_tactic.cpp +++ b/src/tactic/smtlogics/qfauflia_tactic.cpp @@ -33,6 +33,7 @@ tactic * mk_qfauflia_tactic(ast_manager & m, params_ref const & p) { params_ref solver_p; solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module + // TODO: non-deterministic parameter evaluation tactic * preamble_st = and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 07784eb3b..32a5de2a3 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -58,6 +58,7 @@ static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) { hoist_p.set_bool("flat_and_or", false); return + // TODO: non-deterministic parameter evaluation and_then( using_params(mk_simplify_tactic(m), flat_and_or_p), using_params(mk_propagate_values_tactic(m), flat_and_or_p), @@ -107,7 +108,9 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat using_params(smt, solver_p)), cond(mk_is_qfbv_probe(), and_then(mk_bit_blaster_tactic(m), + // TODO: non-deterministic parameter evaluation when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), + // TODO: non-deterministic parameter evaluation and_then(using_params(and_then(mk_simplify_tactic(m), mk_solve_eqs_tactic(m)), local_ctx_p), @@ -122,7 +125,9 @@ static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat tactic * mk_qfbv_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * new_sat = cond(mk_produce_proofs_probe(), + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m), mk_smt_tactic(m, p)), mk_psat_tactic(m, p)); return mk_qfbv_tactic(m, p, new_sat, mk_smt_tactic(m, p)); diff --git a/src/tactic/smtlogics/qfidl_tactic.cpp b/src/tactic/smtlogics/qfidl_tactic.cpp index c86789ed0..267c31947 100644 --- a/src/tactic/smtlogics/qfidl_tactic.cpp +++ b/src/tactic/smtlogics/qfidl_tactic.cpp @@ -55,11 +55,13 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { pull_ite_p.set_bool("local_ctx", true); pull_ite_p.set_uint("local_ctx_limit", 10000000); + // TODO: non-deterministic parameter evaluation tactic * preamble_st = and_then(and_then(mk_simplify_tactic(m), mk_fix_dl_var_tactic(m), mk_propagate_values_tactic(m), mk_elim_uncnstr_tactic(m) ), + // TODO: non-deterministic parameter evaluation and_then(mk_solve_eqs_tactic(m), using_params(mk_simplify_tactic(m), lhs_p), mk_propagate_values_tactic(m), @@ -76,6 +78,7 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { // dynamic psm seems to work well. bv_solver_p.set_sym("gc", symbol("dyn_psm")); + // TODO: non-deterministic parameter evaluation tactic * bv_solver = using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), @@ -95,7 +98,11 @@ tactic * mk_qfidl_tactic(ast_manager & m, params_ref const & p) { params_ref diff_neq_p; diff_neq_p.set_uint("diff_neq_max_k", 25); + // TODO: non-deterministic parameter evaluation + // TODO: non-deterministic parameter evaluation + // TODO: non-deterministic parameter evaluation tactic * st = cond(mk_and(mk_lt(mk_num_consts_probe(), mk_const_probe(static_cast(BIG_PROBLEM))), + // TODO: non-deterministic parameter evaluation mk_and(mk_not(mk_produce_proofs_probe()), mk_not(mk_produce_unsat_cores_probe()))), using_params(and_then(preamble_st, diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index e728a33ac..07b88a02b 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -86,6 +86,7 @@ static tactic * mk_bv2sat_tactic(ast_manager & m) { // dynamic psm seems to work well. solver_p.set_sym("gc", symbol("dyn_psm")); + // TODO: non-deterministic parameter evaluation return using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), mk_solve_eqs_tactic(m), @@ -110,6 +111,7 @@ static tactic * mk_pb_tactic(ast_manager & m) { and_then(fail_if_not(mk_is_pb_probe()), fail_if(mk_produce_proofs_probe()), fail_if(mk_produce_unsat_cores_probe()), + // TODO: non-deterministic parameter evaluation or_else(and_then(fail_if(mk_ge(mk_num_exprs_probe(), mk_const_probe(SMALL_SIZE))), fail_if_not(mk_is_ilp_probe()), // try_for(mk_mip_tactic(m), 8000), @@ -129,6 +131,7 @@ static tactic * mk_lia2sat_tactic(ast_manager & m) { return annotate_tactic( "lia2sat-tactic", + // TODO: non-deterministic parameter evaluation and_then(fail_if(mk_is_unbounded_probe()), fail_if(mk_produce_proofs_probe()), fail_if(mk_produce_unsat_cores_probe()), @@ -152,6 +155,8 @@ static tactic * mk_ilp_model_finder_tactic(ast_manager & m) { return annotate_tactic( "ilp-model-finder-tactic", + // TODO: non-deterministic parameter evaluation + // TODO: non-deterministic parameter evaluation and_then(fail_if_not(mk_and(mk_is_ilp_probe(), mk_is_unbounded_probe())), fail_if(mk_produce_proofs_probe()), fail_if(mk_produce_unsat_cores_probe()), @@ -198,6 +203,7 @@ tactic * mk_preamble_tactic(ast_manager& m) { lia2card_p.set_uint("lia2card.max_ite_nesting", 1); return + // TODO: non-deterministic parameter evaluation and_then( mk_simplify_tactic(m), mk_propagate_values_tactic(m), @@ -228,6 +234,7 @@ tactic * mk_qflia_tactic(ast_manager & m, params_ref const & p) { and_then( mk_preamble_tactic(m), using_params(mk_simplify_tactic(m), lhs_p), + // TODO: non-deterministic parameter evaluation or_else(mk_ilp_model_finder_tactic(m), mk_pb_tactic(m), and_then(fail_if_not(mk_is_quasi_pb_probe()), diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 25dc34d9c..4f1cca0bb 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -48,6 +48,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { mem_p.set_uint("max_conflicts", 500); + // TODO: non-deterministic parameter evaluation tactic * r = using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_simplify_tactic(m), simp2_p), @@ -73,6 +74,7 @@ static tactic * mk_qfnia_preamble(ast_manager & m, params_ref const & p_ref) { elim_p.set_uint("max_memory",20); return + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), @@ -89,6 +91,7 @@ static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) { params_ref simp_p = p; simp_p.set_bool("hoist_mul", true); // hoist multipliers to create smaller circuits. + // TODO: non-deterministic parameter evaluation return and_then(using_params(mk_simplify_tactic(m), simp_p), mk_nla2bv_tactic(m, nia2sat_p), skip_if_failed(mk_qfnia_bv_solver(m, p)), @@ -114,9 +117,11 @@ static tactic * mk_qfnia_smt_solver(ast_manager& m, params_ref const& p) { } tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation return and_then( mk_report_verbose_tactic("(qfnia-tactic)", 10), mk_qfnia_preamble(m, p), + // TODO: non-deterministic parameter evaluation or_else(mk_qfnia_sat_solver(m, p), try_for(mk_qfnia_smt_solver(m, p), 2000), mk_qfnia_nlsat_solver(m, p), diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 79e0a4b39..94d8c328e 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -39,6 +39,7 @@ tactic * mk_qfnra_very_small_solver(ast_manager& m, params_ref const& p) { params_ref p_sc = p; p_sc.set_bool("simple_check", true); // p_sc.set_uint("seed", 997); + // TODO: non-deterministic parameter evaluation ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 10 * 1000)); } { @@ -95,6 +96,7 @@ tactic * mk_qfnra_small_solver(ast_manager& m, params_ref const& p) { params_ref p_sc = p; p_sc.set_bool("simple_check", true); // p_sc.set_uint("seed", 997); + // TODO: non-deterministic parameter evaluation ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 20 * 1000)); } { @@ -152,6 +154,7 @@ tactic * mk_qfnra_middle_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); + // TODO: non-deterministic parameter evaluation ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 30 * 1000)); } { @@ -210,6 +213,7 @@ tactic * mk_qfnra_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); + // TODO: non-deterministic parameter evaluation ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 50 * 1000)); } { @@ -264,6 +268,7 @@ tactic * mk_qfnra_very_large_solver(ast_manager& m, params_ref const& p) { { params_ref p_sc = p; p_sc.set_bool("simple_check", true); + // TODO: non-deterministic parameter evaluation ts.push_back(try_for(and_then(mk_qfnra_nlsat_tactic(m, p_sc), mk_fail_if_undecided_tactic()), 100 * 1000)); } { @@ -305,12 +310,16 @@ tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) { auto middle_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_middle_solver(m, p); }); auto large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_large_solver(m, p); }); auto very_large_t = mk_lazy_tactic(m, p, [&](ast_manager& m, params_ref const& p) {return mk_qfnra_very_large_solver(m, p); }); + // TODO: non-deterministic parameter evaluation return cond(mk_lt(mk_memory_probe(), mk_const_probe(VERY_SMALL_THRESHOLD)), very_small_t, + // TODO: non-deterministic parameter evaluation cond(mk_lt(mk_memory_probe(), mk_const_probe(SMALL_THRESHOLD)), small_t, + // TODO: non-deterministic parameter evaluation cond(mk_lt(mk_memory_probe(), mk_const_probe(MIDDLE_THRESHOLD)), middle_t, + // TODO: non-deterministic parameter evaluation cond(mk_lt(mk_memory_probe(), mk_const_probe(LARGE_THRESHOLD)), large_t, very_large_t @@ -322,6 +331,7 @@ tactic * mk_qfnra_mixed_solver(ast_manager& m, params_ref const& p) { tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { + // TODO: non-deterministic parameter evaluation return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), mk_qfnra_mixed_solver(m, p) diff --git a/src/tactic/smtlogics/qfuf_tactic.cpp b/src/tactic/smtlogics/qfuf_tactic.cpp index 609107a48..b0ddaaf11 100644 --- a/src/tactic/smtlogics/qfuf_tactic.cpp +++ b/src/tactic/smtlogics/qfuf_tactic.cpp @@ -29,6 +29,7 @@ tactic * mk_qfuf_tactic(ast_manager & m, params_ref const & p) { s2_p.set_bool("pull_cheap_ite", true); s2_p.set_bool("local_ctx", true); s2_p.set_uint("local_ctx_limit", 10000000); + // TODO: non-deterministic parameter evaluation return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), mk_solve_eqs_tactic(m, p), diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 160e56295..f816e348c 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -150,6 +150,7 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { ctx_simp_p.set_uint("max_depth", 32); ctx_simp_p.set_uint("max_steps", 5000000); + // TODO: non-deterministic parameter evaluation return and_then( using_params(mk_simplify_tactic(m), flat_and_or_p), using_params(mk_propagate_values_tactic(m), flat_and_or_p), @@ -166,6 +167,7 @@ static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) { static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) { params_ref simp2_p = p, flat_and_or_p = p; flat_and_or_p.set_bool("flat_and_or", false); + // TODO: non-deterministic parameter evaluation return and_then(using_params(mk_simplify_tactic(m), flat_and_or_p), using_params(mk_propagate_values_tactic(m), flat_and_or_p), mk_solve_eqs_tactic(m), @@ -186,6 +188,7 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params( and_then(preamble_st, + // TODO: non-deterministic parameter evaluation cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), mk_smt_tactic(m, p))), @@ -200,5 +203,6 @@ tactic * mk_qfufbv_ackr_tactic(ast_manager & m, params_ref const & p) { tactic * const actual_tactic = alloc(qfufbv_ackr_tactic, m, p); return and_then(preamble_t, + // TODO: non-deterministic parameter evaluation cond(mk_is_qfufbv_probe(), actual_tactic, mk_smt_tactic(m, p))); } diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp index 77073484b..55862411e 100644 --- a/src/tactic/smtlogics/quant_tactics.cpp +++ b/src/tactic/smtlogics/quant_tactics.cpp @@ -43,10 +43,12 @@ static tactic * mk_quant_preprocessor(ast_manager & m, bool disable_gaussian = f solve_eqs = mk_skip_tactic(); } else { + // TODO: non-deterministic parameter evaluation solve_eqs = when(mk_not(mk_has_pattern_probe()), mk_solve_eqs_tactic(m)); } // remark: investigate if gaussian elimination is useful when patterns are not provided. + // TODO: non-deterministic parameter evaluation return and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_ctx_simplify_tactic(m), ctx_simp_p), @@ -61,6 +63,7 @@ static tactic * mk_no_solve_eq_preprocessor(ast_manager & m) { } tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * st = and_then(mk_no_solve_eq_preprocessor(m), mk_qe_lite_tactic(m, p), mk_smt_tactic(m)); @@ -69,6 +72,7 @@ tactic * mk_ufnia_tactic(ast_manager & m, params_ref const & p) { } tactic * mk_uflra_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * st = and_then(mk_quant_preprocessor(m), mk_smt_tactic(m)); st->updt_params(p); @@ -80,6 +84,7 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) { qi_p.set_str("qi.cost", "0"); TRACE(qi_cost, qi_p.display(tout); tout << "\n" << qi_p.get_str("qi.cost", "") << "\n";); tactic * st = and_then(mk_no_solve_eq_preprocessor(m), + // TODO: non-deterministic parameter evaluation or_else(and_then(fail_if(mk_gt(mk_num_exprs_probe(), mk_const_probe(static_cast(128)))), using_params(mk_smt_tactic(m), qi_p), mk_fail_if_undecided_tactic()), @@ -89,6 +94,7 @@ tactic * mk_auflia_tactic(ast_manager & m, params_ref const & p) { } tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * st = and_then(mk_quant_preprocessor(m), mk_smt_tactic(m)); st->updt_params(p); @@ -96,6 +102,7 @@ tactic * mk_auflira_tactic(ast_manager & m, params_ref const & p) { } tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * st = and_then(mk_quant_preprocessor(m), mk_smt_tactic(m)); st->updt_params(p); @@ -103,10 +110,14 @@ tactic * mk_aufnira_tactic(ast_manager & m, params_ref const & p) { } tactic * mk_lra_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation tactic * st = and_then(mk_quant_preprocessor(m), mk_qe_lite_tactic(m, p), + // TODO: non-deterministic parameter evaluation cond(mk_has_quantifier_probe(), + // TODO: non-deterministic parameter evaluation cond(mk_is_lira_probe(), + // TODO: non-deterministic parameter evaluation or_else(mk_qsat_tactic(m, p), mk_smt_tactic(m)), mk_smt_tactic(m)), mk_smt_tactic(m))); diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index e8495c013..e1154f043 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -32,6 +32,7 @@ Notes: static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) { + // TODO: non-deterministic parameter evaluation return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)), 5); } @@ -39,22 +40,32 @@ static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & params_ref no_elim_and(p); no_elim_and.set_bool("elim_and", false); + // TODO: non-deterministic parameter evaluation return and_then( mk_trace_tactic("ufbv_pre"), + // TODO: non-deterministic parameter evaluation and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), and_then(if_no_proofs(if_no_unsat_cores(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and))), mk_simplify_tactic(m, p)), + // TODO: non-deterministic parameter evaluation and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), mk_elim_and_tactic(m, p), mk_solve_eqs_tactic(m, p), + // TODO: non-deterministic parameter evaluation and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), + // TODO: non-deterministic parameter evaluation and_then(mk_distribute_forall_tactic(m, p), mk_simplify_tactic(m, p))), if_no_unsat_cores( + // TODO: non-deterministic parameter evaluation and_then(and_then(mk_reduce_args_tactic(m, p), mk_simplify_tactic(m, p)), + // TODO: non-deterministic parameter evaluation and_then(mk_macro_finder_tactic(m, p), mk_simplify_tactic(m, p)), + // TODO: non-deterministic parameter evaluation and_then(mk_ufbv_rewriter_tactic(m, p), mk_simplify_tactic(m, p)), + // TODO: non-deterministic parameter evaluation and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)))), + // TODO: non-deterministic parameter evaluation and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), mk_simplify_tactic(m, p), mk_trace_tactic("ufbv_post")); diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index e1dd9d2b2..5a86b7a31 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -786,6 +786,7 @@ Notes: // result => xs[0] + ... + xs[n-1] <= 1 for (unsigned i = 0; i < n; ++i) { for (unsigned j = i + 1; j < n; ++j) { + // TODO: non-deterministic parameter evaluation add_clause(mk_not(result), mk_not(xs[i]), mk_not(xs[j])); } } @@ -877,6 +878,7 @@ Notes: } for (unsigned i = 0; i + 1 < n; ++i) { add_clause(mk_not(xs[i]), ys[i]); + // TODO: non-deterministic parameter evaluation add_clause(mk_not(r), mk_not(ys[i]), mk_not(xs[i + 1])); } @@ -901,7 +903,9 @@ Notes: } if (is_eq) { literal zero = fresh("zero"); + // TODO: non-deterministic parameter evaluation add_clause(mk_not(zero), mk_not(xs[n-1])); + // TODO: non-deterministic parameter evaluation add_clause(mk_not(zero), mk_not(ys[n-2])); add_clause(r, zero, twos.back()); } @@ -939,6 +943,7 @@ Notes: for (unsigned i = 0; i < ors.size(); ++i) { for (unsigned k = 0; k < nbits; ++k) { bool bit_set = (i & (static_cast(1 << k))) != 0; + // TODO: non-deterministic parameter evaluation add_clause(mk_not(result), mk_not(ors[i]), bit_set ? bits[k] : mk_not(bits[k])); } } @@ -1036,6 +1041,7 @@ Notes: void cmp_le(literal x1, literal x2, literal y1, literal y2) { add_clause(mk_not(x1), y1); add_clause(mk_not(x2), y1); + // TODO: non-deterministic parameter evaluation add_clause(mk_not(x1), mk_not(x2), y2); } @@ -1415,6 +1421,7 @@ Notes: } for (unsigned i = 1; i <= a; ++i) { for (unsigned j = 1; j <= b && i + j <= c; ++j) { + // TODO: non-deterministic parameter evaluation add_clause(mk_not(as[i-1]),mk_not(bs[j-1]),out[i+j-1]); } }