diff --git a/src/smt/theory_array_bapa.cpp b/src/smt/theory_array_bapa.cpp index cc4154cde..82a25f1bc 100644 --- a/src/smt/theory_array_bapa.cpp +++ b/src/smt/theory_array_bapa.cpp @@ -388,8 +388,11 @@ 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)); + literal sz_lit = mk_literal(sz); + literal not_sz_lit = ~sz_lit; + literal le_lit = mk_literal(le); + literal eq_lit = mk_eq(nV, fr); + mk_th_axiom(not_sz_lit, le_lit, eq_lit); return result; } diff --git a/src/tactic/arith/lia2card_tactic.cpp b/src/tactic/arith/lia2card_tactic.cpp index d178dec07..8bd6412f5 100644 --- a/src/tactic/arith/lia2card_tactic.cpp +++ b/src/tactic/arith/lia2card_tactic.cpp @@ -163,8 +163,10 @@ 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))); + expr_ref one(a.mk_int(1), m); + expr_ref zero(a.mk_int(0), m); + expr_ref ite(m.mk_ite(v, one, zero), m); + xs.push_back(ite); m_mc->hide(v); last_v = v; } diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp index 9bb4c7f6e..593f0e5c4 100644 --- a/src/tactic/smtlogics/nra_tactic.cpp +++ b/src/tactic/smtlogics/nra_tactic.cpp @@ -35,20 +35,30 @@ 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 + tactic* simplify1 = mk_simplify_tactic(m, p); + tactic* propagate = mk_propagate_values_tactic(m, p); + tactic* qe_lite = mk_qe_lite_tactic(m); + tactic* simplify2 = mk_simplify_tactic(m, p); + + tactic* qfnra_main = mk_qfnra_nlsat_tactic(m, p); + tactic* try_qfnra_main = try_for(qfnra_main, 5000); + tactic* qfnra_alt1 = mk_qfnra_nlsat_tactic(m, p1); + tactic* try_qfnra_alt1 = try_for(qfnra_alt1, 10000); + tactic* qfnra_alt2 = mk_qfnra_nlsat_tactic(m, p2); + tactic* qfnra_branch = or_else(try_qfnra_main, try_qfnra_alt1, qfnra_alt2); + + tactic* nlqsat = mk_nlqsat_tactic(m, p); + tactic* smt = mk_smt_tactic(m, p); + tactic* fallback_branch = or_else(nlqsat, smt); + + probe* qfnra_probe = mk_is_qfnra_probe(); + tactic* conditional = cond(qfnra_probe, qfnra_branch, fallback_branch); + return and_then( - mk_simplify_tactic(m, p), - mk_propagate_values_tactic(m, p), - mk_qe_lite_tactic(m), - mk_simplify_tactic(m, p), - cond(mk_is_qfnra_probe(), - 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)) - )); + simplify1, + propagate, + qe_lite, + simplify2, + conditional); } - diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index 5a86b7a31..0da851ad7 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -784,10 +784,12 @@ Notes: } // result => xs[0] + ... + xs[n-1] <= 1 + literal not_result = mk_not(result); 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])); + literal not_xi = mk_not(xs[i]); + literal not_xj = mk_not(xs[j]); + add_clause(not_result, not_xi, not_xj); } } @@ -876,10 +878,12 @@ Notes: for (unsigned i = 0; i + 2 < n; ++i) { add_clause(mk_not(ys[i]), ys[i + 1]); } + literal not_r = mk_not(r); 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])); + literal not_yi = mk_not(ys[i]); + literal not_x_next = mk_not(xs[i + 1]); + add_clause(not_r, not_yi, not_x_next); } if (is_eq) { @@ -903,10 +907,11 @@ 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])); + literal not_zero = mk_not(zero); + literal not_x_last = mk_not(xs[n-1]); + literal not_y_last = mk_not(ys[n-2]); + add_clause(not_zero, not_x_last); + add_clause(not_zero, not_y_last); add_clause(r, zero, twos.back()); } else { @@ -940,11 +945,13 @@ Notes: for (unsigned k = 0; k < nbits; ++k) { bits.push_back(fresh("bit")); } + literal not_result = mk_not(result); 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])); + literal not_or = mk_not(ors[i]); + literal bit_lit = bit_set ? bits[k] : mk_not(bits[k]); + add_clause(not_result, not_or, bit_lit); } } return result; @@ -1041,8 +1048,9 @@ 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); + literal not_x1 = mk_not(x1); + literal not_x2 = mk_not(x2); + add_clause(not_x1, not_x2, y2); } void cmp_eq(literal x1, literal x2, literal y1, literal y2) { @@ -1421,8 +1429,10 @@ 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]); + literal not_ai = mk_not(as[i-1]); + literal not_bj = mk_not(bs[j-1]); + literal out_lit = out[i + j - 1]; + add_clause(not_ai, not_bj, out_lit); } } }