fix #1741

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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.

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;

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; 
     }  

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();
-        app_ref atom(m);
+        rational offset = -k;
+        u_map<rational> 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) {
-            atom = a.mk_ge(t, a.mk_numeral(k, k.is_int()));
+                    offset = div(offset + g - rational::one(), g);
                 }
                 else {
-            atom = a.mk_le(t, a.mk_numeral(k, k.is_int()));
+                    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(offset, is_int));
+        }
+        else {
+            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) {     
+    void term2coeffs(lp::lar_term const& term, u_map<rational>& coeffs, rational const& coeff, rational& offset) {
-        expr_ref_vector args(m);
         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<rational> 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()) {
+        if (!offset.is_zero()) {
-            args.push_back(a.mk_numeral(term.m_v, is_int));
+            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<rational> coeffs;
+        rational offset;
+        term2coeffs(term, coeffs, rational::one(), offset);
+        return coeffs2app(coeffs, offset, is_int);
+    }
+
+    rational gcd_reduce(u_map<rational>& 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());

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) {
@@ -1271,6 +1274,7 @@ Notes:
             unsigned b, literal const* bs,                    
             literal_vector& out) {
             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"));
             }