diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index b040efc0c..e67300970 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -704,7 +704,7 @@ br_status arith_rewriter::mk_mod_core(expr * arg1, expr * arg2, expr_ref & resul } // propagate mod inside only if not all arguments are not already mod. - if (m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { + if (false && m_util.is_numeral(arg2, v2, is_int) && is_int && v2.is_pos() && (is_add(arg1) || is_mul(arg1))) { TRACE("mod_bug", tout << "mk_mod:\n" << mk_ismt2_pp(arg1, m()) << "\n" << mk_ismt2_pp(arg2, m()) << "\n";); unsigned num_args = to_app(arg1)->get_num_args(); unsigned i; diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index d63f0ae00..770a49c07 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1120,6 +1120,7 @@ namespace qe { st->init(fml); st->m_vars.append(m_vars.size(), m_vars.c_ptr()); SASSERT(invariant()); + TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(fml, m) << "\n";); return st; } @@ -1133,6 +1134,7 @@ namespace qe { m_branch_index.insert(branch_id, index); st->m_vars.append(m_vars.size(), m_vars.c_ptr()); SASSERT(invariant()); + //TRACE("qe", tout << mk_pp(m_fml, m) << " child: " << mk_pp(st->fml(), m) << "\n";); return st; } @@ -1164,6 +1166,16 @@ namespace qe { } } + expr_ref abstract_variable(app* x, expr* fml) const { + expr_ref result(m); + expr* y = x; + expr_abstract(m, 0, 1, &y, fml, result); + symbol X(x->get_decl()->get_name()); + sort* s = m.get_sort(x); + result = m.mk_exists(1, &s, &X, result); + return result; + } + void display_validate(std::ostream& out) const { if (m_children.empty()) { return; @@ -1171,25 +1183,53 @@ namespace qe { expr_ref q(m); expr* x = m_var; if (x) { - expr_abstract(m, 0, 1, &x, m_fml, q); - ptr_vector fmls; + q = abstract_variable(m_var, m_fml); + + expr_ref_vector fmls(m); + expr_ref fml(m); for (unsigned i = 0; i < m_children.size(); ++i) { - expr* fml = m_children[i]->fml(); + search_tree const& child = *m_children[i]; + fml = child.fml(); if (fml) { + // abstract free variables in children. + ptr_vector child_vars, new_vars; + child_vars.append(child.m_vars.size(), child.m_vars.c_ptr()); + if (child.m_var) { + child_vars.push_back(child.m_var); + } + for (unsigned j = 0; j < child_vars.size(); ++j) { + if (!m_vars.contains(child_vars[j]) && + !new_vars.contains(child_vars[j])) { + fml = abstract_variable(child_vars[j], fml); + new_vars.push_back(child_vars[j]); + } + } fmls.push_back(fml); } } - symbol X(m_var->get_decl()->get_name()); - sort* s = m.get_sort(x); - q = m.mk_exists(1, &s, &X, q); - expr_ref tmp(m); - bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), tmp); - expr_ref f(m.mk_not(m.mk_iff(q, tmp)), m); + bool_rewriter(m).mk_or(fmls.size(), fmls.c_ptr(), fml); + + fml = m.mk_not(m.mk_iff(q, fml)); ast_smt_pp pp(m); - out << "(echo " << m_var->get_decl()->get_name() << ")\n"; + out << "; eliminate " << mk_pp(m_var, m) << "\n"; out << "(push)\n"; - pp.display_smt2(out, f); + pp.display_smt2(out, fml); out << "(pop)\n\n"; + DEBUG_CODE( + smt_params params; + params.m_simplify_bit2int = true; + params.m_arith_enum_const_mod = true; + params.m_bv_enable_int2bv2int = true; + params.m_relevancy_lvl = 0; + smt::kernel ctx(m, params); + ctx.assert_expr(fml); + lbool is_sat = ctx.check(); + if (is_sat == l_true) { + std::cout << "; Validation failed:\n"; + std::cout << mk_pp(fml, m) << "\n"; + } +); + } for (unsigned i = 0; i < m_children.size(); ++i) { if (m_children[i]->fml()) { @@ -1410,13 +1450,9 @@ namespace qe { m_solver.assert_expr(m_fml); if (assumption) m_solver.assert_expr(assumption); bool is_sat = false; - while (l_false != m_solver.check()) { + while (l_true == m_solver.check()) { is_sat = true; - model_ref model; - m_solver.get_model(model); - TRACE("qe", model_v2_pp(tout, *model);); - model_evaluator model_eval(*model); - final_check(model_eval); + final_check(); } if (!is_sat) { @@ -1466,14 +1502,30 @@ namespace qe { private: - void final_check(model_evaluator& model_eval) { - TRACE("qe", tout << "\n";); - while (can_propagate_assignment(model_eval)) { - propagate_assignment(model_eval); - } - VERIFY(CHOOSE_VAR == update_current(model_eval, true)); - SASSERT(m_current->fml()); - pop(model_eval); + void final_check() { + model_ref model; + m_solver.get_model(model); + scoped_ptr model_eval = alloc(model_evaluator, *model); + + while (true) { + TRACE("qe", model_v2_pp(tout, *model);); + while (can_propagate_assignment(*model_eval)) { + propagate_assignment(*model_eval); + } + VERIFY(CHOOSE_VAR == update_current(*model_eval, true)); + SASSERT(m_current->fml()); + if (l_true != m_solver.check()) { + return; + } + m_solver.get_model(model); + model_eval = alloc(model_evaluator, *model); + search_tree* st = m_current; + update_current(*model_eval, false); + if (st == m_current) { + break; + } + } + pop(*model_eval); } ast_manager& get_manager() { return m; } @@ -1633,6 +1685,7 @@ namespace qe { nb = m_current->get_num_branches(); expr_ref fml(m_current->fml(), m); if (!eval(model_eval, b, branch) || branch >= nb) { + TRACE("qe", tout << "evaluation failed: setting branch to 0\n";); branch = rational::zero(); } SASSERT(!branch.is_neg()); @@ -1694,11 +1747,12 @@ namespace qe { } // - // The current state is satisfiable - // and the closed portion of the formula - // can be used as the quantifier-free portion. + // The closed portion of the formula + // can be used as the quantifier-free portion, + // unless the current state is unsatisfiable. // if (m.is_true(fml_mixed)) { + SASSERT(l_true == m_solver.check()); m_current = m_current->add_child(fml_closed); for (unsigned i = 0; m_defs && i < m_current->num_free_vars(); ++i) { expr_ref val(m); @@ -1708,6 +1762,7 @@ namespace qe { if (val == x) { model_ref model; lbool is_sat = m_solver.check(); + if (is_sat == l_undef) return; m_solver.get_model(model); SASSERT(is_sat == l_true); model_evaluator model_eval2(*model); @@ -1890,7 +1945,7 @@ namespace qe { vars.reset(); closed = closed && (r != l_undef); } - TRACE("qe", tout << mk_ismt2_pp(fml, m) << "\n";); + TRACE("qe", tout << mk_pp(fml, m) << "\n";); m_current->add_child(fml)->reset_free_vars(); block_assignment(); } @@ -1959,7 +2014,7 @@ namespace qe { class quant_elim_new : public quant_elim { ast_manager& m; - smt_params& m_fparams; + smt_params& m_fparams; expr_ref m_assumption; bool m_produce_models; ptr_vector m_plugins; diff --git a/src/qe/qe_arith_plugin.cpp b/src/qe/qe_arith_plugin.cpp index 7bf0978f6..83c7b79d8 100644 --- a/src/qe/qe_arith_plugin.cpp +++ b/src/qe/qe_arith_plugin.cpp @@ -31,6 +31,7 @@ Revision History: #include "obj_pair_hashtable.h" #include "nlarith_util.h" #include "model_evaluator.h" +#include "smt_kernel.h" namespace qe { @@ -80,9 +81,9 @@ namespace qe { ast_manager& m; i_solver_context& m_ctx; public: - arith_util m_arith; // initialize before m_zero_i, etc. + arith_util m_arith; // initialize before m_zero_i, etc. + th_rewriter simplify; private: - th_rewriter m_rewriter; arith_eq_solver m_arith_solver; bv_util m_bv; @@ -102,7 +103,7 @@ namespace qe { m(m), m_ctx(ctx), m_arith(m), - m_rewriter(m), + simplify(m), m_arith_solver(m), m_bv(m), m_zero_i(m_arith.mk_numeral(numeral(0), true), m), @@ -434,7 +435,6 @@ namespace qe { expr_ref tmp(e, m); simplify(tmp); m_arith_rewriter.mk_le(tmp, mk_zero(e), result); - TRACE("qe_verbose", tout << "mk_le " << mk_pp(result, m) << "\n";); } void mk_lt(expr* e, expr_ref& result) { @@ -521,7 +521,8 @@ namespace qe { expr_ref result1(m), result2(m); // a*s + b*t <= 0 - expr_ref as_bt_le_0(result, m), tmp2(m), tmp3(m), tmp4(m); + expr_ref as_bt_le_0(result, m), tmp2(m), asz_bt_le_0(m), tmp3(m), tmp4(m); + expr_ref b_divides_sz(m); // a*s + b*t + (a-1)(b-1) <= 0 tmp2 = m_arith.mk_add(as_bt, slack); @@ -560,30 +561,36 @@ namespace qe { sz = m_arith.mk_uminus(sz); } tmp4 = mk_add(mk_mul(a1, sz), bt); - mk_le(tmp4, tmp3); + mk_le(tmp4, asz_bt_le_0); - if (to_app(tmp3)->get_arg(0) == x && - m_arith.is_zero(to_app(tmp3)->get_arg(1))) { + if (to_app(asz_bt_le_0)->get_arg(0) == x && + m_arith.is_zero(to_app(asz_bt_le_0)->get_arg(1))) { // exists z in [0 .. |b|-2] . |b| | (z + s) && z <= 0 // <=> // |b| | s mk_divides(abs_b, s, tmp2); } else { - mk_divides(abs_b, sz, tmp2); - mk_and(tmp2, tmp3, tmp4); - mk_big_or(abs_b - numeral(2), x, tmp4, tmp2); - + mk_divides(abs_b, sz, b_divides_sz); + mk_and(b_divides_sz, asz_bt_le_0, tmp4); + mk_big_or(abs_b - numeral(2), x, tmp4, tmp2); + TRACE("qe", + tout << "b | s + z: " << mk_pp(b_divides_sz, m) << "\n"; + tout << "a(s+z) + bt <= 0: " << mk_pp(asz_bt_le_0, m) << "\n"; + ); } mk_flat_and(as_bt_le_0, tmp2, result2); mk_or(result1, result2, result); simplify(result); + + + // a*s + b*t + (a-1)(b-1) <= 0 + // or exists z in [0 .. |b|-2] . |b| | (z + s) && a*n_sign(b)(s + z) + |b|t <= 0 } TRACE("qe", { - expr_ref_vector trail(m); - tout << "is_strict: " << (is_strict?"true":"false") << "\n"; + tout << (is_strict?"strict":"non-strict") << "\n"; bound(m, a, t, false).pp(tout, x); tout << "\n"; bound(m, b, s, false).pp(tout, x); @@ -592,10 +599,6 @@ namespace qe { }); } - void simplify(expr_ref& p) { - m_rewriter(p); - } - struct mul_lt { arith_util& u; mul_lt(arith_qe_util& u): u(u.m_arith) {} @@ -1052,7 +1055,6 @@ namespace qe { } bool reduce_equation(expr* p, expr* fml) { - TRACE("qe", tout << mk_pp(p, m) << "\n";); numeral k; if (m_arith.is_numeral(p, k) && k.is_zero()) { @@ -1555,9 +1557,10 @@ public: mk_non_resolve(bounds, true, is_lower, result); mk_non_resolve(bounds, false, is_lower, result); + m_util.simplify(result); add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term()); TRACE("qe", - tout << vl << " " << mk_pp(x, m) << "\n"; + tout << vl << " " << mk_pp(x, m) << " infinite case\n"; tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n";); return; @@ -1591,19 +1594,22 @@ public: SASSERT(index < bounds.size(is_strict, is_lower)); expr_ref t(bounds.exprs(is_strict, is_lower)[index], m); rational a = bounds.coeffs(is_strict, is_lower)[index]; + - t = x_t.mk_term(a, t); - a = x_t.mk_coeff(a); mk_bounds(bounds, x, true, is_eq, is_strict, is_lower, index, a, t, result); mk_bounds(bounds, x, false, is_eq, is_strict, is_lower, index, a, t, result); + + t = x_t.mk_term(a, t); + a = x_t.mk_coeff(a); mk_resolve(bounds, x, x_t, true, is_eq, is_strict, is_lower, index, a, t, result); mk_resolve(bounds, x, x_t, false, is_eq, is_strict, is_lower, index, a, t, result); + m_util.simplify(result); add_cache(x, fml, v, result, x_t.get_coeff(), x_t.get_term()); TRACE("qe", { - tout << vl << " " << mk_pp(x, m) << "\n"; + tout << vl << " " << mk_pp(bounds.atoms(is_strict, is_lower)[index],m) << "\n"; tout << mk_pp(fml, m) << "\n"; tout << mk_pp(result, m) << "\n"; } @@ -2225,6 +2231,12 @@ public: } } m_util.simplify(result); + TRACE("qe", + tout << (is_strict?"strict":"non-strict") << "\n"; + tout << (is_lower?"is-lower":"is-upper") << "\n"; + tout << "a: " << a << " " << mk_pp(t, m) << "\n"; + tout << "b: " << b << " " << mk_pp(s, m) << "\n"; + tout << mk_pp(result, m) << "\n";); } // @@ -2245,10 +2257,12 @@ public: void mk_bounds(bounds_proc& bounds, - app* x, bool is_strict, bool is_eq_ctx, bool is_strict_ctx, bool is_lower, unsigned index, + app* x, bool is_strict, bool is_eq_ctx, + bool is_strict_ctx, bool is_lower, unsigned index, rational const& a, expr* t, expr_ref& result) { + TRACE("qe", tout << mk_pp(t, m) << "\n";); SASSERT(!is_eq_ctx || !is_strict_ctx); unsigned sz = bounds.size(is_strict, is_lower); expr_ref tmp(m), eq(m); @@ -2258,13 +2272,14 @@ public: for (unsigned i = 0; i < sz; ++i) { app* e = bounds.atoms(is_strict, is_lower)[i]; - expr* s = bounds.exprs(is_strict, is_lower)[i]; + expr_ref s(bounds.exprs(is_strict, is_lower)[i], m); rational b = bounds.coeffs(is_strict, is_lower)[i]; if (same_strict && i == index) { if (non_strict_real) { m_util.mk_eq(a, x, t, eq); - TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << " t: " << mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";); + TRACE("qe", tout << "a:" << a << " x: " << mk_pp(x, m) << "t: " << + mk_pp(t, m) << " eq: " << mk_pp(eq, m) << "\n";); if (is_eq_ctx) { m_ctx.add_constraint(true, eq); } @@ -2292,6 +2307,7 @@ public: (non_strict_real && is_eq_ctx && is_strict) || (same_strict && i < index); + mk_bound(result_is_strict, is_lower, a, t, b, s, tmp); m_util.m_replace.apply_substitution(e, tmp.get(), result); @@ -2330,14 +2346,17 @@ public: s = x_t.mk_term(b, s); b = x_t.mk_coeff(b); m_util.mk_resolve(x, strict_resolve, a, t, b, s, tmp); + expr_ref save_result(result); m_util.m_replace.apply_substitution(e, tmp.get(), result); m_ctx.add_constraint(true, mk_not(e), tmp); TRACE("qe_verbose", tout << mk_pp(atm, m) << " "; - tout << mk_pp(e, m) << " ==> "; + tout << mk_pp(e, m) << " ==>\n"; tout << mk_pp(tmp, m) << "\n"; + tout << "old fml: " << mk_pp(save_result, m) << "\n"; + tout << "new fml: " << mk_pp(result, m) << "\n"; ); } } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index a338be50a..44715c37a 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -1198,6 +1198,7 @@ namespace smt { void theory_bv::relevant_eh(app * n) { ast_manager & m = get_manager(); context & ctx = get_context(); + TRACE("bv", tout << "relevant: " << mk_pp(n, m) << "\n";); if (m.is_bool(n)) { bool_var v = ctx.get_bool_var(n); atom * a = get_bv2a(v); @@ -1210,11 +1211,11 @@ namespace smt { } } } - else if (m_params.m_bv_enable_int2bv2int && m_util.is_bv2int(n)) { + else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_bv2int(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_bv2int_axiom(n); } - else if (m_params.m_bv_enable_int2bv2int && m_util.is_int2bv(n)) { + else if (/*m_params.m_bv_enable_int2bv2int &&*/ m_util.is_int2bv(n)) { ctx.mark_as_relevant(n->get_arg(0)); assert_int2bv_axiom(n); } diff --git a/src/tactic/arith/bv2int_rewriter.cpp b/src/tactic/arith/bv2int_rewriter.cpp index 872981283..00d2f53ad 100644 --- a/src/tactic/arith/bv2int_rewriter.cpp +++ b/src/tactic/arith/bv2int_rewriter.cpp @@ -218,6 +218,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) { if (is_bv2int(s, s1) && is_bv2int(t, t1)) { align_sizes(s1, t1, false); result = m_bv.mk_bv2int(m_bv.mk_bv_urem(s1, t1)); + TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";); return BR_DONE; } @@ -232,6 +233,7 @@ br_status bv2int_rewriter::mk_mod(expr * s, expr * t, expr_ref & result) { u1 = mk_bv_add(s1, u1, false); align_sizes(u1, t1, false); result = m_bv.mk_bv2int(m_bv.mk_bv_urem(u1, t1)); + TRACE("bv2int_rewriter", tout << mk_pp(result,m()) << "\n";); return BR_DONE; }