From 605dcc40a3f0908a7da8bf2815736099334a48cf Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Jul 2018 09:19:13 -0700 Subject: [PATCH] fix #1741 Signed-off-by: Nikolaj Bjorner --- src/api/java/Optimize.java | 17 ++++++ src/ast/proofs/proof_checker.cpp | 2 +- src/ast/rewriter/arith_rewriter.cpp | 22 ++++++++ src/smt/theory_lra.cpp | 86 +++++++++++++++++++++++++---- src/util/sorting_network.h | 7 ++- 5 files changed, 121 insertions(+), 13 deletions(-) diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java index a434b6e9f..c5f8f9449 100644 --- a/src/api/java/Optimize.java +++ b/src/api/java/Optimize.java @@ -314,6 +314,23 @@ public class Optimize extends Z3Object { Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s); } + /** + * The set of asserted formulas. + */ + public BoolExpr[] getAssertions() + { + ASTVector assertions = new ASTVector(getContext(), Native.optimizeGetAssertions(getContext().nCtx(), getNativeObject())); + return assertions.ToBoolExprArray(); + } + + /** + * The set of asserted formulas. + */ + public Expr[] getObjectives() + { + ASTVector objectives = new ASTVector(getContext(), Native.optimizeGetObjectives(getContext().nCtx(), getNativeObject())); + return objectives.ToExprArray(); + } /** * Optimize statistics. diff --git a/src/ast/proofs/proof_checker.cpp b/src/ast/proofs/proof_checker.cpp index fd6ea43e1..448c14fe3 100644 --- a/src/ast/proofs/proof_checker.cpp +++ b/src/ast/proofs/proof_checker.cpp @@ -192,7 +192,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) { expr* t1 = nullptr, *t2 = nullptr; expr* s1 = nullptr, *s2 = nullptr; expr* u1 = nullptr, *u2 = nullptr; - expr* fact = nullptr, *body1 = nullptr, *body2 = nullptr; + expr* fact = nullptr, *body1 = nullptr; expr* l1 = nullptr, *l2 = nullptr, *r1 = nullptr, *r2 = nullptr; func_decl* d1 = nullptr, *d2 = nullptr, *d3 = nullptr; proof* p0 = nullptr, *p1 = nullptr, *p2 = nullptr; diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index ac2313266..6ddce9b80 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -812,6 +812,28 @@ br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & resu result = m().mk_ite(m().mk_eq(arg1, zero), m_util.mk_idiv(zero, zero), m_util.mk_int(1)); return BR_REWRITE3; } + if (m_util.is_numeral(arg2, v2, is_int) && v2.is_pos() && m_util.is_add(arg1)) { + expr_ref_buffer args(m()); + bool change = false; + rational add(0); + for (expr* arg : *to_app(arg1)) { + rational arg_v; + if (m_util.is_numeral(arg, arg_v) && arg_v.is_pos() && mod(arg_v, v2) != arg_v) { + change = true; + args.push_back(m_util.mk_numeral(mod(arg_v, v2), true)); + add += div(arg_v, v2); + } + else { + args.push_back(arg); + } + } + if (change) { + result = m_util.mk_idiv(m().mk_app(to_app(arg1)->get_decl(), args.size(), args.c_ptr()), arg2); + result = m_util.mk_add(m_util.mk_numeral(add, true), result); + TRACE("div_bug", tout << "mk_div result: " << result << "\n";); + return BR_REWRITE3; + } + } if (divides(arg1, arg2, result)) { return BR_REWRITE_FULL; } diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 9315e75ac..17c850330 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1362,22 +1362,46 @@ public: // create a bound atom representing term >= k is lower_bound is true, and term <= k if it is false app_ref mk_bound(lp::lar_term const& term, rational const& k, bool lower_bound) { - app_ref t = mk_term(term, k.is_int()); + bool is_int = k.is_int(); + rational offset = -k; + u_map coeffs; + term2coeffs(term, coeffs, rational::one(), offset); + offset.neg(); + if (is_int) { + // 3x + 6y >= 5 -> x + 3y >= 5/3, then x + 3y >= 2 + // 3x + 6y <= 5 -> x + 3y <= 1 + + rational g = gcd_reduce(coeffs); + if (!g.is_one()) { + if (lower_bound) { + offset = div(offset + g - rational::one(), g); + } + else { + offset = div(offset, g); + } + } + } + app_ref atom(m); + app_ref t = coeffs2app(coeffs, rational::zero(), is_int); if (lower_bound) { - atom = a.mk_ge(t, a.mk_numeral(k, k.is_int())); + atom = a.mk_ge(t, a.mk_numeral(offset, is_int)); } else { - atom = a.mk_le(t, a.mk_numeral(k, k.is_int())); + atom = a.mk_le(t, a.mk_numeral(offset, is_int)); } + + +#if 0 expr_ref atom1(m); proof_ref atomp(m); ctx().get_rewriter()(atom, atom1, atomp); if (!m.is_false(atom1) && !m.is_true(atom1)) { atom = to_app(atom1); } +#endif TRACE("arith", tout << t << ": " << atom << "\n"; - m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";); + m_solver->print_term(term, tout << "bound atom: "); tout << (lower_bound?" <= ":" >= ") << k << "\n";); ctx().internalize(atom, true); ctx().mark_as_relevant(atom.get()); return atom; @@ -1396,6 +1420,7 @@ public: case lp::lia_move::sat: return l_true; case lp::lia_move::branch: { + TRACE("arith", tout << "branch\n";); app_ref b = mk_bound(term, k, !upper); // branch on term >= k + 1 // branch on term <= k @@ -1405,6 +1430,7 @@ public: return l_false; } case lp::lia_move::cut: { + TRACE("arith", tout << "cutn";); ++m_stats.m_gomory_cuts; // m_explanation implies term <= k app_ref b = mk_bound(term, k, !upper); @@ -2809,26 +2835,44 @@ public: return internalize_def(term); } - app_ref mk_term(lp::lar_term const& term, bool is_int) { - expr_ref_vector args(m); + void term2coeffs(lp::lar_term const& term, u_map& coeffs, rational const& coeff, rational& offset) { for (const auto & ti : term) { theory_var w; if (m_solver->is_term(ti.var())) { - w = m_term_index2theory_var[m_solver->adjust_term_index(ti.var())]; + //w = m_term_index2theory_var.get(m_solver->adjust_term_index(ti.var()), null_theory_var); + //if (w == null_theory_var) // if extracing expressions directly from nested term + lp::lar_term const& term1 = m_solver->get_term(ti.var()); + rational coeff2 = coeff * ti.coeff(); + term2coeffs(term1, coeffs, coeff2, offset); + continue; } else { w = m_var_index2theory_var[ti.var()]; } + rational c0(0); + coeffs.find(w, c0); + coeffs.insert(w, c0 + ti.coeff() * coeff); + } + offset += coeff * term.m_v; + } + + app_ref coeffs2app(u_map const& coeffs, rational const& offset, bool is_int) { + expr_ref_vector args(m); + for (auto const& kv : coeffs) { + theory_var w = kv.m_key; expr* o = get_enode(w)->get_owner(); - if (ti.coeff().is_one()) { + if (kv.m_value.is_zero()) { + // continue + } + else if (kv.m_value.is_one()) { args.push_back(o); } else { - args.push_back(a.mk_mul(a.mk_numeral(ti.coeff(), is_int), o)); + args.push_back(a.mk_mul(a.mk_numeral(kv.m_value, is_int), o)); } } - if (!term.m_v.is_zero()) { - args.push_back(a.mk_numeral(term.m_v, is_int)); + if (!offset.is_zero()) { + args.push_back(a.mk_numeral(offset, is_int)); } switch (args.size()) { case 0: @@ -2840,6 +2884,26 @@ public: } } + app_ref mk_term(lp::lar_term const& term, bool is_int) { + u_map coeffs; + rational offset; + term2coeffs(term, coeffs, rational::one(), offset); + return coeffs2app(coeffs, offset, is_int); + } + + rational gcd_reduce(u_map& coeffs) { + rational g(0); + for (auto const& kv : coeffs) { + g = gcd(g, kv.m_value); + } + if (!g.is_one() && !g.is_zero()) { + for (auto& kv : coeffs) { + kv.m_value /= g; + } + } + return g; + } + app_ref mk_obj(theory_var v) { lp::var_index vi = m_theory_var2var_index[v]; bool is_int = a.is_int(get_enode(v)->get_owner()); diff --git a/src/util/sorting_network.h b/src/util/sorting_network.h index d7d8e8bbe..ff083162d 100644 --- a/src/util/sorting_network.h +++ b/src/util/sorting_network.h @@ -977,6 +977,7 @@ Notes: unsigned b, literal const* bs, literal_vector& out) { unsigned nc = m_stats.m_num_compiled_clauses; + (void)nc; if (a == 1 && b == 1) { literal y1 = mk_max(as[0], bs[0]); literal y2 = mk_min(as[0], bs[0]); @@ -1054,6 +1055,7 @@ Notes: literal_vector const& bs, literal_vector& out) { unsigned nc = m_stats.m_num_compiled_clauses; + (void)nc; SASSERT(as.size() >= bs.size()); SASSERT(as.size() <= bs.size() + 2); SASSERT(!as.empty()); @@ -1152,6 +1154,7 @@ Notes: unsigned b, literal const* bs, literal_vector& out) { unsigned nc = m_stats.m_num_compiled_clauses; + (void)nc; if (a == 1 && b == 1 && c == 1) { literal y = mk_max(as[0], bs[0]); if (m_t != GE) { @@ -1270,7 +1273,8 @@ Notes: unsigned a, literal const* as, unsigned b, literal const* bs, literal_vector& out) { - unsigned nc = m_stats.m_num_compiled_clauses; + unsigned nc = m_stats.m_num_compiled_clauses; + (void)nc; SASSERT(a <= c); SASSERT(b <= c); SASSERT(a + b >= c); @@ -1338,6 +1342,7 @@ Notes: SASSERT(m <= n); literal_vector lits; unsigned nc = m_stats.m_num_compiled_clauses; + (void)nc; for (unsigned i = 0; i < m; ++i) { out.push_back(fresh("dsort")); }